-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem T_mul (m n : ℤ) : T R (m * n) = (T R m).comp (T R n)

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ T R (0 * n) = (T R 0).comp (T R n)

Tactic:
simp

Result:
no goals

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℤ
m : ℕ
ih1 : T R ((↑m + 1) * n) = (T R (↑m + 1)).comp (T R n)
ih2 : T R (↑m * n) = (T R ↑m).comp (T R n)
h₁ : 2 * T R ((↑m + 1) * n) * T R n = T R ((↑m + 1) * n + n) + T R ((↑m + 1) * n - n)
h₂ : (fun x => x.comp (T R n)) (T R (↑m + 2)) = (fun x => x.comp (T R n)) (2 * X * T R (↑m + 1) - T R ↑m)
⊢ T R ((↑m + 2) * n) = (T R (↑m + 2)).comp (T R n)

Tactic:
simp only [sub_comp, mul_comp, ofNat_comp, X_comp] at h₂

Result:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℤ
m : ℕ
ih1 : T R ((↑m + 1) * n) = (T R (↑m + 1)).comp (T R n)
ih2 : T R (↑m * n) = (T R ↑m).comp (T R n)
h₁ : 2 * T R ((↑m + 1) * n) * T R n = T R ((↑m + 1) * n + n) + T R ((↑m + 1) * n - n)
h₂ : (T R (↑m + 2)).comp (T R n) = ↑2 * T R n * (T R (↑m + 1)).comp (T R n) - (T R ↑m).comp (T R n)
⊢ T R ((↑m + 2) * n) = (T R (↑m + 2)).comp (T R n)

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℤ
m : ℕ
ih1 : T R (-↑m * n) = (T R (-↑m)).comp (T R n)
ih2 : T R ((-↑m + 1) * n) = (T R (-↑m + 1)).comp (T R n)
h₁ : 2 * T R (-↑m * n) * T R n = T R (-↑m * n + n) + T R (-↑m * n - n)
h₂ :
  (fun x => x.comp (T R n)) (T R (-↑m - 1 + 2)) = (fun x => x.comp (T R n)) (2 * X * T R (-↑m - 1 + 1) - T R (-↑m - 1))
⊢ T R ((-↑m - 1) * n) = (T R (-↑m - 1)).comp (T R n)

Tactic:
simp only [sub_comp, mul_comp, ofNat_comp, X_comp] at h₂

Result:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℤ
m : ℕ
ih1 : T R (-↑m * n) = (T R (-↑m)).comp (T R n)
ih2 : T R ((-↑m + 1) * n) = (T R (-↑m + 1)).comp (T R n)
h₁ : 2 * T R (-↑m * n) * T R n = T R (-↑m * n + n) + T R (-↑m * n - n)
h₂ : (T R (-↑m - 1 + 2)).comp (T R n) = ↑2 * T R n * (T R (-↑m - 1 + 1)).comp (T R n) - (T R (-↑m - 1)).comp (T R n)
⊢ T R ((-↑m - 1) * n) = (T R (-↑m - 1)).comp (T R n)

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℤ
m : ℕ
ih1 : T R ((↑m + 1) * n) = (T R (↑m + 1)).comp (T R n)
ih2 : T R (↑m * n) = (T R ↑m).comp (T R n)
⊢ T R ((↑m + 2) * n) = (T R (↑m + 2)).comp (T R n)

Tactic:
have h₁ := T_mul_T R ((m + 1) * n) n

Result:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℤ
m : ℕ
ih1 : T R ((↑m + 1) * n) = (T R (↑m + 1)).comp (T R n)
ih2 : T R (↑m * n) = (T R ↑m).comp (T R n)
h₁ : 2 * T R ((↑m + 1) * n) * T R n = T R ((↑m + 1) * n + n) + T R ((↑m + 1) * n - n)
⊢ T R ((↑m + 2) * n) = (T R (↑m + 2)).comp (T R n)

Proof state:
case one
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ T R (1 * n) = (T R 1).comp (T R n)

Tactic:
simp

Result:
no goals

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℤ
m : ℕ
ih1 : T R ((↑m + 1) * n) = (T R (↑m + 1)).comp (T R n)
ih2 : T R (↑m * n) = (T R ↑m).comp (T R n)
h₁ : 2 * T R ((↑m + 1) * n) * T R n = T R ((↑m + 1) * n + n) + T R ((↑m + 1) * n - n)
h₂ : (T R (↑m + 2)).comp (T R n) = ↑2 * T R n * (T R (↑m + 1)).comp (T R n) - (T R ↑m).comp (T R n)
⊢ T R ((↑m + 2) * n) = (T R (↑m + 2)).comp (T R n)

Tactic:
linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + 2 * T R n * ih1

Result:
no goals

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℤ
m : ℕ
ih1 : T R (-↑m * n) = (T R (-↑m)).comp (T R n)
ih2 : T R ((-↑m + 1) * n) = (T R (-↑m + 1)).comp (T R n)
h₁ : 2 * T R (-↑m * n) * T R n = T R (-↑m * n + n) + T R (-↑m * n - n)
h₂ : (T R (-↑m - 1 + 2)).comp (T R n) = ↑2 * T R n * (T R (-↑m - 1 + 1)).comp (T R n) - (T R (-↑m - 1)).comp (T R n)
⊢ T R ((-↑m - 1) * n) = (T R (-↑m - 1)).comp (T R n)

Tactic:
linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + 2 * T R n * ih1

Result:
no goals

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℤ
m : ℕ
ih1 : T R (-↑m * n) = (T R (-↑m)).comp (T R n)
ih2 : T R ((-↑m + 1) * n) = (T R (-↑m + 1)).comp (T R n)
⊢ T R ((-↑m - 1) * n) = (T R (-↑m - 1)).comp (T R n)

Tactic:
have h₁ := T_mul_T R ((-m) * n) n

Result:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℤ
m : ℕ
ih1 : T R (-↑m * n) = (T R (-↑m)).comp (T R n)
ih2 : T R ((-↑m + 1) * n) = (T R (-↑m + 1)).comp (T R n)
h₁ : 2 * T R (-↑m * n) * T R n = T R (-↑m * n + n) + T R (-↑m * n - n)
⊢ T R ((-↑m - 1) * n) = (T R (-↑m - 1)).comp (T R n)