address more comments

Mathlib/NumberTheory/FLT/MasonStothers.lean

@@ -59,37 +59,37 @@ theorem max₃_le {a b c d : Nat} : max₃ a b c ≤ d ↔ a ≤ d ∧ b ≤ d 
 
 
 /-- For a given polynomial `a`, `divRadical a` is `a` divided by its radical `radical a`.-/
-def divRadical (a : k[X]) : k[X] := a / (radical a)
+def divRadical (a : k[X]) : k[X] := a / radical a
 
 
-theorem hMul_radical_divRadical (a : k[X]) : (radical a) * (divRadical a) = a := by
+theorem mul_radical_divRadical (a : k[X]) : radical a * divRadical a = a := by
   rw [divRadical]
   rw [← EuclideanDomain.mul_div_assoc]
   ·refine mul_div_cancel_left₀ _ (radical_ne_zero a)
   exact radical_dvd_self a
 
 theorem divRadical_ne_zero {a : k[X]} (ha : a ≠ 0) : divRadical a ≠ 0 := by
-  rw [← hMul_radical_divRadical a] at ha
+  rw [← mul_radical_divRadical a] at ha
   exact right_ne_zero_of_mul ha
 
 theorem divRadical_isUnit {u : k[X]} (hu : IsUnit u) : IsUnit (divRadical u) := by
   rwa [divRadical, radical_unit_eq_one hu, EuclideanDomain.div_one]
 
-theorem eq_divRadical {a x : k[X]} (h : (radical a) * x = a) : x = divRadical a := by
+theorem eq_divRadical {a x : k[X]} (h : radical a * x = a) : x = divRadical a := by
   apply EuclideanDomain.eq_div_of_mul_eq_left (radical_ne_zero a)
   rwa [mul_comm]
 
-theorem divRadical_hMul {a b : k[X]} (hc : IsCoprime a b) :
-    divRadical (a * b) = (divRadical a) * (divRadical b) := by
+theorem divRadical_mul {a b : k[X]} (hc : IsCoprime a b) :
+    divRadical (a * b) = divRadical a * divRadical b := by
   by_cases ha : a = 0
   · rw [ha, MulZeroClass.zero_mul, divRadical, EuclideanDomain.zero_div, MulZeroClass.zero_mul]
   by_cases hb : b = 0
   · rw [hb, MulZeroClass.mul_zero, divRadical, EuclideanDomain.zero_div, MulZeroClass.mul_zero]
   symm; apply eq_divRadical
   rw [radical_mul hc]
-  rw [mul_mul_mul_comm, hMul_radical_divRadical, hMul_radical_divRadical]
+  rw [mul_mul_mul_comm, mul_radical_divRadical, mul_radical_divRadical]
 
-theorem divRadical_dvd_self (a : k[X]) : (divRadical a) ∣ a := by
+theorem divRadical_dvd_self (a : k[X]) : divRadical a ∣ a := by
   rw [divRadical]
   apply EuclideanDomain.div_dvd_of_dvd
   exact radical_dvd_self a
@@ -110,7 +110,7 @@ theorem divRadical_dvd_derivative (a : k[X]) : (divRadical a) ∣ (derivative a)
     · rw [pow_zero, derivative_one]
       apply dvd_zero
     · case succ i =>
-      rw [← mul_dvd_mul_iff_left (radical_ne_zero (p ^ i.succ)), hMul_radical_divRadical,
+      rw [← mul_dvd_mul_iff_left (radical_ne_zero (p ^ i.succ)), mul_radical_divRadical,
         radical_pow_of_prime hp i.succ_pos, derivative_pow_succ, ← mul_assoc]
       apply dvd_mul_of_dvd_left
       rw [mul_comm, mul_assoc]
@@ -122,7 +122,7 @@ theorem divRadical_dvd_derivative (a : k[X]) : (divRadical a) ∣ (derivative a)
       EuclideanDomain.isCoprime_of_dvd
         (fun ⟨hx, hy⟩ => not_isUnit_zero (hpxy (zero_dvd_iff.mpr hx) (zero_dvd_iff.mpr hy)))
         fun p hp _ hpx hpy => hp (hpxy hpx hpy)
-    rw [divRadical_hMul hc, derivative_mul]
+    rw [divRadical_mul hc, derivative_mul]
     exact dvd_add (mul_dvd_mul hx (divRadical_dvd_self y)) (mul_dvd_mul (divRadical_dvd_self x) hy)
 
 theorem divRadical_dvd_wronskian_left (a b : k[X]) : (divRadical a) ∣ wronskian a b := by
@@ -170,8 +170,8 @@ theorem IsCoprime.wronskian_eq_zero_iff {a b : k[X]} (hc : IsCoprime a b) :
 
 protected theorem IsCoprime.divRadical {a b : k[X]} (h : IsCoprime a b) :
     IsCoprime (divRadical a) (divRadical b) := by
-  rw [← hMul_radical_divRadical a] at h
-  rw [← hMul_radical_divRadical b] at h
+  rw [← mul_radical_divRadical a] at h
+  rw [← mul_radical_divRadical b] at h
   exact h.of_mul_left_right.of_mul_right_right
 
 private theorem abc_subcall {a b c w : k[X]} {hw : w ≠ 0} (wab : w = wronskian a b) (ha : a ≠ 0)
@@ -194,16 +194,12 @@ private theorem abc_subcall {a b c w : k[X]} {hw : w ≠ 0} (wab : w = wronskian
         rw [←
           Polynomial.natDegree_mul (divRadical_ne_zero habc) (radical_ne_zero (a * b * c))]
       _ = (a * b * c).natDegree := by
-        rw [mul_comm _ (radical _)]; rw [hMul_radical_divRadical (a * b * c)]
+        rw [mul_comm _ (radical _)]; rw [mul_radical_divRadical (a * b * c)]
       _ = a.natDegree + b.natDegree + c.natDegree := by
         rw [Polynomial.natDegree_mul hab hc, Polynomial.natDegree_mul ha hb]
   rw [t3] at t4
   exact Nat.lt_of_add_lt_add_left t4
 
-private theorem rot3_add {a b c : k[X]} : a + b + c = b + c + a := by ring_nf
-
-private theorem rot3_mul {a b c : k[X]} : a * b * c = b * c * a := by ring_nf
-
 /-- **Polynomial ABC theorem.** -/
 theorem Polynomial.abc {a b c : k[X]} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b)
     (hbc : IsCoprime b c) (hca : IsCoprime c a) (hsum : a + b + c = 0) :
@@ -213,7 +209,7 @@ theorem Polynomial.abc {a b c : k[X]} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠
   have wbc := wronskian_eq_of_sum_zero hsum
   set w := wronskian a b with wab
   have wca : w = wronskian c a := by
-    rw [rot3_add] at hsum
+    rw [add_rotate] at hsum
     have h := wronskian_eq_of_sum_zero hsum
     rw [← wbc] at h; exact h
   have abc_dr_dvd_w : divRadical (a * b * c) ∣ w := by
@@ -229,21 +225,20 @@ theorem Polynomial.abc {a b c : k[X]} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠
     have abdr_dvd_w := cop_ab_dr.mul_dvd adr_dvd_w bdr_dvd_w
     have abcdr_dvd_w := cop_abc_dr.mul_dvd abdr_dvd_w cdr_dvd_w
     convert abcdr_dvd_w using 1
-    rw [← divRadical_hMul hab]
-    rw [← divRadical_hMul _]
+    rw [← divRadical_mul hab]
+    rw [← divRadical_mul _]
     exact hca.symm.mul_left hbc
   by_cases hw : w = 0
   · right
     rw [hw] at wab wbc
     cases' hab.wronskian_eq_zero_iff.mp wab.symm with ga gb
     cases' hbc.wronskian_eq_zero_iff.mp wbc.symm with _ gc
-    refine ⟨ga, gb, gc⟩
+    exact ⟨ga, gb, gc⟩
   · left
     rw [max₃_add_distrib_right, max₃_le]
-    constructor
-    · rw [rot3_mul] at abc_dr_dvd_w ⊢
+    refine ⟨?_, ?_, ?_⟩
+    · rw [mul_rotate] at abc_dr_dvd_w ⊢
       apply abc_subcall wbc <;> assumption
-    constructor
-    · rw [rot3_mul, rot3_mul] at abc_dr_dvd_w ⊢
+    · rw [mul_rotate, mul_rotate] at abc_dr_dvd_w ⊢
       apply abc_subcall wca <;> assumption
     · apply abc_subcall wab <;> assumption