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 (T R 0) = 1
one : eval 1 (T R 1) = 1
⊢ eval 1 (T R n) = 1
have add_two : ∀ (n : ℕ) (ih1 : eval 1 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = 1) (ih2 : eval 1 (T R (↑n : ℤ)) = 1),
  eval 1 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = 1
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 => simp [T_add_two, ih1, ih2]; norm_num
  | neg_add_one n ih1 ih2 => simp [T_sub_one, -T_neg, ih1, ih2]; norm_num
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 (T R 0) = 1
one : eval 1 (T R 1) = 1
add_two :
  ∀ (n : ℕ) (ih1 : eval 1 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = 1) (ih2 : eval 1 (T R (↑n : ℤ)) = 1),
    eval 1 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = 1
⊢ eval 1 (T R n) = 1
have neg_add_one : ∀ (n : ℕ) (ih1 : eval 1 (T R (-(↑n : ℤ))) = 1) (ih2 : eval 1 (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = 1),
  eval 1 (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = 1
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 => simp [T_add_two, ih1, ih2]; norm_num
  | neg_add_one n ih1 ih2 => simp [T_sub_one, -T_neg, ih1, ih2]; norm_num
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval (-1) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R)
ih2 : eval (-1) (T R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R)
⊢ eval (-1) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R)
have add_two : HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) - (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) =
  (↑(↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℤ) (-1) 2) : ℤ) : R)
Tactic: simp only [T_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
      Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, neg_mul, neg_neg, ih2,
      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) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R)
ih2 : eval (-1) (T R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R)
⊢ HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) - (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) =
    (↑(↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℤ) (-1) 2) : ℤ) : R)
have add_two : HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) - (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) =
  (↑(↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 2) : ℤ) : 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) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R)
ih2 : eval (-1) (T R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R)
⊢ HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) - (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) =
    (↑(↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 2) : ℤ) : R)
have add_two : 2 * HPow.hPow (α := R) (-1) n - HPow.hPow (α := R) (-1) n = HPow.hPow (α := R) (-1) n
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) (T R (-(↑n : ℤ))) = (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R)
ih2 : eval (-1) (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = (↑(↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R)
⊢ eval (-1) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = (↑(↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R)
have neg_add_one : -HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) + (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) =
  -(↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R)
Tactic: simp only [T_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1, neg_mul,
      ih2, Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, sub_neg_eq_add,
      Int.negOnePow_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ eval (-1) (T R n) = (↑(↑n.negOnePow : ℤ) : R)
have zero : eval (-1) (T R 0) = (↑(↑(Int.negOnePow 0) : ℤ) : R)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp only [T_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
      Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, neg_mul, neg_neg, ih2,
      Int.negOnePow_def 2]
    norm_cast
    norm_num
    ring
  | neg_add_one n ih1 ih2 =>
    simp only [T_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1, neg_mul,
      ih2, Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, sub_neg_eq_add,
      Int.negOnePow_sub]
    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) (T R 0) = (↑(↑(Int.negOnePow 0) : ℤ) : R)
⊢ eval (-1) (T R n) = (↑(↑n.negOnePow : ℤ) : R)
have one : eval (-1) (T R 1) = (↑(↑(Int.negOnePow 1) : ℤ) : R)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp only [T_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
      Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, neg_mul, neg_neg, ih2,
      Int.negOnePow_def 2]
    norm_cast
    norm_num
    ring
  | neg_add_one n ih1 ih2 =>
    simp only [T_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1, neg_mul,
      ih2, Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, sub_neg_eq_add,
      Int.negOnePow_sub]
    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) (T R 0) = (↑(↑(Int.negOnePow 0) : ℤ) : R)
one : eval (-1) (T R 1) = (↑(↑(Int.negOnePow 1) : ℤ) : R)
⊢ eval (-1) (T R n) = (↑(↑n.negOnePow : ℤ) : R)
have add_two : ∀ (n : ℕ)
  (ih1 : eval (-1) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R))
  (ih2 : eval (-1) (T R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R)),
  eval (-1) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp only [T_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
      Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, neg_mul, neg_neg, ih2,
      Int.negOnePow_def 2]
    norm_cast
    norm_num
    ring
  | neg_add_one n ih1 ih2 =>
    simp only [T_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1, neg_mul,
      ih2, Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, sub_neg_eq_add,
      Int.negOnePow_sub]
    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) (T R 0) = (↑(↑(Int.negOnePow 0) : ℤ) : R)
one : eval (-1) (T R 1) = (↑(↑(Int.negOnePow 1) : ℤ) : R)
add_two :
  ∀ (n : ℕ)
    (ih1 : eval (-1) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R))
    (ih2 : eval (-1) (T R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R)),
    eval (-1) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R)
⊢ eval (-1) (T R n) = (↑(↑n.negOnePow : ℤ) : R)
have neg_add_one : ∀ (n : ℕ) (ih1 : eval (-1) (T R (-(↑n : ℤ))) = (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R))
  (ih2 :
    eval (-1) (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = (↑(↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R)),
  eval (-1) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = (↑(↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R)
Tactic: induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp only [T_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
      Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, neg_mul, neg_neg, ih2,
      Int.negOnePow_def 2]
    norm_cast
    norm_num
    ring
  | neg_add_one n ih1 ih2 =>
    simp only [T_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1, neg_mul,
      ih2, Int.negOnePow_add, Int.negOnePow_one, Units.val_neg, Int.cast_neg, sub_neg_eq_add,
      Int.negOnePow_sub]
    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 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 / 2).negOnePow : ℤ) else 0) : R)
ih2 :
  eval 0 (T R (↑n : ℤ)) =
    (↑(if Even (α := ℤ) (↑n : ℤ) then (↑(HDiv.hDiv (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) else 0) : R)
⊢ eval 0 (T 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 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 / 2).negOnePow : ℤ) else 0) : R)
ih2 :
  eval 0 (T 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 (T 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 (T 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 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 / 2).negOnePow : ℤ) else 0) : R)
ih2 :
  eval 0 (T 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 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
      (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 / 2).negOnePow : ℤ) else 0) : R)
⊢ eval 0 (T 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 (T 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 (T R (-(↑n : ℤ))) =
    (↑(if Even (α := ℤ) (-(↑n : ℤ)) then (↑(HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) 2).negOnePow : ℤ) else 0) : R)
ih2 :
  eval 0 (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(if Even (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) then (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 / 2).negOnePow : ℤ) else 0) :
      R)
⊢ eval 0 (T 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 (T R (-(↑n : ℤ))) =
    (↑(if Even (α := ℤ) (-(↑n : ℤ)) then (↑(HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) 2).negOnePow : ℤ) else 0) : R)
ih2 :
  eval 0 (T 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 (T 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 (T 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 (T R (-(↑n : ℤ))) =
    (↑(if Even (α := ℤ) (-(↑n : ℤ)) then (↑(HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) 2).negOnePow : ℤ) else 0) : R)
ih2 :
  eval 0 (T 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 (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
      (↑(if Even (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) then (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 / 2).negOnePow : ℤ)
          else 0) :
        R)
⊢ eval 0 (T 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 (T 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 (T R n) = (↑(if Even n then (↑(n / 2).negOnePow : ℤ) else 0) : R)
have zero : eval 0 (T 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 [T_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 (T R 0) = (↑(if Even (α := ℤ) 0 then (↑(0 / 2).negOnePow : ℤ) else 0) : R)
⊢ eval 0 (T R n) = (↑(if Even n then (↑(n / 2).negOnePow : ℤ) else 0) : R)
have one : eval 0 (T 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 [T_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 (T R 0) = (↑(if Even (α := ℤ) 0 then (↑(0 / 2).negOnePow : ℤ) else 0) : R)
one : eval 0 (T R 1) = (↑(if Even (α := ℤ) 1 then (↑(1 / 2).negOnePow : ℤ) else 0) : R)
⊢ eval 0 (T R n) = (↑(if Even n then (↑(n / 2).negOnePow : ℤ) else 0) : R)
have add_two : ∀ (n : ℕ)
  (ih1 :
    eval 0 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
      (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 / 2).negOnePow : ℤ) else 0) : R))
  (ih2 :
    eval 0 (T R (↑n : ℤ)) =
      (↑(if Even (α := ℤ) (↑n : ℤ) then (↑(HDiv.hDiv (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) else 0) : R)),
  eval 0 (T 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 [T_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 (T R 0) = (↑(if Even (α := ℤ) 0 then (↑(0 / 2).negOnePow : ℤ) else 0) : R)
one : eval 0 (T R 1) = (↑(if Even (α := ℤ) 1 then (↑(1 / 2).negOnePow : ℤ) else 0) : R)
add_two :
  ∀ (n : ℕ)
    (ih1 :
      eval 0 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
        (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 / 2).negOnePow : ℤ) else 0) :
          R))
    (ih2 :
      eval 0 (T R (↑n : ℤ)) =
        (↑(if Even (α := ℤ) (↑n : ℤ) then (↑(HDiv.hDiv (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) else 0) : R)),
    eval 0 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
      (↑(if Even (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) then (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 / 2).negOnePow : ℤ) else 0) : R)
⊢ eval 0 (T R n) = (↑(if Even n then (↑(n / 2).negOnePow : ℤ) else 0) : R)
have neg_add_one : ∀ (n : ℕ)
  (ih1 :
    eval 0 (T R (-(↑n : ℤ))) =
      (↑(if Even (α := ℤ) (-(↑n : ℤ)) then (↑(HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) 2).negOnePow : ℤ) else 0) : R))
  (ih2 :
    eval 0 (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
      (↑(if Even (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) then (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 / 2).negOnePow : ℤ)
          else 0) :
        R)),
  eval 0 (T 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 [T_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
n : ℕ
ih1 : degree (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ)
ih2 : degree (T R (↑n : ℤ)) = (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
⊢ (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)
have rw : HAdd.hAdd (α := WithBot ℕ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ) 1 = (↑(n + 2) : WithBot ℕ)
Tactic: rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X, ih1]
-- 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 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ)
ih2 : degree (T R (↑n : ℤ)) = (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
⊢ HAdd.hAdd (α := WithBot ℕ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ) 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 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ)
ih2 : degree (T R (↑n : ℤ)) = (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
⊢ degree (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs : WithBot ℕ)
have this : (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)
Tactic: have : (2 * X * T R (n + 1)).degree = ↑(n + 2) := by
      rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X, ih1]
      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 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ)
ih2 : degree (T R (↑n : ℤ)) = (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
this : (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)
⊢ degree (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs : WithBot ℕ)
have add_two : (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree =
  (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs : WithBot ℕ)
Tactic: rw [T_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 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ)
ih2 : degree (T R (↑n : ℤ)) = (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
this : (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)
add_two :
  (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree =
    (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs : WithBot ℕ)
⊢ degree (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs : WithBot ℕ)
have add_two₁ : degree (T R (↑n : ℤ)) < (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree
Tactic: rw [T_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 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ)
ih2 : degree (T R (↑n : ℤ)) = (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
this : (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)
⊢ (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree =
    (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs : WithBot ℕ)
have add_two : Eq (α := WithBot ℕ) (↑(n + 2) : WithBot ℕ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs : WithBot ℕ)
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 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).natAbs : WithBot ℕ)
ih2 : degree (T R (↑n : ℤ)) = (↑(Int.natAbs (↑n : ℤ)) : WithBot ℕ)
this : (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)
⊢ Eq (α := WithBot ℕ) (↑(n + 2) : WithBot ℕ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).natAbs : WithBot ℕ)
have add_two : n + 2 = n + 2
Tactic: norm_cast