feat(archive/100-theorems-list/37_solution_of_cubic): golf (#13012)

Express one of the lemmas for the solution of the cubic as a giant `linear_combination` calculation.

archive/100-theorems-list/37_solution_of_cubic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Jeoff Lee. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeoff Lee
 -/
-import tactic.basic
+import tactic.linear_combination
 import ring_theory.roots_of_unity
 import ring_theory.polynomial.cyclotomic.basic
 
@@ -68,26 +68,18 @@ begin
   have h₁ : ∀ x a₁ a₂ a₃ : K, x = a₁ ∨ x = a₂ ∨ x = a₃ ↔ (x - a₁) * (x - a₂) * (x - a₃) = 0,
   { intros, simp only [mul_eq_zero, sub_eq_zero, or.assoc] },
   rw h₁,
-  suffices : x ^ 3 + 3 * p * x - 2 * q
-    = (x - (s - t)) * (x - (s * ω - t * ω^2)) * (x - (s * ω^2 - t * ω)),
-  { rw this, },
-  have hc : s^3 - t^3 = 2 * q,
-  { have : s ≠ 0 := λ h, by { apply hp_nonzero, rw [h, mul_zero] at ht, exact ht.symm },
-    have h_nonzero: q + r ≠ 0 := by { rw ← hs3, exact pow_ne_zero _ this },
-    have hp3 : p^3 = r^2 - q^2 := by { rw hr, ring },
-    calc    s^3 - t^3
-          = s^3 - p^3/s^3 : by { rw [← ht], field_simp, ring }
-      ... = (q+r) - (r^2-q^2)/(q+r) : by rw [hs3, hp3]
-      ... = (q+r) + (q-r) * ((q+r) / (q+r)) : by ring
-      ... = 2 * q : by { rw div_self h_nonzero, ring } },
-  symmetry,
-  calc (x - (s - t)) * (x - (s * ω - t * ω^2)) * (x - (s * ω^2 - t * ω))
-      = x^3 - (s-t) * (1+ω+ω^2) * x^2
-        + ((s^2+t^2)*ω*(1+ω+ω^2) - s*t*(-3 + 3*(1+ω+ω^2) + ω*(ω^3-1))) * x
-        - (s^3-t^3)*ω^3 + s*t*(s-t)*ω^2*(1+ω+ω^2) : by ring
-  ... = x^3 + 3*(t*s)*x - (s^3-t^3)
-    : by { rw [hω.pow_eq_one, cube_root_of_unity_sum hω], ring }
-  ... = x^3 + 3*p*x - 2*q : by rw [ht, hc]
+  refine eq.congr _ rfl,
+  have hs_nonzero : s ≠ 0,
+  { contrapose! hp_nonzero with hs_nonzero,
+    linear_combination (ht, -1) (hs_nonzero, t) },
+  rw ← mul_left_inj' (pow_ne_zero 3 hs_nonzero),
+  have H := cube_root_of_unity_sum hω,
+  linear_combination
+    (hr, 1)
+    (hs3, - q + r + s ^ 3)
+    (ht, -3 * x * s ^ 3 - (t * s) ^ 2 - (t * s) * p - p ^ 2)
+    (H, (x ^ 2 * (s - t) + x * (- ω * (s ^ 2 + t ^ 2) + s * t * (3 + ω ^ 2 - ω))
+        - (-(s ^ 3 - t ^ 3) * (ω - 1) + s^2 * t * ω ^ 2 - s * t^2 * ω ^ 2)) * s ^ 3),
 end
 
 /-- Roots of a monic cubic whose discriminant is nonzero. -/