refactor(NumberTheory): golf Mathlib/NumberTheory/ADEInequality (#38351)

- golfs `ADEInequality` by replacing repeated `inv_le_inv₀` proof blocks with direct applications of `inv_anti₀`
- shortens `lt_three`, `lt_four`, and `lt_six` by removing the now-unneeded fixed-denominator positivity witnesses

Extracted from #38144

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Author: yuanyi-350

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