awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
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 * θ)
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))
⊢ 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:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
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 (α := ℂ) (↑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:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
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 * θ)
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))
⊢ eval (cos θ) (U ℂ (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) * sin θ =
    sin (HAdd.hAdd (α := ℂ) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) 1 * θ)

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]

Premises used: Polynomial.eval_X, mul_assoc, Polynomial.Chebyshev.U_sub_one, Polynomial.eval_mul, sub_mul, Complex.sin_add_sin, Polynomial.eval_ofNat, Polynomial.eval_sub, sub_eq_iff_eq_add'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
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 * θ)
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))
⊢ 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:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
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 (α := ℂ) (-(↑n : ℂ)) 1 + 1) * θ + (HSub.hSub (α := ℂ) (-(↑n : ℂ)) 1 + 1) * θ) / 2) *
        cos (((HAdd.hAdd (α := ℂ) (-(↑n : ℂ)) 1 + 1) * θ - (HSub.hSub (α := ℂ) (-(↑n : ℂ)) 1 + 1) * θ) / 2))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
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 * θ)
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 * θ)
⊢ eval (cos θ) (U ℂ n) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 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

Premises used: Polynomial.eval_X, Complex.sin_two_mul, mul_assoc, Polynomial.Chebyshev.U_sub_one, Polynomial.eval_mul, one_add_one_eq_two, sub_mul, Polynomial.Chebyshev.U_add_two, sub_eq_iff_eq_add, Complex.sin_add_sin, Polynomial.eval_ofNat, Polynomial.eval_sub, sub_eq_iff_eq_add'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
n : ℤ
⊢ eval (2 * cos θ) (C ℂ n) = 2 * cos ((↑n : ℂ) * θ)

Tactic:
simp [C_eq_two_mul_T_comp_half_mul_X]

Premises used: Polynomial.Chebyshev.C_eq_two_mul_T_comp_half_mul_X
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
n : ℤ
⊢ eval (2 * cos θ) (S ℂ n) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)

Tactic:
simp [S_eq_U_comp_half_mul_X]

Premises used: Polynomial.Chebyshev.S_eq_U_comp_half_mul_X
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
n : ℤ
rw rw₁ : eval (cosh θ) (T ℂ n) = eval (cosh θ) (T ℂ n)
⊢ eval (cosh θ) (T ℂ n) = eval (cos (θ * I)) (T ℂ n)

Tactic:
rw [cos_mul_I]

Premises used: Complex.cos_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
n : ℤ
rw rw₁ : cos ((↑n : ℂ) * (θ * I)) = cos ((↑n : ℂ) * (θ * I))
⊢ cos ((↑n : ℂ) * (θ * I)) = cos ((↑n : ℂ) * θ * I)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
n : ℤ
⊢ eval (cosh θ) (U ℂ n) * sinh θ = eval (cos (θ * I)) (U ℂ n) * sin (θ * I) * -I

Tactic:
simp [cos_mul_I, sin_mul_I, mul_assoc]

Premises used: Complex.cos_mul_I, mul_assoc, Complex.sin_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
n : ℤ
rw rw₁ : sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (θ * I)) * -I = sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (θ * I)) * -I
⊢ eval (cos (θ * I)) (U ℂ n) * sin (θ * I) * -I = sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (θ * I)) * -I

Tactic:
rw [U_complex_cos]

Premises used: Polynomial.Chebyshev.U_complex_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
n : ℤ
rw rw₁ : sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (θ * I)) * -I = sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (θ * I)) * -I
⊢ sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (θ * I)) * -I = sin (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ * I) * -I

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
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 * θ)
rw₅ rw₆ : sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)
⊢ sin (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]

Premises used: Int.cast, HMul.hMul, mul_assoc, neg_neg, HAdd.hAdd, Complex.I_mul_I, Complex.sin_mul_I, mul_one, OfNat.ofNat, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
n : ℤ
⊢ eval (2 * cosh θ) (C ℂ n) = 2 * cosh ((↑n : ℂ) * θ)

Tactic:
simp [C_eq_two_mul_T_comp_half_mul_X]

Premises used: Polynomial.Chebyshev.C_eq_two_mul_T_comp_half_mul_X
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
n : ℤ
⊢ eval (2 * cosh θ) (S ℂ n) * sinh θ = sinh (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ)

Tactic:
simp [S_eq_U_comp_half_mul_X]

Premises used: Polynomial.Chebyshev.S_eq_U_comp_half_mul_X
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℝ
n : ℤ
⊢ eval (cos θ) (T ℝ n) = cos ((↑n : ℝ) * θ)

Tactic:
mod_cast T_complex_cos θ n

Premises used: Int.cast, Polynomial.eval, HMul.hMul, Polynomial.Chebyshev.T, Complex.cos, Real.cos, congrArg, cast, Complex.ofReal, Complex.ofReal_mul._simp_1, Polynomial.Chebyshev.T_complex_cos, Complex.ofReal_cos._simp_1, congr, Polynomial.Chebyshev.complex_ofReal_eval_T._simp_1, congrFun', Complex, Eq, Complex.ofReal_inj._simp_1, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℝ
n : ℤ
⊢ eval (cos θ) (U ℝ n) * sin θ = sin (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * θ)

Tactic:
mod_cast U_complex_cos θ n

Premises used: Int.cast, Polynomial.eval, Real, HMul.hMul, Polynomial.Chebyshev.U, Complex.cos, Real.cos, congrArg, Complex.sin, cast, Polynomial.Chebyshev.complex_ofReal_eval_U._simp_1, Int.cast_add, Complex.ofReal_add, Complex.ofReal, Nat.cast, Complex.ofReal_mul._simp_1, Complex.ofReal_cos._simp_1, HAdd.hAdd, congr, Polynomial.Chebyshev.U_complex_cos, Complex.ofReal_sin._simp_1, Int.cast_add._simp_1, congrFun', Complex, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Real.sin, Int.cast_one, Complex.ofReal_inj._simp_1, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℝ
n : ℤ
⊢ eval (2 * cos θ) (C ℝ n) = 2 * cos ((↑n : ℝ) * θ)

Tactic:
mod_cast C_two_mul_complex_cos θ n

Premises used: Int.cast, Polynomial.eval, HMul.hMul, Complex.cos, Real.cos, congrArg, cast, Polynomial.Chebyshev.complex_ofReal_eval_C._simp_1, Complex.ofReal, Nat.cast, Complex.ofReal_mul._simp_1, Polynomial.Chebyshev.C, Complex.ofReal_cos._simp_1, congr, Polynomial.Chebyshev.C_two_mul_complex_cos, congrFun', Complex, OfNat.ofNat, Eq, Complex.ofReal_inj._simp_1, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℝ
n : ℤ
⊢ eval (2 * cos θ) (S ℝ n) * sin θ = sin (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * θ)

Tactic:
mod_cast S_two_mul_complex_cos θ n

Premises used: Polynomial.Chebyshev.S_two_mul_complex_cos, Int.cast, Polynomial.eval, Real, HMul.hMul, Complex.cos, Real.cos, congrArg, Polynomial.Chebyshev.complex_ofReal_eval_S._simp_1, Complex.sin, cast, Polynomial.Chebyshev.S, Int.cast_add, Complex.ofReal_add, Complex.ofReal, Nat.cast, Complex.ofReal_mul._simp_1, Complex.ofReal_cos._simp_1, HAdd.hAdd, congr, Complex.ofReal_sin._simp_1, Int.cast_add._simp_1, congrFun', Complex, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Real.sin, Int.cast_one, Complex.ofReal_inj._simp_1, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℝ
n : ℤ
⊢ eval (cosh θ) (T ℝ n) = cosh ((↑n : ℝ) * θ)

Tactic:
mod_cast T_complex_cosh θ n

Premises used: Int.cast, Polynomial.eval, HMul.hMul, Polynomial.Chebyshev.T, congrArg, cast, Polynomial.Chebyshev.T_complex_cosh, Complex.ofReal, Complex.ofReal_mul._simp_1, congr, Polynomial.Chebyshev.complex_ofReal_eval_T._simp_1, Real.cosh, Complex.ofReal_cosh._simp_1, congrFun', Complex, Eq, Complex.ofReal_inj._simp_1, Eq.trans, Complex.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℝ
n : ℤ
⊢ eval (cosh θ) (U ℝ n) * sinh θ = sinh (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * θ)

Tactic:
mod_cast U_complex_cosh θ n

Premises used: Int.cast, Polynomial.eval, Real, Complex.sinh, HMul.hMul, Polynomial.Chebyshev.U, congrArg, Complex.ofReal_sinh._simp_1, cast, Polynomial.Chebyshev.complex_ofReal_eval_U._simp_1, Int.cast_add, Real.sinh, Complex.ofReal_add, Complex.ofReal, Nat.cast, Complex.ofReal_mul._simp_1, Polynomial.Chebyshev.U_complex_cosh, HAdd.hAdd, congr, Real.cosh, Complex.ofReal_cosh._simp_1, Int.cast_add._simp_1, congrFun', Complex, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Int.cast_one, Complex.ofReal_inj._simp_1, Eq.trans, Complex.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℝ
n : ℤ
⊢ eval (2 * cosh θ) (C ℝ n) = 2 * cosh ((↑n : ℝ) * θ)

Tactic:
mod_cast C_two_mul_complex_cosh θ n

Premises used: Int.cast, Polynomial.eval, HMul.hMul, congrArg, cast, Polynomial.Chebyshev.C_two_mul_complex_cosh, Polynomial.Chebyshev.complex_ofReal_eval_C._simp_1, Complex.ofReal, Nat.cast, Complex.ofReal_mul._simp_1, Polynomial.Chebyshev.C, congr, Real.cosh, Complex.ofReal_cosh._simp_1, congrFun', Complex, OfNat.ofNat, Eq, Complex.ofReal_inj._simp_1, Eq.trans, Complex.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℝ
n : ℤ
⊢ eval (2 * cosh θ) (S ℝ n) * sinh θ = sinh (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * θ)

Tactic:
mod_cast S_two_mul_complex_cosh θ n

Premises used: Int.cast, Polynomial.eval, Real, Complex.sinh, HMul.hMul, congrArg, Polynomial.Chebyshev.complex_ofReal_eval_S._simp_1, Complex.ofReal_sinh._simp_1, cast, Polynomial.Chebyshev.S, Int.cast_add, Real.sinh, Complex.ofReal_add, Complex.ofReal, Nat.cast, Complex.ofReal_mul._simp_1, HAdd.hAdd, Polynomial.Chebyshev.S_two_mul_complex_cosh, congr, Real.cosh, Complex.ofReal_cosh._simp_1, Int.cast_add._simp_1, congrFun', Complex, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Int.cast_one, Complex.ofReal_inj._simp_1, Eq.trans, Complex.cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
contrapose :
  ∀ (hk : Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) = 1), HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
⊢ Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) ≠ 1

Tactic:
contrapose hk
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) = 1
obtain :
  ∀ (m : ℤ) (hx : HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I = (↑m : ℂ) * (2 * (↑π : ℂ) * I)),
    HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
⊢ HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k

Tactic:
obtain ⟨m, hx⟩ := Complex.exp_eq_one_iff.mp hk

Premises used: Iff.mp, Complex.exp_eq_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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)
apply : Eq (α := ℂ) (↑k : ℂ) (↑(HMul.hMul (α := ℤ) 2 (↑n : ℤ) * m) : ℂ)
⊢ k = HMul.hMul (α := ℤ) 2 (↑n : ℤ) * m

Tactic:
apply (@Int.cast_inj ℂ _ _).mp

Premises used: Int.cast_inj, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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)
a :
  (↑k : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I) * ((↑n : ℂ) / (↑π : ℂ) / I) -
      (HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑m : ℂ) +
        HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I * ((↑n : ℂ) / (↑π : ℂ) / I)) =
    0
⊢ (↑k : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I) * ((↑n : ℂ) / (↑π : ℂ) / I) -
      ((↑(HMul.hMul (α := ℤ) 2 (↑n : ℤ) * m) : ℂ) +
        HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I * ((↑n : ℂ) / (↑π : ℂ) / I)) =
    0

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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)
⊢ Ne (α := ℂ) (↑n : ℂ) 0

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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 : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I) * ((↑n : ℂ) / (↑π : ℂ) / I) -
      (HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑m : ℂ) +
        HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I * ((↑n : ℂ) / (↑π : ℂ) / I)) =
    0

Tactic:
field [show (n : ℂ) ≠ 0 by aesop]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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)
a :
  (↑k : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I) * ((↑n : ℂ) / (↑π : ℂ) / I) -
      ((↑(HMul.hMul (α := ℤ) 2 (↑n : ℤ) * m) : ℂ) +
        HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I * ((↑n : ℂ) / (↑π : ℂ) / I)) =
    0
⊢ Eq (α := ℂ) (↑k : ℂ) (↑(HMul.hMul (α := ℤ) 2 (↑n : ℤ) * m) : ℂ)

Tactic:
linear_combination (norm := (push_cast; field [show (n : ℂ) ≠ 0 by aesop])) hx * (n / π / I)

Premises used: Real.pi, HDiv.hDiv, Complex.ofReal, Nat.cast, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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

Tactic:
have h : k = 2 * n * m := by
    apply (@Int.cast_inj ℂ _ _).mp
    linear_combination (norm := (push_cast; field [show (n : ℂ) ≠ 0 by aesop])) hx * (n / π / I)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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)
h : k = HMul.hMul (α := ℤ) 2 (↑n : ℤ) * m
w : ℤ
h₁ : k = HMul.hMul (α := ℤ) 2 (↑n : ℤ) * m
⊢ HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k

Tactic:
use m
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
this :
  (∑ i ∈ range n,
          Complex.exp
            ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I)) *
        Complex.exp (-((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)) *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
    HPow.hPow (α := ℂ) (-1) k - 1
⊢ (∑ i ∈ range n,
          Complex.exp
            ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I)) *
        (Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I))⁻¹ *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
    HPow.hPow (α := ℂ) (-1) k - 1

Tactic:
rw [Complex.exp_neg] at this

Premises used: Complex.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
this :
  (∑ i ∈ range n,
          Complex.exp
            ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I)) *
        (Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I))⁻¹ *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
    HPow.hPow (α := ℂ) (-1) k - 1
s a b t : ℂ
h : s * a⁻¹ * b = t
ha : a ≠ 0
hb : b ≠ 0
⊢ s + t * a / b - (a / b * t + s * a⁻¹ * b * a / b) = 0

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
this :
  (∑ i ∈ range n,
          Complex.exp
            ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I)) *
        (Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I))⁻¹ *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
    HPow.hPow (α := ℂ) (-1) k - 1
s a b t : ℂ
h : s * a⁻¹ * b = t
ha : a ≠ 0
hb : b ≠ 0
a₁ : s + t * a / b - (a / b * t + s * a⁻¹ * b * a / b) = 0
⊢ s = a / b * t

Tactic:
linear_combination (norm := field) h * a / b
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
this :
  (∑ i ∈ range n,
          Complex.exp
            ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I)) *
        (Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I))⁻¹ *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
    HPow.hPow (α := ℂ) (-1) k - 1
⊢ ∀ {s a b t : ℂ} (h : s * a⁻¹ * b = t) (ha : a ≠ 0) (hb : b ≠ 0), s = a / b * t

Tactic:
have hf {s a b t : ℂ} (h : s * a⁻¹ * b = t) (ha : a ≠ 0) (hb : b ≠ 0) : s = a / b * t := by
      linear_combination (norm := field) h * a / b
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
this :
  (∑ i ∈ range n,
          Complex.exp
            ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I)) *
        (Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I))⁻¹ *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
    HPow.hPow (α := ℂ) (-1) k - 1
hf : ∀ {s a b t : ℂ} (h : s * a⁻¹ * b = t) (ha : a ≠ 0) (hb : b ≠ 0), s = a / b * t
⊢ Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1 ≠ 0

Tactic:
grind [exp_sub_one_ne_zero]

Premises used: _private.0.Polynomial.Chebyshev.exp_sub_one_ne_zero