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 : eval (-2) (S R 0) = (↑(↑(Int.negOnePow 0) : ℤ) : R) * HAdd.hAdd (α := R) (↑0 : R) 1
one : eval (-2) (S R 1) = (↑(↑(Int.negOnePow 1) : ℤ) : R) * HAdd.hAdd (α := R) (↑1 : R) 1
⊢ eval (-2) (S R n) = (↑(↑n.negOnePow : ℤ) : R) * HAdd.hAdd (α := R) (↑n : R) 1
have add_two : ∀ (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
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
one : eval (-2) (S R 1) = (↑(↑(Int.negOnePow 1) : ℤ) : R) * HAdd.hAdd (α := R) (↑1 : R) 1
add_two :
  ∀ (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
⊢ eval (-2) (S R n) = (↑(↑n.negOnePow : ℤ) : R) * HAdd.hAdd (α := R) (↑n : R) 1
have neg_add_one : ∀ (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
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 : ℕ
ih1 : comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) = U R (↑n : ℤ)
⊢ comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two : comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) =
  HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
Tactic: simp_rw [U_add_two, S_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) = U R (↑n : ℤ)
add_two :
  comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
⊢ comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₁ : (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)).comp (HMul.hMul (α := R[X]) 2 X) =
  HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
Tactic: simp_rw [U_add_two, S_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) = U R (↑n : ℤ)
add_two :
  comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
add_two₁ :
  (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)).comp (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
⊢ comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₂ : (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))).comp (HMul.hMul (α := R[X]) 2 X) -
    comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) =
  HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
Tactic: simp_rw [U_add_two, S_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) = U R (↑n : ℤ)
add_two :
  comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
add_two₁ :
  (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)).comp (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
add_two₂ :
  (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))).comp (HMul.hMul (α := R[X]) 2 X) -
      comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
⊢ comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₃ : comp X (HMul.hMul (α := R[X]) 2 X) * comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) -
    comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) =
  HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
Tactic: simp_rw [U_add_two, S_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) = U R (↑n : ℤ)
add_two :
  comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
add_two₁ :
  (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)).comp (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
add_two₂ :
  (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))).comp (HMul.hMul (α := R[X]) 2 X) -
      comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
add_two₃ :
  comp X (HMul.hMul (α := R[X]) 2 X) * comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) -
      comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
⊢ comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₄ : HMul.hMul (α := R[X]) 2 X * comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) -
    comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) =
  HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
Tactic: simp_rw [U_add_two, S_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) = U R (↑n : ℤ)
add_two :
  comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
add_two₁ :
  (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)).comp (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
add_two₂ :
  (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))).comp (HMul.hMul (α := R[X]) 2 X) -
      comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
add_two₃ :
  comp X (HMul.hMul (α := R[X]) 2 X) * comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) -
      comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
add_two₄ :
  HMul.hMul (α := R[X]) 2 X * comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) -
      comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
⊢ comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
have add_two₅ : HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) =
  HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
Tactic: simp_rw [U_add_two, S_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : comp (S R (-(↑n : ℤ))) (HMul.hMul (α := R[X]) 2 X) = U R (-(↑n : ℤ))
ih2 : comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ comp (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one : comp (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
  HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [U_sub_one, S_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : comp (S R (-(↑n : ℤ))) (HMul.hMul (α := R[X]) 2 X) = U R (-(↑n : ℤ))
ih2 : comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  comp (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ comp (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₁ : (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)).comp (HMul.hMul (α := R[X]) 2 X) =
  HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [U_sub_one, S_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : comp (S R (-(↑n : ℤ))) (HMul.hMul (α := R[X]) 2 X) = U R (-(↑n : ℤ))
ih2 : comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  comp (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)).comp
      (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ comp (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₂ : (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ)))).comp (HMul.hMul (α := R[X]) 2 X) -
    comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
  HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [U_sub_one, S_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : comp (S R (-(↑n : ℤ))) (HMul.hMul (α := R[X]) 2 X) = U R (-(↑n : ℤ))
ih2 : comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  comp (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)).comp
      (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₂ :
  (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ)))).comp (HMul.hMul (α := R[X]) 2 X) -
      comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ comp (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₃ : comp X (HMul.hMul (α := R[X]) 2 X) * comp (S R (-(↑n : ℤ))) (HMul.hMul (α := R[X]) 2 X) -
    comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
  HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [U_sub_one, S_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : comp (S R (-(↑n : ℤ))) (HMul.hMul (α := R[X]) 2 X) = U R (-(↑n : ℤ))
ih2 : comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  comp (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)).comp
      (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₂ :
  (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ)))).comp (HMul.hMul (α := R[X]) 2 X) -
      comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₃ :
  comp X (HMul.hMul (α := R[X]) 2 X) * comp (S R (-(↑n : ℤ))) (HMul.hMul (α := R[X]) 2 X) -
      comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ comp (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₄ : HMul.hMul (α := R[X]) 2 X * comp (S R (-(↑n : ℤ))) (HMul.hMul (α := R[X]) 2 X) -
    comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
  HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [U_sub_one, S_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : comp (S R (-(↑n : ℤ))) (HMul.hMul (α := R[X]) 2 X) = U R (-(↑n : ℤ))
ih2 : comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  comp (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)).comp
      (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₂ :
  (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ)))).comp (HMul.hMul (α := R[X]) 2 X) -
      comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₃ :
  comp X (HMul.hMul (α := R[X]) 2 X) * comp (S R (-(↑n : ℤ))) (HMul.hMul (α := R[X]) 2 X) -
      comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₄ :
  HMul.hMul (α := R[X]) 2 X * comp (S R (-(↑n : ℤ))) (HMul.hMul (α := R[X]) 2 X) -
      comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ comp (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
have neg_add_one₅ : HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) -
    comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
  HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: simp_rw [U_sub_one, S_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ comp (S R n) (HMul.hMul (α := R[X]) 2 X) = U R n
have zero : comp (S R 0) (HMul.hMul (α := R[X]) 2 X) = U R 0
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 => simp_rw [U_add_two, S_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
  | neg_add_one n ih1 ih2 => simp_rw [U_sub_one, S_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : comp (S R 0) (HMul.hMul (α := R[X]) 2 X) = U R 0
⊢ comp (S R n) (HMul.hMul (α := R[X]) 2 X) = U R n
have one : comp (S R 1) (HMul.hMul (α := R[X]) 2 X) = U R 1
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 => simp_rw [U_add_two, S_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
  | neg_add_one n ih1 ih2 => simp_rw [U_sub_one, S_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : comp (S R 0) (HMul.hMul (α := R[X]) 2 X) = U R 0
one : comp (S R 1) (HMul.hMul (α := R[X]) 2 X) = U R 1
⊢ comp (S R n) (HMul.hMul (α := R[X]) 2 X) = U R n
have add_two : ∀ (n : ℕ)
  (ih1 : comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
  (ih2 : comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) = U R (↑n : ℤ)),
  comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 => simp_rw [U_add_two, S_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
  | neg_add_one n ih1 ih2 => simp_rw [U_sub_one, S_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : comp (S R 0) (HMul.hMul (α := R[X]) 2 X) = U R 0
one : comp (S R 1) (HMul.hMul (α := R[X]) 2 X) = U R 1
add_two :
  ∀ (n : ℕ)
    (ih1 : comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
    (ih2 : comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) = U R (↑n : ℤ)),
    comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
⊢ comp (S R n) (HMul.hMul (α := R[X]) 2 X) = U R n
have neg_add_one : ∀ (n : ℕ) (ih1 : comp (S R (-(↑n : ℤ))) (HMul.hMul (α := R[X]) 2 X) = U R (-(↑n : ℤ)))
  (ih2 :
    comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)),
  comp (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 => simp_rw [U_add_two, S_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
  | neg_add_one n ih1 ih2 => simp_rw [U_sub_one, S_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ HPow.hPow (α := R[X]) (β := ℕ) (S R 0) 2 + HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) 0 1)) 2 -
      HMul.hMul (α := R[X]) X (S R 0) * S R (HAdd.hAdd (α := ℤ) 0 1) =
    1
have zero : 1 + HPow.hPow (α := R[X]) (β := ℕ) X 2 - HMul.hMul (α := R[X]) X X = 1
Tactic: simp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih :
  HPow.hPow (α := R[X]) (β := ℕ) (S R (↑n : ℤ)) 2 +
        HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2 -
      HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) * S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    1
⊢ HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2 +
        HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) 2 -
      HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) * S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) =
    1
have h₁ : S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)
Tactic: have h₁ := S_add_two R n