diff --git a/HighlyAbundant/Basic.lean b/HighlyAbundant/Basic.lean
index 89c8dce..495982c 100644
--- a/HighlyAbundant/Basic.lean
+++ b/HighlyAbundant/Basic.lean
@@ -63,7 +63,8 @@ lemma factorization_eq {n p k : ℕ} (h₁ : p ^ k ∣ n) (h₂ : ¬ p ^ (k + 1)
     contrapose! h₂
     simp [h₂]
   suffices k ≤ Nat.factorization n p ∧ ¬ (k + 1 ≤ Nat.factorization n p) by lia
-  simp [← hp.pow_dvd_iff_le_factorization hn, *]
+  rw [← hp.pow_dvd_iff_le_factorization hn, ← hp.pow_dvd_iff_le_factorization hn]
+  exact ⟨h₁, h₂⟩
 
 lemma Nat.factorization_finsetLcm {α : Type*} {p : ℕ} {s : Finset α} {f : α → ℕ}
     (h : ∀ x ∈ s, f x ≠ 0) :
diff --git a/HighlyAbundant/PrepareLadder.lean b/HighlyAbundant/PrepareLadder.lean
index 3f53eb2..351f70f 100644
--- a/HighlyAbundant/PrepareLadder.lean
+++ b/HighlyAbundant/PrepareLadder.lean
@@ -115,10 +115,10 @@ lemma h_div_K {i : ℕ} (hi : i ∈ Finset.Icc d.lo d.hi) : d.div ∣ d.K i := b
     exact dvd_lcmRange_of_le (d.h_divs p hp).ne_zero
       (by have := d.h_divs_lo; grind)
   have : p ∉ d.muls.map (·.1) := by have := d.h_disjoint; grind
-  convert_to p ^ (lcmRange i).factorization p ∣ d.K i
-  · rfl
-  · rw [d.h_divs_i hi _ hp, Nat.pow_one]
-  exact Finset.dvd_prod_of_mem _ (by simp [hpl, this])
+  have hf : (lcmRange i).factorization p = 1 := d.h_divs_i hi _ hp
+  have hK : p ^ (lcmRange i).factorization p ∣ d.K i :=
+    Finset.dvd_prod_of_mem _ (by simp [hpl, this])
+  rwa [hf, Nat.pow_one] at hK
 
 lemma L_eq {i : ℕ} :
     lcmRange i = (∏ pki ∈ d.muls.toFinset, pki.1 ^ (lcmRange i).factorization pki.1) * d.K i := by
diff --git a/HighlyAbundant/Prime/PowMod.lean b/HighlyAbundant/Prime/PowMod.lean
index 778c2e1..0808175 100644
--- a/HighlyAbundant/Prime/PowMod.lean
+++ b/HighlyAbundant/Prime/PowMod.lean
@@ -92,15 +92,15 @@ lemma powModTR_aux_eq (n a b c fuel) (hfuel : b < fuel) :
       congr! 3
       lia
 
-lemma powModTR_eq (a b n : ℕ) : powModTR a b n = powMod a b n := by
+lemma powModTR_eq (a b n : ℕ) : powModTR a b n = _root_.powMod a b n := by
   rw [powModTR, powModTR_aux_eq _ _ _ _ _ (by omega)]
-  rw [powModAux, mul_one, powMod, mod_eq_mod, ← Nat.pow_mod]
+  rw [powModAux, mul_one, _root_.powMod, mod_eq_mod, ← Nat.pow_mod]
 
-lemma powMod_eq_of_powModTR (a b n m : ℕ) (h : (powModTR a b n).beq m) : powMod a b n = m := by
+lemma powMod_eq_of_powModTR (a b n m : ℕ) (h : (powModTR a b n).beq m) : _root_.powMod a b n = m := by
   rwa [powModTR_eq, beq_eq] at h
 
 lemma powMod_ne_of_powModTR (a b n m : ℕ) (h : (powModTR a b n).beq m = false) :
-    powMod a b n ≠ m := by
+    _root_.powMod a b n ≠ m := by
   have := Nat.ne_of_beq_eq_false h
   rwa [powModTR_eq] at this
 
@@ -132,7 +132,7 @@ def prove_pow_mod_tac (g : MVarId) : MetaM Unit := do
   | Eq ty lhsE rhsE =>
     unless (← whnfR ty).isConstOf ``Nat do throwError "not an equality of naturals"
     let some rhs := rhsE.nat? | throwError "rhs is not a numeral"
-    let some (aE, bE, nE) := lhsE.app3? ``powMod | throwError "lhs is not a pow-mod"
+    let some (aE, bE, nE) := lhsE.app3? ``_root_.powMod | throwError "lhs is not a pow-mod"
     let some a := aE.nat? | throwError "base is not a numeral"
     let some b := bE.nat? | throwError "exponent is not a numeral"
     let some n := nE.nat? | throwError "modulus is not a numeral"
@@ -141,7 +141,7 @@ def prove_pow_mod_tac (g : MVarId) : MetaM Unit := do
   | Ne ty lhsE rhsE =>
     unless (← whnfR ty).isConstOf ``Nat do throwError "not an equality of naturals"
     let some rhs := rhsE.nat? | throwError "rhs is not a numeral"
-    let some (aE, bE, nE) := lhsE.app3? ``powMod | throwError "lhs is not a pow-mod"
+    let some (aE, bE, nE) := lhsE.app3? ``_root_.powMod | throwError "lhs is not a pow-mod"
     let some a := aE.nat? | throwError "base is not a numeral"
     let some b := bE.nat? | throwError "exponent is not a numeral"
     let some n := nE.nat? | throwError "modulus is not a numeral"
diff --git a/HighlyAbundant/Prime/Pratt.lean b/HighlyAbundant/Prime/Pratt.lean
index 0d78240..0358255 100644
--- a/HighlyAbundant/Prime/Pratt.lean
+++ b/HighlyAbundant/Prime/Pratt.lean
@@ -7,11 +7,11 @@ Authors: Bhavik Mehta
 import HighlyAbundant.Prime.PowMod
 import Mathlib.NumberTheory.LucasPrimality
 
-def pratt_predicate (p a x : ℕ) : Prop := ∀ q ∈ x.primeFactors, powMod a ((p - 1) / q) p ≠ 1
+def pratt_predicate (p a x : ℕ) : Prop := ∀ q ∈ x.primeFactors, _root_.powMod a ((p - 1) / q) p ≠ 1
 
 @[simp]
 lemma pratt_predicate_iff (p a x : ℕ) :
-    pratt_predicate p a x ↔ ∀ q ∈ x.primeFactors, powMod a ((p - 1) / q) p ≠ 1 :=
+    pratt_predicate p a x ↔ ∀ q ∈ x.primeFactors, _root_.powMod a ((p - 1) / q) p ≠ 1 :=
   Iff.rfl
 
 def pratt_zero (p a : ℕ) : pratt_predicate p a 0 := by simp!
@@ -20,7 +20,7 @@ def pratt_axiom (p a : ℕ) : pratt_predicate p a 1 := by simp!
 open Nat
 
 lemma pratt_rule_1 {p a x q : ℕ} (h : pratt_predicate p a x) (hq : q.Prime)
-    (h' : powMod a ((p - 1) / q) p ≠ 1) : pratt_predicate p a (q * x) := by
+    (h' : _root_.powMod a ((p - 1) / q) p ≠ 1) : pratt_predicate p a (q * x) := by
   rcases eq_or_ne x 0 with rfl | hx
   · rwa [mul_zero]
   intro r hr
@@ -32,13 +32,13 @@ lemma pratt_rule_1 {p a x q : ℕ} (h : pratt_predicate p a x) (hq : q.Prime)
 
 lemma pratt_rule_1' (q x : ℕ) {p a y : ℕ} (hq : q.Prime)
     (hy : q * x = y)
-    (h' : powMod a ((p - 1) / q) p ≠ 1) (h : pratt_predicate p a x) : pratt_predicate p a y := by
+    (h' : _root_.powMod a ((p - 1) / q) p ≠ 1) (h : pratt_predicate p a x) : pratt_predicate p a y := by
   rw [← hy]
   exact pratt_rule_1 h hq h'
 
 lemma pratt_rule_2 (a : ℕ) {p : ℕ} (hp : p ≠ 0) (h : pratt_predicate p a (p - 1))
-    (h' : powMod a (p - 1) p = 1) : p.Prime := by
-  rw [powMod] at h'
+    (h' : _root_.powMod a (p - 1) p = 1) : p.Prime := by
+  rw [_root_.powMod] at h'
   rcases p with rfl | rfl | p
   · cases hp rfl
   · simp at h'
@@ -52,11 +52,11 @@ lemma pratt_rule_2 (a : ℕ) {p : ℕ} (hp : p ≠ 0) (h : pratt_predicate p a (
   · rw [← ZMod.natCast_mod, succ_sub_one, h', Nat.cast_one]
   rw [← ZMod.natCast_mod, ←@Nat.cast_one (ZMod (p+2)), ne_eq, ZMod.natCast_eq_natCast_iff,
     Nat.ModEq, mod_mod, one_mod]
-  simp only [powMod] at h
+  simp only [_root_.powMod] at h
   exact h _ hq hq'
 
 lemma pratt_rule_2' (a : ℕ) {p : ℕ} (hp : p ≠ 0)
-    (h' : powMod a (p - 1) p = 1)
+    (h' : _root_.powMod a (p - 1) p = 1)
     (h : pratt_predicate p a (p - 1)) : p.Prime :=
   pratt_rule_2 a hp h h'