feat: the cosine of π / 5 is (1 + √5) / 4 (#17393)

Mathlib/Algebra/QuadraticDiscriminant.lean

@@ -15,7 +15,7 @@ This file defines the discriminant of a quadratic and gives the solution to a qu
 
 ## Main definition
 
-- `discrim a b c`: the discriminant of a quadratic `a * x * x + b * x + c` is `b * b - 4 * a * c`.
+- `discrim a b c`: the discriminant of a quadratic `a * (x * x) + b * x + c` is `b * b - 4 * a * c`.
 
 ## Main statements
 
@@ -48,7 +48,7 @@ def discrim [Ring R] (a b c : R) : R :=
 
 variable [CommRing R] {a b c : R}
 
-lemma discrim_eq_sq_of_quadratic_eq_zero {x : R} (h : a * x * x + b * x + c = 0) :
+lemma discrim_eq_sq_of_quadratic_eq_zero {x : R} (h : a * (x * x) + b * x + c = 0) :
     discrim a b c = (2 * a * x + b) ^ 2 := by
   rw [discrim]
   linear_combination -4 * a * h
@@ -57,7 +57,7 @@ lemma discrim_eq_sq_of_quadratic_eq_zero {x : R} (h : a * x * x + b * x + c = 0)
 -/
 theorem quadratic_eq_zero_iff_discrim_eq_sq [NeZero (2 : R)] [NoZeroDivisors R]
     (ha : a ≠ 0) (x : R) :
-    a * x * x + b * x + c = 0 ↔ discrim a b c = (2 * a * x + b) ^ 2 := by
+    a * (x * x) + b * x + c = 0 ↔ discrim a b c = (2 * a * x + b) ^ 2 := by
   refine ⟨discrim_eq_sq_of_quadratic_eq_zero, fun h ↦ ?_⟩
   rw [discrim] at h
   have ha : 2 * 2 * a ≠ 0 := mul_ne_zero (mul_ne_zero (NeZero.ne _) (NeZero.ne _)) ha
@@ -66,7 +66,7 @@ theorem quadratic_eq_zero_iff_discrim_eq_sq [NeZero (2 : R)] [NoZeroDivisors R]
 
 /-- A quadratic has no root if its discriminant has no square root. -/
 theorem quadratic_ne_zero_of_discrim_ne_sq (h : ∀ s : R, discrim a b c ≠ s^2) (x : R) :
-    a * x * x + b * x + c ≠ 0 :=
+    a * (x * x) + b * x + c ≠ 0 :=
   mt discrim_eq_sq_of_quadratic_eq_zero (h _)
 
 end Ring
@@ -77,7 +77,7 @@ variable {K : Type*} [Field K] [NeZero (2 : K)] {a b c x : K}
 
 /-- Roots of a quadratic equation. -/
 theorem quadratic_eq_zero_iff (ha : a ≠ 0) {s : K} (h : discrim a b c = s * s) (x : K) :
-    a * x * x + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a) := by
+    a * (x * x) + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a) := by
   rw [quadratic_eq_zero_iff_discrim_eq_sq ha, h, sq, mul_self_eq_mul_self_iff]
   field_simp
   apply or_congr
@@ -86,15 +86,15 @@ theorem quadratic_eq_zero_iff (ha : a ≠ 0) {s : K} (h : discrim a b c = s * s)
 
 /-- A quadratic has roots if its discriminant has square roots -/
 theorem exists_quadratic_eq_zero (ha : a ≠ 0) (h : ∃ s, discrim a b c = s * s) :
-    ∃ x, a * x * x + b * x + c = 0 := by
+    ∃ x, a * (x * x) + b * x + c = 0 := by
   rcases h with ⟨s, hs⟩
   use (-b + s) / (2 * a)
   rw [quadratic_eq_zero_iff ha hs]
   simp
 
 /-- Root of a quadratic when its discriminant equals zero -/
 theorem quadratic_eq_zero_iff_of_discrim_eq_zero (ha : a ≠ 0) (h : discrim a b c = 0) (x : K) :
-    a * x * x + b * x + c = 0 ↔ x = -b / (2 * a) := by
+    a * (x * x) + b * x + c = 0 ↔ x = -b / (2 * a) := by
   have : discrim a b c = 0 * 0 := by rw [h, mul_zero]
   rw [quadratic_eq_zero_iff ha this, add_zero, sub_zero, or_self_iff]
 
@@ -105,7 +105,7 @@ section LinearOrderedField
 variable {K : Type*} [LinearOrderedField K] {a b c : K}
 
 /-- If a polynomial of degree 2 is always nonnegative, then its discriminant is nonpositive -/
-theorem discrim_le_zero (h : ∀ x : K, 0 ≤ a * x * x + b * x + c) : discrim a b c ≤ 0 := by
+theorem discrim_le_zero (h : ∀ x : K, 0 ≤ a * (x * x) + b * x + c) : discrim a b c ≤ 0 := by
   rw [discrim, sq]
   obtain ha | rfl | ha : a < 0 ∨ a = 0 ∨ 0 < a := lt_trichotomy a 0
   -- if a < 0
@@ -114,7 +114,7 @@ theorem discrim_le_zero (h : ∀ x : K, 0 ≤ a * x * x + b * x + c) : discrim a
         ((tendsto_atBot_add_const_right _ b (tendsto_id.const_mul_atTop_of_neg ha)).atBot_mul_atTop
           tendsto_id)
     rcases (this.eventually (eventually_lt_atBot 0)).exists with ⟨x, hx⟩
-    exact False.elim ((h x).not_lt <| by rwa [← add_mul])
+    exact False.elim ((h x).not_lt <| by rwa [← mul_assoc, ← add_mul])
   -- if a = 0
   · rcases eq_or_ne b 0 with (rfl | hb)
     · simp
@@ -127,22 +127,22 @@ theorem discrim_le_zero (h : ∀ x : K, 0 ≤ a * x * x + b * x + c) : discrim a
     field_simp
     ring
 
-lemma discrim_le_zero_of_nonpos (h : ∀ x : K, a * x * x + b * x + c ≤ 0) : discrim a b c ≤ 0 :=
+lemma discrim_le_zero_of_nonpos (h : ∀ x : K, a * (x * x) + b * x + c ≤ 0) : discrim a b c ≤ 0 :=
   discrim_neg a b c ▸ discrim_le_zero <| by simpa only [neg_mul, ← neg_add, neg_nonneg]
 
 /-- If a polynomial of degree 2 is always positive, then its discriminant is negative,
 at least when the coefficient of the quadratic term is nonzero.
 -/
-theorem discrim_lt_zero (ha : a ≠ 0) (h : ∀ x : K, 0 < a * x * x + b * x + c) :
+theorem discrim_lt_zero (ha : a ≠ 0) (h : ∀ x : K, 0 < a * (x * x) + b * x + c) :
     discrim a b c < 0 := by
-  have : ∀ x : K, 0 ≤ a * x * x + b * x + c := fun x => le_of_lt (h x)
+  have : ∀ x : K, 0 ≤ a * (x * x) + b * x + c := fun x => le_of_lt (h x)
   refine lt_of_le_of_ne (discrim_le_zero this) fun h' ↦ ?_
   have := h (-b / (2 * a))
   have : a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0 := by
-    rw [quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))]
+    rw [mul_assoc, quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))]
   linarith
 
-lemma discrim_lt_zero_of_neg (ha : a ≠ 0) (h : ∀ x : K, a * x * x + b * x + c < 0) :
+lemma discrim_lt_zero_of_neg (ha : a ≠ 0) (h : ∀ x : K, a * (x * x) + b * x + c < 0) :
     discrim a b c < 0 :=
   discrim_neg a b c ▸ discrim_lt_zero (neg_ne_zero.2 ha) <| by
     simpa only [neg_mul, ← neg_add, neg_pos]

Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin Davidson
 -/
+import Mathlib.Algebra.QuadraticDiscriminant
 import Mathlib.Analysis.SpecialFunctions.Exp
 import Mathlib.Tactic.Positivity.Core
 import Mathlib.Algebra.Ring.NegOnePow
@@ -795,6 +796,49 @@ theorem sin_pi_div_three : sin (π / 3) = √3 / 2 := by
   congr
   ring
 
+theorem quadratic_root_cos_pi_div_five :
+    letI c := cos (π / 5)
+    4 * c ^ 2 - 2 * c - 1 = 0 := by
+  set θ := π / 5 with hθ
+  set c := cos θ
+  set s := sin θ
+  suffices 2 * c = 4 * c ^ 2 - 1 by simp [this]
+  have hs : s ≠ 0 := by
+    rw [ne_eq, sin_eq_zero_iff, hθ]
+    push_neg
+    intro n hn
+    replace hn : n * 5 = 1 := by field_simp [mul_comm _ π, mul_assoc] at hn; norm_cast at hn
+    rcases Int.mul_eq_one_iff_eq_one_or_neg_one.mp hn with ⟨_, h⟩ | ⟨_, h⟩ <;> norm_num at h
+  suffices s * (2 * c) = s * (4 * c ^ 2 - 1) from mul_left_cancel₀ hs this
+  calc s * (2 * c) = 2 * s * c := by rw [← mul_assoc, mul_comm 2]
+                 _ = sin (2 * θ) := by rw [sin_two_mul]
+                 _ = sin (π - 2 * θ) := by rw [sin_pi_sub]
+                 _ = sin (2 * θ + θ) := by congr; field_simp [hθ]; linarith
+                 _ = sin (2 * θ) * c + cos (2 * θ) * s := sin_add (2 * θ) θ
+                 _ = 2 * s * c * c + cos (2 * θ) * s := by rw [sin_two_mul]
+                 _ = 2 * s * c * c + (2 * c ^ 2 - 1) * s := by rw [cos_two_mul]
+                 _ = s * (2 * c * c) + s * (2 * c ^ 2 - 1) := by linarith
+                 _ = s * (4 * c ^ 2 - 1) := by linarith
+
+open Polynomial in
+theorem Polynomial.isRoot_cos_pi_div_five :
+    (4 • X ^ 2 - 2 • X - C 1 : ℝ[X]).IsRoot (cos (π / 5)) := by
+  simpa using quadratic_root_cos_pi_div_five
+
+/-- The cosine of `π / 5` is `(1 + √5) / 4`. -/
+@[simp]
+theorem cos_pi_div_five : cos (π / 5) = (1 + √5) / 4 := by
+  set c := cos (π / 5)
+  have : 4 * (c * c) + (-2) * c + (-1) = 0 := by
+    rw [← sq, neg_mul, ← sub_eq_add_neg, ← sub_eq_add_neg]
+    exact quadratic_root_cos_pi_div_five
+  have hd : discrim 4 (-2) (-1) = (2 * √5) * (2 * √5) := by norm_num [discrim, mul_mul_mul_comm]
+  rcases (quadratic_eq_zero_iff (by norm_num) hd c).mp this with h | h
+  · field_simp [h]; linarith
+  · absurd (show 0 ≤ c from cos_nonneg_of_mem_Icc <| by constructor <;> linarith [pi_pos.le])
+    rw [not_le, h]
+    exact div_neg_of_neg_of_pos (by norm_num [lt_sqrt]) (by positivity)
+
 end CosDivSq
 
 /-- `Real.sin` as an `OrderIso` between `[-(π / 2), π / 2]` and `[-1, 1]`. -/

Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean

@@ -172,7 +172,7 @@ theorem cos_eq_iff_quadratic {z w : ℂ} :
 
 theorem cos_surjective : Function.Surjective cos := by
   intro x
-  obtain ⟨w, w₀, hw⟩ : ∃ w ≠ 0, 1 * w * w + -2 * x * w + 1 = 0 := by
+  obtain ⟨w, w₀, hw⟩ : ∃ w ≠ 0, 1 * (w * w) + -2 * x * w + 1 = 0 := by
     rcases exists_quadratic_eq_zero one_ne_zero
         ⟨_, (cpow_nat_inv_pow _ two_ne_zero).symm.trans <| pow_two _⟩ with
       ⟨w, hw⟩

Mathlib/Geometry/Euclidean/Basic.lean

@@ -113,8 +113,9 @@ another point. -/
 theorem dist_smul_vadd_eq_dist {v : V} (p₁ p₂ : P) (hv : v ≠ 0) (r : ℝ) :
     dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂ ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫ / ⟪v, v⟫ := by
   conv_lhs =>
-    rw [← mul_self_inj_of_nonneg dist_nonneg dist_nonneg, dist_smul_vadd_sq, ← sub_eq_zero,
-      add_sub_assoc, dist_eq_norm_vsub V p₁ p₂, ← real_inner_self_eq_norm_mul_norm, sub_self]
+    rw [← mul_self_inj_of_nonneg dist_nonneg dist_nonneg, dist_smul_vadd_sq, mul_assoc,
+      ← sub_eq_zero, add_sub_assoc, dist_eq_norm_vsub V p₁ p₂, ← real_inner_self_eq_norm_mul_norm,
+      sub_self]
   have hvi : ⟪v, v⟫ ≠ 0 := by simpa using hv
   have hd : discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 = 2 * ⟪v, p₁ -ᵥ p₂⟫ * (2 * ⟪v, p₁ -ᵥ p₂⟫) := by
     rw [discrim]