awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
inst_2 : Algebra R R'
x : R
n : ℤ
⊢ Eq.{u_2 + 1} (α := R') ((algebraMap R R' : (a : R) → R') (eval x (C R n)) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (C R' n) : R')
have rw : Eq.{u_2 + 1} (α := R') (((aeval ((algebraMap R R' : (a : R) → R') x) : R[X] →ₐ[R] R') : (a : R[X]) → R') (C R n) : R')
  (eval ((algebraMap R R' : (a : R) → R') x) (C R' n) : R')
Tactic: rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
inst_2 : Algebra R R'
x : R
n : ℤ
rw :
  Eq.{u_2 + 1} (α := R') (((aeval ((algebraMap R R' : (a : R) → R') x) : R[X] →ₐ[R] R') : (a : R[X]) → R') (C R n) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (C R' n) : R')
⊢ Eq.{u_2 + 1} (α := R') ((algebraMap R R' : (a : R) → R') (eval x (C R n)) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (C R' n) : R')
have rw₁ : Eq.{u_2 + 1} (α := R') (eval ((algebraMap R R' : (a : R) → R') x) (C R' n) : R')
  (eval ((algebraMap R R' : (a : R) → R') x) (C R' n) : R')
Tactic: rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_C]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
inst_2 : Algebra R R'
x : R
n : ℤ
⊢ Eq.{u_2 + 1} (α := R') ((algebraMap R R' : (a : R) → R') (eval x (S R n)) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (S R' n) : R')
have rw : Eq.{u_2 + 1} (α := R') (((aeval ((algebraMap R R' : (a : R) → R') x) : R[X] →ₐ[R] R') : (a : R[X]) → R') (S R n) : R')
  (eval ((algebraMap R R' : (a : R) → R') x) (S R' n) : R')
Tactic: rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_S]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
inst_2 : Algebra R R'
x : R
n : ℤ
rw :
  Eq.{u_2 + 1} (α := R') (((aeval ((algebraMap R R' : (a : R) → R') x) : R[X] →ₐ[R] R') : (a : R[X]) → R') (S R n) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (S R' n) : R')
⊢ Eq.{u_2 + 1} (α := R') ((algebraMap R R' : (a : R) → R') (eval x (S R n)) : R')
    (eval ((algebraMap R R' : (a : R) → R') x) (S R' n) : R')
have rw₁ : Eq.{u_2 + 1} (α := R') (eval ((algebraMap R R' : (a : R) → R') x) (S R' n) : R')
  (eval ((algebraMap R R' : (a : R) → R') x) (S R' n) : R')
Tactic: rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_S]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R[X]) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 :
  (derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) =
    HMul.hMul (α := R[X]) (↑(↑n : ℤ) : R[X]) (U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
⊢ (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : R[X]) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1))
have h₁ : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) : R[X])
  ((derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)) :
    R[X])
Tactic: have h₁ := congr_arg derivative (T_add_two R n)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R[X]) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 :
  (derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) =
    HMul.hMul (α := R[X]) (↑(↑n : ℤ) : R[X]) (U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
h₁ :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) : R[X])
    ((derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)) :
      R[X])
⊢ (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : R[X]) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1))
have h₂ : U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) 2 X * U R (↑n : ℤ) - U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
Tactic: have h₂ := U_sub_one R n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R[X]) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 :
  (derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) =
    HMul.hMul (α := R[X]) (↑(↑n : ℤ) : R[X]) (U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
h₁ :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) : R[X])
    ((derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)) :
      R[X])
h₂ :
  U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) 2 X * U R (↑n : ℤ) - U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
⊢ (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : R[X]) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1))
have h₃ : T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
  U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
Tactic: have h₃ := T_eq_U_sub_X_mul_U R (n + 1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R[X]) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 :
  (derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) =
    HMul.hMul (α := R[X]) (↑(↑n : ℤ) : R[X]) (U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
h₁ :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) : R[X])
    ((derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)) :
      R[X])
h₂ :
  U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) 2 X * U R (↑n : ℤ) - U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
h₃ :
  T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
⊢ (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : R[X]) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1))
have h₄ : (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
  HSub.hSub (β := R[X])
    ((HMul.hMul (α := R[X]) 0 X + HMul.hMul (α := R[X]) 2 1) * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) +
      HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 2 X)
        ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) : R[X]))
    ((derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) : R[X])
Tactic: simp only [derivative_sub, derivative_mul, derivative_ofNat, derivative_X] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R[X]) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 :
  (derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) =
    HMul.hMul (α := R[X]) (↑(↑n : ℤ) : R[X]) (U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
h₂ :
  U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) 2 X * U R (↑n : ℤ) - U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
h₃ :
  T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
h₁ :
  (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    HSub.hSub (β := R[X])
      ((HMul.hMul (α := R[X]) 0 X + HMul.hMul (α := R[X]) 2 1) * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) +
        HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 2 X)
          ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) : R[X]))
      ((derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : R[X]) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1))
have a : HAdd.hAdd (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) : R[X])
      (HAdd.hAdd (β := R[X])
              (HSub.hSub (β := R[X])
                ((HMul.hMul (α := R[X]) 0 X + HMul.hMul (α := R[X]) 2 1) * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) +
                  HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 2 X)
                    ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) : R[X]))
                ((derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) : R[X]))
              ((derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) : R[X]) +
            HMul.hMul (α := R[X]) 2 X *
              HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R[X])
                (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)) +
          2 *
            (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))) +
        HMul.hMul (α := R[X]) (↑n : R[X]) (U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))) -
    (HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : R[X]) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1)) +
      (HAdd.hAdd (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) : R[X])
              (HMul.hMul (α := R[X]) (↑(↑n : ℤ) : R[X]) (U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))) +
            HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 2 X)
              ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) : R[X]) +
          HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) +
        (↑n : R[X]) * (HMul.hMul (α := R[X]) 2 X * U R (↑n : ℤ) - U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))) =
  0
Tactic: linear_combination (norm := (push_cast; ring_nf))
      h₁ - ih2 + 2 * (X : R[X]) * ih1 + 2 * h₃ - n * h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  (derivative : (a : R[X]) → R[X]) (T R (-(↑n : ℤ))) =
    HMul.hMul (α := R[X]) (↑(-(↑n : ℤ)) : R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
ih2 :
  (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R[X]) (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1))
⊢ (derivative : (a : R[X]) → R[X]) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R[X]) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1))
have h₁ : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) : R[X])
  ((derivative : (a : R[X]) → R[X])
      (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) :
    R[X])
Tactic: have h₁ := congr_arg derivative (T_sub_one R (-n))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  (derivative : (a : R[X]) → R[X]) (T R (-(↑n : ℤ))) =
    HMul.hMul (α := R[X]) (↑(-(↑n : ℤ)) : R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
ih2 :
  (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R[X]) (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1))
h₁ :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) : R[X])
    ((derivative : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) :
      R[X])
⊢ (derivative : (a : R[X]) → R[X]) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R[X]) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1))
have h₂ : U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2) =
  HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) - U R (-(↑n : ℤ))
Tactic: have h₂ := U_sub_two R (-n)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  (derivative : (a : R[X]) → R[X]) (T R (-(↑n : ℤ))) =
    HMul.hMul (α := R[X]) (↑(-(↑n : ℤ)) : R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
ih2 :
  (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R[X]) (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1))
h₁ :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) : R[X])
    ((derivative : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) :
      R[X])
h₂ :
  U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) - U R (-(↑n : ℤ))
⊢ (derivative : (a : R[X]) → R[X]) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R[X]) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1))
have h₃ : T R (-(↑n : ℤ)) = U R (-(↑n : ℤ)) - HMul.hMul (α := R[X]) X (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
Tactic: have h₃ := T_eq_U_sub_X_mul_U R (-n)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  (derivative : (a : R[X]) → R[X]) (T R (-(↑n : ℤ))) =
    HMul.hMul (α := R[X]) (↑(-(↑n : ℤ)) : R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
ih2 :
  (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R[X]) (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1))
h₁ :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) : R[X])
    ((derivative : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) :
      R[X])
h₂ :
  U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) - U R (-(↑n : ℤ))
h₃ : T R (-(↑n : ℤ)) = U R (-(↑n : ℤ)) - HMul.hMul (α := R[X]) X (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
⊢ (derivative : (a : R[X]) → R[X]) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R[X]) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1))
have h₄ : (derivative : (a : R[X]) → R[X]) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
  HSub.hSub (β := R[X])
    ((HMul.hMul (α := R[X]) 0 X + HMul.hMul (α := R[X]) 2 1) * T R (-(↑n : ℤ)) +
      HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 2 X) ((derivative : (a : R[X]) → R[X]) (T R (-(↑n : ℤ))) : R[X]))
    ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) : R[X])
Tactic: simp only [derivative_sub, derivative_mul, derivative_ofNat, derivative_X] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  (derivative : (a : R[X]) → R[X]) (T R (-(↑n : ℤ))) =
    HMul.hMul (α := R[X]) (↑(-(↑n : ℤ)) : R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
ih2 :
  (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R[X]) (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1))
h₂ :
  U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) - U R (-(↑n : ℤ))
h₃ : T R (-(↑n : ℤ)) = U R (-(↑n : ℤ)) - HMul.hMul (α := R[X]) X (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
h₁ :
  (derivative : (a : R[X]) → R[X]) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
    HSub.hSub (β := R[X])
      ((HMul.hMul (α := R[X]) 0 X + HMul.hMul (α := R[X]) 2 1) * T R (-(↑n : ℤ)) +
        HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 2 X) ((derivative : (a : R[X]) → R[X]) (T R (-(↑n : ℤ))) : R[X]))
      ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R[X]) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1))
have a : HAdd.hAdd (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) : R[X])
      (HAdd.hAdd (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) : R[X])
              (HMul.hMul (α := R[X]) 2 X *
                HMul.hMul (α := R[X]) (↑(-(↑n : ℤ)) : R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))) +
            HSub.hSub (β := R[X])
              ((HMul.hMul (α := R[X]) 0 X + HMul.hMul (α := R[X]) 2 1) * T R (-(↑n : ℤ)) +
                HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 2 X)
                  ((derivative : (a : R[X]) → R[X]) (T R (-(↑n : ℤ))) : R[X]))
              ((derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) : R[X]) +
          2 * (U R (-(↑n : ℤ)) - HMul.hMul (α := R[X]) X (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))) +
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 *
          (HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) - U R (-(↑n : ℤ)))) -
    (HMul.hMul (α := R[X]) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1)) +
      (HAdd.hAdd (β := R[X])
            (HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R[X])
                (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1)) +
              HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 2 X)
                ((derivative : (a : R[X]) → R[X]) (T R (-(↑n : ℤ))) : R[X]))
            ((derivative : (a : R[X]) → R[X]) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) : R[X]) +
          HMul.hMul (α := R[X]) 2 (T R (-(↑n : ℤ))) +
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2))) =
  0
Tactic: linear_combination (norm := (push_cast; ring_nf))
      -ih2 + 2 * (X : R[X]) * ih1 + h₁ + 2 * h₃ + (n + 1) * h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ (derivative : (a : R[X]) → R[X]) (T R n) = HMul.hMul (α := R[X]) (↑n : R[X]) (U R (n - 1))
have zero : (derivative : (a : R[X]) → R[X]) (T R 0) = HMul.hMul (α := R[X]) (↑0 : R[X]) (U R (HSub.hSub (α := ℤ) 0 1))
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one =>
    simp
  | 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₂
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : (derivative : (a : R[X]) → R[X]) (T R 0) = HMul.hMul (α := R[X]) (↑0 : R[X]) (U R (HSub.hSub (α := ℤ) 0 1))
⊢ (derivative : (a : R[X]) → R[X]) (T R n) = HMul.hMul (α := R[X]) (↑n : R[X]) (U R (n - 1))
have one : (derivative : (a : R[X]) → R[X]) (T R 1) = HMul.hMul (α := R[X]) (↑1 : R[X]) (U R (HSub.hSub (α := ℤ) 1 1))
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one =>
    simp
  | 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₂
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : (derivative : (a : R[X]) → R[X]) (T R 0) = HMul.hMul (α := R[X]) (↑0 : R[X]) (U R (HSub.hSub (α := ℤ) 0 1))
one : (derivative : (a : R[X]) → R[X]) (T R 1) = HMul.hMul (α := R[X]) (↑1 : R[X]) (U R (HSub.hSub (α := ℤ) 1 1))
⊢ (derivative : (a : R[X]) → R[X]) (T R n) = HMul.hMul (α := R[X]) (↑n : R[X]) (U R (n - 1))
have add_two : ∀ (n : ℕ)
  (ih1 :
    (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
      HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R[X]) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)))
  (ih2 :
    (derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) =
      HMul.hMul (α := R[X]) (↑(↑n : ℤ) : R[X]) (U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))),
  (derivative : (a : R[X]) → R[X]) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    HMul.hMul (α := R[X]) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : R[X]) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1))
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one =>
    simp
  | 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₂
Cleared hypotheses: n