awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
ih :
  (↑(∏ l ∈ Finset.range k, (2 * l + 3)) : R) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) =
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
        R) *
      HAdd.hAdd (α := R) (↑n : R) 1
push_cast :
  ∀
    (ih :
      (∏ x ∈ Finset.range k, (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
          eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k] (U R n)) =
        (∏ x ∈ Finset.range k,
            (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 -
              HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
          HAdd.hAdd (α := R) (↑n : R) 1),
    (∏ x ∈ Finset.range (k + 1), (HMul.hMul (α := R) 2 (↑x : R) + 3)) *
        eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
      (∏ x ∈ Finset.range (k + 1),
          (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑n : R) 1) 2 -
            HPow.hPow (β := ℕ) (HAdd.hAdd (α := R) (↑x : R) 1) 2)) *
        HAdd.hAdd (α := R) (↑n : R) 1
⊢ (↑(∏ l ∈ Finset.range (k + 1), (2 * l + 3)) : R) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (U R n)) =
    (↑(∏ l ∈ Finset.range (k + 1),
            (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
        R) *
      HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
push_cast at ih ⊢
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ eval 1 ((derivative : (a : R[X]) → R[X]) (T R n)) = HPow.hPow (α := R) (β := ℕ) (↑n : R) 2

Tactic:
simp [T_derivative_eq_U, sq]

Premises used: Polynomial.Chebyshev.T_derivative_eq_U, sq
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ (↑(∏ l ∈ Finset.range 1, (2 * l + 3)) : R) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[1] (U R n)) =
    (↑(∏ l ∈ Finset.range 1, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
        R) *
      HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
have h := iterate_derivative_U_eval_one (R := R) n 1
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h :
  (↑(∏ l ∈ Finset.range 1, (2 * l + 3)) : R) * eval 1 ((⇑derivative : (a : R[X]) → R[X])^[1] (U R n)) =
    (↑(∏ l ∈ Finset.range 1, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
        R) *
      HAdd.hAdd (α := R) (↑n : R) 1
⊢ HMul.hMul (α := R) (↑(HMul.hMul (α := ℕ) 2 0 + 3) : R) (eval 1 ((derivative : (a : R[X]) → R[X]) (U R n))) =
    (↑(HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) 2) : R) *
      HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
simp only [Finset.range_one, Finset.prod_singleton, Function.iterate_one] at h

Premises used: Finset.prod_singleton, Function.iterate_one, Finset.range_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h :
  HMul.hMul (α := R) (↑(HMul.hMul (α := ℕ) 2 0 + 3) : R) (eval 1 ((derivative : (a : R[X]) → R[X]) (U R n))) =
    (↑(HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1) 2) : R) *
      HAdd.hAdd (α := R) (↑n : R) 1
⊢ HMul.hMul (α := R) 3 (eval 1 ((derivative : (a : R[X]) → R[X]) (U R n))) =
    HAdd.hAdd (α := R) (↑n : R) 2 * HAdd.hAdd (α := R) (↑n : R) 1 * (↑n : R)

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
𝔽 : Type u_3
inst : Field 𝔽
inst_1 : CharZero 𝔽
n : ℤ
k x : ℕ
h : x ∈ Finset.range k
⊢ 2 * x + 1 ≠ 0

Tactic:
positivity
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
𝔽 : Type u_3
inst : Field 𝔽
inst_1 : CharZero 𝔽
n : ℤ
k : ℕ
rw :
  eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (T 𝔽 n)) * (↑(∏ l ∈ Finset.range k, (2 * l + 1)) : 𝔽) =
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : 𝔽)
rw₁ :
  (↑(∏ l ∈ Finset.range k, (2 * l + 1)) : 𝔽) * eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (T 𝔽 n)) =
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : 𝔽)
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := 𝔽) (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : 𝔽)
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : 𝔽)
⊢ eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (T 𝔽 n)) =
    HDiv.hDiv (α := 𝔽) (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : 𝔽)
      (↑(∏ l ∈ Finset.range k, (2 * l + 1)) : 𝔽)

Tactic:
rw [eq_div_iff (Nat.cast_ne_zero.mpr (Finset.prod_ne_zero_iff.mpr (fun _ _ => by positivity))),
    mul_comm, iterate_derivative_T_eval_one]

Premises used: mul_comm, Polynomial.Chebyshev.iterate_derivative_T_eval_one, eq_div_iff
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
𝔽 : Type u_3
inst : Field 𝔽
inst_1 : CharZero 𝔽
n : ℤ
k x : ℕ
h : x ∈ Finset.range k
⊢ 2 * x + 3 ≠ 0

Tactic:
positivity
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
𝔽 : Type u_3
inst : Field 𝔽
inst_1 : CharZero 𝔽
n : ℤ
k : ℕ
rw :
  eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (U 𝔽 n)) * (↑(∏ l ∈ Finset.range k, (2 * l + 3)) : 𝔽) =
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
        𝔽) *
      HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 1
rw₁ :
  (↑(∏ l ∈ Finset.range k, (2 * l + 3)) : 𝔽) * eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (U 𝔽 n)) =
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
        𝔽) *
      HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 1
rw₂ rw₃ :
  (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) : 𝔽) *
      HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 1 =
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
        𝔽) *
      HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 1
⊢ eval 1 ((⇑derivative : (a : 𝔽[X]) → 𝔽[X])^[k] (U 𝔽 n)) =
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
          𝔽) *
        HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 1 /
      (↑(∏ l ∈ Finset.range k, (2 * l + 3)) : 𝔽)

Tactic:
rw [eq_div_iff (Nat.cast_ne_zero.mpr (Finset.prod_ne_zero_iff.mpr (fun _ _ => by positivity))),
    mul_comm, iterate_derivative_U_eval_one]

Premises used: Polynomial.Chebyshev.iterate_derivative_U_eval_one, mul_comm, eq_div_iff
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
𝔽 : Type u_3
inst : Field 𝔽
n : ℤ
k : ℕ
⊢ Dvd.dvd.{u_3} (α := 𝔽) (↑(∏ l ∈ Finset.range k, (2 * l + 1)) : 𝔽)
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) n 2 - HPow.hPow (α := ℤ) (β := ℕ) (↑l : ℤ) 2)) : 𝔽)

Tactic:
dvd_of_mul_right_eq _ <| iterate_derivative_T_eval_one n k

Premises used: dvd_of_mul_right_eq, Polynomial.Chebyshev.iterate_derivative_T_eval_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
𝔽 : Type u_3
inst : Field 𝔽
n : ℤ
k : ℕ
⊢ (↑(∏ l ∈ Finset.range k, (2 * l + 3)) : 𝔽) ∣
    (↑(∏ l ∈ Finset.range k, (HPow.hPow (β := ℕ) (n + 1) 2 - HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℤ) (↑l : ℤ) 1) 2)) :
        𝔽) *
      HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 1

Tactic:
dvd_of_mul_right_eq _ <| iterate_derivative_U_eval_one n k

Premises used: dvd_of_mul_right_eq, Polynomial.Chebyshev.iterate_derivative_U_eval_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
𝔽 : Type u_3
inst : Field 𝔽
neZero3 : NeZero.{u_3} (R := 𝔽) 3
n : ℤ
⊢ eval 1 ((derivative : (a : 𝔽[X]) → 𝔽[X]) (U 𝔽 n)) =
    HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 2 * HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 1 * (↑n : 𝔽) / 3

Tactic:
eq_div_of_mul_eq neZero3.ne ((mul_comm ..).trans (derivative_U_eval_one n))

Premises used: eq_div_of_mul_eq, Polynomial.Chebyshev.derivative_U_eval_one, mul_comm, Eq.trans, NeZero.ne
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
𝔽 : Type u_3
inst : Field 𝔽
n : ℤ
⊢ 3 ∣ HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 2 * HAdd.hAdd (α := 𝔽) (↑n : 𝔽) 1 * (↑n : 𝔽)

Tactic:
dvd_of_mul_right_eq _ (derivative_U_eval_one n)

Premises used: dvd_of_mul_right_eq, Polynomial.Chebyshev.derivative_U_eval_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R 0 = HAdd.hAdd (α := R[X]) (T R (m + 0)) (T R (m - 0))

Tactic:
simp [two_mul]

Premises used: two_mul
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
one : HMul.hMul (α := R[X]) 2 (T R m) * X = HMul.hMul (α := R[X]) 2 X * T R m - T R (m - 1) + T R (m - 1)
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R 1 = HAdd.hAdd (α := R[X]) (T R (m + 1)) (T R (m - 1))

Tactic:
rw [T_add_one, T_one]

Premises used: Polynomial.Chebyshev.T_add_one, Polynomial.Chebyshev.T_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
⊢ HMul.hMul (α := R[X]) 2 (T R m) * X = HMul.hMul (α := R[X]) 2 X * T R m - T R (m - 1) + T R (m - 1)

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1))
ih2 : HMul.hMul (α := R[X]) 2 (T R m) * T R (↑k : ℤ) = HAdd.hAdd (α := R[X]) (T R (m + (↑k : ℤ))) (T R (m - (↑k : ℤ)))
⊢ T R (m + (↑k : ℤ) + 2) = HMul.hMul (α := R[X]) 2 X * T R (m + (↑k : ℤ) + 1) - T R (m + (↑k : ℤ))

Tactic:
have h₁ := T_add_two R (m + k)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1))
ih2 : HMul.hMul (α := R[X]) 2 (T R m) * T R (↑k : ℤ) = HAdd.hAdd (α := R[X]) (T R (m + (↑k : ℤ))) (T R (m - (↑k : ℤ)))
h₁ : T R (m + (↑k : ℤ) + 2) = HMul.hMul (α := R[X]) 2 X * T R (m + (↑k : ℤ) + 1) - T R (m + (↑k : ℤ))
⊢ T R (m - (↑k : ℤ) - 2) = HMul.hMul (α := R[X]) 2 X * T R (m - (↑k : ℤ) - 1) - T R (m - (↑k : ℤ))

Tactic:
have h₂ := T_sub_two R (m - k)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1))
ih2 : HMul.hMul (α := R[X]) 2 (T R m) * T R (↑k : ℤ) = HAdd.hAdd (α := R[X]) (T R (m + (↑k : ℤ))) (T R (m - (↑k : ℤ)))
h₁ : T R (m + (↑k : ℤ) + 2) = HMul.hMul (α := R[X]) 2 X * T R (m + (↑k : ℤ) + 1) - T R (m + (↑k : ℤ))
h₂ : T R (m - (↑k : ℤ) - 2) = HMul.hMul (α := R[X]) 2 X * T R (m - (↑k : ℤ) - 1) - T R (m - (↑k : ℤ))
⊢ T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) = HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) - T R (↑k : ℤ)

Tactic:
have h₃ := T_add_two R k
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1))
ih2 : HMul.hMul (α := R[X]) 2 (T R m) * T R (↑k : ℤ) = HAdd.hAdd (α := R[X]) (T R (m + (↑k : ℤ))) (T R (m - (↑k : ℤ)))
h₁ : T R (m + (↑k : ℤ) + 2) = HMul.hMul (α := R[X]) 2 X * T R (m + (↑k : ℤ) + 1) - T R (m + (↑k : ℤ))
h₂ : T R (m - (↑k : ℤ) - 2) = HMul.hMul (α := R[X]) 2 X * T R (m - (↑k : ℤ) - 1) - T R (m - (↑k : ℤ))
h₃ :
  T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) = HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) - T R (↑k : ℤ)
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) +
        (HMul.hMul (α := R[X]) 2 (T R m) *
                  (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) - T R (↑k : ℤ)) +
                T R (m - (↑k : ℤ) - 2) +
              T R (m + (↑k : ℤ) + 2) +
            HMul.hMul (α := R[X]) 2 (T R m) * T R (↑k : ℤ) +
          HMul.hMul (α := R[X]) 2 X *
            HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1))) -
      (HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) +
        (HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) +
                (HMul.hMul (α := R[X]) 2 X * T R (m - (↑k : ℤ) - 1) - T R (m - (↑k : ℤ))) +
              (HMul.hMul (α := R[X]) 2 X * T R (m + (↑k : ℤ) + 1) - T R (m + (↑k : ℤ))) +
            HAdd.hAdd (α := R[X]) (T R (m + (↑k : ℤ))) (T R (m - (↑k : ℤ))) +
          HMul.hMul (α := R[X]) 2 X * (HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)))) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1))
ih2 : HMul.hMul (α := R[X]) 2 (T R m) * T R (↑k : ℤ) = HAdd.hAdd (α := R[X]) (T R (m + (↑k : ℤ))) (T R (m - (↑k : ℤ)))
h₁ : T R (m + (↑k : ℤ) + 2) = HMul.hMul (α := R[X]) 2 X * T R (m + (↑k : ℤ) + 1) - T R (m + (↑k : ℤ))
h₂ : T R (m - (↑k : ℤ) - 2) = HMul.hMul (α := R[X]) 2 X * T R (m - (↑k : ℤ) - 1) - T R (m - (↑k : ℤ))
h₃ :
  T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) = HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) - T R (↑k : ℤ)
a :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) +
        (HMul.hMul (α := R[X]) 2 (T R m) *
                  (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) - T R (↑k : ℤ)) +
                T R (m - (↑k : ℤ) - 2) +
              T R (m + (↑k : ℤ) + 2) +
            HMul.hMul (α := R[X]) 2 (T R m) * T R (↑k : ℤ) +
          HMul.hMul (α := R[X]) 2 X *
            HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1))) -
      (HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) +
        (HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) +
                (HMul.hMul (α := R[X]) 2 X * T R (m - (↑k : ℤ) - 1) - T R (m - (↑k : ℤ))) +
              (HMul.hMul (α := R[X]) 2 X * T R (m + (↑k : ℤ) + 1) - T R (m + (↑k : ℤ))) +
            HAdd.hAdd (α := R[X]) (T R (m + (↑k : ℤ))) (T R (m - (↑k : ℤ))) +
          HMul.hMul (α := R[X]) 2 X * (HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)))) =
    0
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2))

Tactic:
linear_combination (norm := ring_nf) 2 * T R m * h₃ - h₂ - h₁ - ih2 + 2 * (X : R[X]) * ih1

Premises used: Polynomial.Chebyshev.T, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (-(↑k : ℤ)) = HAdd.hAdd (α := R[X]) (T R (m + -(↑k : ℤ))) (T R (m - -(↑k : ℤ)))
ih2 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1))
⊢ T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) -
      T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)

Tactic:
have h₁ := T_add_two R (m + (-k - 1))
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (-(↑k : ℤ)) = HAdd.hAdd (α := R[X]) (T R (m + -(↑k : ℤ))) (T R (m - -(↑k : ℤ)))
ih2 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1))
h₁ :
  T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) -
      T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)
⊢ T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 2) =
    HMul.hMul (α := R[X]) 2 X * T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 1) -
      T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)

Tactic:
have h₂ := T_sub_two R (m - (-k - 1))
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (-(↑k : ℤ)) = HAdd.hAdd (α := R[X]) (T R (m + -(↑k : ℤ))) (T R (m - -(↑k : ℤ)))
ih2 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1))
h₁ :
  T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) -
      T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)
h₂ :
  T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 2) =
    HMul.hMul (α := R[X]) 2 X * T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 1) -
      T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)
⊢ T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) - T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)

Tactic:
have h₃ := T_add_two R (-k - 1)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (-(↑k : ℤ)) = HAdd.hAdd (α := R[X]) (T R (m + -(↑k : ℤ))) (T R (m - -(↑k : ℤ)))
ih2 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1))
h₁ :
  T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) -
      T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)
h₂ :
  T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 2) =
    HMul.hMul (α := R[X]) 2 X * T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 1) -
      T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)
h₃ :
  T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) - T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) +
        (HMul.hMul (α := R[X]) 2 (T R m) *
                  (HMul.hMul (α := R[X]) 2 X * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) -
                    T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) +
                T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 2) +
              T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) +
            HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1) +
          HMul.hMul (α := R[X]) 2 X * HAdd.hAdd (α := R[X]) (T R (m + -(↑k : ℤ))) (T R (m - -(↑k : ℤ)))) -
      (HAdd.hAdd (α := R[X]) (T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) +
        (HMul.hMul (α := R[X]) 2 (T R m) * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) +
                (HMul.hMul (α := R[X]) 2 X * T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 1) -
                  T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) +
              (HMul.hMul (α := R[X]) 2 X * T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) -
                T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) +
            HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1))
              (T R (m - HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) +
          HMul.hMul (α := R[X]) 2 X * (HMul.hMul (α := R[X]) 2 (T R m) * T R (-(↑k : ℤ))))) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
k : ℕ
ih1 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (-(↑k : ℤ)) = HAdd.hAdd (α := R[X]) (T R (m + -(↑k : ℤ))) (T R (m - -(↑k : ℤ)))
ih2 :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1))
h₁ :
  T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) -
      T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)
h₂ :
  T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 2) =
    HMul.hMul (α := R[X]) 2 X * T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 1) -
      T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)
h₃ :
  T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) - T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)
a :
  HMul.hMul (α := R[X]) 2 (T R m) * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) +
        (HMul.hMul (α := R[X]) 2 (T R m) *
                  (HMul.hMul (α := R[X]) 2 X * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) -
                    T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) +
                T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 2) +
              T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) +
            HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1) +
          HMul.hMul (α := R[X]) 2 X * HAdd.hAdd (α := R[X]) (T R (m + -(↑k : ℤ))) (T R (m - -(↑k : ℤ)))) -
      (HAdd.hAdd (α := R[X]) (T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) +
        (HMul.hMul (α := R[X]) 2 (T R m) * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 2) +
                (HMul.hMul (α := R[X]) 2 X * T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 - 1) -
                  T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) +
              (HMul.hMul (α := R[X]) 2 X * T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1 + 1) -
                T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) +
            HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1))
              (T R (m - HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1)) +
          HMul.hMul (α := R[X]) 2 X * (HMul.hMul (α := R[X]) 2 (T R m) * T R (-(↑k : ℤ))))) =
    0
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) =
    HAdd.hAdd (α := R[X]) (T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1))

Tactic:
linear_combination (norm := ring_nf) 2 * T R m * h₃ - h₂ - h₁ - ih2 + 2 * (X : R[X]) * ih1

Premises used: Polynomial.Chebyshev.T, Polynomial.X