-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem T_derivative_eq_U (n : ℤ) : derivative (T R n) = n * U R (n - 1)

Proof state:
case a.a
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : derivative (T R (↑n + 1)) = ↑(↑n + 1) * U R (↑n + 1 - 1)
ih2 : derivative (T R ↑n) = ↑↑n * U R (↑n - 1)
h₂ : U R (↑n - 1) = 2 * X * U R ↑n - U R (↑n + 1)
h₃ : T R (↑n + 1) = U R (↑n + 1) - X * U R (↑n + 1 - 1)
h₁ :
  derivative (T R (↑n + 2)) = (0 * X + 2 * 1) * T R (↑n + 1) + 2 * X * derivative (T R (↑n + 1)) - derivative (T R ↑n)
⊢ derivative (T R (↑n + 2)) +
        ((0 * X + 2 * 1) * T R (↑n + 1) + 2 * X * derivative (T R (↑n + 1)) - derivative (T R ↑n) +
                derivative (T R ↑n) +
              2 * X * (↑(↑n + 1) * U R (↑n + 1 - 1)) +
            2 * (U R (↑n + 1) - X * U R (↑n + 1 - 1)) +
          ↑n * U R (↑n - 1)) -
      (↑(↑n + 2) * U R (↑n + 2 - 1) +
        (derivative (T R (↑n + 2)) + ↑↑n * U R (↑n - 1) + 2 * X * derivative (T R (↑n + 1)) + 2 * T R (↑n + 1) +
          ↑n * (2 * X * U R ↑n - U R (↑n + 1)))) =
    0

Tactic:
push_cast

Result:
case a.a
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : derivative (T R (↑n + 1)) = ↑(↑n + 1) * U R (↑n + 1 - 1)
ih2 : derivative (T R ↑n) = ↑↑n * U R (↑n - 1)
h₂ : U R (↑n - 1) = 2 * X * U R ↑n - U R (↑n + 1)
h₃ : T R (↑n + 1) = U R (↑n + 1) - X * U R (↑n + 1 - 1)
h₁ :
  derivative (T R (↑n + 2)) = (0 * X + 2 * 1) * T R (↑n + 1) + 2 * X * derivative (T R (↑n + 1)) - derivative (T R ↑n)
⊢ derivative (T R (↑n + 2)) +
        ((0 * X + 2 * 1) * T R (↑n + 1) + 2 * X * derivative (T R (↑n + 1)) - derivative (T R ↑n) +
                derivative (T R ↑n) +
              2 * X * ((↑n + 1) * U R (↑n + 1 - 1)) +
            2 * (U R (↑n + 1) - X * U R (↑n + 1 - 1)) +
          ↑n * U R (↑n - 1)) -
      ((↑n + 2) * U R (↑n + 2 - 1) +
        (derivative (T R (↑n + 2)) + ↑n * U R (↑n - 1) + 2 * X * derivative (T R (↑n + 1)) + 2 * T R (↑n + 1) +
          ↑n * (2 * X * U R ↑n - U R (↑n + 1)))) =
    0

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : derivative (T R (↑n + 1)) = ↑(↑n + 1) * U R (↑n + 1 - 1)
ih2 : derivative (T R ↑n) = ↑↑n * U R (↑n - 1)
h₂ : U R (↑n - 1) = 2 * X * U R ↑n - U R (↑n + 1)
h₃ : T R (↑n + 1) = U R (↑n + 1) - X * U R (↑n + 1 - 1)
h₁ :
  derivative (T R (↑n + 2)) = (0 * X + 2 * 1) * T R (↑n + 1) + 2 * X * derivative (T R (↑n + 1)) - derivative (T R ↑n)
⊢ derivative (T R (↑n + 2)) = ↑(↑n + 2) * U R (↑n + 2 - 1)

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

Result:
no goals

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : derivative (T R (↑n + 1)) = ↑(↑n + 1) * U R (↑n + 1 - 1)
ih2 : derivative (T R ↑n) = ↑↑n * U R (↑n - 1)
⊢ derivative (T R (↑n + 2)) = ↑(↑n + 2) * U R (↑n + 2 - 1)

Tactic:
have h₁ := congr_arg derivative (T_add_two R n)

Result:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : derivative (T R (↑n + 1)) = ↑(↑n + 1) * U R (↑n + 1 - 1)
ih2 : derivative (T R ↑n) = ↑↑n * U R (↑n - 1)
h₁ : derivative (T R (↑n + 2)) = derivative (2 * X * T R (↑n + 1) - T R ↑n)
⊢ derivative (T R (↑n + 2)) = ↑(↑n + 2) * U R (↑n + 2 - 1)

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : derivative (T R (-↑n)) = ↑(-↑n) * U R (-↑n - 1)
ih2 : derivative (T R (-↑n + 1)) = ↑(-↑n + 1) * U R (-↑n + 1 - 1)
h₁ : derivative (T R (-↑n - 1)) = derivative (2 * X * T R (-↑n) - T R (-↑n + 1))
h₂ : U R (-↑n - 2) = 2 * X * U R (-↑n - 1) - U R (-↑n)
h₃ : T R (-↑n) = U R (-↑n) - X * U R (-↑n - 1)
⊢ derivative (T R (-↑n - 1)) = ↑(-↑n - 1) * U R (-↑n - 1 - 1)

Tactic:
simp only [derivative_sub, derivative_mul, derivative_ofNat, derivative_X] at h₁

Result:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : derivative (T R (-↑n)) = ↑(-↑n) * U R (-↑n - 1)
ih2 : derivative (T R (-↑n + 1)) = ↑(-↑n + 1) * U R (-↑n + 1 - 1)
h₂ : U R (-↑n - 2) = 2 * X * U R (-↑n - 1) - U R (-↑n)
h₃ : T R (-↑n) = U R (-↑n) - X * U R (-↑n - 1)
h₁ :
  derivative (T R (-↑n - 1)) = (0 * X + 2 * 1) * T R (-↑n) + 2 * X * derivative (T R (-↑n)) - derivative (T R (-↑n + 1))
⊢ derivative (T R (-↑n - 1)) = ↑(-↑n - 1) * U R (-↑n - 1 - 1)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ derivative (T R n) = ↑n * U R (n - 1)

Tactic:
induction n using Polynomial.Chebyshev.induct with
| zero => simp
| one =>
  simp [T_two, U_one, derivative_sub, derivative_one, derivative_mul, derivative_X_pow, add_mul]
| add_two n ih1 ih2 =>
  have h₁ := congr_arg derivative (T_add_two R n)
  have h₂ := U_sub_one R n
  have h₃ := T_eq_U_sub_X_mul_U R (n + 1)
  simp only [derivative_sub, derivative_mul, derivative_ofNat, derivative_X] at h₁
  linear_combination (norm := (push_cast; ring_nf))
    h₁ - ih2 + 2 * (X : R[X]) * ih1 + 2 * h₃ - n * h₂
| neg_add_one n ih1 ih2 =>
  have h₁ := congr_arg derivative (T_sub_one R (-n))
  have h₂ := U_sub_two R (-n)
  have h₃ := T_eq_U_sub_X_mul_U R (-n)
  simp only [derivative_sub, derivative_mul, derivative_ofNat, derivative_X] at h₁
  linear_combination (norm := (push_cast; ring_nf))
    -ih2 + 2 * (X : R[X]) * ih1 + h₁ + 2 * h₃ + (n + 1) * h₂

Result:
no goals

Proof state:
case neg_add_one
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : derivative (T R (-↑n)) = ↑(-↑n) * U R (-↑n - 1)
ih2 : derivative (T R (-↑n + 1)) = ↑(-↑n + 1) * U R (-↑n + 1 - 1)
h₂ : U R (-↑n - 2) = 2 * X * U R (-↑n - 1) - U R (-↑n)
h₃ : T R (-↑n) = U R (-↑n) - X * U R (-↑n - 1)
h₁ :
  derivative (T R (-↑n - 1)) = (0 * X + 2 * 1) * T R (-↑n) + 2 * X * derivative (T R (-↑n)) - derivative (T R (-↑n + 1))
⊢ derivative (T R (-↑n - 1)) = ↑(-↑n - 1) * U R (-↑n - 1 - 1)

Tactic:
linear_combination (norm := (push_cast; ring_nf))
  -ih2 + 2 * (X : R[X]) * ih1 + h₁ + 2 * h₃ + (n + 1) * h₂

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝ : CommRing R
⊢ derivative (T R 0) = ↑0 * U R (0 - 1)

Tactic:
simp

Result:
no goals

Proof state:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : derivative (T R (↑n + 1)) = ↑(↑n + 1) * U R (↑n + 1 - 1)
ih2 : derivative (T R ↑n) = ↑↑n * U R (↑n - 1)
h₁ : derivative (T R (↑n + 2)) = derivative (2 * X * T R (↑n + 1) - T R ↑n)
h₂ : U R (↑n - 1) = 2 * X * U R ↑n - U R (↑n + 1)
h₃ : T R (↑n + 1) = U R (↑n + 1) - X * U R (↑n + 1 - 1)
⊢ derivative (T R (↑n + 2)) = ↑(↑n + 2) * U R (↑n + 2 - 1)

Tactic:
simp only [derivative_sub, derivative_mul, derivative_ofNat, derivative_X] at h₁

Result:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : derivative (T R (↑n + 1)) = ↑(↑n + 1) * U R (↑n + 1 - 1)
ih2 : derivative (T R ↑n) = ↑↑n * U R (↑n - 1)
h₂ : U R (↑n - 1) = 2 * X * U R ↑n - U R (↑n + 1)
h₃ : T R (↑n + 1) = U R (↑n + 1) - X * U R (↑n + 1 - 1)
h₁ :
  derivative (T R (↑n + 2)) = (0 * X + 2 * 1) * T R (↑n + 1) + 2 * X * derivative (T R (↑n + 1)) - derivative (T R ↑n)
⊢ derivative (T R (↑n + 2)) = ↑(↑n + 2) * U R (↑n + 2 - 1)

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

Tactic:
have h₃ := T_eq_U_sub_X_mul_U R (n + 1)

Result:
case add_two
R : Type u_1
inst✝ : CommRing R
n : ℕ
ih1 : derivative (T R (↑n + 1)) = ↑(↑n + 1) * U R (↑n + 1 - 1)
ih2 : derivative (T R ↑n) = ↑↑n * U R (↑n - 1)
h₁ : derivative (T R (↑n + 2)) = derivative (2 * X * T R (↑n + 1) - T R ↑n)
h₂ : U R (↑n - 1) = 2 * X * U R ↑n - U R (↑n + 1)
h₃ : T R (↑n + 1) = U R (↑n + 1) - X * U R (↑n + 1 - 1)
⊢ derivative (T R (↑n + 2)) = ↑(↑n + 2) * U R (↑n + 2 - 1)