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 : S R (HAdd.hAdd (α := ℤ) 0 2) = HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) 0 1)) - S R 0
⊢ S R 2 = HPow.hPow (α := R[X]) (β := ℕ) X 2 - 1
have this₁ : S R 2 = HMul.hMul (α := R[X]) X X - 1
Tactic: simp only [zero_add, S_one, S_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]) (S R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)) (-S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 : Eq (α := R[X]) (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (-S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
⊢ Eq (α := R[X]) (S R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1)) (-S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1))
have h₁ : S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) - S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)
Tactic: have h₁ := S_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]) (S R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)) (-S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 : Eq (α := R[X]) (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (-S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
h₁ : S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) - S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)
⊢ Eq (α := R[X]) (S R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1)) (-S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1))
have h₂ : S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 2) =
  HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1)) - S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: have h₂ := S_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]) (S R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)) (-S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 : Eq (α := R[X]) (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (-S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
h₁ : S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) - S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)
h₂ :
  S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 2) =
    HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1)) - S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
⊢ Eq (α := R[X]) (S R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1)) (-S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1))
have a : S R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1) +
      (HMul.hMul (α := R[X]) X (-S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)) + S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) +
          (HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) - S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) +
        (HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1)) -
          S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))) -
    (-S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1) +
      (HMul.hMul (α := R[X]) X (S R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)) + -S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) +
          S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) +
        S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 2))) =
  0
Tactic: linear_combination (norm := ring_nf) (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]) (S R (HSub.hSub (α := ℤ) (- -(↑n : ℤ)) 1)) (-S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
ih2 : Eq (α := R[X]) (S R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1))
⊢ Eq (α := R[X]) (S R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1))
have h₁ : S R (↑n : ℤ) = HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) - S R (HSub.hSub (α := ℤ) (↑n : ℤ) 2)
Tactic: have h₁ := S_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]) (S R (HSub.hSub (α := ℤ) (- -(↑n : ℤ)) 1)) (-S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
ih2 : Eq (α := R[X]) (S R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1))
h₁ : S R (↑n : ℤ) = HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) - S R (HSub.hSub (α := ℤ) (↑n : ℤ) 2)
⊢ Eq (α := R[X]) (S R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1))
have h₂ : S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2) =
  HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) - S R (-(↑n : ℤ))
Tactic: have h₂ := S_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]) (S R (HSub.hSub (α := ℤ) (- -(↑n : ℤ)) 1)) (-S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
ih2 : Eq (α := R[X]) (S R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1))
h₁ : S R (↑n : ℤ) = HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) - S R (HSub.hSub (α := ℤ) (↑n : ℤ) 2)
h₂ :
  S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) - S R (-(↑n : ℤ))
⊢ Eq (α := R[X]) (S R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1))
have a : S R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1) +
      (HMul.hMul (α := R[X]) X (-S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) + S R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1) +
          (HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) - S R (HSub.hSub (α := ℤ) (↑n : ℤ) 2)) +
        (HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) - S R (-(↑n : ℤ)))) -
    (-S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1) +
      (HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (- -(↑n : ℤ)) 1)) +
            -S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1) +
          S R (↑n : ℤ) +
        S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2))) =
  0
Tactic: linear_combination (norm := ring_nf) (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]) (S R (-n - 1)) (-S R (n - 1))
have zero : Eq (α := R[X]) (S R (HSub.hSub (α := ℤ) (-0) 1)) (-S R (HSub.hSub (α := ℤ) 0 1))
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    have h₁ := S_add_one R n
    have h₂ := S_sub_two R (-n - 1)
    linear_combination (norm := ring_nf) (X : R[X]) * ih1 - ih2 + h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := S_eq R n
    have h₂ := S_sub_two R (-n)
    linear_combination (norm := ring_nf) (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]) (S R (HSub.hSub (α := ℤ) (-0) 1)) (-S R (HSub.hSub (α := ℤ) 0 1))
⊢ Eq (α := R[X]) (S R (-n - 1)) (-S R (n - 1))
have one : Eq (α := R[X]) (S R (HSub.hSub (α := ℤ) (-1) 1)) (-S R (HSub.hSub (α := ℤ) 1 1))
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    have h₁ := S_add_one R n
    have h₂ := S_sub_two R (-n - 1)
    linear_combination (norm := ring_nf) (X : R[X]) * ih1 - ih2 + h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := S_eq R n
    have h₂ := S_sub_two R (-n)
    linear_combination (norm := ring_nf) (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]) (S R (HSub.hSub (α := ℤ) (-0) 1)) (-S R (HSub.hSub (α := ℤ) 0 1))
one : Eq (α := R[X]) (S R (HSub.hSub (α := ℤ) (-1) 1)) (-S R (HSub.hSub (α := ℤ) 1 1))
⊢ Eq (α := R[X]) (S R (-n - 1)) (-S R (n - 1))
have add_two : ∀ (n : ℕ) (ih1 : Eq (α := R[X]) (S R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)) (-S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)))
  (ih2 : Eq (α := R[X]) (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (-S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))),
  Eq (α := R[X]) (S R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1)) (-S 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₁ := S_add_one R n
    have h₂ := S_sub_two R (-n - 1)
    linear_combination (norm := ring_nf) (X : R[X]) * ih1 - ih2 + h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := S_eq R n
    have h₂ := S_sub_two R (-n)
    linear_combination (norm := ring_nf) (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]) (S R (HSub.hSub (α := ℤ) (-0) 1)) (-S R (HSub.hSub (α := ℤ) 0 1))
one : Eq (α := R[X]) (S R (HSub.hSub (α := ℤ) (-1) 1)) (-S R (HSub.hSub (α := ℤ) 1 1))
add_two :
  ∀ (n : ℕ) (ih1 : Eq (α := R[X]) (S R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)) (-S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)))
    (ih2 : Eq (α := R[X]) (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (-S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))),
    Eq (α := R[X]) (S R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1)) (-S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1))
⊢ Eq (α := R[X]) (S R (-n - 1)) (-S R (n - 1))
have neg_add_one : ∀ (n : ℕ) (ih1 : Eq (α := R[X]) (S R (HSub.hSub (α := ℤ) (- -(↑n : ℤ)) 1)) (-S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)))
  (ih2 : Eq (α := R[X]) (S R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1))),
  Eq (α := R[X]) (S R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-S 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₁ := S_add_one R n
    have h₂ := S_sub_two R (-n - 1)
    linear_combination (norm := ring_nf) (X : R[X]) * ih1 - ih2 + h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := S_eq R n
    have h₂ := S_sub_two R (-n)
    linear_combination (norm := ring_nf) (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 2 (S 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 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R) 1
ih2 : eval 2 (S R (↑n : ℤ)) = HAdd.hAdd (α := R) (↑(↑n : ℤ) : R) 1
⊢ eval 2 (S 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 [S_add_two, eval_sub, eval_mul, eval_X, 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 2 (S R (-(↑n : ℤ))) = HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1
ih2 : eval 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R) 1
⊢ eval 2 (S 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 [S_sub_one, eval_sub, eval_mul, eval_X,
      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 2 (S R n) = HAdd.hAdd (α := R) (↑n : R) 1
have zero : eval 2 (S 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 [S_add_two, eval_sub, eval_mul, eval_X, ih1,
      Int.cast_add, Int.cast_natCast, Int.cast_one, ih2, Int.cast_ofNat]
    ring
  | neg_add_one n ih1 ih2 =>
    simp only [S_sub_one, eval_sub, eval_mul, eval_X,
      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 2 (S R 0) = HAdd.hAdd (α := R) (↑0 : R) 1
⊢ eval 2 (S R n) = HAdd.hAdd (α := R) (↑n : R) 1
have one : eval 2 (S 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 [S_add_two, eval_sub, eval_mul, eval_X, ih1,
      Int.cast_add, Int.cast_natCast, Int.cast_one, ih2, Int.cast_ofNat]
    ring
  | neg_add_one n ih1 ih2 =>
    simp only [S_sub_one, eval_sub, eval_mul, eval_X,
      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 2 (S R 0) = HAdd.hAdd (α := R) (↑0 : R) 1
one : eval 2 (S R 1) = HAdd.hAdd (α := R) (↑1 : R) 1
⊢ eval 2 (S R n) = HAdd.hAdd (α := R) (↑n : R) 1
have add_two : ∀ (n : ℕ)
  (ih1 : eval 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R) 1)
  (ih2 : eval 2 (S R (↑n : ℤ)) = HAdd.hAdd (α := R) (↑(↑n : ℤ) : R) 1),
  eval 2 (S 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 [S_add_two, eval_sub, eval_mul, eval_X, ih1,
      Int.cast_add, Int.cast_natCast, Int.cast_one, ih2, Int.cast_ofNat]
    ring
  | neg_add_one n ih1 ih2 =>
    simp only [S_sub_one, eval_sub, eval_mul, eval_X,
      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 2 (S R 0) = HAdd.hAdd (α := R) (↑0 : R) 1
one : eval 2 (S R 1) = HAdd.hAdd (α := R) (↑1 : R) 1
add_two :
  ∀ (n : ℕ)
    (ih1 : eval 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R) 1)
    (ih2 : eval 2 (S R (↑n : ℤ)) = HAdd.hAdd (α := R) (↑(↑n : ℤ) : R) 1),
    eval 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : R) 1
⊢ eval 2 (S R n) = HAdd.hAdd (α := R) (↑n : R) 1
have neg_add_one : ∀ (n : ℕ) (ih1 : eval 2 (S R (-(↑n : ℤ))) = HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1)
  (ih2 :
    eval 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R) 1),
  eval 2 (S 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 [S_add_two, eval_sub, eval_mul, eval_X, ih1,
      Int.cast_add, Int.cast_natCast, Int.cast_one, ih2, Int.cast_ofNat]
    ring
  | neg_add_one n ih1 ih2 =>
    simp only [S_sub_one, eval_sub, eval_mul, eval_X,
      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 (-2) (S 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 (-2) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R) 1
ih2 : eval (-2) (S R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * HAdd.hAdd (α := R) (↑(↑n : ℤ) : R) 1
⊢ eval (-2) (S 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 [S_add_two, eval_sub, eval_mul, eval_X, 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 (-2) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R) 1
ih2 : eval (-2) (S 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 : Eq.{u_1 + 1} (α := R)
  (↑(-(2 * ((↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) * (↑(n + 1 + 1) : ℤ))) -
        (↑(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 (-2) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R) 1
ih2 : eval (-2) (S R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * HAdd.hAdd (α := R) (↑(↑n : ℤ) : R) 1
⊢ Eq.{u_1 + 1} (α := R)
    (↑(-(2 * ((↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) * (↑(n + 1 + 1) : ℤ))) -
          (↑(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 (-2) (S R (-(↑n : ℤ))) = (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) * HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1
ih2 :
  eval (-2) (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R) 1
⊢ eval (-2) (S 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 [S_sub_one, eval_sub, eval_mul, eval_X, mul_neg, 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 (-2) (S R (-(↑n : ℤ))) = (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) * HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1
ih2 :
  eval (-2) (S 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 (-2) (S R (-(↑n : ℤ))) = (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) * HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1
ih2 :
  eval (-2) (S 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 (-2) (S R n) = (↑(↑n.negOnePow : ℤ) : R) * HAdd.hAdd (α := R) (↑n : R) 1
have zero : eval (-2) (S 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 [S_add_two, eval_sub, eval_mul, eval_X, 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 [S_sub_one, eval_sub, eval_mul, eval_X, mul_neg, 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : eval (-2) (S R 0) = (↑(↑(Int.negOnePow 0) : ℤ) : R) * HAdd.hAdd (α := R) (↑0 : R) 1
⊢ eval (-2) (S R n) = (↑(↑n.negOnePow : ℤ) : R) * HAdd.hAdd (α := R) (↑n : R) 1
have one : eval (-2) (S R 1) = (↑(↑(Int.negOnePow 1) : ℤ) : R) * 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 [S_add_two, eval_sub, eval_mul, eval_X, 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 [S_sub_one, eval_sub, eval_mul, eval_X, mul_neg, 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