awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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])
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
⊢ (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:
linear_combination (norm := (push_cast; ring_nf))
      h₁ - ih2 + 2 * (X : R[X]) * ih1 + 2 * h₃ - n * h₂

Premises used: Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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))
⊢ 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))
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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])
⊢ 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)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 : ℤ))
⊢ 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)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)) =
    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₁

Premises used: Polynomial.derivative_mul, Polynomial.derivative_ofNat, Polynomial.derivative_X, Polynomial.derivative_sub
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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])
⊢ 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 : ℤ)))) -
      (HSub.hSub (α := R[X]) (-(↑n : R[X])) 1 * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1) +
        (HAdd.hAdd (β := R[X])
              (HAdd.hAdd (α := R[X]) (-(↑n : R[X])) 1 * 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:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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])
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
⊢ (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))

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

Premises used: HAdd.hAdd, OfNat.ofNat, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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))
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))
neg_add_one :
  ∀ (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))
⊢ (derivative : (a : R[X]) → R[X]) (T R n) = HMul.hMul (α := R[X]) (↑n : R[X]) (U R (n - 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₂

Premises used: Polynomial.derivative_mul, Polynomial.derivative_ofNat, Polynomial.derivative_X, HAdd.hAdd, Polynomial.derivative_sub, OfNat.ofNat, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
pos :
  ∀ (hn : n = 0),
    Membership.mem (α := R[X]) (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Ico 0 n))
      ((derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) : R[X])
neg :
  ∀ (hn : n ≠ 0),
    Membership.mem (α := R[X]) (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Ico 0 n))
      ((derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) : R[X])
⊢ Membership.mem (α := R[X]) (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Ico 0 n))
    ((derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) : R[X])

Tactic:
by_cases! hn : n = 0
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hn : n = 0
⊢ Membership.mem (α := R[X]) (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Ico 0 n))
    ((derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) : R[X])

Tactic:
simp [hn]
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hn : n ≠ 0
neg :
  Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Ico 0 n))
    (HSMul.hSMul (α := R[X]) (β := R[X]) (↑(↑n : ℤ) : R[X]) (U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)))
⊢ Membership.mem (α := R[X]) (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Ico 0 n))
    ((derivative : (a : R[X]) → R[X]) (T R (↑n : ℤ)) : R[X])

Tactic:
rw [T_derivative_eq_U, ← smul_eq_mul]

Premises used: Polynomial.Chebyshev.T_derivative_eq_U, smul_eq_mul
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hn : n ≠ 0
neg :
  Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Ico 0 n))
    (HSMul.hSMul (β := R[X]) n (U R (Int.subNatNat n 1)))
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Ico 0 n))
    (HSMul.hSMul (α := R[X]) (β := R[X]) (↑(↑n : ℤ) : R[X]) (U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)))

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hn : n ≠ 0
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Ico 0 n))
    (HSMul.hSMul (β := R[X]) n (U R (Int.subNatNat n 1)))

Tactic:
Submodule.smul_of_tower_mem _ n ?_

Premises used: Submodule.smul_of_tower_mem
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hn : n ≠ 0
neg :
  Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Ico 0 n))
    (U R (Int.subNatNat n 1))
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Ico 0 n))
    (HSMul.hSMul (β := R[X]) n (U R (Int.subNatNat n 1)))

Tactic:
refine Submodule.smul_of_tower_mem _ n ?_

Premises used: Submodule.smul_of_tower_mem
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hn : n ≠ 0
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - 1)))
    (U R (↑(n - 1) : ℤ))

Tactic:
U_mem_span_T R (n - 1)

Premises used: HSub.hSub, OfNat.ofNat, Polynomial.Chebyshev.U_mem_span_T
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hn : n ≠ 0
h :
  Eq.{u_1 + 1} (α := Set R[X]) ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Ico 0 n)
    ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - 1))
h₁ : Int.subNatNat n 1 = (↑(n - 1) : ℤ)
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Ico 0 n))
    (U R (Int.subNatNat n 1))

Tactic:
convert! U_mem_span_T R (n - 1) using 2

Premises used: HSub.hSub, OfNat.ofNat, Polynomial.Chebyshev.U_mem_span_T
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hn : n ≠ 0
⊢ Eq.{u_1 + 1} (α := Set R[X]) ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Ico 0 n)
    ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - 1))

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hn : n ≠ 0
⊢ Int.subNatNat n 1 = (↑(n - 1) : ℤ)

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n k : ℕ
induction :
  Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - 0)))
    ((⇑derivative : (a : R[X]) → R[X])^[0] (T R (↑n : ℤ)))
succ :
  ∀ (n_1 : ℕ),
    Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - n_1)))
        ((⇑derivative : (a : R[X]) → R[X])^[n_1] (T R (↑n : ℤ))) →
      Membership.mem (γ := Submodule ℕ R[X])
        (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - (n_1 + 1))))
        ((⇑derivative : (a : R[X]) → R[X])^[n_1 + 1] (T R (↑n : ℤ)))
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - k)))
    ((⇑derivative : (a : R[X]) → R[X])^[k] (T R (↑n : ℤ)))

Tactic:
induction k
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ n ∈ Set.Icc 0 (n - 0) ∧ Eq (α := R[X]) ((fun (m : ℕ) ↦ (T R (↑m : ℤ) : R[X])) n) (T R (↑n : ℤ))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - 0)))
    (T R (↑n : ℤ))

Tactic:
exact Submodule.mem_span_of_mem ⟨n, by simp⟩
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - 0)))
    ((⇑derivative : (a : R[X]) → R[X])^[0] (T R (↑n : ℤ)))

Tactic:
case zero =>
    rw [Function.iterate_zero_apply]
    exact Submodule.mem_span_of_mem ⟨n, by simp⟩

Premises used: Function.iterate_zero_apply
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n k : ℕ
ih :
  Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - k)))
    ((⇑derivative : (a : R[X]) → R[X])^[k] (T R (↑n : ℤ)))
rw :
  Membership.mem (α := R[X]) (γ := Submodule ℕ R[X])
    (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - (k + 1))))
    ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R (↑n : ℤ))) : R[X])
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - (k + 1))))
    ((⇑derivative : (a : R[X]) → R[X])^[k + 1] (T R (↑n : ℤ)))

Tactic:
rw [Function.iterate_succ_apply']

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n k : ℕ
ih :
  Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - k)))
    ((⇑derivative : (a : R[X]) → R[X])^[k] (T R (↑n : ℤ)))
this :
  LE.le.{u_1} (α := Submodule ℕ R[X])
    (Submodule.span ℕ ((fun (m : ℕ) ↦ (derivative : (a : R[X]) → R[X]) (T R (↑m : ℤ))) '' Set.Icc 0 (n - k)))
    (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - (k + 1))))
a :
  Membership.mem (α := R[X]) (γ := Submodule ℕ R[X])
    (Submodule.span ℕ ((fun (m : ℕ) ↦ (derivative : (a : R[X]) → R[X]) (T R (↑m : ℤ))) '' Set.Icc 0 (n - k)))
    ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R (↑n : ℤ))) : R[X])
⊢ Membership.mem (α := R[X]) (γ := Submodule ℕ R[X])
    (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - (k + 1))))
    ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (T R (↑n : ℤ))) : R[X])

Tactic:
apply this