awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h₁ :
  HMul.hMul (α := R[X]) (↑(n + 2) : R[X]) (U R (n + 2 - 1)) =
    HMul.hMul (α := R[X]) 1 (T R (n + 1)) + X * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)) -
      ((0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1)) * U R n +
        HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]))
h₂ : T R (n + 1) = U R (n + 1) - HMul.hMul (α := R[X]) X (U R (n + 1 - 1))
⊢ HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * T R (n + 1) =
    HMul.hMul (α := R[X]) X (U R n) -
      HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) ((derivative : (a : R[X]) → R[X]) (U R n) : R[X])
have a : HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * T R (n + 1) +
      (HMul.hMul (α := R[X]) 1 (T R (n + 1)) + X * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)) -
          ((0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1)) * U R n +
            HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
              ((derivative : (a : R[X]) → R[X]) (U R n) : R[X])) +
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * (U R (n + 1) - HMul.hMul (α := R[X]) X (U R (n + 1 - 1)))) -
    (HMul.hMul (α := R[X]) X (U R n) -
        HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) +
      (HMul.hMul (α := R[X]) (↑(n + 2) : R[X]) (U R (n + 2 - 1)) + HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * T R (n + 1))) =
  0
Tactic: linear_combination (norm := (push_cast; ring_nf))
    h₁ + (n + 2) * h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * T R (n + 1) =
    HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) (↑n : R[X]) X)
        ((derivative : (a : R[X]) → R[X]) (T R (n + 1)) : R[X]) -
      HMul.hMul (β := R[X]) (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1) ((derivative : (a : R[X]) → R[X]) (T R n) : R[X])
have h : T R (n - 1 + 2) = HMul.hMul (α := R[X]) X (U R (n - 1 + 1)) - U R (n - 1)
Tactic: have h := T_eq_X_mul_U_sub_U (R := R) (n - 1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h : T R (n - 1 + 2) = HMul.hMul (α := R[X]) X (U R (n - 1 + 1)) - U R (n - 1)
⊢ HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * T R (n + 1) =
    HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) (↑n : R[X]) X)
        ((derivative : (a : R[X]) → R[X]) (T R (n + 1)) : R[X]) -
      HMul.hMul (β := R[X]) (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1) ((derivative : (a : R[X]) → R[X]) (T R n) : R[X])
have rw : HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * T R (n + 1) =
  HMul.hMul (α := R[X]) (↑n : R[X]) X * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)) -
    HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑n : R[X]) (U R (n - 1))
Tactic: rw [T_derivative_eq_U, T_derivative_eq_U]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h : T R (n - 1 + 2) = HMul.hMul (α := R[X]) X (U R (n - 1 + 1)) - U R (n - 1)
⊢ HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * T R (n + 1) +
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * (HMul.hMul (α := R[X]) X (U R (n - 1 + 1)) - U R (n - 1)) -
      (HMul.hMul (α := R[X]) (↑n : R[X]) X * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)) -
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑n : R[X]) (U R (n - 1)) +
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * T R (n - 1 + 2)) =
    0
have a : HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * T R (n + 1) +
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * (HMul.hMul (α := R[X]) X (U R (n - 1 + 1)) - U R (n - 1)) -
    (HMul.hMul (α := R[X]) (↑n : R[X]) X * (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * U R (n + 1 - 1)) -
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑n : R[X]) (U R (n - 1)) +
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * T R (n - 1 + 2)) =
  0
Tactic: push_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h : T R (n - 1 + 2) = HMul.hMul (α := R[X]) X (U R (n - 1 + 1)) - U R (n - 1)
⊢ HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * T R (n + 1) =
    HMul.hMul (α := R[X]) (↑n : R[X]) X * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)) -
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑n : R[X]) (U R (n - 1))
have a : HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * T R (n + 1) +
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * (HMul.hMul (α := R[X]) X (U R (n - 1 + 1)) - U R (n - 1)) -
    (HMul.hMul (α := R[X]) (↑n : R[X]) X * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)) -
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑n : R[X]) (U R (n - 1)) +
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (↑n : R[X]) * T R (n - 1 + 2)) =
  0
Tactic: linear_combination (norm := (push_cast; ring_nf))
    (n + 1) * n * h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[2] (T R n) =
    HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) -
      HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * T R n
have h₁ : Eq (α := R[X])
  ((derivative : (a : R[X]) → R[X])
      (HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
        ((derivative : (a : R[X]) → R[X]) (T R (n - 1 + 1)) : R[X])) :
    R[X])
  ((derivative : (a : R[X]) → R[X])
      (HAdd.hAdd (α := R[X]) (↑(n - 1) : R[X]) 1 * (T R (n - 1) - HMul.hMul (α := R[X]) X (T R (n - 1 + 1)))) :
    R[X])
Tactic: have h₁ := congr_arg derivative <| one_sub_X_sq_mul_derivative_T_eq_poly_in_T (R := R) (n - 1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h₁ :
  Eq (α := R[X])
    ((derivative : (a : R[X]) → R[X])
        (HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) (T R (n - 1 + 1)) : R[X])) :
      R[X])
    ((derivative : (a : R[X]) → R[X])
        (HAdd.hAdd (α := R[X]) (↑(n - 1) : R[X]) 1 * (T R (n - 1) - HMul.hMul (α := R[X]) X (T R (n - 1 + 1)))) :
      R[X])
⊢ (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[2] (T R n) =
    HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) -
      HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * T R n
have h₂ : HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
      ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) +
    HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
      ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (T R n)) : R[X]) =
  0 * (T R (n - 1) - HMul.hMul (α := R[X]) X (T R n)) +
    (↑n : R[X]) *
      HSub.hSub (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (n - 1)) : R[X])
        (HMul.hMul (α := R[X]) 1 (T R n) +
          HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]))
Tactic: simp only [derivative_sub, derivative_mul, derivative_X, derivative_one, derivative_X_pow,
    C_eq_natCast, sub_add_cancel, Int.cast_sub, Int.cast_one, derivative_intCast] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h₁ :
  HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
        ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) +
      HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
        ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (T R n)) : R[X]) =
    0 * (T R (n - 1) - HMul.hMul (α := R[X]) X (T R n)) +
      (↑n : R[X]) *
        HSub.hSub (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (n - 1)) : R[X])
          (HMul.hMul (α := R[X]) 1 (T R n) +
            HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]))
⊢ (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[2] (T R n) =
    HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) -
      HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * T R n
have h₂ : HAdd.hAdd (α := R[X]) (↑(n - 1) : R[X]) 1 * (↑(n - 1) : R[X]) * T R (n - 1 + 1) =
  HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) (↑(n - 1) : R[X]) X)
      ((derivative : (a : R[X]) → R[X]) (T R (n - 1 + 1)) : R[X]) -
    HMul.hMul (β := R[X]) (HAdd.hAdd (α := R[X]) (↑(n - 1) : R[X]) 1)
      ((derivative : (a : R[X]) → R[X]) (T R (n - 1)) : R[X])
Tactic: have h₂ := add_one_mul_self_mul_T_eq_poly_in_T (R := R) (n - 1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h₁ :
  HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
        ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) +
      HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
        ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (T R n)) : R[X]) =
    0 * (T R (n - 1) - HMul.hMul (α := R[X]) X (T R n)) +
      (↑n : R[X]) *
        HSub.hSub (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (n - 1)) : R[X])
          (HMul.hMul (α := R[X]) 1 (T R n) +
            HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]))
h₂ :
  HAdd.hAdd (α := R[X]) (↑(n - 1) : R[X]) 1 * (↑(n - 1) : R[X]) * T R (n - 1 + 1) =
    HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) (↑(n - 1) : R[X]) X)
        ((derivative : (a : R[X]) → R[X]) (T R (n - 1 + 1)) : R[X]) -
      HMul.hMul (β := R[X]) (HAdd.hAdd (α := R[X]) (↑(n - 1) : R[X]) 1)
        ((derivative : (a : R[X]) → R[X]) (T R (n - 1)) : R[X])
⊢ HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
      ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (T R n)) : R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) -
      HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * T R n
have a : HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
        ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (T R n)) : R[X]) +
      (0 * (T R (n - 1) - HMul.hMul (α := R[X]) X (T R n)) +
          (↑n : R[X]) *
            HSub.hSub (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (n - 1)) : R[X])
              (HMul.hMul (α := R[X]) 1 (T R n) +
                HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X])) +
        (HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) (↑(n - 1) : R[X]) X)
            ((derivative : (a : R[X]) → R[X]) (T R (n - 1 + 1)) : R[X]) -
          HMul.hMul (β := R[X]) (HAdd.hAdd (α := R[X]) (↑(n - 1) : R[X]) 1)
            ((derivative : (a : R[X]) → R[X]) (T R (n - 1)) : R[X]))) -
    (HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) -
        HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * T R n +
      (HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
            ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) +
          HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
            ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (T R n)) : R[X]) +
        HAdd.hAdd (α := R[X]) (↑(n - 1) : R[X]) 1 * (↑(n - 1) : R[X]) * T R (n - 1 + 1))) =
  0
Tactic: linear_combination (norm := (push_cast; ring_nf))
    h₁ + h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[2] (U R n) =
    HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 3 X) ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * (↑n : R[X]) * U R n
have h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * T R (n + 1)) : R[X])
  ((derivative : (a : R[X]) → R[X])
      (HMul.hMul (α := R[X]) X (U R n) -
        HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) (U R n) : R[X])) :
    R[X])
Tactic: have h := congr_arg derivative <| add_one_mul_T_eq_poly_in_U (R := R) n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * T R (n + 1)) : R[X])
    ((derivative : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) X (U R n) -
          HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
            ((derivative : (a : R[X]) → R[X]) (U R n) : R[X])) :
      R[X])
⊢ (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[2] (U R n) =
    HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 3 X) ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * (↑n : R[X]) * U R n
have h₁ : HAdd.hAdd (α := R[X]) 0 0 * T R (n + 1) +
    HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)) =
  HMul.hMul (α := R[X]) 1 (U R n) +
      HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
    (HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
        ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) +
      HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
        ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]))
Tactic: simp only [derivative_add, derivative_sub, derivative_mul, derivative_X, derivative_one,
    derivative_X_pow, derivative_intCast, C_eq_natCast, T_derivative_eq_U] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h :
  HAdd.hAdd (α := R[X]) 0 0 * T R (n + 1) +
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)) =
    HMul.hMul (α := R[X]) 1 (U R n) +
        HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
      (HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
          ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) +
        HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]))
⊢ HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]) +
        (HMul.hMul (α := R[X]) 1 (U R n) +
            HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
          (HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
              ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) +
            HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
              ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]))) -
      (HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 3 X) ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * (↑n : R[X]) * U R n +
        (HAdd.hAdd (α := R[X]) 0 0 * T R (n + 1) +
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)))) =
    0
have a : HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
        ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]) +
      (HMul.hMul (α := R[X]) 1 (U R n) +
          HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
        (HMul.hMul (β := R[X]) (0 - 2 * HPow.hPow (α := R[X]) (β := ℕ) X 1)
            ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) +
          HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
            ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]))) -
    (HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 3 X) ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * (↑n : R[X]) * U R n +
      (HAdd.hAdd (α := R[X]) 0 0 * T R (n + 1) +
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * U R (n + 1 - 1)))) =
  0
Tactic: push_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h :
  HAdd.hAdd (α := R[X]) 0 0 * T R (n + 1) +
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)) =
    HMul.hMul (α := R[X]) 1 (U R n) +
        HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
      (HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
          ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) +
        HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]))
⊢ HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
      ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]) =
    HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 3 X) ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
      HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * (↑n : R[X]) * U R n
have a : HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
        ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]) +
      (HMul.hMul (α := R[X]) 1 (U R n) +
          HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
        (HMul.hMul (β := R[X]) (0 - (↑2 : R[X]) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1))
            ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) +
          HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
            ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) (U R n)) : R[X]))) -
    (HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) 3 X) ((derivative : (a : R[X]) → R[X]) (U R n) : R[X]) -
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * (↑n : R[X]) * U R n +
      (HAdd.hAdd (α := R[X]) 0 0 * T R (n + 1) +
        HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1)))) =
  0
Tactic: linear_combination (norm := (push_cast; ring_nf)) h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
⊢ (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) =
    (HMul.hMul (α := R[X]) 2 (↑k : R[X]) + 1) * X * (⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n) -
      (HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 - HPow.hPow (α := R[X]) (β := ℕ) (↑k : R[X]) 2) *
        (⇑derivative : (a : R[X]) → R[X])^[k] (T R n)
have h : (⇑derivative : (a : R[X]) → R[X])^[k]
    ((1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[2] (T R n)) =
  (⇑derivative : (a : R[X]) → R[X])^[k]
    (HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) -
      HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * T R n)
Tactic: have h := congr_arg derivative^[k] <| one_sub_X_sq_mul_derivative_derivative_T_eq_poly_in_T
    (R := R) n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative : (a : R[X]) → R[X])^[k]
      ((1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[2] (T R n)) =
    (⇑derivative : (a : R[X]) → R[X])^[k]
      (HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) -
        HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 * T R n)
⊢ (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) =
    (HMul.hMul (α := R[X]) 2 (↑k : R[X]) + 1) * X * (⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n) -
      (HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 - HPow.hPow (α := R[X]) (β := ℕ) (↑k : R[X]) 2) *
        (⇑derivative : (a : R[X]) → R[X])^[k] (T R n)
have h₁ : (⇑derivative : (a : R[X]) → R[X])^[k]
    ((1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[2] (T R n)) =
  (⇑derivative : (a : R[X]) → R[X])^[k]
    (HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) -
      HMul.hMul (α := R[X]) (↑(HPow.hPow (β := ℕ) n 2) : R[X]) (T R n))
Tactic: norm_cast at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
k : ℕ
h :
  (⇑derivative : (a : R[X]) → R[X])^[k]
      ((1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[2] (T R n)) =
    (⇑derivative : (a : R[X]) → R[X])^[k]
      (HMul.hMul (α := R[X]) (β := R[X]) X ((derivative : (a : R[X]) → R[X]) (T R n) : R[X]) -
        HMul.hMul (α := R[X]) (↑(HPow.hPow (β := ℕ) n 2) : R[X]) (T R n))
⊢ (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * (⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) =
    (HMul.hMul (α := R[X]) 2 (↑k : R[X]) + 1) * X * (⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n) -
      (HPow.hPow (α := R[X]) (β := ℕ) (↑n : R[X]) 2 - HPow.hPow (α := R[X]) (β := ℕ) (↑k : R[X]) 2) *
        (⇑derivative : (a : R[X]) → R[X])^[k] (T R n)
have h₁ : (⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) -
    ((⇑derivative : (a : R[X]) → R[X])^[k + 2] (T R n) * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        HSMul.hSMul (β := R[X]) (2 * k) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) * X +
      HSMul.hSMul (β := R[X]) (k * (k - 1)) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))) =
  HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R n)) X +
      HSMul.hSMul (β := R[X]) k ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n)) -
    HMul.hMul (α := R[X]) (↑(HPow.hPow (β := ℕ) n 2) : R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R n))
Tactic: rw [sub_mul, iterate_derivative_sub, one_mul, ← Function.iterate_add_apply, mul_comm (X ^ 2),
    iterate_derivative_sub, mul_comm X, iterate_derivative_intCast_mul,
    iterate_derivative_derivative_mul_X_sq, iterate_derivative_derivative_mul_X] at h
Cleared hypotheses: h