awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval (-1) (U R (-(↑n : ℤ))) = (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) * HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1
ih2 :
  eval (-1) (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R) 1
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)
⊢ eval (-1) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : R) 1

Tactic:
simp only [U_sub_one, eval_sub, eval_mul, eval_ofNat, eval_X, mul_neg, mul_one, ih1,
      Int.cast_neg, Int.cast_natCast, Int.negOnePow_neg, neg_mul, ih2, Int.cast_add, Int.cast_one,
      Int.cast_sub, sub_add_cancel, Int.negOnePow_sub, Int.negOnePow_add]

Premises used: Int.cast_neg, Int.cast_natCast, Int.cast_sub, Polynomial.eval_X, Polynomial.Chebyshev.U_sub_one, Int.negOnePow_add, Int.cast_add, Int.negOnePow_neg, Polynomial.eval_mul, Int.negOnePow_sub, neg_mul, Polynomial.eval_ofNat, mul_one, Polynomial.eval_sub, sub_add_cancel, Int.cast_one, mul_neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval (-1) (U R (-(↑n : ℤ))) = (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) * HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1
ih2 :
  eval (-1) (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R) 1
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)
⊢ -(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:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval (-1) (U R (-(↑n : ℤ))) = (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) * HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1
ih2 :
  eval (-1) (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R) 1
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)
⊢ -(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_num
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval (-1) (U R (-(↑n : ℤ))) = (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) * HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1
ih2 :
  eval (-1) (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R) 1
⊢ -(2 * (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:
ring
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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
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
⊢ eval (-1) (U R n) = (↑(↑n.negOnePow : ℤ) : R) * HAdd.hAdd (α := R) (↑n : 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

Premises used: Int.cast_neg, Int.cast_natCast, Int.cast_sub, Polynomial.eval_X, Polynomial.Chebyshev.U_sub_one, Int.negOnePow_add, Int.cast_add, Int.negOnePow_neg, Polynomial.eval_mul, Int.cast_ofNat, Int.negOnePow_def, Polynomial.Chebyshev.U_add_two, Int.negOnePow_sub, neg_mul, Polynomial.eval_ofNat, mul_one, OfNat.ofNat, Polynomial.eval_sub, sub_add_cancel, Int.cast_one, mul_neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ eval 0 (U R 0) = (↑(if Even (α := ℤ) 0 then (↑(0 / 2).negOnePow : ℤ) else 0) : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ eval 0 (U R 1) = (↑(if Even (α := ℤ) 1 then (↑(1 / 2).negOnePow : ℤ) else 0) : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 / 2 = HDiv.hDiv (α := ℤ) (↑n : ℤ) 2 + 1

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 / 2 = HDiv.hDiv (α := ℤ) (↑n : ℤ) 2 + 1

Tactic:
have : ((n : ℤ) + 2) / 2 = (n : ℤ) / 2 + 1 := by lia
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
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)
⊢ 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

Premises used: Even
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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
h : 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:
simp_all [Int.negOnePow_add]

Premises used: Int.negOnePow_add
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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
h : ¬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:
simp_all [Int.negOnePow_add]

Premises used: Int.negOnePow_add
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
⊢ HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 / 2 = HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 / 2 + 1

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
⊢ HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 / 2 = HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 / 2 + 1

Tactic:
have : (-(n : ℤ) + 1) / 2 = (-(n : ℤ) - 1) / 2 + 1 := by lia
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
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)
⊢ 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

Premises used: Even
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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
h : 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:
simp_all [U_sub_one, ← Int.not_even_iff_odd, Int.negOnePow_add]

Premises used: Polynomial.Chebyshev.U_sub_one, Int.negOnePow_add, Int.not_even_iff_odd
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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
h : ¬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:
simp_all [U_sub_one, ← Int.not_even_iff_odd, Int.negOnePow_add]

Premises used: Polynomial.Chebyshev.U_sub_one, Int.negOnePow_add, Int.not_even_iff_odd
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
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)
⊢ eval 0 (U R n) = (↑(if Even n then (↑(n / 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]

Premises used: Polynomial.Chebyshev.U_sub_one, Int.negOnePow_add, Int.not_even_iff_odd, Even
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
hn : Even n
⊢ eval 0 (U R n) = (↑(↑(n / 2).negOnePow : ℤ) : R)

Tactic:
simp [U_eval_zero, hn]

Premises used: Polynomial.Chebyshev.U_eval_zero
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ eval 0 (U R (2 * n)) = (↑(↑n.negOnePow : ℤ) : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
hn : Odd n
⊢ eval 0 (U R n) = 0

Tactic:
simp [U_eval_zero, ← Int.not_odd_iff_even, hn]

Premises used: Polynomial.Chebyshev.U_eval_zero, Int.not_odd_iff_even
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
⊢ degree (U R (↑0 : ℤ)) = (↑0 : WithBot ℕ)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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
one₂ one₃ : Eq (α := WithBot ℕ) 1 1
⊢ degree (U R 1) = 1

Tactic:
rw [U_one, ← C_ofNat, degree_C_mul_X two_ne_zero]

Premises used: Polynomial.Chebyshev.U_one, two_ne_zero, Polynomial.C_ofNat, Polynomial.degree_C_mul_X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 ℕ)
more : degree (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 2
⊢ degree (U R (↑(n + 2) : ℤ)) = (↑(n + 2) : WithBot ℕ)

Tactic:
push_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 : ℤ) 1)) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 1

Tactic:
push_cast at ih2
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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
rw : HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 1 + 1 = (↑(n + 2) : WithBot ℕ)
⊢ (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree = (↑(n + 2) : WithBot ℕ)

Tactic:
rw [mul_assoc, ← C_ofNat, degree_C_mul two_ne_zero, mul_comm, degree_mul_X, ih2]

Premises used: mul_assoc, two_ne_zero, Polynomial.C_ofNat, Polynomial.degree_C_mul, mul_comm, Polynomial.degree_mul_X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : n + 1 + 1 = n + 2
⊢ HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 1 + 1 = (↑(n + 2) : WithBot ℕ)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 ℕ)

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
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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
more₁ : degree (U R (↑n : ℤ)) < (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree
⊢ degree (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 2

Tactic:
rw [U_add_two, degree_sub_eq_left_of_degree_lt]

Premises used: Polynomial.Chebyshev.U_add_two, Polynomial.degree_sub_eq_left_of_degree_lt
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 : (↑(n + 2) : WithBot ℕ) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 2
⊢ (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree =
    HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 2

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 more₁ more₂ more₃ : n + 2 = n + 2
⊢ (↑(n + 2) : WithBot ℕ) = HAdd.hAdd (α := WithBot ℕ) (↑n : WithBot ℕ) 2

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 : LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ) (↑(n + 2) : WithBot ℕ)
⊢ degree (U R (↑n : ℤ)) < (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)).degree

Tactic:
rw [ih1, this]
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 : n < n + 2
⊢ LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ) (↑(n + 2) : WithBot ℕ)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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 < n + 2

Tactic:
omega