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 (-1) (U R 0) = (↑(↑(Int.negOnePow 0) : ℤ) : R) * HAdd.hAdd (α := R) (↑0 : R) 1
⊢ eval (-1) (U R n) = (↑(↑n.negOnePow : ℤ) : R) * HAdd.hAdd (α := R) (↑n : R) 1
have one : eval (-1) (U 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 [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
-- 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) = (↑(↑(Int.negOnePow 0) : ℤ) : R) * HAdd.hAdd (α := R) (↑0 : R) 1
one : eval (-1) (U R 1) = (↑(↑(Int.negOnePow 1) : ℤ) : R) * HAdd.hAdd (α := R) (↑1 : R) 1
⊢ eval (-1) (U R n) = (↑(↑n.negOnePow : ℤ) : R) * HAdd.hAdd (α := R) (↑n : R) 1
have add_two : ∀ (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
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
-- 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) = (↑(↑(Int.negOnePow 0) : ℤ) : R) * HAdd.hAdd (α := R) (↑0 : R) 1
one : eval (-1) (U R 1) = (↑(↑(Int.negOnePow 1) : ℤ) : R) * HAdd.hAdd (α := R) (↑1 : R) 1
add_two :
  ∀ (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
⊢ eval (-1) (U R n) = (↑(↑n.negOnePow : ℤ) : R) * HAdd.hAdd (α := R) (↑n : R) 1
have neg_add_one : ∀ (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
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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  eval 0 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 / 2).negOnePow : ℤ) else 0) : R)
ih2 :
  eval 0 (U R (↑n : ℤ)) =
    (↑(if Even (α := ℤ) (↑n : ℤ) then (↑(HDiv.hDiv (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) else 0) : R)
⊢ eval 0 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 / 2).negOnePow : ℤ) else 0) : R)
have this : HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 / 2 = HDiv.hDiv (α := ℤ) (↑n : ℤ) 2 + 1
Tactic: have : ((n : ℤ) + 2) / 2 = (n : ℤ) / 2 + 1 := by lia
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  eval 0 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 / 2).negOnePow : ℤ) else 0) : R)
ih2 :
  eval 0 (U R (↑n : ℤ)) =
    (↑(if Even (α := ℤ) (↑n : ℤ) then (↑(HDiv.hDiv (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) else 0) : R)
this : HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 / 2 = HDiv.hDiv (α := ℤ) (↑n : ℤ) 2 + 1
⊢ eval 0 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 / 2).negOnePow : ℤ) else 0) : R)
have pos : Even n →
  eval 0 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 / 2).negOnePow : ℤ) else 0) : R)
Tactic: by_cases Even n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  eval 0 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 / 2).negOnePow : ℤ) else 0) : R)
ih2 :
  eval 0 (U R (↑n : ℤ)) =
    (↑(if Even (α := ℤ) (↑n : ℤ) then (↑(HDiv.hDiv (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) else 0) : R)
this : HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 / 2 = HDiv.hDiv (α := ℤ) (↑n : ℤ) 2 + 1
pos :
  Even n →
    eval 0 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
      (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 / 2).negOnePow : ℤ) else 0) : R)
⊢ eval 0 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 / 2).negOnePow : ℤ) else 0) : R)
have neg : ¬Even n →
  eval 0 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 / 2).negOnePow : ℤ) else 0) : R)
Tactic: by_cases Even n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  eval 0 (U R (-(↑n : ℤ))) =
    (↑(if Even (α := ℤ) (-(↑n : ℤ)) then (↑(HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) 2).negOnePow : ℤ) else 0) : R)
ih2 :
  eval 0 (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(if Even (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) then (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 / 2).negOnePow : ℤ) else 0) :
      R)
⊢ eval 0 (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(if Even (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) then (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 / 2).negOnePow : ℤ) else 0) :
      R)
have this : HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 / 2 = HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 / 2 + 1
Tactic: have : (-(n : ℤ) + 1) / 2 = (-(n : ℤ) - 1) / 2 + 1 := by lia
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  eval 0 (U R (-(↑n : ℤ))) =
    (↑(if Even (α := ℤ) (-(↑n : ℤ)) then (↑(HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) 2).negOnePow : ℤ) else 0) : R)
ih2 :
  eval 0 (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(if Even (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) then (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 / 2).negOnePow : ℤ) else 0) :
      R)
this : HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 / 2 = HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 / 2 + 1
⊢ eval 0 (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(if Even (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) then (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 / 2).negOnePow : ℤ) else 0) :
      R)
have pos : Even n →
  eval 0 (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(if Even (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) then (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 / 2).negOnePow : ℤ) else 0) :
      R)
Tactic: by_cases Even n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  eval 0 (U R (-(↑n : ℤ))) =
    (↑(if Even (α := ℤ) (-(↑n : ℤ)) then (↑(HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) 2).negOnePow : ℤ) else 0) : R)
ih2 :
  eval 0 (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(if Even (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) then (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 / 2).negOnePow : ℤ) else 0) :
      R)
this : HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 / 2 = HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 / 2 + 1
pos :
  Even n →
    eval 0 (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
      (↑(if Even (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) then (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 / 2).negOnePow : ℤ)
          else 0) :
        R)
⊢ eval 0 (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(if Even (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) then (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 / 2).negOnePow : ℤ) else 0) :
      R)
have neg : ¬Even n →
  eval 0 (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(if Even (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) then (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 / 2).negOnePow : ℤ) else 0) :
      R)
Tactic: by_cases Even n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ eval 0 (U R n) = (↑(if Even n then (↑(n / 2).negOnePow : ℤ) else 0) : R)
have zero : eval 0 (U R 0) = (↑(if Even (α := ℤ) 0 then (↑(0 / 2).negOnePow : ℤ) else 0) : R)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    have : ((n : ℤ) + 2) / 2 = (n : ℤ) / 2 + 1 := by lia
    by_cases Even n <;> simp_all [Int.negOnePow_add]
  | neg_add_one n ih1 ih2 =>
    have : (-(n : ℤ) + 1) / 2 = (-(n : ℤ) - 1) / 2 + 1 := by lia
    by_cases Even n <;> simp_all [U_sub_one, ← Int.not_even_iff_odd, Int.negOnePow_add]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : eval 0 (U R 0) = (↑(if Even (α := ℤ) 0 then (↑(0 / 2).negOnePow : ℤ) else 0) : R)
⊢ eval 0 (U R n) = (↑(if Even n then (↑(n / 2).negOnePow : ℤ) else 0) : R)
have one : eval 0 (U R 1) = (↑(if Even (α := ℤ) 1 then (↑(1 / 2).negOnePow : ℤ) else 0) : R)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    have : ((n : ℤ) + 2) / 2 = (n : ℤ) / 2 + 1 := by lia
    by_cases Even n <;> simp_all [Int.negOnePow_add]
  | neg_add_one n ih1 ih2 =>
    have : (-(n : ℤ) + 1) / 2 = (-(n : ℤ) - 1) / 2 + 1 := by lia
    by_cases Even n <;> simp_all [U_sub_one, ← Int.not_even_iff_odd, Int.negOnePow_add]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : eval 0 (U R 0) = (↑(if Even (α := ℤ) 0 then (↑(0 / 2).negOnePow : ℤ) else 0) : R)
one : eval 0 (U R 1) = (↑(if Even (α := ℤ) 1 then (↑(1 / 2).negOnePow : ℤ) else 0) : R)
⊢ eval 0 (U R n) = (↑(if Even n then (↑(n / 2).negOnePow : ℤ) else 0) : R)
have add_two : ∀ (n : ℕ)
  (ih1 :
    eval 0 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
      (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 / 2).negOnePow : ℤ) else 0) : R))
  (ih2 :
    eval 0 (U R (↑n : ℤ)) =
      (↑(if Even (α := ℤ) (↑n : ℤ) then (↑(HDiv.hDiv (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) else 0) : R)),
  eval 0 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 / 2).negOnePow : ℤ) else 0) : R)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    have : ((n : ℤ) + 2) / 2 = (n : ℤ) / 2 + 1 := by lia
    by_cases Even n <;> simp_all [Int.negOnePow_add]
  | neg_add_one n ih1 ih2 =>
    have : (-(n : ℤ) + 1) / 2 = (-(n : ℤ) - 1) / 2 + 1 := by lia
    by_cases Even n <;> simp_all [U_sub_one, ← Int.not_even_iff_odd, Int.negOnePow_add]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : eval 0 (U R 0) = (↑(if Even (α := ℤ) 0 then (↑(0 / 2).negOnePow : ℤ) else 0) : R)
one : eval 0 (U R 1) = (↑(if Even (α := ℤ) 1 then (↑(1 / 2).negOnePow : ℤ) else 0) : R)
add_two :
  ∀ (n : ℕ)
    (ih1 :
      eval 0 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
        (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 / 2).negOnePow : ℤ) else 0) :
          R))
    (ih2 :
      eval 0 (U R (↑n : ℤ)) =
        (↑(if Even (α := ℤ) (↑n : ℤ) then (↑(HDiv.hDiv (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) else 0) : R)),
    eval 0 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
      (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 / 2).negOnePow : ℤ) else 0) : R)
⊢ eval 0 (U R n) = (↑(if Even n then (↑(n / 2).negOnePow : ℤ) else 0) : R)
have neg_add_one : ∀ (n : ℕ)
  (ih1 :
    eval 0 (U R (-(↑n : ℤ))) =
      (↑(if Even (α := ℤ) (-(↑n : ℤ)) then (↑(HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) 2).negOnePow : ℤ) else 0) : R))
  (ih2 :
    eval 0 (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
      (↑(if Even (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) then (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 / 2).negOnePow : ℤ)
          else 0) :
        R)),
  eval 0 (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(if Even (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) then (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 / 2).negOnePow : ℤ) else 0) :
      R)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    have : ((n : ℤ) + 2) / 2 = (n : ℤ) / 2 + 1 := by lia
    by_cases Even n <;> simp_all [Int.negOnePow_add]
  | neg_add_one n ih1 ih2 =>
    have : (-(n : ℤ) + 1) / 2 = (-(n : ℤ) - 1) / 2 + 1 := by lia
    by_cases Even n <;> simp_all [U_sub_one, ← Int.not_even_iff_odd, Int.negOnePow_add]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
⊢ degree (U R 1) = 1
have one : (HMul.hMul (α := R[X]) 2 X).degree = 1
Tactic: rw [U_one, ← C_ofNat, degree_C_mul_X two_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
one : (HMul.hMul (α := R[X]) 2 X).degree = 1
⊢ degree (U R 1) = 1
have one₁ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X).degree = 1
Tactic: rw [U_one, ← C_ofNat, degree_C_mul_X two_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
one : (HMul.hMul (α := R[X]) 2 X).degree = 1
one₁ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X).degree = 1
⊢ degree (U R 1) = 1
have one₂ : Eq (α := WithBot ℕ) 1 1
Tactic: rw [U_one, ← C_ofNat, degree_C_mul_X two_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 : degree (U R (↑n : ℤ)) = (↑n : WithBot ℕ)
ih2 : degree (U R (↑(n + 1) : ℤ)) = (↑(n + 1) : WithBot ℕ)
⊢ degree (U R (↑(n + 2) : ℤ)) = (↑(n + 2) : WithBot ℕ)
have more : degree (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 2
Tactic: push_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 : degree (U R (↑n : ℤ)) = (↑n : WithBot ℕ)
ih2 : degree (U R (↑(n + 1) : ℤ)) = (↑(n + 1) : WithBot ℕ)
⊢ degree (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 2
have ih2₁ : degree (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 1
Tactic: push_cast at ih2
Cleared hypotheses: ih2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 : degree (U R (↑n : ℤ)) = (↑n : WithBot ℕ)
ih2 : degree (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 1
⊢ (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)
have rw : HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 1 + 1 = (↑(n + 2) : WithBot ℕ)
Tactic: rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X, ih2]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 : degree (U R (↑n : ℤ)) = (↑n : WithBot ℕ)
ih2 : degree (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 1
⊢ HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 1 + 1 = (↑(n + 2) : WithBot ℕ)
have norm_cast : n + 1 + 1 = n + 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 : degree (U R (↑n : ℤ)) = (↑n : WithBot ℕ)
ih2 : degree (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 1
⊢ degree (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 2
have this : (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)
Tactic: have : (2 * X * U R (n + 1)).degree = ↑(n + 2) := by
      rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X, ih2]
      norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 : degree (U R (↑n : ℤ)) = (↑n : WithBot ℕ)
ih2 : degree (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 1
this : (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)
⊢ degree (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 2
have more : (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 2
Tactic: rw [U_add_two, degree_sub_eq_left_of_degree_lt]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 : degree (U R (↑n : ℤ)) = (↑n : WithBot ℕ)
ih2 : degree (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 1
this : (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)
more :
  (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree =
    HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 2
⊢ degree (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 2
have more₁ : degree (U R (↑n : ℤ)) < (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree
Tactic: rw [U_add_two, degree_sub_eq_left_of_degree_lt]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 : degree (U R (↑n : ℤ)) = (↑n : WithBot ℕ)
ih2 : degree (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 1
this : (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)
⊢ (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree =
    HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 2
have more : (↑(n + 2) : WithBot ℕ) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 2
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 : degree (U R (↑n : ℤ)) = (↑n : WithBot ℕ)
ih2 : degree (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 1
this : (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)
⊢ (↑(n + 2) : WithBot ℕ) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 2
have more : n + 2 = n + 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 : degree (U R (↑n : ℤ)) = (↑n : WithBot ℕ)
ih2 : degree (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 1
this : (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)
⊢ degree (U R (↑n : ℤ)) < (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree
have more : LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ) (↑(n + 2) : WithBot ℕ)
Tactic: rw [ih1, this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
ih1 : degree (U R (↑n : ℤ)) = (↑n : WithBot ℕ)
ih2 : degree (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 1
this : (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)
⊢ LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ) (↑(n + 2) : WithBot ℕ)
have more : n < n + 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
⊢ degree (U R (↑n : ℤ)) = (↑n : WithBot ℕ)
have zero : degree (U R (↑0 : ℤ)) = (↑0 : WithBot ℕ)
Tactic: induction n using Nat.twoStepInduction with
  | zero => simp
  | one =>
    norm_cast
    rw [U_one, ← C_ofNat, degree_C_mul_X two_ne_zero]
  | more n ih1 ih2 =>
    push_cast; push_cast at ih2
    have : (2 * X * U R (n + 1)).degree = ↑(n + 2) := by
      rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X, ih2]
      norm_cast
    rw [U_add_two, degree_sub_eq_left_of_degree_lt]
    · rw [this]; norm_cast
    · rw [ih1, this]; norm_cast; omega
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
n : ℕ
zero : degree (U R (↑0 : ℤ)) = (↑0 : WithBot ℕ)
⊢ degree (U R (↑n : ℤ)) = (↑n : WithBot ℕ)
have one : degree (U R (↑1 : ℤ)) = (↑1 : WithBot ℕ)
Tactic: induction n using Nat.twoStepInduction with
  | zero => simp
  | one =>
    norm_cast
    rw [U_one, ← C_ofNat, degree_C_mul_X two_ne_zero]
  | more n ih1 ih2 =>
    push_cast; push_cast at ih2
    have : (2 * X * U R (n + 1)).degree = ↑(n + 2) := by
      rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X, ih2]
      norm_cast
    rw [U_add_two, degree_sub_eq_left_of_degree_lt]
    · rw [this]; norm_cast
    · rw [ih1, this]; norm_cast; omega
Cleared hypotheses: n