diff --git a/Mathlib/NumberTheory/ADEInequality.lean b/Mathlib/NumberTheory/ADEInequality.lean
index 3342ba492e9536..b78ce1794502d1 100644
--- a/Mathlib/NumberTheory/ADEInequality.lean
+++ b/Mathlib/NumberTheory/ADEInequality.lean
@@ -152,52 +152,31 @@ theorem Admissible.one_lt_sumInv {pqr : Multiset ℕ+} : Admissible pqr → 1 <
     norm_num
 
 theorem lt_three {p q r : ℕ+} (hpq : p ≤ q) (hqr : q ≤ r) (H : 1 < sumInv {p, q, r}) : p < 3 := by
-  have h3 : (0 : ℚ) < 3 := by simp
   contrapose! H
   rw [sumInv_pqr]
   have h3q := H.trans hpq
   have h3r := h3q.trans hqr
-  have hp : (p : ℚ)⁻¹ ≤ 3⁻¹ := by
-    rw [inv_le_inv₀ _ h3]
-    · assumption_mod_cast
-    · simp
-  have hq : (q : ℚ)⁻¹ ≤ 3⁻¹ := by
-    rw [inv_le_inv₀ _ h3]
-    · assumption_mod_cast
-    · simp
-  have hr : (r : ℚ)⁻¹ ≤ 3⁻¹ := by
-    rw [inv_le_inv₀ _ h3]
-    · assumption_mod_cast
-    · simp
+  have hp : (p : ℚ)⁻¹ ≤ 3⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast H)
+  have hq : (q : ℚ)⁻¹ ≤ 3⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast h3q)
+  have hr : (r : ℚ)⁻¹ ≤ 3⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast h3r)
   calc
     (p : ℚ)⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹ ≤ 3⁻¹ + 3⁻¹ + 3⁻¹ := add_le_add (add_le_add hp hq) hr
     _ = 1 := by norm_num
 
 theorem lt_four {q r : ℕ+} (hqr : q ≤ r) (H : 1 < sumInv {2, q, r}) : q < 4 := by
-  have h4 : (0 : ℚ) < 4 := by simp
   contrapose! H
   rw [sumInv_pqr]
   have h4r := H.trans hqr
-  have hq : (q : ℚ)⁻¹ ≤ 4⁻¹ := by
-    rw [inv_le_inv₀ _ h4]
-    · assumption_mod_cast
-    · simp
-  have hr : (r : ℚ)⁻¹ ≤ 4⁻¹ := by
-    rw [inv_le_inv₀ _ h4]
-    · assumption_mod_cast
-    · simp
+  have hq : (q : ℚ)⁻¹ ≤ 4⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast H)
+  have hr : (r : ℚ)⁻¹ ≤ 4⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast h4r)
   calc
     (2⁻¹ + (q : ℚ)⁻¹ + (r : ℚ)⁻¹) ≤ 2⁻¹ + 4⁻¹ + 4⁻¹ := add_le_add (add_le_add le_rfl hq) hr
     _ = 1 := by norm_num
 
 theorem lt_six {r : ℕ+} (H : 1 < sumInv {2, 3, r}) : r < 6 := by
-  have h6 : (0 : ℚ) < 6 := by simp
   contrapose! H
   rw [sumInv_pqr]
-  have hr : (r : ℚ)⁻¹ ≤ 6⁻¹ := by
-    rw [inv_le_inv₀ _ h6]
-    · assumption_mod_cast
-    · simp
+  have hr : (r : ℚ)⁻¹ ≤ 6⁻¹ := inv_anti₀ (by positivity) (by exact_mod_cast H)
   calc
     (2⁻¹ + 3⁻¹ + (r : ℚ)⁻¹ : ℚ) ≤ 2⁻¹ + 3⁻¹ + 6⁻¹ := add_le_add (add_le_add le_rfl le_rfl) hr
     _ = 1 := by norm_num
diff --git a/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean b/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean
index f7387bd07f224d..657cf8dfc035da 100644
--- a/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean
+++ b/Mathlib/NumberTheory/ArithmeticFunction/Defs.lean
@@ -262,15 +262,11 @@ theorem mul_smul' (f g : ArithmeticFunction R) (h : ArithmeticFunction M) :
 
 theorem one_smul' (b : ArithmeticFunction M) : (1 : ArithmeticFunction R) • b = b := by
   ext x
-  rw [smul_apply]
-  by_cases x0 : x = 0
-  · simp [x0]
-  have h : {(1, x)} ⊆ divisorsAntidiagonal x := by simp [x0]
-  rw [← sum_subset h]
+  rw [smul_apply, ← Nat.map_div_right_divisors, sum_map, sum_eq_single 1]
   · simp
-  intro y ymem ynotMem
-  have y1ne : y.fst ≠ 1 := fun con => by simp_all [Prod.ext_iff]
-  simp [y1ne]
+  · intro d hd hd1
+    simp [one_apply_ne hd1]
+  · simpa using fun hx : x = 0 => by simp [hx]
 
 end Module
 
@@ -282,17 +278,11 @@ instance instMonoid : Monoid (ArithmeticFunction R) where
   one_mul := one_smul'
   mul_one f := by
     ext x
-    rw [mul_apply]
-    by_cases x0 : x = 0
-    · simp [x0]
-    have h : {(x, 1)} ⊆ divisorsAntidiagonal x := by simp [x0]
-    rw [← sum_subset h]
+    rw [mul_apply, ← Nat.map_div_left_divisors, sum_map, sum_eq_single 1]
     · simp
-    intro ⟨y₁, y₂⟩ ymem ynotMem
-    have y2ne : y₂ ≠ 1 := by
-      intro con
-      simp_all
-    simp [y2ne]
+    · intro d hd hd1
+      simp [one_apply_ne hd1]
+    · simpa using fun hx : x = 0 => by simp [hx]
   mul_assoc := mul_smul'
 
 instance instSemiring : Semiring (ArithmeticFunction R) where
diff --git a/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean b/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean
index ab67f48c8097c5..7026d8b0cc6742 100644
--- a/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean
+++ b/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean
@@ -78,18 +78,14 @@ theorem coe_zeta_mul_apply [Semiring R] {f : ArithmeticFunction R} {x : ℕ} :
     (ζ * f) x = ∑ i ∈ divisors x, f i :=
   coe_zeta_smul_apply
 
-theorem coe_mul_zeta_apply [Semiring R] {f : ArithmeticFunction R} {x : ℕ} :
-    (f * ζ) x = ∑ i ∈ divisors x, f i := by
-  rw [mul_apply]
-  trans ∑ i ∈ divisorsAntidiagonal x, f i.1
-  · refine sum_congr rfl fun i hi => ?_
-    rcases mem_divisorsAntidiagonal.1 hi with ⟨rfl, h⟩
-    rw [natCoe_apply, zeta_apply_ne (right_ne_zero_of_mul h), cast_one, mul_one]
-  · rw [← map_div_right_divisors, sum_map, Function.Embedding.coeFn_mk]
-
 theorem coe_zeta_mul_comm [Semiring R] {f : ArithmeticFunction R} : ζ * f = f * ζ := by
   ext x
-  rw [coe_zeta_mul_apply, coe_mul_zeta_apply]
+  rw [mul_apply, ← map_swap_divisorsAntidiagonal, Finset.sum_map]
+  simp [mul_apply]
+
+theorem coe_mul_zeta_apply [Semiring R] {f : ArithmeticFunction R} {x : ℕ} :
+    (f * ζ) x = ∑ i ∈ divisors x, f i := by
+  rw [← coe_zeta_mul_comm, coe_zeta_mul_apply]
 
 theorem zeta_mul_apply {f : ArithmeticFunction ℕ} {x : ℕ} : (ζ * f) x = ∑ i ∈ divisors x, f i := by
   rw [← natCoe_nat ζ, coe_zeta_mul_apply]
diff --git a/Mathlib/NumberTheory/BernoulliPolynomials.lean b/Mathlib/NumberTheory/BernoulliPolynomials.lean
index 8e4f886c8e9ece..6bdf44d048949e 100644
--- a/Mathlib/NumberTheory/BernoulliPolynomials.lean
+++ b/Mathlib/NumberTheory/BernoulliPolynomials.lean
@@ -80,12 +80,8 @@ theorem bernoulli_one : bernoulli 1 = X - C 2⁻¹ := by
 
 @[simp]
 theorem bernoulli_eval_zero (n : ℕ) : (bernoulli n).eval 0 = _root_.bernoulli n := by
-  rw [bernoulli, eval_finset_sum, sum_range_succ]
-  have : ∑ x ∈ range n, _root_.bernoulli x * n.choose x * 0 ^ (n - x) = 0 := by
-    apply sum_eq_zero fun x hx => _
-    intro x hx
-    simp [tsub_eq_zero_iff_le, mem_range.1 hx]
-  simp [this]
+  rw [← coeff_zero_eq_eval_zero, coeff_bernoulli, if_pos (Nat.zero_le n), Nat.sub_zero,
+    Nat.choose_zero_right, Nat.cast_one, mul_one]
 
 @[simp]
 theorem bernoulli_eval_one (n : ℕ) : (bernoulli n).eval 1 = bernoulli' n := by
@@ -147,15 +143,10 @@ nonrec theorem sum_bernoulli (n : ℕ) :
   simp only [add_eq_left, mul_one, cast_one, cast_add, add_tsub_cancel_left,
     choose_succ_self_right, one_smul, _root_.bernoulli_zero, sum_singleton, zero_add,
     map_add, range_one, mul_one]
-  apply sum_eq_zero fun x hx => _
-  have f : ∀ x ∈ range n, ¬n + 1 - x = 1 := by grind
+  refine sum_eq_zero ?_
   intro x hx
-  rw [sum_bernoulli]
-  have g : ite (n + 1 - x = 1) (1 : ℚ) 0 = 0 := by
-    simp only [ite_eq_right_iff, one_ne_zero]
-    intro h₁
-    exact (f x hx) h₁
-  rw [g, zero_smul]
+  have hx1 : n + 1 - x ≠ 1 := by grind
+  simp [_root_.sum_bernoulli, hx1]
 
 /-- Another version of `Polynomial.sum_bernoulli`. -/
 theorem bernoulli_eq_sub_sum (n : ℕ) :
diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean
index f4861f75d916b5..fb188d33d9d298 100644
--- a/Mathlib/NumberTheory/Cyclotomic/Basic.lean
+++ b/Mathlib/NumberTheory/Cyclotomic/Basic.lean
@@ -549,42 +549,24 @@ theorem nonempty_algEquiv_adjoin_of_isSepClosed [IsCyclotomicExtension S K L]
   have := isSeparable S K L
   let i : L →ₐ[K] M := IsSepClosed.lift
   refine ⟨(show L ≃ₐ[K] i.fieldRange from AlgEquiv.ofInjectiveField i).trans
-    (IntermediateField.equivOfEq (le_antisymm ?_ ?_))⟩
-  · rintro x (hx : x ∈ i.range)
-    let e := Subalgebra.equivOfEq _ _ ((IsCyclotomicExtension.iff_adjoin_eq_top S K L).1 ‹_›).2
-      |>.trans Subalgebra.topEquiv
-    have hrange : i.range = (i.comp (AlgHomClass.toAlgHom e)).range := by
-      ext x
-      simp only [AlgHom.mem_range, AlgHom.coe_comp, AlgHom.coe_coe, Function.comp_apply]
-      constructor
-      · rintro ⟨y, rfl⟩; exact ⟨e.symm y, by simp⟩
-      · rintro ⟨y, rfl⟩; exact ⟨e y, rfl⟩
-    rw [hrange, AlgHom.mem_range] at hx
-    obtain ⟨⟨y, hy⟩, rfl⟩ := hx
-    induction hy using Algebra.adjoin_induction with
-    | mem x hx =>
-      obtain ⟨n, hn, h1, h2⟩ := hx
-      apply IntermediateField.subset_adjoin
-      use n, hn, h1
-      rw [← map_pow, ← map_one (i.comp (AlgHomClass.toAlgHom e))]
-      congr 1
-      apply_fun _ using Subtype.val_injective
-      simpa
-    | algebraMap x =>
-      convert IntermediateField.algebraMap_mem _ x
-      exact AlgHom.commutes _ x
-    | add x y hx hy ihx ihy =>
-      convert add_mem ihx ihy
-      exact map_add (i.comp (AlgHomClass.toAlgHom e)) ⟨x, hx⟩ ⟨y, hy⟩
-    | mul x y hx hy ihx ihy =>
-      convert mul_mem ihx ihy
-      exact map_mul (i.comp (AlgHomClass.toAlgHom e)) ⟨x, hx⟩ ⟨y, hy⟩
-  · rw [IntermediateField.adjoin_le_iff]
-    rintro x ⟨n, hn, h1, h2⟩
-    have := NeZero.mk h1
+    (IntermediateField.equivOfEq ?_)⟩
+  rw [AlgHom.fieldRange_eq_map]
+  have htop : IntermediateField.adjoin K {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤ := by
+    exact IntermediateField.adjoin_eq_top_of_algebra (F := K)
+      (S := {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
+      (((IsCyclotomicExtension.iff_adjoin_eq_top S K L).1 ‹_›).2)
+  rw [← htop, IntermediateField.adjoin_map]
+  apply le_antisymm <;> rw [IntermediateField.adjoin_le_iff]
+  · rintro _ ⟨y, ⟨n, hn, h1, h2⟩, rfl⟩
+    exact IntermediateField.subset_adjoin (F := K)
+      (S := {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ⟨n, hn, h1, by
+        simpa using congrArg i h2⟩
+  · rintro x ⟨n, hn, h1, h2⟩
+    have : NeZero n := ⟨h1⟩
     obtain ⟨y, hy⟩ := exists_isPrimitiveRoot K L hn h1
     obtain ⟨m, -, rfl⟩ := (hy.map_of_injective (f := i) i.injective).eq_pow_of_pow_eq_one h2
-    exact ⟨y ^ m, by simp⟩
+    exact pow_mem (IntermediateField.subset_adjoin (F := K)
+      (S := i '' {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ⟨y, ⟨n, hn, h1, hy.pow_eq_one⟩, rfl⟩) m
 
 theorem isGalois [IsCyclotomicExtension S K L] : IsGalois K L := by
   rw [isGalois_iff]
diff --git a/Mathlib/NumberTheory/Cyclotomic/Gal.lean b/Mathlib/NumberTheory/Cyclotomic/Gal.lean
index 4fa73cdc884f22..6fc270613b9202 100644
--- a/Mathlib/NumberTheory/Cyclotomic/Gal.lean
+++ b/Mathlib/NumberTheory/Cyclotomic/Gal.lean
@@ -56,24 +56,10 @@ variable [CommRing L] [IsDomain L] (hμ : IsPrimitiveRoot μ n) [Algebra K L]
 field extension. -/
 theorem autToPow_injective : Function.Injective <| hμ.autToPow K := by
   intro f g hfg
-  apply_fun Units.val at hfg
-  simp only [IsPrimitiveRoot.coe_autToPow_apply] at hfg
-  generalize_proofs hf' hg' at hfg
-  have hf := hf'.choose_spec
-  have hg := hg'.choose_spec
-  generalize_proofs hζ at hf hg
-  suffices f (hμ.toRootsOfUnity : Lˣ) = g (hμ.toRootsOfUnity : Lˣ) by
-    apply AlgEquiv.coe_algHom_injective
-    apply (hμ.powerBasis K).algHom_ext
-    exact this
-  rw [ZMod.natCast_eq_natCast_iff] at hfg
-  refine (hf.trans ?_).trans hg.symm
-  rw [← rootsOfUnity.coe_pow _ hf'.choose, ← rootsOfUnity.coe_pow _ hg'.choose]
-  congr 2
-  rw [pow_eq_pow_iff_modEq]
-  convert hfg
-  conv => enter [2]; rw [hμ.eq_orderOf, ← hμ.val_toRootsOfUnity_coe]
-  rw [orderOf_units, Subgroup.orderOf_coe]
+  apply AlgEquiv.coe_algHom_injective
+  apply (hμ.powerBasis K).algHom_ext
+  simpa only [IsPrimitiveRoot.autToPow_spec] using
+    congrArg (fun t : (ZMod n)ˣ ↦ μ ^ (t : ZMod n).val) hfg
 
 end IsPrimitiveRoot
 
diff --git a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
index dbc584d9b0124c..89702f2373b5ee 100644
--- a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
+++ b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
@@ -507,15 +507,9 @@ theorem norm_pow_sub_one_eq_prime_pow_of_ne_zero {k s : ℕ} (hζ : IsPrimitiveR
     (hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)) (hs : s ≤ k) (hk : k ≠ 0) :
     norm K (ζ ^ p ^ s - 1) = (p : K) ^ p ^ s := by
   by_cases htwo : p ^ (k - s + 1) = 2
-  · have hp : p = 2 := by
-      rw [← pow_one 2] at htwo
-      exact eq_of_prime_pow_eq (prime_iff.1 hpri.out) (prime_iff.1 Nat.prime_two) (succ_pos _) htwo
-    replace hs : s = k := by
-      rw [hp] at htwo
-      nth_rw 2 [← pow_one 2] at htwo
-      replace htwo := Nat.pow_right_injective rfl.le htwo
-      rw [add_eq_right, Nat.sub_eq_zero_iff_le] at htwo
-      exact le_antisymm hs htwo
+  · obtain ⟨hp, hks⟩ := (Nat.prime_two.pow_eq_iff).1 htwo
+    simp only [add_eq_right] at hks
+    replace hs : s = k := le_antisymm hs (Nat.sub_eq_zero_iff_le.mp hks)
     simp only [hp, hs] at hζ hirr hcycl ⊢
     obtain ⟨k₁, hk₁⟩ := Nat.exists_eq_succ_of_ne_zero hk
     rw [hζ.norm_pow_sub_one_two hirr, hk₁, _root_.pow_succ', pow_mul, neg_eq_neg_one_mul,
diff --git a/Mathlib/NumberTheory/Dioph.lean b/Mathlib/NumberTheory/Dioph.lean
index 55e4c5cd58f4bf..f6036bd8ce9efd 100644
--- a/Mathlib/NumberTheory/Dioph.lean
+++ b/Mathlib/NumberTheory/Dioph.lean
@@ -567,12 +567,8 @@ theorem sub_dioph : DiophFn fun v => f v - g v :=
     (diophFn_vec _).2 <|
       ext (D&1 D= D&0 D+ D&2 D∨ D&1 D≤ D&2 D∧ D&0 D= D.0) <|
         (vectorAll_iff_forall _).1 fun x y z =>
-          show y = x + z ∨ y ≤ z ∧ x = 0 ↔ y - z = x from
-            ⟨fun o => by
-              rcases o with (ae | ⟨yz, x0⟩)
-              · rw [ae, add_tsub_cancel_right]
-              · rw [x0, tsub_eq_zero_iff_le.mpr yz], by
-              lia⟩
+          show y = x + z ∨ y ≤ z ∧ x = 0 ↔ y - z = x by
+            grind
 
 @[inherit_doc]
 scoped infixl:80 " D- " => Dioph.sub_dioph
@@ -623,16 +619,10 @@ theorem div_dioph : DiophFn fun v => f v / g v :=
       ext this <|
         (vectorAll_iff_forall _).1 fun z x y =>
           show y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ x / y = z by
-            refine Iff.trans ?_ eq_comm
-            exact y.eq_zero_or_pos.elim
-              (fun y0 => by
-                rw [y0, Nat.div_zero]
-                exact ⟨fun o => (o.resolve_right fun ⟨_, h2⟩ => Nat.not_lt_zero _ h2).right,
-                  fun z0 => Or.inl ⟨rfl, z0⟩⟩)
-              fun ypos =>
-                Iff.trans ⟨fun o => o.resolve_left fun ⟨h1, _⟩ => Nat.ne_of_gt ypos h1, Or.inr⟩
-                  (le_antisymm_iff.trans <| and_congr (Nat.le_div_iff_mul_le ypos) <|
-                    Iff.trans ⟨lt_succ_of_le, le_of_lt_succ⟩ (div_lt_iff_lt_mul ypos)).symm
+            rcases y.eq_zero_or_pos with rfl | hy
+            · simp [eq_comm]
+            · rw [Nat.div_eq_iff hy, Nat.succ_mul]
+              grind
 
 end
 
diff --git a/Mathlib/NumberTheory/DiophantineApproximation/Basic.lean b/Mathlib/NumberTheory/DiophantineApproximation/Basic.lean
index fb3cee6e8ebfde..01103590a9dc78 100644
--- a/Mathlib/NumberTheory/DiophantineApproximation/Basic.lean
+++ b/Mathlib/NumberTheory/DiophantineApproximation/Basic.lean
@@ -338,18 +338,12 @@ theorem convergent_succ (ξ : ℝ) (n : ℕ) :
 /-- All convergents of `0` are zero. -/
 @[simp]
 theorem convergent_of_zero (n : ℕ) : convergent 0 n = 0 := by
-  induction n with
-  | zero => simp only [convergent_zero, floor_zero, cast_zero]
-  | succ n ih =>
-    simp only [ih, convergent_succ, floor_zero, cast_zero, fract_zero, add_zero, inv_zero]
+  induction n <;> simp [convergent, *]
 
 /-- If `ξ` is an integer, all its convergents equal `ξ`. -/
 @[simp]
 theorem convergent_of_int {ξ : ℤ} (n : ℕ) : convergent ξ n = ξ := by
-  cases n
-  · simp only [convergent_zero, floor_intCast]
-  · simp only [convergent_succ, floor_intCast, fract_intCast, convergent_of_zero, add_zero,
-      inv_zero]
+  cases n <;> simp [convergent, convergent_of_zero]
 
 end Real
 
diff --git a/Mathlib/NumberTheory/Divisors.lean b/Mathlib/NumberTheory/Divisors.lean
index 2985b5a21df28f..62d1c95d72b2d5 100644
--- a/Mathlib/NumberTheory/Divisors.lean
+++ b/Mathlib/NumberTheory/Divisors.lean
@@ -476,20 +476,13 @@ theorem Prime.prod_divisors {α : Type*} [CommMonoid α] {p : ℕ} {f : ℕ →
   rw [← cons_self_properDivisors h.ne_zero, prod_cons, h.prod_properDivisors]
 
 theorem properDivisors_eq_singleton_one_iff_prime : n.properDivisors = {1} ↔ n.Prime := by
-  refine ⟨?_, ?_⟩
-  · intro h
-    refine Nat.prime_def.mpr ⟨?_, fun m hdvd => ?_⟩
-    · match n with
-      | 0 => contradiction
-      | 1 => contradiction
-      | Nat.succ (Nat.succ n) => simp
-    · rw [← mem_singleton, ← h, mem_properDivisors]
-      have := Nat.le_of_dvd ?_ hdvd
-      · simpa [hdvd, this] using (le_iff_eq_or_lt.mp this).symm
-      · by_contra!
-        simp only [nonpos_iff_eq_zero.mp this] at h
-        contradiction
-  · exact fun h => Prime.properDivisors h
+  refine ⟨?_, Prime.properDivisors⟩
+  intro h
+  rw [Nat.prime_def_lt]
+  refine ⟨Nat.succ_le_iff.mpr <| one_mem_properDivisors_iff_one_lt.mp (by simp [h]), ?_⟩
+  intro m hm hdvd
+  have hm' : m ∈ n.properDivisors := mem_properDivisors.2 ⟨hdvd, hm⟩
+  simpa [h] using hm'
 
 theorem sum_properDivisors_eq_one_iff_prime : ∑ x ∈ n.properDivisors, x = 1 ↔ n.Prime := by
   rcases n with - | n
@@ -507,25 +500,18 @@ theorem sum_properDivisors_eq_one_iff_prime : ∑ x ∈ n.properDivisors, x = 1
 
 theorem mem_properDivisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) {x : ℕ} :
     x ∈ properDivisors (p ^ k) ↔ ∃ (j : ℕ) (_ : j < k), x = p ^ j := by
-  rw [mem_properDivisors, Nat.dvd_prime_pow pp, ← exists_and_right]
-  simp only [exists_prop, and_assoc]
-  apply exists_congr
-  intro a
-  constructor <;> intro h
-  · rcases h with ⟨_h_left, rfl, h_right⟩
-    rw [Nat.pow_lt_pow_iff_right pp.one_lt] at h_right
-    exact ⟨h_right, rfl⟩
-  · rcases h with ⟨h_left, rfl⟩
-    rw [Nat.pow_lt_pow_iff_right pp.one_lt]
-    simp [h_left, le_of_lt]
+  rw [mem_properDivisors, Nat.dvd_prime_pow pp]
+  constructor
+  · rintro ⟨⟨j, hjk, rfl⟩, hlt⟩
+    exact ⟨j, (Nat.pow_lt_pow_iff_right pp.one_lt).1 hlt, rfl⟩
+  · rintro ⟨j, hjk, rfl⟩
+    exact ⟨⟨j, le_of_lt hjk, rfl⟩, (Nat.pow_lt_pow_iff_right pp.one_lt).2 hjk⟩
 
 theorem properDivisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) :
     properDivisors (p ^ k) = (Finset.range k).map ⟨(p ^ ·), Nat.pow_right_injective pp.two_le⟩ := by
   ext a
-  simp only [mem_properDivisors, mem_map, mem_range, Function.Embedding.coeFn_mk]
-  have := mem_properDivisors_prime_pow pp k (x := a)
-  rw [mem_properDivisors] at this
-  grind
+  rw [mem_properDivisors_prime_pow pp]
+  simp [eq_comm]
 
 @[to_additive (attr := simp)]
 theorem prod_properDivisors_prime_pow {α : Type*} [CommMonoid α] {k p : ℕ} {f : ℕ → α}
@@ -562,19 +548,13 @@ lemma primeFactors_filter_dvd_of_dvd {m n : ℕ} (hn : n ≠ 0) (hmn : m ∣ n)
 @[simp]
 theorem image_div_divisors_eq_divisors (n : ℕ) :
     image (fun x : ℕ => n / x) n.divisors = n.divisors := by
-  by_cases hn : n = 0
-  · simp [hn]
-  ext a
-  constructor
-  · rw [mem_image]
-    rintro ⟨x, hx1, hx2⟩
-    rw [mem_divisors] at *
-    refine ⟨?_, hn⟩
-    rw [← hx2]
-    exact div_dvd_of_dvd hx1.1
-  · rw [mem_divisors, mem_image]
-    rintro ⟨h1, -⟩
-    exact ⟨n / a, mem_divisors.mpr ⟨div_dvd_of_dvd h1, hn⟩, Nat.div_div_self h1 hn⟩
+  calc
+    image (fun x : ℕ => n / x) n.divisors =
+        (n.divisors.map ⟨fun d => (n / d, d), fun _ _ => congr_arg Prod.snd⟩).image Prod.fst := by
+      rw [map_eq_image, image_image]
+      rfl
+    _ = n.divisorsAntidiagonal.image Prod.fst := by rw [map_div_left_divisors]
+    _ = n.divisors := image_fst_divisorsAntidiagonal
 
 @[to_additive (attr := simp) sum_div_divisors]
 theorem prod_div_divisors {α : Type*} [CommMonoid α] (n : ℕ) (f : ℕ → α) :
diff --git a/Mathlib/NumberTheory/EllipticDivisibilitySequence.lean b/Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
index d4bfbabee3cd4c..40c1765bbc97d6 100644
--- a/Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
+++ b/Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@@ -329,14 +329,9 @@ lemma normEDS_dvd_normEDS_two_mul (k : ℤ) : normEDS b c d k ∣ normEDS b c d
 lemma complEDS₂_mul_b (k : ℤ) : complEDS₂ b c d k * b =
     normEDS b c d (k - 1) ^ 2 * normEDS b c d (k + 2) -
       normEDS b c d (k - 2) * normEDS b c d (k + 1) ^ 2 := by
-  induction k using Int.negInduction with
-  | nat k =>
-    simp_rw [complEDS₂, normEDS, Int.even_add, Int.even_sub, even_two, iff_true, Int.not_even_one,
-      iff_false]
-    split_ifs <;> ring1
-  | neg ih =>
-    simp_rw [complEDS₂_neg, ← sub_neg_eq_add, ← neg_sub', ← neg_add', normEDS_neg, ih]
-    ring1
+  simp_rw [complEDS₂, normEDS, Int.even_add, Int.even_sub, even_two, iff_true, Int.not_even_one,
+    iff_false]
+  split_ifs <;> ring1
 
 lemma normEDS_even (m : ℤ) : normEDS b c d (2 * m) * b =
     normEDS b c d (m - 1) ^ 2 * normEDS b c d m * normEDS b c d (m + 2) -
diff --git a/Mathlib/NumberTheory/EulerProduct/Basic.lean b/Mathlib/NumberTheory/EulerProduct/Basic.lean
index e431e9b7960932..6d96ee82315380 100644
--- a/Mathlib/NumberTheory/EulerProduct/Basic.lean
+++ b/Mathlib/NumberTheory/EulerProduct/Basic.lean
@@ -366,15 +366,11 @@ This version is stated in the form of convergence of finite partial products. -/
 theorem eulerProduct_completely_multiplicative {f : ℕ →*₀ F} (hsum : Summable (‖f ·‖)) :
     Tendsto (fun n : ℕ ↦ ∏ p ∈ primesBelow n, (1 - f p)⁻¹) atTop (𝓝 (∑' n, f n)) := by
   have hmul {m n} (_ : Nat.Coprime m n) := f.map_mul m n
-  have := (eulerProduct_hasProd_mulIndicator f.map_one hmul hsum f.map_zero).tendsto_prod_nat
-  have H (n : ℕ) : ∏ p ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) p =
-                     ∏ p ∈ primesBelow n, (1 - f p)⁻¹ :=
-    prod_mulIndicator_eq_prod_filter
-      (range n) (fun _ ↦ fun p ↦ (1 - f p)⁻¹) (fun _ ↦ {p | Nat.Prime p}) id
-  have H' : {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) =
-              {p | Nat.Prime p}.mulIndicator (fun p ↦ ∑' e : ℕ, f (p ^ e)) :=
-    Set.mulIndicator_congr fun p hp ↦ one_sub_inv_eq_geometric_of_summable_norm hp hsum
-  simpa only [← H, H'] using this
+  have H (n : ℕ) :
+      ∏ p ∈ primesBelow n, (1 - f p)⁻¹ = ∏ p ∈ primesBelow n, ∑' e, f (p ^ e) := by
+    refine prod_congr rfl fun p hp ↦ ?_
+    exact one_sub_inv_eq_geometric_of_summable_norm (Nat.prime_of_mem_primesBelow hp) hsum
+  simpa [H] using (eulerProduct f.map_one hmul hsum f.map_zero)
 
 end EulerProduct
 
diff --git a/Mathlib/NumberTheory/FLT/Four.lean b/Mathlib/NumberTheory/FLT/Four.lean
index ecaa9ad5254fa0..8700d46b6fe258 100644
--- a/Mathlib/NumberTheory/FLT/Four.lean
+++ b/Mathlib/NumberTheory/FLT/Four.lean
@@ -112,16 +112,11 @@ theorem neg_of_minimal {a b c : ℤ} : Minimal a b c → Minimal a b (-c) := by
 theorem exists_odd_minimal {a b c : ℤ} (h : Fermat42 a b c) :
     ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 := by
   obtain ⟨a0, b0, c0, hf⟩ := exists_minimal h
-  rcases Int.emod_two_eq_zero_or_one a0 with hap | hap
-  · rcases Int.emod_two_eq_zero_or_one b0 with hbp | hbp
-    · exfalso
-      have h1 : 2 ∣ (Int.gcd a0 b0 : ℤ) :=
-        Int.dvd_coe_gcd (Int.dvd_of_emod_eq_zero hap) (Int.dvd_of_emod_eq_zero hbp)
-      rw [Int.isCoprime_iff_gcd_eq_one.mp (coprime_of_minimal hf)] at h1
-      revert h1
-      decide
-    · exact ⟨b0, ⟨a0, ⟨c0, minimal_comm hf, hbp⟩⟩⟩
-  exact ⟨a0, ⟨b0, ⟨c0, hf, hap⟩⟩⟩
+  rcases Int.emod_two_eq_zero_or_one a0 with ha0 | ha0
+  · refine ⟨b0, a0, c0, minimal_comm hf, ?_⟩
+    exact Int.odd_iff.mp <| Int.isCoprime_two_left.mp <|
+      IsCoprime.of_isCoprime_of_dvd_left (coprime_of_minimal hf) (Int.dvd_of_emod_eq_zero ha0)
+  · exact ⟨a0, b0, c0, hf, ha0⟩
 
 /-- We can assume that a minimal solution to `a ^ 4 + b ^ 4 = c ^ 2` has
 `a` odd and `c` positive. -/
@@ -188,10 +183,9 @@ theorem not_minimal {a b c : ℤ} (h : Minimal a b c) (ha2 : a % 2 = 1) (hc : 0
   -- Now use the fact that (b / 2) ^ 2 = m * r * s, and m, r and s are pairwise coprime to obtain
   -- i, j and k such that m = i ^ 2, r = j ^ 2 and s = k ^ 2.
   -- m and r * s are coprime because m = r ^ 2 + s ^ 2 and r and s are coprime.
-  have hcp : Int.gcd m (r * s) = 1 := by
+  have hcp : IsCoprime m (r * s) := by
     rw [htt3]
-    exact Int.isCoprime_iff_gcd_eq_one.mp
-      (Int.isCoprime_of_sq_sum' (Int.isCoprime_iff_gcd_eq_one.mpr htt4))
+    exact Int.isCoprime_of_sq_sum' (Int.isCoprime_iff_gcd_eq_one.mpr htt4)
   -- b is even because b ^ 2 = 2 * m * n.
   have hb2 : 2 ∣ b := by
     apply @Int.Prime.dvd_pow' _ 2 _ Nat.prime_two
@@ -203,27 +197,20 @@ theorem not_minimal {a b c : ℤ} (h : Minimal a b c) (ha2 : a % 2 = 1) (hc : 0
     linear_combination (-b - 2 * b') * hb2' + ht2 + 2 * m * htt2
   have hrsz : r * s ≠ 0 := by grind
   have h2b0 : b' ≠ 0 := by grind
-  obtain ⟨i, hi⟩ := Int.sq_of_gcd_eq_one hcp hs.symm
+  obtain ⟨i, hi⟩ := Int.sq_of_isCoprime hcp hs.symm
   -- use m is positive to exclude m = - i ^ 2
   have hi' : ¬m = -i ^ 2 := by
-    by_contra h1
-    have hit : -i ^ 2 ≤ 0 := neg_nonpos.mpr (sq_nonneg i)
-    rw [← h1] at hit
-    apply absurd h4 (not_lt.mpr hit)
+    intro h1
+    nlinarith [sq_nonneg i, h4, h1]
   replace hi : m = i ^ 2 := Or.resolve_right hi hi'
   rw [mul_comm] at hs
-  rw [Int.gcd_comm] at hcp
   -- obtain d such that r * s = d ^ 2
-  obtain ⟨d, hd⟩ := Int.sq_of_gcd_eq_one hcp hs.symm
+  obtain ⟨d, hd⟩ := Int.sq_of_isCoprime hcp.symm hs.symm
   -- (b / 2) ^ 2 and m are positive so r * s is positive
   have hd' : ¬r * s = -d ^ 2 := by
-    by_contra h1
+    intro h1
     rw [h1] at hs
-    have h2 : b' ^ 2 ≤ 0 := by
-      rw [hs, (by ring : -d ^ 2 * m = -(d ^ 2 * m))]
-      exact neg_nonpos.mpr ((mul_nonneg_iff_of_pos_right h4).mpr (sq_nonneg d))
-    have h2' : 0 ≤ b' ^ 2 := by apply sq_nonneg b'
-    exact absurd (lt_of_le_of_ne h2' (Ne.symm (pow_ne_zero _ h2b0))) (not_lt.mpr h2)
+    nlinarith [sq_nonneg d, h4, hs, sq_pos_of_ne_zero h2b0]
   replace hd : r * s = d ^ 2 := Or.resolve_right hd hd'
   -- r = +/- j ^ 2
   obtain ⟨j, hj⟩ := Int.sq_of_gcd_eq_one htt4 hd
diff --git a/Mathlib/NumberTheory/FLT/Polynomial.lean b/Mathlib/NumberTheory/FLT/Polynomial.lean
index b0a8332e0e8335..04b8a3e7837986 100644
--- a/Mathlib/NumberTheory/FLT/Polynomial.lean
+++ b/Mathlib/NumberTheory/FLT/Polynomial.lean
@@ -10,6 +10,7 @@ public import Mathlib.Algebra.GroupWithZero.Defs
 public import Mathlib.NumberTheory.FLT.Basic
 public import Mathlib.NumberTheory.FLT.MasonStothers
 public import Mathlib.RingTheory.Polynomial.Content
+public import Mathlib.RingTheory.Polynomial.IsIntegral
 public import Mathlib.Tactic.GCongr
 
 /-!
@@ -245,12 +246,8 @@ theorem fermatLastTheoremWith'_polynomial {n : ℕ} (hn : 3 ≤ n) (chn : (n : k
   set d := gcd a b
   have hd : d ≠ 0 := gcd_ne_zero_of_left ha
   rw [eq_a, eq_b, mul_pow, mul_pow, ← mul_add] at heq
-  have hdc : d ∣ c := by
-    -- TODO: This is basically reproving `IsIntegrallyClosed.pow_dvd_pow_iff`
-    have hn : 0 < n := by lia
-    have hdncn : d ^ n ∣ c ^ n := ⟨_, heq.symm⟩
-    simpa [dvd_iff_normalizedFactors_le_normalizedFactors, Multiset.le_iff_count, *] using hdncn
-  obtain ⟨c', eq_c⟩ := hdc
+  obtain ⟨c', eq_c⟩ := (IsIntegrallyClosed.pow_dvd_pow_iff (R := k[X]) (show n ≠ 0 by omega)).mp
+    ⟨_, heq.symm⟩
   rw [eq_a, mul_ne_zero_iff] at ha
   rw [eq_b, mul_ne_zero_iff] at hb
   rw [eq_c, mul_ne_zero_iff] at hc
@@ -266,8 +263,6 @@ theorem fermatLastTheoremWith'_polynomial {n : ℕ} (hn : 3 ≤ n) (chn : (n : k
     rw [← hc', C_ne_zero] at hc
     exact ⟨ha.right.isUnit_C, hb.right.isUnit_C, hc.right.isUnit_C⟩
   apply flt hn chn ha.right hb.right hc.right _ heq
-  convert isCoprime_div_gcd_div_gcd _
-  · exact EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_a.symm
-  · exact EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_b.symm
-  · rw [eq_b]
-    exact mul_ne_zero hb.right hb.left
+  simpa [EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_a.symm,
+    EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_b.symm] using
+    (isCoprime_div_gcd_div_gcd_of_gcd_ne_zero hd)
diff --git a/Mathlib/NumberTheory/FrobeniusNumber.lean b/Mathlib/NumberTheory/FrobeniusNumber.lean
index 961cb7ac5732a6..9a8dacc7137be5 100644
--- a/Mathlib/NumberTheory/FrobeniusNumber.lean
+++ b/Mathlib/NumberTheory/FrobeniusNumber.lean
@@ -72,18 +72,9 @@ theorem frobeniusNumber_pair (cop : Coprime m n) (hm : 1 < m) (hn : 1 < n) :
   · intro k hk
     dsimp at hk
     contrapose! hk
-    let x := chineseRemainder cop 0 k
-    have hx : x.val < m * n := chineseRemainder_lt_mul cop 0 k (ne_bot_of_gt hm) (ne_bot_of_gt hn)
-    suffices key : x.1 ≤ k by
-      obtain ⟨a, ha⟩ := modEq_zero_iff_dvd.mp x.2.1
-      obtain ⟨b, hb⟩ := (modEq_iff_dvd' key).mp x.2.2
-      exact ⟨a, b, by rw [mul_comm, ← ha, mul_comm, ← hb, Nat.add_sub_of_le key]⟩
-    refine x.2.2.le_of_lt_add (lt_of_le_of_lt ?_ (add_lt_add_left hk n))
-    rw [Nat.sub_add_cancel (le_tsub_of_add_le_left hmn)]
-    exact
-      ModEq.le_of_lt_add
-        (x.2.1.trans (modEq_zero_iff_dvd.mpr (Nat.dvd_sub (dvd_mul_right m n) dvd_rfl)).symm)
-        (lt_of_lt_of_le hx le_tsub_add)
+    obtain ⟨a, b, h⟩ := Nat.exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le m n k
+      (by simp [cop.gcd_eq_one]) (by grind [Nat.pred_mul, Nat.mul_pred, Nat.pred_eq_sub_one])
+    exact ⟨a, b, succ_inj.mp (congrArg succ h)⟩
 
 namespace Nat
 
diff --git a/Mathlib/NumberTheory/GaussSum.lean b/Mathlib/NumberTheory/GaussSum.lean
index dfe725f1e1c7d2..3bbcee92752b83 100644
--- a/Mathlib/NumberTheory/GaussSum.lean
+++ b/Mathlib/NumberTheory/GaussSum.lean
@@ -317,16 +317,8 @@ theorem FiniteField.two_pow_card {F : Type*} [Fintype F] [Field F] (hF : ringCha
   have h₁ : (fun (a : Fin 8) ↦ ↑(χ₈ a) * τ ^ (a : ℕ)) = fun a ↦ χ a * ↑(ψ₈char a) := by
     ext1; congr; apply pow_one
   have hg₁ : gaussSum χ ψ₈char = 2 * (τ - τ ^ 3) := by
-    rw [gaussSum, ← h₁, Fin.sum_univ_eight,
-      -- evaluate `χ₈`
-      show χ₈ 0 = 0 from rfl, show χ₈ 1 = 1 from rfl, show χ₈ 2 = 0 from rfl,
-      show χ₈ 3 = -1 from rfl, show χ₈ 4 = 0 from rfl, show χ₈ 5 = -1 from rfl,
-      show χ₈ 6 = 0 from rfl, show χ₈ 7 = 1 from rfl,
-      -- normalize exponents
-      show ((3 : Fin 8) : ℕ) = 3 from rfl, show ((5 : Fin 8) : ℕ) = 5 from rfl,
-      show ((7 : Fin 8) : ℕ) = 7 from rfl]
-    simp only [Int.cast_zero, zero_mul, Int.cast_one, Fin.val_one, pow_one, one_mul, zero_add,
-      Fin.val_two, add_zero, Int.reduceNeg, Int.cast_neg]
+    rw [gaussSum, ← h₁, Fin.sum_univ_eight]
+    norm_num [χ₈_nat_eq_if_mod_eight]
     linear_combination (τ ^ 3 - τ) * τ_spec
   have hg : gaussSum χ ψ₈char ^ 2 = χ (-1) * Fintype.card (ZMod 8) := by
     rw [hχ, one_mul, ZMod.card, Nat.cast_ofNat, hg₁]
diff --git a/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean b/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
index 0cd81ec05199da..ba9ee75e85b136 100644
--- a/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
+++ b/Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
@@ -273,15 +273,9 @@ lemma hf_modif_int :
     fun_prop (discharger := assumption)
   refine LocallyIntegrableOn.add (fun x hx ↦ ?_) (fun x hx ↦ ?_)
   · obtain ⟨s, hs, hs'⟩ := P.hf_int.sub (locallyIntegrableOn_const _) x hx
-    refine ⟨s, hs, ?_⟩
-    rw [IntegrableOn, integrable_indicator_iff measurableSet_Ioi, IntegrableOn,
-      Measure.restrict_restrict measurableSet_Ioi, ← IntegrableOn]
-    exact hs'.mono_set Set.inter_subset_right
+    exact ⟨s, hs, hs'.indicator measurableSet_Ioi⟩
   · obtain ⟨s, hs, hs'⟩ := P.hf_int.sub this x hx
-    refine ⟨s, hs, ?_⟩
-    rw [IntegrableOn, integrable_indicator_iff measurableSet_Ioo, IntegrableOn,
-      Measure.restrict_restrict measurableSet_Ioo, ← IntegrableOn]
-    exact hs'.mono_set Set.inter_subset_right
+    exact ⟨s, hs, hs'.indicator measurableSet_Ioo⟩
 
 lemma hf_modif_FE (x : ℝ) (hx : 0 < x) :
     P.f_modif (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x := by
diff --git a/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean b/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
index 44961ac970d49b..b6bd0e447a5270 100644
--- a/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
+++ b/Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
@@ -74,14 +74,8 @@ private theorem gauss_lemma_aux₁ (p : ℕ) [Fact p.Prime] {a : ℤ} (hap : (a
         split_ifs <;> simp)
     _ = (-1 : ZMod p) ^ #{x ∈ Ico 1 (p / 2).succ | ¬(a * x.cast : ZMod p).val ≤ p / 2} *
           ∏ x ∈ Ico 1 (p / 2).succ, ↑((a * x : ZMod p).valMinAbs.natAbs) := by
-      have :
-          (∏ x ∈ Ico 1 (p / 2).succ, if (a * x : ZMod p).val ≤ p / 2 then (1 : ZMod p) else -1) =
-          ∏ x ∈ Ico 1 (p / 2).succ with ¬(a * x.cast : ZMod p).val ≤ p / 2, -1 :=
-        prod_bij_ne_one (fun x _ _ => x)
-          (fun x => by split_ifs <;> (dsimp; simp_all))
-          (fun _ _ _ _ _ _ => id) (fun b h _ => ⟨b, by simp_all [-not_le]⟩)
-          (by intros; split_ifs at * <;> simp_all)
-      rw [prod_mul_distrib, this, prod_const]
+      rw [prod_mul_distrib, Finset.prod_ite]
+      simp
     _ = (-1 : ZMod p) ^ #{x ∈ Ico 1 (p / 2).succ | ¬(a * x.cast : ZMod p).val ≤ p / 2} *
           (p / 2)! := by
       rw [← prod_natCast, Finset.prod_eq_multiset_prod,
diff --git a/Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean b/Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
index c2e8ed6841c1f1..02f0187bd57beb 100644
--- a/Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
+++ b/Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
@@ -49,15 +49,8 @@ theorem Gamma_mem' {N} {γ : SL(2, ℤ)} : γ ∈ Gamma N ↔ SLMOD(N) γ = 1 :=
 @[simp]
 theorem Gamma_mem {N} {γ : SL(2, ℤ)} : γ ∈ Gamma N ↔ (γ 0 0 : ZMod N) = 1 ∧
     (γ 0 1 : ZMod N) = 0 ∧ (γ 1 0 : ZMod N) = 0 ∧ (γ 1 1 : ZMod N) = 1 := by
-  rw [Gamma_mem']
-  constructor
-  · intro h
-    simp [← SL_reduction_mod_hom_val N γ, h]
-  · intro h
-    ext i j
-    rw [SL_reduction_mod_hom_val N γ]
-    fin_cases i <;> fin_cases j <;> simp only
-    exacts [h.1, h.2.1, h.2.2.1, h.2.2.2]
+  rw [Gamma_mem', Matrix.SpecialLinearGroup.ext_iff]
+  simp [SL_reduction_mod_hom_val, Fin.forall_fin_two, and_assoc]
 
 theorem Gamma_normal : Subgroup.Normal (Gamma N) :=
   SLMOD(N).normal_ker
@@ -73,11 +66,7 @@ theorem Gamma_zero_bot : Gamma 0 = ⊥ := rfl
 
 lemma ModularGroup_T_pow_mem_Gamma (N M : ℤ) (hNM : N ∣ M) :
     (ModularGroup.T ^ M) ∈ Gamma (Int.natAbs N) := by
-  simp only [Gamma_mem, Fin.isValue, ModularGroup.coe_T_zpow, of_apply, cons_val', cons_val_zero,
-    empty_val', cons_val_fin_one, Int.cast_one, cons_val_one,
-    Int.cast_zero, and_self, and_true, true_and]
-  refine Iff.mpr (ZMod.intCast_zmod_eq_zero_iff_dvd M (Int.natAbs N)) ?_
-  simp only [Int.natCast_natAbs, abs_dvd, hNM]
+  simp [Gamma_mem, ModularGroup.coe_T_zpow, hNM, ZMod.intCast_zmod_eq_zero_iff_dvd, abs_dvd]
 
 instance instFiniteIndexGamma [NeZero N] : (Gamma N).FiniteIndex := Subgroup.finiteIndex_ker _
 
@@ -88,18 +77,15 @@ def Gamma0 : Subgroup SL(2, ℤ) where
   one_mem' := by simp
   mul_mem' := by
     intro a b ha hb
-    simp only [Set.mem_setOf_eq]
-    have h := (Matrix.two_mul_expl a.1 b.1).2.2.1
-    simp only [coe_mul, Set.mem_setOf_eq] at *
-    rw [h]
+    change (a 1 0 : ZMod N) = 0 at ha
+    change (b 1 0 : ZMod N) = 0 at hb
+    change (((a : Matrix (Fin 2) (Fin 2) ℤ) * b) 1 0 : ZMod N) = 0
+    rw [(Matrix.two_mul_expl a.1 b.1).2.2.1]
     simp [ha, hb]
   inv_mem' := by
     intro a ha
-    simp only [Set.mem_setOf_eq]
     rw [SL2_inv_expl a]
-    simp only [cons_val_zero, cons_val_one,
-      Int.cast_neg, neg_eq_zero, Set.mem_setOf_eq] at *
-    exact ha
+    simpa using ha
 
 @[simp]
 theorem Gamma0_mem {N} {A : SL(2, ℤ)} : A ∈ Gamma0 N ↔ (A 1 0 : ZMod N) = 0 :=
diff --git a/Mathlib/NumberTheory/ModularForms/Derivative.lean b/Mathlib/NumberTheory/ModularForms/Derivative.lean
index b557c4adfb676e..307338571f1eb2 100644
--- a/Mathlib/NumberTheory/ModularForms/Derivative.lean
+++ b/Mathlib/NumberTheory/ModularForms/Derivative.lean
@@ -61,16 +61,6 @@ theorem normalizedDerivOfComplex_add (F G : ℍ → ℂ) (hF : MDiff F) (hG : MD
   rw [show (F + G) ∘ ofComplex = F ∘ ofComplex + G ∘ ofComplex from rfl,
     deriv_add hFz hGz, mul_add]
 
-@[simp]
-theorem normalizedDerivOfComplex_sub (F G : ℍ → ℂ) (hF : MDiff F) (hG : MDiff G) :
-    D (F - G) = D F - D G := by
-  ext z
-  have hFz := UpperHalfPlane.mdifferentiableAt_iff.mp (hF z)
-  have hGz := UpperHalfPlane.mdifferentiableAt_iff.mp (hG z)
-  simp only [normalizedDerivOfComplex, Pi.sub_apply]
-  rw [show (F - G) ∘ ofComplex = F ∘ ofComplex - G ∘ ofComplex from rfl,
-    deriv_sub hFz hGz, mul_sub]
-
 @[simp]
 theorem normalizedDerivOfComplex_const (c : ℂ) : D (fun _ ↦ c) = 0 := by
   ext z
@@ -94,6 +84,11 @@ theorem normalizedDerivOfComplex_neg (F : ℍ → ℂ) (hF : MDiff F) : D (-F) =
   simp
 
 @[simp]
+theorem normalizedDerivOfComplex_sub (F G : ℍ → ℂ) (hF : MDiff F) (hG : MDiff G) :
+    D (F - G) = D F - D G := by
+  simpa [sub_eq_add_neg, normalizedDerivOfComplex_neg G hG] using
+    normalizedDerivOfComplex_add F (-G) hF hG.neg
+
 theorem normalizedDerivOfComplex_mul (F G : ℍ → ℂ) (hF : MDiff F) (hG : MDiff G) :
     D (F * G) = D F * G + F * D G := by
   ext z
diff --git a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/MDifferentiable.lean b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/MDifferentiable.lean
index aefab5b501e602..6a984fc91c380f 100644
--- a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/MDifferentiable.lean
+++ b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/MDifferentiable.lean
@@ -52,11 +52,7 @@ lemma eisSummand_extension_differentiableOn (k : ℤ) (a : Fin 2 → ℤ) :
 /-- Eisenstein series are MDifferentiable (i.e. holomorphic functions from `ℍ → ℂ`). -/
 theorem eisensteinSeriesSIF_mdifferentiable {k : ℤ} {N : ℕ} (hk : 3 ≤ k) (a : Fin 2 → ZMod N) :
     MDiff (eisensteinSeriesSIF a k) := by
-  intro τ
-  suffices DifferentiableAt ℂ (↑ₕeisensteinSeriesSIF a k) τ.1 by
-    convert MDifferentiableAt.comp τ (DifferentiableAt.mdifferentiableAt this) τ.mdifferentiable_coe
-    exact funext fun z ↦ (comp_ofComplex (eisensteinSeriesSIF a k) z).symm
-  refine DifferentiableOn.differentiableAt ?_ (isOpen_upperHalfPlaneSet.mem_nhds τ.2)
+  rw [UpperHalfPlane.mdifferentiable_iff]
   exact (eisensteinSeries_tendstoLocallyUniformlyOn hk a).differentiableOn
     (Eventually.of_forall fun s ↦ DifferentiableOn.fun_sum
     fun _ _ ↦ eisSummand_extension_differentiableOn _ _) isOpen_upperHalfPlaneSet
diff --git a/Mathlib/NumberTheory/ModularForms/SlashActions.lean b/Mathlib/NumberTheory/ModularForms/SlashActions.lean
index fed236496873e1..5b07a03c22e802 100644
--- a/Mathlib/NumberTheory/ModularForms/SlashActions.lean
+++ b/Mathlib/NumberTheory/ModularForms/SlashActions.lean
@@ -222,15 +222,11 @@ lemma prod_slash_sum_weights {ι : Type*} {k : ι → ℤ} {g : GL (Fin 2) ℝ}
   classical
   induction s using Finset.induction_on with
   | empty =>
-    simp only [sum_empty, prod_empty, Matrix.GeneralLinearGroup.val_det_apply, card_empty,
-      CharP.cast_eq_zero, zero_sub, Int.reduceNeg, zpow_neg, zpow_one]
     ext _
     simp [slash_apply]
   | insert i t hi IH =>
-    rcases t.eq_empty_or_nonempty with rfl | ht
-    · simp
     simp only [prod_insert hi, card_insert_of_notMem hi, Nat.cast_succ, add_sub_cancel_right,
-    show ∑ i ∈ insert i t, k i = (k i) + ∑ i ∈ t, k i by grind, mul_slash, IH, mul_smul_comm,
+      show ∑ i ∈ insert i t, k i = (k i) + ∑ i ∈ t, k i by grind, mul_slash, IH, mul_smul_comm,
       ← mul_smul]
     congr 1
     nth_rw 2 [show (#t : ℤ) = 1 + (#t - 1) by grind]
diff --git a/Mathlib/NumberTheory/NumberField/Basic.lean b/Mathlib/NumberTheory/NumberField/Basic.lean
index c1f618ca0f17ae..9a42072dc9ec8c 100644
--- a/Mathlib/NumberTheory/NumberField/Basic.lean
+++ b/Mathlib/NumberTheory/NumberField/Basic.lean
@@ -179,12 +179,8 @@ lemma mk_eq_mk (x y : K) (hx hy) : (⟨x, hx⟩ : 𝓞 K) = ⟨y, hy⟩ ↔ x =
 
 /-- The ring homomorphism `(𝓞 K) →+* (𝓞 L)` given by restricting a ring homomorphism
   `f : K →+* L` to `𝓞 K`. -/
-def mapRingHom {K L : Type*} [Field K] [Field L] (f : K →+* L) : (𝓞 K) →+* (𝓞 L) where
-  toFun k := ⟨f k.val, map_isIntegral_int f k.2⟩
-  map_zero' := by ext; simp only [map_mk, map_zero]
-  map_one' := by ext; simp only [map_mk, map_one]
-  map_add' x y := by ext; simp only [map_mk, map_add]
-  map_mul' x y := by ext; simp only [map_mk, map_mul]
+def mapRingHom {K L : Type*} [Field K] [Field L] (f : K →+* L) : (𝓞 K) →+* (𝓞 L) :=
+  f.toIntAlgHom.mapIntegralClosure.toRingHom
 
 @[simp]
 theorem mapRingHom_apply {K L : Type*} [Field K] [Field L] (f : K →+* L) (x : 𝓞 K) :
diff --git a/Mathlib/NumberTheory/NumberField/CMField.lean b/Mathlib/NumberTheory/NumberField/CMField.lean
index 91832e9ee88db2..0de92dc55ba7ed 100644
--- a/Mathlib/NumberTheory/NumberField/CMField.lean
+++ b/Mathlib/NumberTheory/NumberField/CMField.lean
@@ -439,6 +439,7 @@ theorem regOfFamily_realFunSystem :
     show f.symm w = (equivInfinitePlace K).symm w.1 by rfl,
     show algebraMap (𝓞 K) K _ = algebraMap K⁺ K _ by rfl, equivInfinitePlace_symm_apply]
   simp [f, g]
+  rfl
 
 theorem regulator_div_regulator_eq_two_pow_mul_indexRealUnits_inv :
     regulator K / regulator K⁺ = 2 ^ rank K * (indexRealUnits K : ℝ)⁻¹ := by
diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
index 0b4e379c0fbf4b..de6d39dd1b5878 100644
--- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
+++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
@@ -950,14 +950,9 @@ theorem norm_negAt [NumberField K] (x : mixedSpace K) :
 theorem negAt_symm :
     (negAt s).symm = negAt s := by
   ext x w
-  · by_cases hw : w ∈ s
-    · simp_rw [negAt_apply_isReal_and_mem _ hw, negAt, prodCongr_symm,
-        prodCongr_apply, piCongrRight_symm_apply, if_pos hw, symm_neg,
-        neg_apply]
-    · simp_rw [negAt_apply_isReal_and_notMem _ hw, negAt, prodCongr_symm,
-        prodCongr_apply, piCongrRight_symm_apply, if_neg hw, refl_symm,
-        refl_apply]
-  · rfl
+  · simp [negAt, ContinuousLinearEquiv.prodCongr_symm]
+    split_ifs <;> rfl
+  · simp [negAt, ContinuousLinearEquiv.prodCongr_symm]
 
 /-- For `x : mixedSpace K`, the set `signSet x` is the set of real places `w` s.t. `x w ≤ 0`. -/
 def signSet (x : mixedSpace K) : Set {w : InfinitePlace K // IsReal w} := {w | x.1 w ≤ 0}
diff --git a/Mathlib/NumberTheory/NumberField/Norm.lean b/Mathlib/NumberTheory/NumberField/Norm.lean
index 102e45e93da818..b65dd7b958957a 100644
--- a/Mathlib/NumberTheory/NumberField/Norm.lean
+++ b/Mathlib/NumberTheory/NumberField/Norm.lean
@@ -68,21 +68,6 @@ theorem norm_algebraMap (x : 𝓞 K) : norm K (algebraMap (𝓞 K) (𝓞 L) x) =
     RingOfIntegers.algebraMap_norm_algebraMap, Algebra.norm_algebraMap,
     RingOfIntegers.coe_eq_algebraMap, map_pow]
 
-theorem isUnit_norm_of_isGalois [FiniteDimensional K L] [IsGalois K L] {x : 𝓞 L} :
-    IsUnit (norm K x) ↔ IsUnit x := by
-  classical
-  refine ⟨fun hx => ?_, IsUnit.map _⟩
-  replace hx : IsUnit (algebraMap (𝓞 K) (𝓞 L) <| norm K x) := hx.map (algebraMap (𝓞 K) <| 𝓞 L)
-  refine @isUnit_of_mul_isUnit_right (𝓞 L) _ _
-    ⟨(univ \ {AlgEquiv.refl}).prod fun σ : Gal(L/K) => σ x,
-      prod_mem fun σ _ => x.2.map (σ : L →+* L).toIntAlgHom⟩ _ ?_
-  convert hx using 1
-  ext
-  convert_to ((univ \ {AlgEquiv.refl}).prod fun σ : Gal(L/K) => σ x) *
-    ∏ σ ∈ {(AlgEquiv.refl : Gal(L/K))}, σ x = _
-  · simp
-  · rw [prod_sdiff <| subset_univ _, ← norm_eq_prod_automorphisms, coe_algebraMap_norm]
-
 /-- If `L/K` is a finite Galois extension of fields, then, for all `(x : 𝓞 L)` we have that
 `x ∣ algebraMap (𝓞 K) (𝓞 L) (norm K x)`. -/
 theorem dvd_norm [FiniteDimensional K L] [IsGalois K L] (x : 𝓞 L) :
@@ -97,6 +82,11 @@ theorem dvd_norm [FiniteDimensional K L] [IsGalois K L] (x : 𝓞 L) :
   rw [coe_algebraMap_norm K x, norm_eq_prod_automorphisms]
   simp [← Finset.mul_prod_erase _ _ (mem_univ AlgEquiv.refl)]
 
+theorem isUnit_norm_of_isGalois [FiniteDimensional K L] [IsGalois K L] {x : 𝓞 L} :
+    IsUnit (norm K x) ↔ IsUnit x := by
+  refine ⟨fun hx => ?_, IsUnit.map _⟩
+  exact isUnit_of_dvd_unit (dvd_norm K x) (hx.map (algebraMap (𝓞 K) (𝓞 L)))
+
 variable (F : Type*) [Field F] [Algebra K F] [FiniteDimensional K F]
 
 theorem norm_norm [Algebra F L] [FiniteDimensional F L] [IsScalarTower K F L] (x : 𝓞 L) :
diff --git a/Mathlib/NumberTheory/Padics/Hensel.lean b/Mathlib/NumberTheory/Padics/Hensel.lean
index 9c4b4023cd42e1..72cfc150b69c63 100644
--- a/Mathlib/NumberTheory/Padics/Hensel.lean
+++ b/Mathlib/NumberTheory/Padics/Hensel.lean
@@ -101,6 +101,30 @@ theorem limit_zero_of_norm_tendsto_zero : F.aeval ncs.lim = 0 := by
 
 end
 
+private theorem a_soln_is_unique {p : ℕ} [Fact p.Prime] {R : Type*} [CommSemiring R]
+    [Algebra R ℤ_[p]] {F : Polynomial R} {a : ℤ_[p]} (ha : F.aeval a = 0) (z' : ℤ_[p])
+    (hz' : F.aeval z' = 0) (hnormz' : ‖z' - a‖ < ‖F.derivative.aeval a‖) : z' = a := by
+  let h := z' - a
+  let ⟨q, hq⟩ := (F.map (algebraMap R ℤ_[p])).binomExpansion a h
+  simp only [Polynomial.eval_map_algebraMap, Polynomial.derivative_map] at hq
+  have : (F.derivative.aeval a + q * h) * h = 0 :=
+    Eq.symm
+      (calc
+        0 = F.aeval (a + h) := show 0 = F.aeval (a + (z' - a)) by simp [hz']
+        _ = F.derivative.aeval a * h + q * h ^ 2 := by rw [hq, ha, zero_add]
+        _ = (F.derivative.aeval a + q * h) * h := by rw [sq, right_distrib, mul_assoc])
+  have : h = 0 :=
+    by_contra fun hne =>
+      have : F.derivative.aeval a + q * h = 0 :=
+        (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right hne
+      have : F.derivative.aeval a = -q * h := by simpa using eq_neg_of_add_eq_zero_left this
+      lt_irrefl ‖F.derivative.aeval a‖
+        (calc
+          ‖F.derivative.aeval a‖ = ‖q‖ * ‖h‖ := by simp [this]
+          _ ≤ 1 * ‖h‖ := by gcongr; apply PadicInt.norm_le_one
+          _ < ‖F.derivative.aeval a‖ := by simpa)
+  exact eq_of_sub_eq_zero (by rw [← this])
+
 section Hensel
 
 open Nat
@@ -411,64 +435,20 @@ private theorem soln_dist_to_a_lt_deriv : ‖soln - a‖ < ‖F.derivative.aeval
 
 private theorem soln_unique (z : ℤ_[p]) (hev : F.aeval z = 0)
     (hnlt : ‖z - a‖ < ‖F.derivative.aeval a‖) : z = soln := by
-  have soln_dist : ‖z - soln‖ < ‖F.derivative.aeval a‖ :=
+  have hsoln : ‖z - soln‖ < ‖F.derivative.aeval soln‖ := by
+    rw [soln_deriv_norm]
     calc
       ‖z - soln‖ = ‖z - a + (a - soln)‖ := by rw [sub_add_sub_cancel]
       _ ≤ max ‖z - a‖ ‖a - soln‖ := PadicInt.nonarchimedean _ _
       _ < ‖F.derivative.aeval a‖ :=
         max_lt hnlt ((norm_sub_rev soln a ▸ (soln_dist_to_a_lt_deriv hnorm)) hnsol)
-  let h := z - soln
-  let ⟨q, hq⟩ := (F.map (algebraMap R ℤ_[p])).binomExpansion soln h
-  simp only [Polynomial.eval_map_algebraMap, Polynomial.derivative_map] at hq
-  have : (F.derivative.aeval soln + q * h) * h = 0 :=
-    Eq.symm
-      (calc
-        0 = F.aeval (soln + h) := by simp [h, hev]
-        _ = F.derivative.aeval soln * h + q * h ^ 2 := by rw [hq, eval_soln, zero_add]
-        _ = (F.derivative.aeval soln + q * h) * h := by rw [sq, right_distrib, mul_assoc])
-  have : h = 0 :=
-    by_contra fun hne =>
-      have : F.derivative.aeval soln + q * h = 0 :=
-        (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right hne
-      have : F.derivative.aeval soln = -q * h := by simpa using eq_neg_of_add_eq_zero_left this
-      lt_irrefl ‖F.derivative.aeval soln‖
-        (calc
-          ‖F.derivative.aeval soln‖ = ‖-q * h‖ := by rw [this]
-          _ ≤ 1 * ‖h‖ := by
-            rw [norm_mul]
-            exact mul_le_mul_of_nonneg_right (PadicInt.norm_le_one _) (norm_nonneg _)
-          _ = ‖z - soln‖ := by simp [h]
-          _ < ‖F.derivative.aeval soln‖ := by rw [soln_deriv_norm]; apply soln_dist)
-  exact eq_of_sub_eq_zero (by rw [← this])
+  exact a_soln_is_unique (a := soln) (eval_soln hnorm) z hev hsoln
 
 end Hensel
 
 variable {p : ℕ} [Fact p.Prime] {R : Type*} [CommSemiring R] [Algebra R ℤ_[p]]
   {F : Polynomial R} {a : ℤ_[p]}
 
-private theorem a_soln_is_unique (ha : F.aeval a = 0) (z' : ℤ_[p]) (hz' : F.aeval z' = 0)
-    (hnormz' : ‖z' - a‖ < ‖F.derivative.aeval a‖) : z' = a := by
-  let h := z' - a
-  let ⟨q, hq⟩ := (F.map (algebraMap R ℤ_[p])).binomExpansion a h
-  simp only [Polynomial.eval_map_algebraMap, Polynomial.derivative_map] at hq
-  have : (F.derivative.aeval a + q * h) * h = 0 :=
-    Eq.symm
-      (calc
-        0 = F.aeval (a + h) := show 0 = F.aeval (a + (z' - a)) by simp [hz']
-        _ = F.derivative.aeval a * h + q * h ^ 2 := by rw [hq, ha, zero_add]
-        _ = (F.derivative.aeval a + q * h) * h := by rw [sq, right_distrib, mul_assoc])
-  have : h = 0 :=
-    by_contra fun hne =>
-      have : F.derivative.aeval a + q * h = 0 :=
-        (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right hne
-      have : F.derivative.aeval a = -q * h := by simpa using eq_neg_of_add_eq_zero_left this
-      lt_irrefl ‖F.derivative.aeval a‖
-        (calc
-          ‖F.derivative.aeval a‖ = ‖q‖ * ‖h‖ := by simp [this]
-          _ ≤ 1 * ‖h‖ := by gcongr; apply PadicInt.norm_le_one
-          _ < ‖F.derivative.aeval a‖ := by simpa)
-  exact eq_of_sub_eq_zero (by rw [← this])
-
 variable (hnorm : ‖F.aeval a‖ < ‖F.derivative.aeval a‖ ^ 2)
 include hnorm
 
diff --git a/Mathlib/NumberTheory/Padics/PadicNorm.lean b/Mathlib/NumberTheory/Padics/PadicNorm.lean
index 1da53df08a88fe..c982f7d244048b 100644
--- a/Mathlib/NumberTheory/Padics/PadicNorm.lean
+++ b/Mathlib/NumberTheory/Padics/PadicNorm.lean
@@ -6,6 +6,7 @@ Authors: Robert Y. Lewis
 module
 
 public import Mathlib.Algebra.Order.AbsoluteValue.Basic
+public import Mathlib.Algebra.Order.Ring.IsNonarchimedean
 public import Mathlib.NumberTheory.Padics.PadicVal.Basic
 
 /-!
@@ -195,28 +196,6 @@ protected theorem sub {q r : ℚ} : padicNorm p (q - r) ≤ max (padicNorm p q)
   rw [sub_eq_add_neg, ← padicNorm.neg r]
   exact padicNorm.nonarchimedean
 
-/-- If the `p`-adic norms of `q` and `r` are different, then the norm of `q + r` is equal to the max
-of the norms of `q` and `r`. -/
-theorem add_eq_max_of_ne {q r : ℚ} (hne : padicNorm p q ≠ padicNorm p r) :
-    padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r) := by
-  wlog hlt : padicNorm p r < padicNorm p q
-  · rw [add_comm, max_comm]
-    exact this hne.symm (hne.lt_or_gt.resolve_right hlt)
-  have : padicNorm p q ≤ max (padicNorm p (q + r)) (padicNorm p r) :=
-    calc
-      padicNorm p q = padicNorm p (q + r + (-r)) := by ring_nf
-      _ ≤ max (padicNorm p (q + r)) (padicNorm p (-r)) := padicNorm.nonarchimedean
-      _ = max (padicNorm p (q + r)) (padicNorm p r) := by simp
-  have hnge : padicNorm p r ≤ padicNorm p (q + r) := by
-    apply le_of_not_gt
-    intro hgt
-    rw [max_eq_right_of_lt hgt] at this
-    exact not_lt_of_ge this hlt
-  have : padicNorm p q ≤ padicNorm p (q + r) := by rwa [max_eq_left hnge] at this
-  apply _root_.le_antisymm
-  · apply padicNorm.nonarchimedean
-  · rwa [max_eq_left_of_lt hlt]
-
 /-- The `p`-adic norm is an absolute value: positive-definite and multiplicative, satisfying the
 triangle inequality. -/
 instance : IsAbsoluteValue (padicNorm p) where
@@ -225,6 +204,14 @@ instance : IsAbsoluteValue (padicNorm p) where
   abv_add' := padicNorm.triangle_ineq
   abv_mul' := padicNorm.mul
 
+/-- If the `p`-adic norms of `q` and `r` are different, then the norm of `q + r` is equal to the max
+of the norms of `q` and `r`. -/
+theorem add_eq_max_of_ne {q r : ℚ} (hne : padicNorm p q ≠ padicNorm p r) :
+    padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r) := by
+  simpa using IsNonarchimedean.add_eq_max_of_ne
+    (f := IsAbsoluteValue.toAbsoluteValue (padicNorm p))
+    (fun q r => padicNorm.nonarchimedean (p := p) (q := q) (r := r)) hne
+
 theorem dvd_iff_norm_le {n : ℕ} {z : ℤ} : ↑(p ^ n) ∣ z ↔ padicNorm p z ≤ (p : ℚ) ^ (-n : ℤ) := by
   unfold padicNorm; split_ifs with hz
   · norm_cast at hz
@@ -282,28 +269,21 @@ theorem not_int_of_not_padic_int (p : ℕ) {a : ℚ} [hp : Fact (Nat.Prime p)]
 theorem sum_lt {α : Type*} {F : α → ℚ} {t : ℚ} {s : Finset α} :
     s.Nonempty → (∀ i ∈ s, padicNorm p (F i) < t) → padicNorm p (∑ i ∈ s, F i) < t := by
   classical
-    refine s.induction_on (by rintro ⟨-, ⟨⟩⟩) ?_
-    rintro a S haS IH - ht
-    by_cases hs : S.Nonempty
-    · rw [Finset.sum_insert haS]
-      exact
-        lt_of_le_of_lt padicNorm.nonarchimedean
-          (max_lt (ht a (Finset.mem_insert_self a S))
-            (IH hs fun b hb ↦ ht b (Finset.mem_insert_of_mem hb)))
-    · simp_all
+  intro hs hF
+  exact lt_of_le_of_lt
+    (IsNonarchimedean.apply_sum_le_sup_of_isNonarchimedean
+      (f := padicNorm p) (nonarch := fun q r => padicNorm.nonarchimedean (p := p) (q := q) (r := r))
+      (s := s) hs (l := F))
+    ((Finset.sup'_lt_iff (s := s) (H := hs) (f := fun i => padicNorm p (F i))).2 hF)
 
 theorem sum_le {α : Type*} {F : α → ℚ} {t : ℚ} {s : Finset α} :
     s.Nonempty → (∀ i ∈ s, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ s, F i) ≤ t := by
   classical
-    refine s.induction_on (by rintro ⟨-, ⟨⟩⟩) ?_
-    rintro a S haS IH - ht
-    by_cases hs : S.Nonempty
-    · rw [Finset.sum_insert haS]
-      exact
-        padicNorm.nonarchimedean.trans
-          (max_le (ht a (Finset.mem_insert_self a S))
-            (IH hs fun b hb ↦ ht b (Finset.mem_insert_of_mem hb)))
-    · simp_all
+  intro hs hF
+  refine (IsNonarchimedean.apply_sum_le_sup_of_isNonarchimedean
+      (f := padicNorm p) (nonarch := fun q r => padicNorm.nonarchimedean (p := p) (q := q) (r := r))
+      (s := s) hs (l := F)).trans ?_
+  exact (Finset.sup'_le_iff (s := s) (H := hs) (f := fun i => padicNorm p (F i))).2 hF
 
 theorem sum_lt' {α : Type*} {F : α → ℚ} {t : ℚ} {s : Finset α}
     (hF : ∀ i ∈ s, padicNorm p (F i) < t) (ht : 0 < t) : padicNorm p (∑ i ∈ s, F i) < t := by
diff --git a/Mathlib/NumberTheory/Pell.lean b/Mathlib/NumberTheory/Pell.lean
index dfc17ffe74a9bb..9803dee41c9086 100644
--- a/Mathlib/NumberTheory/Pell.lean
+++ b/Mathlib/NumberTheory/Pell.lean
@@ -594,15 +594,10 @@ theorem eq_pow_of_nonneg {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : So
   rcases hay.eq_or_lt with hy | hy
   · -- case 1: `a = 1`
     refine ⟨0, ?_⟩
-    simp only [pow_zero]
-    ext <;> simp only [x_one, y_one]
-    · have prop := a.prop
-      rw [← hy, sq (0 : ℤ), zero_mul, mul_zero, sub_zero,
-        sq_eq_one_iff] at prop
-      refine prop.resolve_right fun hf => ?_
-      have := (hax.trans_eq hax').le.trans_eq hf
-      norm_num at this
-    · exact hy.symm
+    rcases eq_one_or_neg_one_iff_y_eq_zero.2 hy.symm with rfl | rfl
+    · simp
+    · exfalso
+      simp at hax'
   · -- case 2: `a ≥ a₁`
     have hx₁ : 1 < a.x := by nlinarith [a.prop, h.d_pos]
     have hxx₁ := h.mul_inv_x_pos hx₁ hy
diff --git a/Mathlib/NumberTheory/PellMatiyasevic.lean b/Mathlib/NumberTheory/PellMatiyasevic.lean
index 6d37f7176a03e6..49a8a2878b03d3 100644
--- a/Mathlib/NumberTheory/PellMatiyasevic.lean
+++ b/Mathlib/NumberTheory/PellMatiyasevic.lean
@@ -469,13 +469,7 @@ theorem dvd_of_ysq_dvd {n t} (h : yn a1 n * yn a1 n ∣ yn a1 t) : yn a1 n ∣ t
 set_option backward.isDefEq.respectTransparency false in
 theorem pellZd_succ_succ (n) :
     pellZd a1 (n + 2) + pellZd a1 n = (2 * a : ℕ) * pellZd a1 (n + 1) := by
-  have : (1 : ℤ√(d a1)) + ⟨a, 1⟩ * ⟨a, 1⟩ = ⟨a, 1⟩ * (2 * a) := by
-    rw [Zsqrtd.natCast_val]
-    change (⟨_, _⟩ : ℤ√(d a1)) = ⟨_, _⟩
-    rw [dz_val]
-    dsimp [az]
-    ext <;> dsimp <;> ring_nf
-  simpa [mul_add, mul_comm, mul_left_comm, add_comm] using congr_arg (· * pellZd a1 n) this
+  ext <;> simp [pellZd, xn_succ, yn_succ, dz_val, az] <;> ring_nf
 
 theorem xy_succ_succ (n) :
     xn a1 (n + 2) + xn a1 n =
diff --git a/Mathlib/NumberTheory/PrimeCounting.lean b/Mathlib/NumberTheory/PrimeCounting.lean
index e40e4157f90e8c..c4c1a2372d2426 100644
--- a/Mathlib/NumberTheory/PrimeCounting.lean
+++ b/Mathlib/NumberTheory/PrimeCounting.lean
@@ -82,11 +82,7 @@ theorem add_two_le_nth_prime (n : ℕ) : n + 2 ≤ nth Prime n :=
 theorem surjective_primeCounting' : Function.Surjective π' :=
   Nat.surjective_count_of_infinite_setOf infinite_setOf_prime
 
-theorem surjective_primeCounting : Function.Surjective π := by
-  suffices Function.Surjective (π ∘ fun n => n - 1) from this.of_comp
-  convert surjective_primeCounting'
-  ext
-  exact primeCounting_sub_one _
+theorem surjective_primeCounting : Function.Surjective π := fun n => ⟨nth Prime n - 1, by simp⟩
 
 open Filter
 
diff --git a/Mathlib/NumberTheory/PythagoreanTriples.lean b/Mathlib/NumberTheory/PythagoreanTriples.lean
index b48468311a88ab..3ce038ab7319ea 100644
--- a/Mathlib/NumberTheory/PythagoreanTriples.lean
+++ b/Mathlib/NumberTheory/PythagoreanTriples.lean
@@ -143,16 +143,11 @@ theorem even_odd_of_coprime (hc : Int.gcd x y = 1) :
 
 theorem gcd_dvd : (Int.gcd x y : ℤ) ∣ z := by
   by_cases h0 : Int.gcd x y = 0
-  · have hx : x = 0 := by
-      apply Int.natAbs_eq_zero.mp
-      apply Nat.eq_zero_of_gcd_eq_zero_left h0
-    have hy : y = 0 := by
-      apply Int.natAbs_eq_zero.mp
-      apply Nat.eq_zero_of_gcd_eq_zero_right h0
+  · obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0
     have hz : z = 0 := by
       simpa only [PythagoreanTriple, hx, hy, add_zero, zero_eq_mul, mul_zero,
         or_self_iff] using h
-    simp only [hz, dvd_zero]
+    simp [h0, hz]
   obtain ⟨k, x0, y0, _, h2, rfl, rfl⟩ :
     ∃ (k : ℕ) (x0 y0 : _), 0 < k ∧ Int.gcd x0 y0 = 1 ∧ x = x0 * k ∧ y = y0 * k :=
     Int.exists_gcd_one' (Nat.pos_of_ne_zero h0)
@@ -163,17 +158,11 @@ theorem gcd_dvd : (Int.gcd x y : ℤ) ∣ z := by
 
 theorem normalize : PythagoreanTriple (x / Int.gcd x y) (y / Int.gcd x y) (z / Int.gcd x y) := by
   by_cases h0 : Int.gcd x y = 0
-  · have hx : x = 0 := by
-      apply Int.natAbs_eq_zero.mp
-      apply Nat.eq_zero_of_gcd_eq_zero_left h0
-    have hy : y = 0 := by
-      apply Int.natAbs_eq_zero.mp
-      apply Nat.eq_zero_of_gcd_eq_zero_right h0
+  · obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0
     have hz : z = 0 := by
       simpa only [PythagoreanTriple, hx, hy, add_zero, zero_eq_mul, mul_zero,
         or_self_iff] using h
-    simp only [hx, hy, hz]
-    exact zero
+    simpa [h0, hx, hy, hz] using PythagoreanTriple.zero
   rcases h.gcd_dvd with ⟨z0, rfl⟩
   obtain ⟨k, x0, y0, k0, h2, rfl, rfl⟩ :
     ∃ (k : ℕ) (x0 y0 : _), 0 < k ∧ Int.gcd x0 y0 = 1 ∧ x = x0 * k ∧ y = y0 * k :=
@@ -528,12 +517,7 @@ theorem isPrimitiveClassified_of_coprime (hc : Int.gcd x y = 1) : h.IsPrimitiveC
 
 theorem classified : h.IsClassified := by
   by_cases h0 : Int.gcd x y = 0
-  · have hx : x = 0 := by
-      apply Int.natAbs_eq_zero.mp
-      apply Nat.eq_zero_of_gcd_eq_zero_left h0
-    have hy : y = 0 := by
-      apply Int.natAbs_eq_zero.mp
-      apply Nat.eq_zero_of_gcd_eq_zero_right h0
+  · obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0
     use 0, 1, 0
     simp [hx, hy]
   apply h.isClassified_of_normalize_isPrimitiveClassified
diff --git a/Mathlib/NumberTheory/RamificationInertia/Basic.lean b/Mathlib/NumberTheory/RamificationInertia/Basic.lean
index 05e2ed79846948..ec284285dbc2d5 100644
--- a/Mathlib/NumberTheory/RamificationInertia/Basic.lean
+++ b/Mathlib/NumberTheory/RamificationInertia/Basic.lean
@@ -399,16 +399,12 @@ theorem quotientToQuotientRangePowQuotSucc_surjective [IsDedekindDomain S]
     refine ⟨⟨_, Ideal.mem_map_of_mem _ (Submodule.neg_mem _ hz)⟩, ?_⟩
     rw [powQuotSuccInclusion_apply_coe, Subtype.coe_mk, Ideal.Quotient.mk_eq_mk, map_add,
       sub_add_cancel_left, map_neg]
-  letI := Classical.decEq (Ideal S)
-  rw [sup_eq_prod_inf_factors _ (pow_ne_zero _ hP0), normalizedFactors_pow,
-    normalizedFactors_irreducible ((Ideal.prime_iff_isPrime hP0).mpr hP).irreducible, normalize_eq,
-    Multiset.nsmul_singleton, Multiset.inter_replicate, Multiset.prod_replicate]
-  · rw [← Submodule.span_singleton_le_iff_mem, Ideal.submodule_span_eq] at a_mem a_notMem
-    rwa [Ideal.count_normalizedFactors_eq a_mem a_notMem, min_eq_left i.le_succ]
-  · intro ha
-    rw [Ideal.span_singleton_eq_bot.mp ha] at a_notMem
-    have := (P ^ (i + 1)).zero_mem
-    contradiction
+  rw [← Submodule.span_singleton_le_iff_mem, Ideal.submodule_span_eq] at a_mem a_notMem
+  have hspan0 : Ideal.span {a} ≠ ⊥ := by
+    intro ha
+    exact a_notMem (ha ▸ bot_le)
+  rw [sup_comm, irreducible_pow_sup hspan0 ((Ideal.prime_iff_isPrime hP0).mpr hP).irreducible]
+  rwa [Ideal.count_normalizedFactors_eq a_mem a_notMem, min_eq_left i.le_succ]
 
 /-- Quotienting `P^i / P^e` by its subspace `P^(i+1) ⧸ P^e` is
 `R ⧸ p`-linearly isomorphic to `S ⧸ P`. -/
diff --git a/Mathlib/NumberTheory/SmoothNumbers.lean b/Mathlib/NumberTheory/SmoothNumbers.lean
index ea9c32b88dd564..c7f743b8839274 100644
--- a/Mathlib/NumberTheory/SmoothNumbers.lean
+++ b/Mathlib/NumberTheory/SmoothNumbers.lean
@@ -224,35 +224,16 @@ def equivProdNatFactoredNumbers {s : Finset ℕ} {p : ℕ} (hp : p.Prime) (hs :
                             ⟨(m.primeFactorsList.filter (· ∈ s)).prod, prod_mem_factoredNumbers ..⟩)
   left_inv := by
     rintro ⟨e, m, hm₀, hm⟩
+    have hpm : ¬ p ∣ m := hp.coprime_iff_not_dvd.mp <| hp.factoredNumbers_coprime hs ⟨hm₀, hm⟩
     simp (etaStruct := .all) only [Prod.mk.injEq, Subtype.mk.injEq]
     constructor
-    · rw [factorization_mul (pos_iff_ne_zero.mp <| Nat.pow_pos hp.pos) hm₀]
-      simp only [factorization_pow, Finsupp.coe_add, Finsupp.coe_smul, nsmul_eq_mul,
-        Pi.natCast_def, cast_id, Pi.add_apply, Pi.mul_apply, hp.factorization_self,
-        mul_one, add_eq_left]
-      rw [← primeFactorsList_count_eq, count_eq_zero]
-      exact fun H ↦ hs (hm p H)
-    · nth_rewrite 2 [← prod_primeFactorsList hm₀]
-      refine prod_eq <|
-        (filter _ <| perm_primeFactorsList_mul (pow_ne_zero e hp.ne_zero) hm₀).trans ?_
-      rw [filter_append, hp.primeFactorsList_pow,
-          filter_eq_nil_iff.mpr fun q hq ↦ by rw [mem_replicate] at hq; simp [hq.2, hs],
-          nil_append, filter_eq_self.mpr fun q hq ↦ by simp only [hm q hq, decide_true]]
+    · rw [factorization_mul (pow_ne_zero e hp.ne_zero) hm₀, Finsupp.add_apply,
+        factorization_pow_self hp, factorization_eq_zero_of_not_dvd hpm, add_zero]
+    · simpa using Nat.ordCompl_pow_mul_of_not_dvd e hp hpm
   right_inv := by
     rintro ⟨m, hm₀, hm⟩
     simp only [Subtype.mk.injEq]
-    rw [← primeFactorsList_count_eq, ← prod_replicate, ← prod_append]
-    nth_rewrite 3 [← prod_primeFactorsList hm₀]
-    have : m.primeFactorsList.filter (· = p) = m.primeFactorsList.filter (· ∉ s) := by
-      refine (filter_congr fun q hq ↦ ?_).symm
-      simp only [decide_not]
-      rcases Finset.mem_insert.mp <| hm _ hq with h | h
-      · simp only [h, hs, decide_false, Bool.not_false, decide_true]
-      · simp only [h, decide_true, Bool.not_true, false_eq_decide_iff]
-        exact fun H ↦ hs <| H ▸ h
-    refine prod_eq <| (filter_eq p).symm ▸ this ▸ perm_append_comm.trans ?_
-    simp only [decide_not]
-    exact filter_append_perm (· ∈ s) (primeFactorsList m)
+    simpa using Nat.ordProj_mul_ordCompl_eq_self m p
 
 @[simp]
 lemma equivProdNatFactoredNumbers_apply {s : Finset ℕ} {p e m : ℕ} (hp : p.Prime) (hs : p ∉ s)
diff --git a/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean b/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
index 3d034f2c564cb5..7bdc8bc35c38a9 100644
--- a/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
+++ b/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
@@ -177,10 +177,8 @@ theorem toComplex_im_div (x y : ℤ[i]) : ((x / y : ℤ[i]) : ℂ).im = round (x
 
 theorem normSq_le_normSq_of_re_le_of_im_le {x y : ℂ} (hre : |x.re| ≤ |y.re|)
     (him : |x.im| ≤ |y.im|) : Complex.normSq x ≤ Complex.normSq y := by
-  rw [normSq_apply, normSq_apply, ← _root_.abs_mul_self, _root_.abs_mul, ←
-      _root_.abs_mul_self y.re, _root_.abs_mul y.re, ← _root_.abs_mul_self x.im,
-      _root_.abs_mul x.im, ← _root_.abs_mul_self y.im, _root_.abs_mul y.im]
-  gcongr
+  rw [Complex.normSq_apply, Complex.normSq_apply]
+  nlinarith [sq_le_sq.mpr hre, sq_le_sq.mpr him]
 
 theorem normSq_div_sub_div_lt_one (x y : ℤ[i]) :
     Complex.normSq ((x / y : ℂ) - ((x / y : ℤ[i]) : ℂ)) < 1 :=