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

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

Tactic:
simp

Result:
no goals

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

Tactic:
simp

Result:
no goals

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

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

Result:
no goals

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

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

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

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

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

Result:
no goals

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

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

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

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

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

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

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

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

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