awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
_ : ‖2 * sin (x / 2)‖ = 2 * |sin (x / 2)|
⊢ ‖2 * sin (x / 2)‖ ≤ ‖x‖
have _₁ : 2 * |x / 2| = ‖x‖
Tactic: calc
    _ = 2 * |Real.sin (x / 2)| := by simp
    _ ≤ 2 * |x / 2| := (mul_le_mul_iff_of_pos_left zero_lt_two).mpr Real.abs_sin_le_abs
    _ = _ := by rw [abs_div, Nat.abs_ofNat, Real.norm_eq_abs]; ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
⊢ ‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖ₑ ≤ ‖x‖ₑ
have rw : ENNReal.ofReal ‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖ ≤ ‖x‖ₑ
Tactic: rw [← enorm_norm, Real.enorm_of_nonneg (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
⊢ ENNReal.ofReal ‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖ ≤ ‖x‖ₑ
have rw : ENNReal.ofReal ‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖ ≤ ENNReal.ofReal ‖x‖
Tactic: rw [← enorm_norm, Real.enorm_of_nonneg (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
⊢ ‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖ₑ ≤ ‖x‖ₑ
have iterate : ENNReal.ofReal ‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖ ≤ ENNReal.ofReal ‖x‖
Tactic: iterate 2 rw [← enorm_norm, Real.enorm_of_nonneg (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds (goal)
Goal:
x : ℝ
⊢ ‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖₊ ≤ ‖x‖₊
have rw : (↑‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖₊ : ENNReal) ≤ (↑‖x‖₊ : ENNReal)
Tactic: rw [← ENNReal.coe_le_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = cos ((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) * θ)
ih2 : eval (cos θ) (T ℂ (↑n : ℤ)) = cos ((↑(↑n : ℤ) : ℂ) * θ)
⊢ eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = cos ((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) * θ)
have add_two : 2 * cos θ * cos ((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) * θ) =
  2 * cos (((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) * θ + (↑(↑n : ℤ) : ℂ) * θ) / 2) *
    cos (((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) * θ - (↑(↑n : ℤ) : ℂ) * θ) / 2)
Tactic: simp only [T_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add,
      cos_add_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = cos ((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) * θ)
ih2 : eval (cos θ) (T ℂ (↑n : ℤ)) = cos ((↑(↑n : ℤ) : ℂ) * θ)
⊢ 2 * cos θ * cos ((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) * θ) =
    2 * cos (((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) * θ + (↑(↑n : ℤ) : ℂ) * θ) / 2) *
      cos (((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) * θ - (↑(↑n : ℤ) : ℂ) * θ) / 2)
have add_two : 2 * cos θ * cos (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) =
  2 * cos ((HAdd.hAdd (α := ℂ) (↑n : ℂ) 2 * θ + (↑n : ℂ) * θ) / 2) *
    cos ((HAdd.hAdd (α := ℂ) (↑n : ℂ) 2 * θ - (↑n : ℂ) * θ) / 2)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (T ℂ (-(↑n : ℤ))) = cos ((↑(-(↑n : ℤ)) : ℂ) * θ)
ih2 : eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = cos ((↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ)
⊢ eval (cos θ) (T ℂ (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = cos ((↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ)
have neg_add_one : 2 * cos θ * cos ((↑(-(↑n : ℤ)) : ℂ) * θ) =
  2 * cos (((↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ + (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ) / 2) *
    cos (((↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ - (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ) / 2)
Tactic: simp only [T_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add',
      cos_add_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (T ℂ (-(↑n : ℤ))) = cos ((↑(-(↑n : ℤ)) : ℂ) * θ)
ih2 : eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = cos ((↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ)
⊢ 2 * cos θ * cos ((↑(-(↑n : ℤ)) : ℂ) * θ) =
    2 * cos (((↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ + (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ) / 2) *
      cos (((↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ - (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ) / 2)
have neg_add_one : 2 * cos θ * cos (-(↑n : ℂ) * θ) =
  2 * cos ((HAdd.hAdd (α := ℂ) (-(↑n : ℂ)) 1 * θ + HSub.hSub (α := ℂ) (-(↑n : ℂ)) 1 * θ) / 2) *
    cos ((HAdd.hAdd (α := ℂ) (-(↑n : ℂ)) 1 * θ - HSub.hSub (α := ℂ) (-(↑n : ℂ)) 1 * θ) / 2)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℤ
⊢ eval (cos θ) (T ℂ n) = cos ((↑n : ℂ) * θ)
have zero : eval (cos θ) (T ℂ 0) = cos ((↑0 : ℂ) * θ)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp only [T_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add,
      cos_add_cos]
    push_cast
    ring_nf
  | neg_add_one n ih1 ih2 =>
    simp only [T_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add',
      cos_add_cos]
    push_cast
    ring_nf
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℤ
zero : eval (cos θ) (T ℂ 0) = cos ((↑0 : ℂ) * θ)
⊢ eval (cos θ) (T ℂ n) = cos ((↑n : ℂ) * θ)
have one : eval (cos θ) (T ℂ 1) = cos ((↑1 : ℂ) * θ)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp only [T_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add,
      cos_add_cos]
    push_cast
    ring_nf
  | neg_add_one n ih1 ih2 =>
    simp only [T_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add',
      cos_add_cos]
    push_cast
    ring_nf
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℤ
zero : eval (cos θ) (T ℂ 0) = cos ((↑0 : ℂ) * θ)
one : eval (cos θ) (T ℂ 1) = cos ((↑1 : ℂ) * θ)
⊢ eval (cos θ) (T ℂ n) = cos ((↑n : ℂ) * θ)
have add_two : ∀ (n : ℕ) (ih1 : eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = cos ((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) * θ))
  (ih2 : eval (cos θ) (T ℂ (↑n : ℤ)) = cos ((↑(↑n : ℤ) : ℂ) * θ)),
  eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = cos ((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) * θ)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp only [T_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add,
      cos_add_cos]
    push_cast
    ring_nf
  | neg_add_one n ih1 ih2 =>
    simp only [T_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add',
      cos_add_cos]
    push_cast
    ring_nf
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℤ
zero : eval (cos θ) (T ℂ 0) = cos ((↑0 : ℂ) * θ)
one : eval (cos θ) (T ℂ 1) = cos ((↑1 : ℂ) * θ)
add_two :
  ∀ (n : ℕ)
    (ih1 : eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = cos ((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) * θ))
    (ih2 : eval (cos θ) (T ℂ (↑n : ℤ)) = cos ((↑(↑n : ℤ) : ℂ) * θ)),
    eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = cos ((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) * θ)
⊢ eval (cos θ) (T ℂ n) = cos ((↑n : ℂ) * θ)
have neg_add_one : ∀ (n : ℕ) (ih1 : eval (cos θ) (T ℂ (-(↑n : ℤ))) = cos ((↑(-(↑n : ℤ)) : ℂ) * θ))
  (ih2 : eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = cos ((↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ)),
  eval (cos θ) (T ℂ (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = cos ((↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp only [T_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add,
      cos_add_cos]
    push_cast
    ring_nf
  | neg_add_one n ih1 ih2 =>
    simp only [T_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add',
      cos_add_cos]
    push_cast
    ring_nf
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
⊢ eval (cos θ) (U ℂ 1) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑1 : ℂ) 1 * θ)
have one : 2 * cos θ * sin θ = 2 * sin θ * cos θ
Tactic: simp [one_add_one_eq_two, sin_two_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℕ
ih1 :
  eval (cos θ) (U ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) * sin θ =
    sin (HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) 1 * θ)
ih2 : eval (cos θ) (U ℂ (↑n : ℤ)) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑(↑n : ℤ) : ℂ) 1 * θ)
⊢ eval (cos θ) (U ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) * sin θ =
    sin (HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) 1 * θ)
have add_two : 2 * (cos θ * sin (HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) 1 * θ)) =
  2 *
    (sin
        ((HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) 1 * θ + HAdd.hAdd (α := ℂ) (↑(↑n : ℤ) : ℂ) 1 * θ) /
          2) *
      cos
        ((HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) 1 * θ - HAdd.hAdd (α := ℂ) (↑(↑n : ℤ) : ℂ) 1 * θ) /
          2))
Tactic: simp only [U_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
      mul_assoc, ih1, ih2, sub_eq_iff_eq_add, sin_add_sin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℕ
ih1 :
  eval (cos θ) (U ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) * sin θ =
    sin (HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) 1 * θ)
ih2 : eval (cos θ) (U ℂ (↑n : ℤ)) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑(↑n : ℤ) : ℂ) 1 * θ)
⊢ 2 * (cos θ * sin (HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) 1 * θ)) =
    2 *
      (sin
          ((HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) 1 * θ +
              HAdd.hAdd (α := ℂ) (↑(↑n : ℤ) : ℂ) 1 * θ) /
            2) *
        cos
          ((HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) 1 * θ -
              HAdd.hAdd (α := ℂ) (↑(↑n : ℤ) : ℂ) 1 * θ) /
            2))
have add_two : 2 * (cos θ * sin ((HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + 1) * θ)) =
  2 *
    (sin (((HAdd.hAdd (α := ℂ) (↑n : ℂ) 2 + 1) * θ + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) / 2) *
      cos (((HAdd.hAdd (α := ℂ) (↑n : ℂ) 2 + 1) * θ - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) / 2))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (-(↑n : ℤ))) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑(-(↑n : ℤ)) : ℂ) 1 * θ)
ih2 :
  eval (cos θ) (U ℂ (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) * sin θ =
    sin (HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) 1 * θ)
⊢ eval (cos θ) (U ℂ (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) * sin θ =
    sin (HAdd.hAdd (α := ℂ) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) 1 * θ)
have neg_add_one : 2 * (cos θ * sin (HAdd.hAdd (α := ℂ) (↑(-(↑n : ℤ)) : ℂ) 1 * θ)) =
  2 *
    (sin
        ((HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) 1 * θ +
            HAdd.hAdd (α := ℂ) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) 1 * θ) /
          2) *
      cos
        ((HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) 1 * θ -
            HAdd.hAdd (α := ℂ) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) 1 * θ) /
          2))
Tactic: simp only [U_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
      mul_assoc, ih1, ih2, sub_eq_iff_eq_add', sin_add_sin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (U ℂ (-(↑n : ℤ))) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑(-(↑n : ℤ)) : ℂ) 1 * θ)
ih2 :
  eval (cos θ) (U ℂ (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) * sin θ =
    sin (HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) 1 * θ)
⊢ 2 * (cos θ * sin (HAdd.hAdd (α := ℂ) (↑(-(↑n : ℤ)) : ℂ) 1 * θ)) =
    2 *
      (sin
          ((HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) 1 * θ +
              HAdd.hAdd (α := ℂ) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) 1 * θ) /
            2) *
        cos
          ((HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) 1 * θ -
              HAdd.hAdd (α := ℂ) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) 1 * θ) /
            2))
have neg_add_one : 2 * (cos θ * sin (HAdd.hAdd (α := ℂ) (-(↑n : ℂ)) 1 * θ)) =
  2 *
    (sin (((HAdd.hAdd (α := ℂ) (-(↑n : ℂ)) 1 + 1) * θ + (HSub.hSub (α := ℂ) (-(↑n : ℂ)) 1 + 1) * θ) / 2) *
      cos (((HAdd.hAdd (α := ℂ) (-(↑n : ℂ)) 1 + 1) * θ - (HSub.hSub (α := ℂ) (-(↑n : ℂ)) 1 + 1) * θ) / 2))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℤ
⊢ eval (cos θ) (U ℂ n) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
have zero : eval (cos θ) (U ℂ 0) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1 * θ)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp [one_add_one_eq_two, sin_two_mul]; ring
  | add_two n ih1 ih2 =>
    simp only [U_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
      mul_assoc, ih1, ih2, sub_eq_iff_eq_add, sin_add_sin]
    push_cast
    ring_nf
  | neg_add_one n ih1 ih2 =>
    simp only [U_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
      mul_assoc, ih1, ih2, sub_eq_iff_eq_add', sin_add_sin]
    push_cast
    ring_nf
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℤ
zero : eval (cos θ) (U ℂ 0) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1 * θ)
⊢ eval (cos θ) (U ℂ n) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
have one : eval (cos θ) (U ℂ 1) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑1 : ℂ) 1 * θ)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp [one_add_one_eq_two, sin_two_mul]; ring
  | add_two n ih1 ih2 =>
    simp only [U_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
      mul_assoc, ih1, ih2, sub_eq_iff_eq_add, sin_add_sin]
    push_cast
    ring_nf
  | neg_add_one n ih1 ih2 =>
    simp only [U_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
      mul_assoc, ih1, ih2, sub_eq_iff_eq_add', sin_add_sin]
    push_cast
    ring_nf
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℤ
zero : eval (cos θ) (U ℂ 0) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1 * θ)
one : eval (cos θ) (U ℂ 1) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑1 : ℂ) 1 * θ)
⊢ eval (cos θ) (U ℂ n) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
have add_two : ∀ (n : ℕ)
  (ih1 :
    eval (cos θ) (U ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) * sin θ =
      sin (HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) 1 * θ))
  (ih2 : eval (cos θ) (U ℂ (↑n : ℤ)) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑(↑n : ℤ) : ℂ) 1 * θ)),
  eval (cos θ) (U ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) * sin θ =
    sin (HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) 1 * θ)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp [one_add_one_eq_two, sin_two_mul]; ring
  | add_two n ih1 ih2 =>
    simp only [U_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
      mul_assoc, ih1, ih2, sub_eq_iff_eq_add, sin_add_sin]
    push_cast
    ring_nf
  | neg_add_one n ih1 ih2 =>
    simp only [U_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
      mul_assoc, ih1, ih2, sub_eq_iff_eq_add', sin_add_sin]
    push_cast
    ring_nf
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℤ
zero : eval (cos θ) (U ℂ 0) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1 * θ)
one : eval (cos θ) (U ℂ 1) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑1 : ℂ) 1 * θ)
add_two :
  ∀ (n : ℕ)
    (ih1 :
      eval (cos θ) (U ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) * sin θ =
        sin (HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) 1 * θ))
    (ih2 : eval (cos θ) (U ℂ (↑n : ℤ)) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑(↑n : ℤ) : ℂ) 1 * θ)),
    eval (cos θ) (U ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) * sin θ =
      sin (HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) 1 * θ)
⊢ eval (cos θ) (U ℂ n) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
have neg_add_one : ∀ (n : ℕ) (ih1 : eval (cos θ) (U ℂ (-(↑n : ℤ))) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑(-(↑n : ℤ)) : ℂ) 1 * θ))
  (ih2 :
    eval (cos θ) (U ℂ (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) * sin θ =
      sin (HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) 1 * θ)),
  eval (cos θ) (U ℂ (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) * sin θ =
    sin (HAdd.hAdd (α := ℂ) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) 1 * θ)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp [one_add_one_eq_two, sin_two_mul]; ring
  | add_two n ih1 ih2 =>
    simp only [U_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
      mul_assoc, ih1, ih2, sub_eq_iff_eq_add, sin_add_sin]
    push_cast
    ring_nf
  | neg_add_one n ih1 ih2 =>
    simp only [U_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
      mul_assoc, ih1, ih2, sub_eq_iff_eq_add', sin_add_sin]
    push_cast
    ring_nf
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℤ
⊢ eval (cosh θ) (T ℂ n) = eval (cos (θ * I)) (T ℂ n)
have rw : eval (cosh θ) (T ℂ n) = eval (cosh θ) (T ℂ n)
Tactic: rw [cos_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℤ
⊢ cos ((↑n : ℂ) * (θ * I)) = cos ((↑n : ℂ) * θ * I)
have rw : cos ((↑n : ℂ) * (θ * I)) = cos ((↑n : ℂ) * (θ * I))
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℤ
⊢ eval (cos (θ * I)) (U ℂ n) * sin (θ * I) * -I = sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (θ * I)) * -I
have rw : sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (θ * I)) * -I = sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (θ * I)) * -I
Tactic: rw [U_complex_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℤ
⊢ sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (θ * I)) * -I = sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ * I) * -I
have rw : sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (θ * I)) * -I = sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (θ * I)) * -I
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℤ
⊢ sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ * I) * -I = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
have rw : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * I * -I = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
Tactic: rw [sin_mul_I ((n + 1) * θ), mul_assoc, mul_neg, I_mul_I, neg_neg, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℤ
rw : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * I * -I = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
⊢ sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ * I) * -I = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
have rw₁ : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * (I * -I) = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
Tactic: rw [sin_mul_I ((n + 1) * θ), mul_assoc, mul_neg, I_mul_I, neg_neg, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℤ
rw : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * I * -I = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
rw₁ : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * (I * -I) = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
⊢ sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ * I) * -I = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
have rw₂ : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * -(I * I) = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
Tactic: rw [sin_mul_I ((n + 1) * θ), mul_assoc, mul_neg, I_mul_I, neg_neg, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℤ
rw : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * I * -I = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
rw₁ : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * (I * -I) = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
rw₂ : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * -(I * I) = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
⊢ sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ * I) * -I = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
have rw₃ : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * - -1 = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
Tactic: rw [sin_mul_I ((n + 1) * θ), mul_assoc, mul_neg, I_mul_I, neg_neg, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℤ
rw : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * I * -I = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
rw₁ : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * (I * -I) = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
rw₂ : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * -(I * I) = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
rw₃ : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * - -1 = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
⊢ sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ * I) * -I = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
have rw₄ : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * 1 = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
Tactic: rw [sin_mul_I ((n + 1) * θ), mul_assoc, mul_neg, I_mul_I, neg_neg, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic (goal)
Goal:
θ : ℂ
n : ℤ
rw : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * I * -I = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
rw₁ : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * (I * -I) = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
rw₂ : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * -(I * I) = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
rw₃ : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * - -1 = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
rw₄ : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) * 1 = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
⊢ sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ * I) * -I = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
have rw₅ : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
Tactic: rw [sin_mul_I ((n + 1) * θ), mul_assoc, mul_neg, I_mul_I, neg_neg, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
⊢ Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) ≠ 1
have contrapose : ∀ (hk : Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) = 1), HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
Tactic: contrapose hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) = 1
⊢ HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
have obtain : ∀ (m : ℤ) (hx : HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I = (↑m : ℂ) * (2 * (↑π : ℂ) * I)),
  HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
Tactic: obtain ⟨m, hx⟩ := Complex.exp_eq_one_iff.mp hk
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) = 1
m : ℤ
hx : HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I = (↑m : ℂ) * (2 * (↑π : ℂ) * I)
⊢ k = HMul.hMul (α := ℤ) 2 (↑n : ℤ) * m
have apply : Eq (α := ℂ) (↑k : ℂ) (↑(HMul.hMul (α := ℤ) 2 (↑n : ℤ) * m) : ℂ)
Tactic: apply (@Int.cast_inj ℂ _ _).mp