-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem C_mul_C (m k : ℤ) : C R m * C R k = C R (m + k) + C R (m - k)

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

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

Result:
no goals

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

Tactic:
have h₂ := C_sub_two R (m - k)

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

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

Tactic:
have h₃ := C_add_two R (-k - 1)

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

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

Tactic:
have h₁ := C_add_two R (m + (-k - 1))

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

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

Tactic:
have h₃ := C_add_two R k

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

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
m : ℤ
⊢ C R m * C R 0 = C R (m + 0) + C R (m - 0)

Tactic:
simp [mul_two]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
m k : ℤ
⊢ C R m * C R k = C R (m + k) + C R (m - k)

Tactic:
induction k using Polynomial.Chebyshev.induct with
| zero => simp [mul_two]
| one => rw [C_add_one, C_one]; ring
| add_two k ih1 ih2 =>
  have h₁ := C_add_two R (m + k)
  have h₂ := C_sub_two R (m - k)
  have h₃ := C_add_two R k
  linear_combination (norm := ring_nf) C R m * h₃ - h₂ - h₁ - ih2 + (X:R[X]) * ih1
| neg_add_one k ih1 ih2 =>
  have h₁ := C_add_two R (m + (-k - 1))
  have h₂ := C_sub_two R (m - (-k - 1))
  have h₃ := C_add_two R (-k - 1)
  linear_combination (norm := ring_nf) C R m * h₃ - h₂ - h₁ - ih2 + (X:R[X]) * ih1

Result:
no goals

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

Tactic:
have h₂ := C_sub_two R (m - (-k - 1))

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

Proof state:
case one
R : Type u_1
inst✝ : CommRing R
m : ℤ
⊢ C R m * C R 1 = C R (m + 1) + C R (m - 1)

Tactic:
rw [C_add_one, C_one]

Result:
case one
R : Type u_1
inst✝ : CommRing R
m : ℤ
⊢ C R m * X = X * C R m - C R (m - 1) + C R (m - 1)

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

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

Result:
no goals

Proof state:
case one
R : Type u_1
inst✝ : CommRing R
m : ℤ
⊢ C R m * X = X * C R m - C R (m - 1) + C R (m - 1)

Tactic:
ring

Result:
no goals

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

Tactic:
have h₁ := C_add_two R (m + k)

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