diff --git a/PrimeCert/Interval.lean b/PrimeCert/Interval.lean
index 2ab97df..1c6d0ff 100644
--- a/PrimeCert/Interval.lean
+++ b/PrimeCert/Interval.lean
@@ -18,12 +18,11 @@ section forallB
 
 noncomputable def forallB (f : ℕ → Bool) (start len : ℕ) (step : ℕ := 1) : Bool :=
   (Nat.rec (motive := fun _ ↦ ℕ × Bool) (start, true)
-    (fun _ ih ↦ ih.rec fun i b ↦ (i.add step, (f i).and' b)) len).2
+    (fun _ ih ↦ ih.rec fun i b ↦ (i.add step, (f i).and b)) len).2
 
 theorem forallB_iff_range' (f : ℕ → Bool) (start len step : ℕ) :
     forallB f start len step ↔ ∀ n ∈ List.range' start len step, f n := by
   unfold forallB
-  simp only [Bool.and'_eq_and]
   induction len with
   | zero => simp
   | succ len ih =>
diff --git a/PrimeCert/Pocklington.lean b/PrimeCert/Pocklington.lean
index c801581..5173157 100644
--- a/PrimeCert/Pocklington.lean
+++ b/PrimeCert/Pocklington.lean
@@ -36,27 +36,14 @@ theorem Nat.modEq_finset_prod_iff {a b : ℕ} {ι : Type*} (s : Finset ι) (e :
   · simp_rw [List.mem_toFinset]
   · rwa [← List.pairwise_iff_coe_toFinset_pairwise hl]
 
-theorem multiplicity_zero_right {α : Type*} [MonoidWithZero α] (x : α) : multiplicity x 0 = 1 :=
-  multiplicity_eq_one_of_not_finiteMultiplicity fun h ↦ h.ne_zero rfl
-
-theorem Nat.modEq_iff_forall_prime_dvd {a b n : ℕ} :
+theorem Nat.modEq_iff_forall_prime_dvd {a b n : ℕ} (hn₀ : n ≠ 0) :
     a ≡ b [MOD n] ↔ ∀ p : ℕ, p ∣ n → p.Prime → a ≡ b [MOD p ^ multiplicity p n] := by
-  by_cases hn₀ : n = 0
-  · subst hn₀
-    simp_rw [modEq_zero_iff, dvd_zero, true_imp_iff]
-    constructor
-    · rintro rfl; exact fun _ _ ↦ by rfl
-    · intro h
-      obtain ⟨p, hbp, hp⟩ := exists_infinite_primes (a + b + 1)
-      specialize h p hp
-      rw [multiplicity_zero_right, pow_one] at h
-      exact h.eq_of_lt_of_lt (by linarith) (by linarith)
-  · conv_lhs => rw [← prod_factorization_pow_eq_self hn₀]
-    rw [Finsupp.prod, modEq_finset_prod_iff]
-    · simp_rw [support_factorization, mem_primeFactors_of_ne_zero hn₀, and_comm, and_imp]
-      refine forall_congr' fun p ↦ imp_congr_right fun hpn ↦ imp_congr_right fun hp ↦ ?_
-      rw [multiplicity_eq_factorization hp hn₀]
-    · grind [support_factorization, coprime_pow_primes, Set.Pairwise]
+  conv_lhs => rw [← prod_factorization_pow_eq_self hn₀]
+  rw [Finsupp.prod, modEq_finset_prod_iff]
+  · simp_rw [support_factorization, mem_primeFactors_of_ne_zero hn₀, and_comm, and_imp]
+    refine forall_congr' fun p ↦ imp_congr_right fun hpn ↦ imp_congr_right fun hp ↦ ?_
+    rw [multiplicity_eq_factorization hp]
+  · grind [support_factorization, coprime_pow_primes, Set.Pairwise]
 
 theorem Nat.pow_multiplicity_dvd_of_dvd_of_not_dvd_div
     {q n x : ℕ} (hq : q.Prime) (hxn : x ∣ n) (hxnq : ¬ x ∣ n / q) :
@@ -72,7 +59,7 @@ theorem Nat.pow_multiplicity_dvd_of_dvd_of_not_dvd_div
     rw [← Nat.factorization_le_iff_dvd hx₀ hqn₀] at hxn
     rw [Nat.factorization_mul hq.ne_zero hn₀, hq.factorization, add_comm] at hxn
     refine pow_dvd_of_le_multiplicity ?_
-    rw [multiplicity_eq_factorization hq hqn₀, multiplicity_eq_factorization hq hx₀,
+    rw [multiplicity_eq_factorization hq, multiplicity_eq_factorization hq,
       Nat.factorization_mul hq.ne_zero hn₀, Finsupp.add_apply, hq.factorization,
       Finsupp.single_apply, if_pos rfl, add_comm]
     refine le_of_not_gt fun h ↦ hxnq fun p ↦ ?_
@@ -80,7 +67,7 @@ theorem Nat.pow_multiplicity_dvd_of_dvd_of_not_dvd_div
     · subst hpq; exact Nat.lt_succ_iff.mp h
     convert hxn p using 1
     rw [Finsupp.add_apply, Finsupp.single_apply, if_neg (Ne.symm hpq), add_zero]
-  · rw [multiplicity_eq_zero.mpr hqn, pow_zero]
+  · rw [multiplicity_eq_zero_of_not_dvd hqn, pow_zero]
     exact one_dvd _
 
 /-- Let `N` be a natural number whose primality we want to certify.
@@ -102,7 +89,7 @@ theorem pocklington_test (N F₁ : ℕ) (hn₀ : 0 < N) (hf₁ : F₁ ∣ N - 1)
     rintro rfl
     rw [zero_dvd_iff] at hf₁
     omega
-  rw [Nat.modEq_iff_forall_prime_dvd]
+  rw [Nat.modEq_iff_forall_prime_dvd hf₀]
   intro q hqf hq
   have := Fact.mk hp
   have := (Nat.prime_iff_card_units _).mp hp
@@ -113,7 +100,7 @@ theorem pocklington_test (N F₁ : ℕ) (hn₀ : 0 < N) (hf₁ : F₁ ∣ N - 1)
   let a' : (ZMod p)ˣ := Units.ofPowEqOne _ _ hanp (by grind)
   refine dvd_trans ?_ (orderOf_dvd_card (x := a'))
   have : multiplicity q F₁ ≤ multiplicity q (N - 1) := by
-    rw [Nat.multiplicity_eq_factorization hq hf₀, Nat.multiplicity_eq_factorization hq (by grind)]
+    rw [Nat.multiplicity_eq_factorization hq, Nat.multiplicity_eq_factorization hq]
     exact (Nat.factorization_le_iff_dvd hf₀ (by grind)).mpr hf₁ _
   refine dvd_trans (pow_dvd_pow _ this) ?_
   refine Nat.pow_multiplicity_dvd_of_dvd_of_not_dvd_div hq ?_ ?_
diff --git a/PrimeCert/PowMod.lean b/PrimeCert/PowMod.lean
index 6f8a8e4..da96158 100644
--- a/PrimeCert/PowMod.lean
+++ b/PrimeCert/PowMod.lean
@@ -98,15 +98,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
 
@@ -138,7 +138,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"
@@ -147,7 +147,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"