awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
this : U R (HAdd.hAdd (α := ℤ) 0 2) = HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) 0 1) - U R 0
⊢ U R 2 = 4 * HPow.hPow (α := R[X]) (β := ℕ) X 2 - 1
have this₁ : U R 2 = HMul.hMul (α := R[X]) 2 X * HMul.hMul (α := R[X]) 2 X - 1
Tactic: simp only [zero_add, U_one, U_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)) (-U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (-U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
⊢ Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1)) (-U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1))
have h₁ : U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) 2 X * U R (↑n : ℤ) - U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)
Tactic: have h₁ := U_add_one R n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)) (-U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (-U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
h₁ :
  U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) 2 X * U R (↑n : ℤ) - U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)
⊢ Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1)) (-U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1))
have h₂ : U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 2) =
  HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1) - U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: have h₂ := U_sub_two R (-n - 1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)) (-U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (-U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
h₁ :
  U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) 2 X * U R (↑n : ℤ) - U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)
h₂ :
  U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 2) =
    HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1) - U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
⊢ Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1)) (-U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1))
have a : U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1) +
      (HMul.hMul (α := R[X]) 2 X * -U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1) + U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) +
          (HMul.hMul (α := R[X]) 2 X * U R (↑n : ℤ) - U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) +
        (HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1) -
          U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))) -
    (-U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1) +
      (HMul.hMul (α := R[X]) 2 X * U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1) + -U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) +
          U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) +
        U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 2))) =
  0
Tactic: linear_combination (norm := ring_nf) 2 * (X : R[X]) * ih1 - ih2 + h₁ + h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (- -(↑n : ℤ)) 1)) (-U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
ih2 : Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1))
⊢ Eq (α := R[X]) (U R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1))
have h₁ : U R (↑n : ℤ) = HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) - U R (HSub.hSub (α := ℤ) (↑n : ℤ) 2)
Tactic: have h₁ := U_eq R n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (- -(↑n : ℤ)) 1)) (-U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
ih2 : Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1))
h₁ :
  U R (↑n : ℤ) = HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) - U R (HSub.hSub (α := ℤ) (↑n : ℤ) 2)
⊢ Eq (α := R[X]) (U R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1))
have h₂ : U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2) =
  HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) - U R (-(↑n : ℤ))
Tactic: have h₂ := U_sub_two R (-n)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (- -(↑n : ℤ)) 1)) (-U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
ih2 : Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1))
h₁ :
  U R (↑n : ℤ) = HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) - U R (HSub.hSub (α := ℤ) (↑n : ℤ) 2)
h₂ :
  U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) - U R (-(↑n : ℤ))
⊢ Eq (α := R[X]) (U R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1))
have a : U R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1) +
      (HMul.hMul (α := R[X]) 2 X * -U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) +
            U R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1) +
          (HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) - U R (HSub.hSub (α := ℤ) (↑n : ℤ) 2)) +
        (HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) - U R (-(↑n : ℤ)))) -
    (-U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1) +
      (HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (- -(↑n : ℤ)) 1) +
            -U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1) +
          U R (↑n : ℤ) +
        U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2))) =
  0
Tactic: linear_combination (norm := ring_nf) 2 * (X : R[X]) * ih1 - ih2 + h₁ + h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ Eq (α := R[X]) (U R (-n - 1)) (-U R (n - 1))
have zero : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (-0) 1)) (-U R (HSub.hSub (α := ℤ) 0 1))
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    have h₁ := U_add_one R n
    have h₂ := U_sub_two R (-n - 1)
    linear_combination (norm := ring_nf) 2 * (X : R[X]) * ih1 - ih2 + h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := U_eq R n
    have h₂ := U_sub_two R (-n)
    linear_combination (norm := ring_nf) 2 * (X : R[X]) * ih1 - ih2 + h₁ + h₂
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (-0) 1)) (-U R (HSub.hSub (α := ℤ) 0 1))
⊢ Eq (α := R[X]) (U R (-n - 1)) (-U R (n - 1))
have one : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (-1) 1)) (-U R (HSub.hSub (α := ℤ) 1 1))
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    have h₁ := U_add_one R n
    have h₂ := U_sub_two R (-n - 1)
    linear_combination (norm := ring_nf) 2 * (X : R[X]) * ih1 - ih2 + h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := U_eq R n
    have h₂ := U_sub_two R (-n)
    linear_combination (norm := ring_nf) 2 * (X : R[X]) * ih1 - ih2 + h₁ + h₂
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (-0) 1)) (-U R (HSub.hSub (α := ℤ) 0 1))
one : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (-1) 1)) (-U R (HSub.hSub (α := ℤ) 1 1))
⊢ Eq (α := R[X]) (U R (-n - 1)) (-U R (n - 1))
have add_two : ∀ (n : ℕ) (ih1 : Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)) (-U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)))
  (ih2 : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (-U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))),
  Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1)) (-U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1))
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    have h₁ := U_add_one R n
    have h₂ := U_sub_two R (-n - 1)
    linear_combination (norm := ring_nf) 2 * (X : R[X]) * ih1 - ih2 + h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := U_eq R n
    have h₂ := U_sub_two R (-n)
    linear_combination (norm := ring_nf) 2 * (X : R[X]) * ih1 - ih2 + h₁ + h₂
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (-0) 1)) (-U R (HSub.hSub (α := ℤ) 0 1))
one : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (-1) 1)) (-U R (HSub.hSub (α := ℤ) 1 1))
add_two :
  ∀ (n : ℕ) (ih1 : Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)) (-U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)))
    (ih2 : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (-U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))),
    Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1)) (-U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1))
⊢ Eq (α := R[X]) (U R (-n - 1)) (-U R (n - 1))
have neg_add_one : ∀ (n : ℕ) (ih1 : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (- -(↑n : ℤ)) 1)) (-U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)))
  (ih2 : Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1))),
  Eq (α := R[X]) (U R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-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₁ := U_add_one R n
    have h₂ := U_sub_two R (-n - 1)
    linear_combination (norm := ring_nf) 2 * (X : R[X]) * ih1 - ih2 + h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := U_eq R n
    have h₂ := U_sub_two R (-n)
    linear_combination (norm := ring_nf) 2 * (X : R[X]) * ih1 - ih2 + h₁ + h₂
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ eval 1 (U R 1) = HAdd.hAdd (α := R) (↑1 : R) 1
have one : 2 = HAdd.hAdd (α := R) 1 1
Tactic: simp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval 1 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R) 1
ih2 : eval 1 (U R (↑n : ℤ)) = HAdd.hAdd (α := R) (↑(↑n : ℤ) : R) 1
⊢ eval 1 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : R) 1
have add_two : 2 * (HAdd.hAdd (α := R) (↑n : R) 1 + 1) - HAdd.hAdd (α := R) (↑n : R) 1 = HAdd.hAdd (α := R) (↑n : R) 2 + 1
Tactic: simp only [U_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one, ih1,
      Int.cast_add, Int.cast_natCast, Int.cast_one, ih2, Int.cast_ofNat]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval 1 (U R (-(↑n : ℤ))) = HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1
ih2 : eval 1 (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R) 1
⊢ eval 1 (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = HAdd.hAdd (α := R) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : R) 1
have neg_add_one : 2 * HAdd.hAdd (α := R) (-(↑n : R)) 1 - (HAdd.hAdd (α := R) (-(↑n : R)) 1 + 1) = -(↑n : R)
Tactic: simp only [U_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one,
      ih1, Int.cast_neg, Int.cast_natCast, ih2, Int.cast_add, Int.cast_one, Int.cast_sub,
      sub_add_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ eval 1 (U R n) = HAdd.hAdd (α := R) (↑n : R) 1
have zero : eval 1 (U R 0) = HAdd.hAdd (α := R) (↑0 : R) 1
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp; norm_num
  | add_two n ih1 ih2 =>
    simp only [U_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one, ih1,
      Int.cast_add, Int.cast_natCast, Int.cast_one, ih2, Int.cast_ofNat]
    ring
  | neg_add_one n ih1 ih2 =>
    simp only [U_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one,
      ih1, Int.cast_neg, Int.cast_natCast, ih2, Int.cast_add, Int.cast_one, Int.cast_sub,
      sub_add_cancel]
    ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : eval 1 (U R 0) = HAdd.hAdd (α := R) (↑0 : R) 1
⊢ eval 1 (U R n) = HAdd.hAdd (α := R) (↑n : R) 1
have one : eval 1 (U R 1) = HAdd.hAdd (α := R) (↑1 : R) 1
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp; norm_num
  | add_two n ih1 ih2 =>
    simp only [U_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one, ih1,
      Int.cast_add, Int.cast_natCast, Int.cast_one, ih2, Int.cast_ofNat]
    ring
  | neg_add_one n ih1 ih2 =>
    simp only [U_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one,
      ih1, Int.cast_neg, Int.cast_natCast, ih2, Int.cast_add, Int.cast_one, Int.cast_sub,
      sub_add_cancel]
    ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : eval 1 (U R 0) = HAdd.hAdd (α := R) (↑0 : R) 1
one : eval 1 (U R 1) = HAdd.hAdd (α := R) (↑1 : R) 1
⊢ eval 1 (U R n) = HAdd.hAdd (α := R) (↑n : R) 1
have add_two : ∀ (n : ℕ)
  (ih1 : eval 1 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R) 1)
  (ih2 : eval 1 (U R (↑n : ℤ)) = HAdd.hAdd (α := R) (↑(↑n : ℤ) : R) 1),
  eval 1 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : R) 1
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp; norm_num
  | add_two n ih1 ih2 =>
    simp only [U_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one, ih1,
      Int.cast_add, Int.cast_natCast, Int.cast_one, ih2, Int.cast_ofNat]
    ring
  | neg_add_one n ih1 ih2 =>
    simp only [U_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one,
      ih1, Int.cast_neg, Int.cast_natCast, ih2, Int.cast_add, Int.cast_one, Int.cast_sub,
      sub_add_cancel]
    ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : eval 1 (U R 0) = HAdd.hAdd (α := R) (↑0 : R) 1
one : eval 1 (U R 1) = HAdd.hAdd (α := R) (↑1 : R) 1
add_two :
  ∀ (n : ℕ)
    (ih1 : eval 1 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R) 1)
    (ih2 : eval 1 (U R (↑n : ℤ)) = HAdd.hAdd (α := R) (↑(↑n : ℤ) : R) 1),
    eval 1 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : R) 1
⊢ eval 1 (U R n) = HAdd.hAdd (α := R) (↑n : R) 1
have neg_add_one : ∀ (n : ℕ) (ih1 : eval 1 (U R (-(↑n : ℤ))) = HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1)
  (ih2 :
    eval 1 (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R) 1),
  eval 1 (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = HAdd.hAdd (α := R) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : R) 1
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp; norm_num
  | add_two n ih1 ih2 =>
    simp only [U_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one, ih1,
      Int.cast_add, Int.cast_natCast, Int.cast_one, ih2, Int.cast_ofNat]
    ring
  | neg_add_one n ih1 ih2 =>
    simp only [U_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one,
      ih1, Int.cast_neg, Int.cast_natCast, ih2, Int.cast_add, Int.cast_one, Int.cast_sub,
      sub_add_cancel]
    ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ eval (-1) (U R 1) = (↑(↑(Int.negOnePow 1) : ℤ) : R) * HAdd.hAdd (α := R) (↑1 : R) 1
have one : -2 = HAdd.hAdd (α := R) (-1) (-1)
Tactic: simp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  eval (-1) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R) 1
ih2 : eval (-1) (U R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * HAdd.hAdd (α := R) (↑(↑n : ℤ) : R) 1
⊢ eval (-1) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : R) 1
have add_two : -(2 * ((↑(↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) : R) * (HAdd.hAdd (α := R) (↑n : R) 1 + 1))) -
    (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * HAdd.hAdd (α := R) (↑n : R) 1 =
  (↑(↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℤ) (-1) 2) : ℤ) : R) * (HAdd.hAdd (α := R) (↑n : R) 2 + 1)
Tactic: simp only [U_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
      Int.cast_add, Int.cast_natCast, Int.cast_one, neg_mul, ih2, Int.cast_ofNat, Int.negOnePow_add,
      Int.negOnePow_def 2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  eval (-1) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R) 1
ih2 : eval (-1) (U R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * HAdd.hAdd (α := R) (↑(↑n : ℤ) : R) 1
⊢ -(2 * ((↑(↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) : R) * (HAdd.hAdd (α := R) (↑n : R) 1 + 1))) -
      (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * HAdd.hAdd (α := R) (↑n : R) 1 =
    (↑(↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℤ) (-1) 2) : ℤ) : R) * (HAdd.hAdd (α := R) (↑n : R) 2 + 1)
have add_two : -HMul.hMul (α := R) 2 (↑((↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) * (↑(n + 1 + 1) : ℤ)) : R) -
    (↑((↑(Int.negOnePow (↑n : ℤ)) : ℤ) * (↑(n + 1) : ℤ)) : R) =
  (↑((↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 2) : ℤ) * (↑(n + 2 + 1) : ℤ)) : R)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  eval (-1) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R) 1
ih2 : eval (-1) (U R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * HAdd.hAdd (α := R) (↑(↑n : ℤ) : R) 1
⊢ -HMul.hMul (α := R) 2 (↑((↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) * (↑(n + 1 + 1) : ℤ)) : R) -
      (↑((↑(Int.negOnePow (↑n : ℤ)) : ℤ) * (↑(n + 1) : ℤ)) : R) =
    (↑((↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 2) : ℤ) * (↑(n + 2 + 1) : ℤ)) : R)
have add_two : 2 * (HPow.hPow (α := R) (-1) n * (HAdd.hAdd (α := R) (↑n : R) 1 + 1)) -
    HPow.hPow (α := R) (-1) n * HAdd.hAdd (α := R) (↑n : R) 1 =
  HPow.hPow (α := R) (-1) n * (HAdd.hAdd (α := R) (↑n : R) 2 + 1)
Tactic: norm_num
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval (-1) (U R (-(↑n : ℤ))) = (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) * HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1
ih2 :
  eval (-1) (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R) 1
⊢ eval (-1) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : R) 1
have neg_add_one : -(2 * ((↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * HAdd.hAdd (α := R) (-(↑n : R)) 1)) -
    (↑(↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) : R) * (HAdd.hAdd (α := R) (-(↑n : R)) 1 + 1) =
  -HMul.hMul (α := R) (↑(↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) : R) (↑n : R)
Tactic: simp only [U_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
      Int.cast_neg, Int.cast_natCast, Int.negOnePow_neg, neg_mul, ih2, Int.cast_add, Int.cast_one,
      Int.cast_sub, sub_add_cancel, Int.negOnePow_sub, Int.negOnePow_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval (-1) (U R (-(↑n : ℤ))) = (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) * HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1
ih2 :
  eval (-1) (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R) 1
⊢ -(2 * ((↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * HAdd.hAdd (α := R) (-(↑n : R)) 1)) -
      (↑(↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) : R) * (HAdd.hAdd (α := R) (-(↑n : R)) 1 + 1) =
    -HMul.hMul (α := R) (↑(↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) : R) (↑n : R)
have neg_add_one : -(2 * ((↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * HAdd.hAdd (α := R) (-(↑n : R)) 1)) -
    (↑(↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) : R) * (HAdd.hAdd (α := R) (-(↑n : R)) 1 + 1) =
  (↑(-((↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) * (↑n : ℤ))) : R)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval (-1) (U R (-(↑n : ℤ))) = (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) * HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1
ih2 :
  eval (-1) (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R) 1
⊢ -(2 * ((↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * HAdd.hAdd (α := R) (-(↑n : R)) 1)) -
      (↑(↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) : R) * (HAdd.hAdd (α := R) (-(↑n : R)) 1 + 1) =
    (↑(-((↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) * (↑n : ℤ))) : R)
have neg_add_one : -(2 * (HPow.hPow (α := R) (-1) n * HAdd.hAdd (α := R) (-(↑n : R)) 1)) +
    HPow.hPow (α := R) (-1) n * (HAdd.hAdd (α := R) (-(↑n : R)) 1 + 1) =
  HPow.hPow (α := R) (-1) n * (↑n : R)
Tactic: norm_num
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ eval (-1) (U R n) = (↑(↑n.negOnePow : ℤ) : R) * HAdd.hAdd (α := R) (↑n : R) 1
have zero : eval (-1) (U R 0) = (↑(↑(Int.negOnePow 0) : ℤ) : R) * HAdd.hAdd (α := R) (↑0 : R) 1
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp; norm_num
  | add_two n ih1 ih2 =>
    simp only [U_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
      Int.cast_add, Int.cast_natCast, Int.cast_one, neg_mul, ih2, Int.cast_ofNat, Int.negOnePow_add,
      Int.negOnePow_def 2]
    norm_cast
    norm_num
    ring
  | neg_add_one n ih1 ih2 =>
    simp only [U_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
      Int.cast_neg, Int.cast_natCast, Int.negOnePow_neg, neg_mul, ih2, Int.cast_add, Int.cast_one,
      Int.cast_sub, sub_add_cancel, Int.negOnePow_sub, Int.negOnePow_add]
    norm_cast
    norm_num
    ring
Cleared hypotheses: n