chore: delete unused private lemma in Complex/exponential (#19263)

leanprover-community · Nov 20, 2024 · ef950f1 · ef950f1
1 parent 650a3f8
commit ef950f1
Showing 1 changed file with 0 additions and 5 deletions.
diff --git a/Mathlib/Data/Complex/Exponential.lean b/Mathlib/Data/Complex/Exponential.lean
@@ -456,9 +456,6 @@ theorem cos_zero : cos 0 = 1 := by simp [cos]
 @[simp]
 theorem cos_neg : cos (-x) = cos x := by simp [cos, sub_eq_add_neg, exp_neg, add_comm]
 
-private theorem cos_add_aux {a b c d : ℂ} :
-    (a + b) * (c + d) - (b - a) * (d - c) * -1 = 2 * (a * c + b * d) := by ring
-
 theorem cos_add : cos (x + y) = cos x * cos y - sin x * sin y := by
   rw [← cosh_mul_I, add_mul, cosh_add, cosh_mul_I, cosh_mul_I, sinh_mul_I, sinh_mul_I,
     mul_mul_mul_comm, I_mul_I, mul_neg_one, sub_eq_add_neg]
@@ -1498,5 +1495,3 @@ theorem abs_exp_eq_iff_re_eq {x y : ℂ} : abs (exp x) = abs (exp y) ↔ x.re =
   rw [abs_exp, abs_exp, Real.exp_eq_exp]
 
 end Complex
-
-set_option linter.style.longFile 1700