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 : ℤ
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))
⊢ (derivative : (a : R[X]) → R[X]) (T R n) = HMul.hMul (α := R[X]) (↑n : R[X]) (U R (n - 1))
have 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))
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 : ℕ
⊢ 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])
have 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])
Tactic: by_cases! hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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])
⊢ 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])
have 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])
Tactic: by_cases! hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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])
have 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)))
Tactic: rw [T_derivative_eq_U, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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]) (β := R[X]) (↑(↑n : ℤ) : R[X]) (U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)))
have 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)))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)))
have neg : Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Ico 0 n))
  (U R (Int.subNatNat n 1))
Tactic: refine Submodule.smul_of_tower_mem _ n ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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))
    (U R (Int.subNatNat n 1))
have 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))
Tactic: convert! U_mem_span_T R (n - 1) using 2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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))
⊢ Membership.mem (γ := Submodule ℕ R[X]) (Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Ico 0 n))
    (U R (Int.subNatNat n 1))
have h₁ : Int.subNatNat n 1 = (↑(n - 1) : ℤ)
Tactic: convert! U_mem_span_T R (n - 1) using 2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n k : ℕ
⊢ 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 : ℤ)))
have 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 : ℤ)))
Tactic: induction k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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 : ℤ)))
⊢ 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 : ℤ)))
have 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 : ℤ)))
Tactic: induction k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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 : ℤ)))
⊢ 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 : ℤ)))
have 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])
Tactic: rw [Function.iterate_succ_apply']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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 ℕ ((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])
have 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])
Tactic: apply this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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 ℕ ((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])
have 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)))
Tactic: convert! Submodule.apply_mem_span_image_of_mem_span (derivative.restrictScalars ℕ) ih using 2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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 : ℤ)))
⊢ 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])
have 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))))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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))))
have 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])
Tactic: refine Submodule.span_le.mpr (fun x hx => ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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
⊢ x ∈ (↑(Submodule.span ℕ ((fun (m : ℕ) ↦ T R (↑m : ℤ)) '' Set.Icc 0 (n - (k + 1)))) : Set R[X])
have 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])
Tactic: obtain ⟨m, hm, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing 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]) =
    HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (T R n - HMul.hMul (α := R[X]) X (T R (n + 1)))
have H₁ : (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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
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)
⊢ 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)))
have H₂ : (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)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
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))
⊢ 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)))
have h₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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) * 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
have 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
Tactic: push_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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]) =
    HAdd.hAdd (α := R[X]) (↑n : R[X]) 1 * (T R n - HMul.hMul (α := R[X]) X (T R (n + 1)))
have 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
Tactic: linear_combination (norm := (push_cast; ring_nf))
    (-n - 1) * h₁ + (-(X : R[X]) ^ 2 + 1) * H₂ + (n + 1) * 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 * 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 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])
Tactic: have h₁ := congr_arg derivative <| T_eq_X_mul_T_sub_pol_U 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]) (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])
⊢ 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 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]))
Tactic: simp only [derivative_sub, derivative_mul, derivative_X, derivative_one, derivative_X_pow,
    T_derivative_eq_U, C_eq_natCast] 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]) (↑(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]))
⊢ 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 h₂ : 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)
-- 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]) 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
have 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
Tactic: push_cast