awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (T R (- -(↑n : ℤ))) (T R (-(↑n : ℤ)))
ih2 : Eq (α := R[X]) (T R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))
h₁ :
  T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) 2 X * T R (↑n : ℤ) - T R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)
h₂ :
  T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) =
    HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ T R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) +
        (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) + T R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) +
            (HMul.hMul (α := R[X]) 2 X * T R (↑n : ℤ) - T R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) +
          T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) -
      (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) +
        (HMul.hMul (α := R[X]) 2 X * T R (- -(↑n : ℤ)) + T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) +
            T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) +
          (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)))) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (T R (- -(↑n : ℤ))) (T R (-(↑n : ℤ)))
ih2 : Eq (α := R[X]) (T R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))
h₁ :
  T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) 2 X * T R (↑n : ℤ) - T R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)
h₂ :
  T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) =
    HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
a :
  T R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) +
        (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) + T R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) +
            (HMul.hMul (α := R[X]) 2 X * T R (↑n : ℤ) - T R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) +
          T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) -
      (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) +
        (HMul.hMul (α := R[X]) 2 X * T R (- -(↑n : ℤ)) + T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) +
            T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) +
          (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)))) =
    0
⊢ Eq (α := R[X]) (T R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))

Tactic:
linear_combination (norm := ring_nf) (2 * (X : R[X])) * ih1 - ih2 + h₁ - h₂

Premises used: HMul.hMul, OfNat.ofNat, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : Eq (α := R[X]) (T R (-0)) (T R 0)
one : Eq (α := R[X]) (T R (-1)) (T R 1)
add_two :
  ∀ (n : ℕ) (ih1 : Eq (α := R[X]) (T R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))
    (ih2 : Eq (α := R[X]) (T R (-(↑n : ℤ))) (T R (↑n : ℤ))),
    Eq (α := R[X]) (T R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2))
neg_add_one :
  ∀ (n : ℕ) (ih1 : Eq (α := R[X]) (T R (- -(↑n : ℤ))) (T R (-(↑n : ℤ))))
    (ih2 : Eq (α := R[X]) (T R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))),
    Eq (α := R[X]) (T R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
⊢ Eq (α := R[X]) (T R (-n)) (T R n)

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => rfl
  | one => simp only [T_neg_one, T_one]
  | add_two n ih1 ih2 =>
    have h₁ := T_add_two R n
    have h₂ := T_sub_two R (-n)
    linear_combination (norm := ring_nf) (2 * (X : R[X])) * ih1 - ih2 - h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := T_add_one R n
    have h₂ := T_sub_one R (-n)
    linear_combination (norm := ring_nf) (2 * (X : R[X])) * ih1 - ih2 + h₁ - h₂

Premises used: HMul.hMul, Polynomial.Chebyshev.T_one, Polynomial.Chebyshev.T_neg_one, OfNat.ofNat, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
inl : ∀ (h : n = (↑n.natAbs : ℤ)), Eq (α := R[X]) (T R (↑n.natAbs : ℤ)) (T R n)
inr : ∀ (h : n = -(↑n.natAbs : ℤ)), Eq (α := R[X]) (T R (↑n.natAbs : ℤ)) (T R n)
⊢ Eq (α := R[X]) (T R (↑n.natAbs : ℤ)) (T R n)

Tactic:
obtain h | h := Int.natAbs_eq n

Premises used: Int.natAbs_eq
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h : n = (↑n.natAbs : ℤ)
inl inl₁ : Eq (α := R[X]) (T R (↑n.natAbs : ℤ)) (T R (↑n.natAbs : ℤ))
⊢ Eq (α := R[X]) (T R (↑n.natAbs : ℤ)) (T R n)

Tactic:
nth_rw 2 [h]
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h : n = -(↑n.natAbs : ℤ)
inr : Eq (α := R[X]) (T R (↑n.natAbs : ℤ)) (T R (-(↑n.natAbs : ℤ)))
⊢ Eq (α := R[X]) (T R (↑n.natAbs : ℤ)) (T R n)

Tactic:
nth_rw 2 [h]
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h : n = -(↑n.natAbs : ℤ)
⊢ Eq (α := R[X]) (T R (↑n.natAbs : ℤ)) (T R (-(↑n.natAbs : ℤ)))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ T R (-2) = 2 * HPow.hPow (α := R[X]) (β := ℕ) X 2 - 1

Tactic:
simp [T_two]

Premises used: Polynomial.Chebyshev.T_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ eval 1 (T R 0) = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ eval 1 (T R 1) = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval 1 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = 1
ih2 : eval 1 (T R (↑n : ℤ)) = 1
add_two : HSub.hSub (α := R) 2 1 = 1
⊢ eval 1 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = 1

Tactic:
simp [T_add_two, ih1, ih2]

Premises used: Polynomial.Chebyshev.T_add_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval 1 (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = 1
ih2 : eval 1 (T R (↑n : ℤ)) = 1
⊢ HSub.hSub (α := R) 2 1 = 1

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval 1 (T R (-(↑n : ℤ))) = 1
ih2 : eval 1 (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = 1
neg_add_one : HSub.hSub (α := R) 2 1 = 1
⊢ eval 1 (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = 1

Tactic:
simp [T_sub_one, -T_neg, ih1, ih2]

Premises used: Polynomial.Chebyshev.T_neg, Polynomial.Chebyshev.T_sub_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval 1 (T R (-(↑n : ℤ))) = 1
ih2 : eval 1 (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = 1
⊢ HSub.hSub (α := R) 2 1 = 1

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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
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
⊢ eval 1 (T R n) = 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

Premises used: Polynomial.Chebyshev.T_neg, Polynomial.Chebyshev.T_sub_one, Polynomial.Chebyshev.T_add_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ eval (-1) (T R 0) = (↑(↑(Int.negOnePow 0) : ℤ) : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ eval (-1) (T R 1) = (↑(↑(Int.negOnePow 1) : ℤ) : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
add_two :
  HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) - (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) =
    (↑(↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℤ) (-1) 2) : ℤ) : R)
⊢ eval (-1) (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : 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]

Premises used: Int.cast_neg, Polynomial.eval_X, Int.negOnePow_add, neg_neg, Polynomial.eval_mul, Int.negOnePow_one, Int.negOnePow_def, Units.val_neg, neg_mul, Polynomial.eval_ofNat, mul_one, Polynomial.Chebyshev.T_add_two, OfNat.ofNat, Polynomial.eval_sub, mul_neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
add_two :
  HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) - (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) =
    (↑(↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 2) : ℤ) : R)
⊢ HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) - (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) =
    (↑(↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℤ) (-1) 2) : ℤ) : R)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
add_two : 2 * HPow.hPow (α := R) (-1) n - HPow.hPow (α := R) (-1) n = HPow.hPow (α := R) (-1) n
⊢ HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) - (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) =
    (↑(↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 2) : ℤ) : R)

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
⊢ 2 * HPow.hPow (α := R) (-1) n - HPow.hPow (α := R) (-1) n = HPow.hPow (α := R) (-1) n

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
neg_add_one :
  -HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) + (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) =
    -(↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R)
⊢ eval (-1) (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = (↑(↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : 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]

Premises used: Int.cast_neg, Polynomial.eval_X, Int.negOnePow_add, Polynomial.eval_mul, Int.negOnePow_one, Units.val_neg, Int.negOnePow_sub, Polynomial.Chebyshev.T_sub_one, neg_mul, Polynomial.eval_ofNat, mul_one, Polynomial.eval_sub, sub_neg_eq_add, mul_neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
⊢ -HMul.hMul (α := R) 2 (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) + (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) =
    -(↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R)

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
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)
⊢ eval (-1) (T R n) = (↑(↑n.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

Premises used: Int.cast_neg, Polynomial.eval_X, Int.negOnePow_add, neg_neg, Polynomial.eval_mul, Int.negOnePow_one, Int.negOnePow_def, Units.val_neg, Int.negOnePow_sub, Polynomial.Chebyshev.T_sub_one, neg_mul, Polynomial.eval_ofNat, mul_one, Polynomial.Chebyshev.T_add_two, OfNat.ofNat, Polynomial.eval_sub, sub_neg_eq_add, mul_neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ eval 0 (T 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 (T 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 (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)
⊢ 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 (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)
⊢ 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 (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)
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)
⊢ 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

Premises used: Even
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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
h : 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:
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 (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
h : ¬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:
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 (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)
⊢ 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 (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)
⊢ 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 (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)
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)
⊢ 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

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

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

Premises used: Int.negOnePow_add, Int.not_even_iff_odd, Polynomial.Chebyshev.T_sub_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
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)
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)
⊢ eval 0 (T 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 [T_sub_one, ← Int.not_even_iff_odd, Int.negOnePow_add]

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

Tactic:
simp [T_eval_zero, hn]

Premises used: Polynomial.Chebyshev.T_eval_zero
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ eval 0 (T 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 (T R n) = 0

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

Premises used: Polynomial.Chebyshev.T_eval_zero, Int.not_odd_iff_even