awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))))
⊢ Membership.mem (α := R[X]) (γ := Submodule ℕ R[X])
    (Submodule.span ℕ
      (Set.image (α := R[X])
        (⇑((↑ℕ :
                {S M M₂ : Type u_1} →
                  [inst : Semiring ℕ] →
                    [inst_1 : Semiring S] →
                      [inst_2 : AddCommMonoid M] →
                        [inst_3 : AddCommMonoid M₂] →
                          [inst_4 : Module ℕ M] →
                            [inst_5 : Module ℕ M₂] →
                              [inst_6 : Module S M] →
                                [inst_7 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ ℕ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℕ] M₂)
              derivative) :
          (a : R[X]) → R[X])
        ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - k))))
    (((↑ℕ :
              {S M M₂ : Type u_1} →
                [inst : Semiring ℕ] →
                  [inst_1 : Semiring S] →
                    [inst_2 : AddCommMonoid M] →
                      [inst_3 : AddCommMonoid M₂] →
                        [inst_4 : Module ℕ M] →
                          [inst_5 : Module ℕ M₂] →
                            [inst_6 : Module S M] →
                              [inst_7 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℕ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℕ] M₂)
            derivative :
          (a : R[X]) → R[X])
        ((⇑derivative : (a : R[X]) → R[X])^[k] (T R (↑n : ℤ))) :
      R[X])

Tactic:
Submodule.apply_mem_span_image_of_mem_span (derivative.restrictScalars ℕ) ih

Premises used: Polynomial.derivative, LinearMap.restrictScalars, Nat, Submodule.apply_mem_span_image_of_mem_span
-- 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))))
h :
  Eq.{u_1 + 1} (α := Set R[X]) ((fun (m : ℕ) ↦ (derivative : (a : R[X]) → R[X]) (T R (↑m : ℤ))) '' Set.Icc 0 (n - k))
    (Set.image (α := R[X])
      (⇑((↑ℕ :
              {S M M₂ : Type u_1} →
                [inst : Semiring ℕ] →
                  [inst_1 : Semiring S] →
                    [inst_2 : AddCommMonoid M] →
                      [inst_3 : AddCommMonoid M₂] →
                        [inst_4 : Module ℕ M] →
                          [inst_5 : Module ℕ M₂] →
                            [inst_6 : Module S M] →
                              [inst_7 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℕ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℕ] M₂)
            derivative) :
        (a : R[X]) → R[X])
      ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - k)))
⊢ 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])

Tactic:
convert! Submodule.apply_mem_span_image_of_mem_span (derivative.restrictScalars ℕ) ih using 2

Premises used: Polynomial.derivative, LinearMap.restrictScalars, Nat, Submodule.apply_mem_span_image_of_mem_span
-- 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))))
⊢ Eq.{u_1 + 1} (α := Set R[X]) ((fun (m : ℕ) ↦ (derivative : (a : R[X]) → R[X]) (T R (↑m : ℤ))) '' Set.Icc 0 (n - k))
    (Set.image (α := R[X])
      (⇑((↑ℕ :
              {S M M₂ : Type u_1} →
                [inst : Semiring ℕ] →
                  [inst_1 : Semiring S] →
                    [inst_2 : AddCommMonoid M] →
                      [inst_3 : AddCommMonoid M₂] →
                        [inst_4 : Module ℕ M] →
                          [inst_5 : Module ℕ M₂] →
                            [inst_6 : Module S M] →
                              [inst_7 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℕ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℕ] M₂)
            derivative) :
        (a : R[X]) → R[X])
      ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - k)))

Tactic:
simp [Set.image]

Premises used: Set.image
-- 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 : ℤ)))
suffices :
  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))))
⊢ 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:
suffices Submodule.span ℕ ((fun m : ℕ => derivative (T R m)) '' Set.Icc 0 (n - k)) ≤
      Submodule.span ℕ ((fun m : ℕ => T R m) '' Set.Icc 0 (n - (k + 1))) by
      apply this
      convert! Submodule.apply_mem_span_image_of_mem_span (derivative.restrictScalars ℕ) ih using 2
      simp [Set.image]
-- 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 : ℤ)))
⊢ 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))))

Tactic:
Submodule.span_le.mpr (fun x hx => ?_)

Premises used: Iff.mpr, Submodule.span_le
-- 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 : ℤ)))
refine :
  ∀ (x : R[X])
    (hx :
      Membership.mem (γ := Set R[X])
        ((fun (m : ℕ) ↦ (derivative : (a : R[X]) → R[X]) (T R (↑m : ℤ))) '' Set.Icc 0 (n - k)) x),
    x ∈ (↑(Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - (k + 1)))) : Set R[X])
⊢ 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))))

Tactic:
refine Submodule.span_le.mpr (fun x hx => ?_)

Premises used: Iff.mpr, Submodule.span_le
-- 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 : ℤ)))
x : R[X]
hx :
  Membership.mem (γ := Set R[X]) ((fun (m : ℕ) ↦ (derivative : (a : R[X]) → R[X]) (T R (↑m : ℤ))) '' Set.Icc 0 (n - k))
    x
obtain :
  ∀ (m : ℕ) (hm : m ∈ Set.Icc 0 (n - k)),
    (fun (m : ℕ) ↦ ((derivative : (a : R[X]) → R[X]) (T R (↑m : ℤ)) : R[X])) m ∈
      (↑(Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - (k + 1)))) : Set R[X])
⊢ x ∈ (↑(Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - (k + 1)))) : Set R[X])

Tactic:
obtain ⟨m, hm, rfl⟩ := hx

Premises used: rfl
-- 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 : ℤ)))
m : ℕ
hm : m ∈ Set.Icc 0 (n - k)
⊢ Subset.{u_1} (α := Set R[X]) ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Ico 0 m)
    ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - (k + 1)))

Tactic:
grind
-- 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 : ℤ)))
m : ℕ
hm : m ∈ Set.Icc 0 (n - k)
⊢ (fun (m : ℕ) ↦ ((derivative : (a : R[X]) → R[X]) (T R (↑m : ℤ)) : R[X])) m ∈
    (↑(Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - (k + 1)))) : Set R[X])

Tactic:
refine (Submodule.span_mono (by grind)) (T_derivative_mem_span_T (R := R) m)

Premises used: Submodule.span_mono, Polynomial.Chebyshev.T_derivative_mem_span_T
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n = HMul.hMul (α := R[X]) X (T R (n + 1)) - T R (n + 2)

Tactic:
have H₁ := one_sub_X_sq_mul_U_eq_pol_in_T R n
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
H₁ : (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n = HMul.hMul (α := R[X]) X (T R (n + 1)) - T R (n + 2)
⊢ (derivative : (a : R[X]) → R[X]) (T R (n + 1)) = HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1))

Tactic:
have H₂ := T_derivative_eq_U (R := R) (n + 1)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
H₁ : (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n = HMul.hMul (α := R[X]) X (T R (n + 1)) - T R (n + 2)
H₂ : (derivative : (a : R[X]) → R[X]) (T R (n + 1)) = HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1))
⊢ T R (n + 2) = HMul.hMul (α := R[X]) 2 X * T R (n + 1) - T R n

Tactic:
have h₁ := T_add_two R n
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
H₁ : (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n = HMul.hMul (α := R[X]) X (T R (n + 1)) - T R (n + 2)
H₂ : (derivative : (a : R[X]) → R[X]) (T R (n + 1)) = HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1))
h₁ : T R (n + 2) = HMul.hMul (α := R[X]) 2 X * T R (n + 1) - T R n
a :
  HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) (T R (n + 1)) : R[X]) +
        (HSub.hSub (α := R[X]) (-(↑n : R[X])) 1 * (HMul.hMul (α := R[X]) 2 X * T R (n + 1) - T R n) +
            (-HPow.hPow (α := R[X]) (β := ℕ) X 2 + 1) * (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]) X (T R (n + 1)) - T R (n + 2))) -
      (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (T R n - HMul.hMul (α := R[X]) X (T R (n + 1))) +
        (HSub.hSub (α := R[X]) (-(↑n : R[X])) 1 * T R (n + 2) +
            HMul.hMul (β := R[X]) (-HPow.hPow (α := R[X]) (β := ℕ) X 2 + 1)
              ((derivative : (a : R[X]) → R[X]) (T R (n + 1)) : R[X]) +
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * ((1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n))) =
    0
⊢ HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) (T R (n + 1)) : R[X]) +
        (HSub.hSub (α := R[X]) (-(↑n : R[X])) 1 * (HMul.hMul (α := R[X]) 2 X * T R (n + 1) - T R n) +
            (-HPow.hPow (α := R[X]) (β := ℕ) X 2 + 1) * 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]) X (T R (n + 1)) - T R (n + 2))) -
      (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (T R n - HMul.hMul (α := R[X]) X (T R (n + 1))) +
        (HSub.hSub (α := R[X]) (-(↑n : R[X])) 1 * T R (n + 2) +
            HMul.hMul (β := R[X]) (-HPow.hPow (α := R[X]) (β := ℕ) X 2 + 1)
              ((derivative : (a : R[X]) → R[X]) (T R (n + 1)) : R[X]) +
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * ((1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n))) =
    0

Tactic:
push_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
H₁ : (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n = HMul.hMul (α := R[X]) X (T R (n + 1)) - T R (n + 2)
H₂ : (derivative : (a : R[X]) → R[X]) (T R (n + 1)) = HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1))
h₁ : T R (n + 2) = HMul.hMul (α := R[X]) 2 X * T R (n + 1) - T R n
⊢ HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) (T R (n + 1)) : R[X]) +
        (HSub.hSub (α := R[X]) (-(↑n : R[X])) 1 * (HMul.hMul (α := R[X]) 2 X * T R (n + 1) - T R n) +
            (-HPow.hPow (α := R[X]) (β := ℕ) X 2 + 1) * (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]) X (T R (n + 1)) - T R (n + 2))) -
      (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (T R n - HMul.hMul (α := R[X]) X (T R (n + 1))) +
        (HSub.hSub (α := R[X]) (-(↑n : R[X])) 1 * T R (n + 2) +
            HMul.hMul (β := R[X]) (-HPow.hPow (α := R[X]) (β := ℕ) X 2 + 1)
              ((derivative : (a : R[X]) → R[X]) (T R (n + 1)) : R[X]) +
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * ((1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n))) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
H₁ : (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n = HMul.hMul (α := R[X]) X (T R (n + 1)) - T R (n + 2)
H₂ : (derivative : (a : R[X]) → R[X]) (T R (n + 1)) = HMul.hMul (α := R[X]) (↑(n + 1) : R[X]) (U R (n + 1 - 1))
h₁ : T R (n + 2) = HMul.hMul (α := R[X]) 2 X * T R (n + 1) - T R n
a :
  HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
          ((derivative : (a : R[X]) → R[X]) (T R (n + 1)) : R[X]) +
        (HSub.hSub (α := R[X]) (-(↑n : R[X])) 1 * (HMul.hMul (α := R[X]) 2 X * T R (n + 1) - T R n) +
            (-HPow.hPow (α := R[X]) (β := ℕ) X 2 + 1) * 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]) X (T R (n + 1)) - T R (n + 2))) -
      (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (T R n - HMul.hMul (α := R[X]) X (T R (n + 1))) +
        (HSub.hSub (α := R[X]) (-(↑n : R[X])) 1 * T R (n + 2) +
            HMul.hMul (β := R[X]) (-HPow.hPow (α := R[X]) (β := ℕ) X 2 + 1)
              ((derivative : (a : R[X]) → R[X]) (T R (n + 1)) : R[X]) +
          HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * ((1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n))) =
    0
⊢ HMul.hMul (β := R[X]) (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2)
      ((derivative : (a : R[X]) → R[X]) (T R (n + 1)) : R[X]) =
    HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (T R n - HMul.hMul (α := R[X]) X (T R (n + 1)))

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

Premises used: HSub.hSub, HPow.hPow, HAdd.hAdd, OfNat.ofNat, Polynomial.X, Neg.neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (n + 2)) : R[X])
    ((derivative : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) X (T R (n + 1)) - (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n) :
      R[X])

Tactic:
have h₁ := congr_arg derivative <| T_eq_X_mul_T_sub_pol_U R n
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h₁ :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (T R (n + 2)) : R[X])
    ((derivative : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) X (T R (n + 1)) - (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n) :
      R[X])
⊢ 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]))

Tactic:
simp only [derivative_sub, derivative_mul, derivative_X, derivative_one, derivative_X_pow,
    T_derivative_eq_U, C_eq_natCast] at h₁

Premises used: Polynomial.derivative_mul, Polynomial.derivative_X, Polynomial.Chebyshev.T_derivative_eq_U, Polynomial.C_eq_natCast, Polynomial.derivative_X_pow, Polynomial.derivative_sub, Polynomial.derivative_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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]))
⊢ T R (n + 1) = U R (n + 1) - HMul.hMul (α := R[X]) X (U R (n + 1 - 1))

Tactic:
have h₂ := T_eq_U_sub_X_mul_U R (n + 1)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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))
a :
  HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * T R (n + 1) +
        (HMul.hMul (α := R[X]) 1 (T R (n + 1)) + X * (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * U R (n + 1 - 1)) -
            ((0 - 2 * HPow.hPow (α := R[X]) (β := ℕ) X 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]) +
        (HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * U R (n + 2 - 1) + HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * T R (n + 1))) =
    0
⊢ 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:
push_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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]) 1 (T R (n + 1)) + X * (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * U R (n + 1 - 1)) -
            ((0 - 2 * HPow.hPow (α := R[X]) (β := ℕ) X 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]) +
        (HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * U R (n + 2 - 1) + HAdd.hAdd (α := R[X]) (↑n : R[X]) 2 * T R (n + 1))) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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))
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
⊢ 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])

Tactic:
linear_combination (norm := (push_cast; ring_nf))
    h₁ + (n + 2) * h₂

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ 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)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
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))
⊢ 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])

Tactic:
rw [T_derivative_eq_U, T_derivative_eq_U]

Premises used: Polynomial.Chebyshev.T_derivative_eq_U