awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
this : S R 2 = HMul.hMul (α := R[X]) X X - 1
⊢ S R 2 = HPow.hPow (α := R[X]) (β := ℕ) X 2 - 1

Tactic:
linear_combination this
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (S R (-2)) (-1)

Tactic:
simpa [zero_sub, Int.reduceNeg, S_neg_one, mul_zero, S_zero] using S_sub_two R 0

Premises used: Int.reduceNeg, MulZeroClass.mul_zero, Polynomial.Chebyshev.S_zero, OfNat.ofNat, zero_sub, Polynomial.Chebyshev.S_sub_two, Polynomial.Chebyshev.S_neg_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (S R (HSub.hSub (α := ℤ) (-0) 1)) (-S R (HSub.hSub (α := ℤ) 0 1))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (S R (HSub.hSub (α := ℤ) (-1) 1)) (-S R (HSub.hSub (α := ℤ) 1 1))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (S R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)) (-S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 : Eq (α := R[X]) (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (-S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
⊢ S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) - S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)

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

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

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

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

Premises used: Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (S R (HSub.hSub (α := ℤ) (- -(↑n : ℤ)) 1)) (-S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
ih2 : Eq (α := R[X]) (S R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1))
⊢ S R (↑n : ℤ) = HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) - S R (HSub.hSub (α := ℤ) (↑n : ℤ) 2)

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

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

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

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

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

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    have h₁ := S_add_one R n
    have h₂ := S_sub_two R (-n - 1)
    linear_combination (norm := ring_nf) (X : R[X]) * ih1 - ih2 + h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := S_eq R n
    have h₂ := S_sub_two R (-n)
    linear_combination (norm := ring_nf) (X : R[X]) * ih1 - ih2 + h₁ + h₂

Premises used: Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ Eq (α := R[X]) (S R (-n)) (-S R (n - 2))

Tactic:
simpa [sub_sub] using S_neg_sub_one R (n - 1)

Premises used: HSub.hSub, sub_sub, Polynomial.Chebyshev.S_neg_sub_one, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ Eq (α := R[X]) (S R (-n - 2)) (-S R n)

Tactic:
simpa [sub_eq_add_neg, add_comm] using S_neg R (n + 2)

Premises used: sub_eq_add_neg, add_comm, Polynomial.Chebyshev.S_neg, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ eval 2 (S R 0) = HAdd.hAdd (α := R) (↑0 : R) 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
one : 2 = HAdd.hAdd (α := R) 1 1
⊢ eval 2 (S R 1) = HAdd.hAdd (α := R) (↑1 : R) 1

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

Tactic:
simp only [S_add_two, eval_sub, eval_mul, eval_X, ih1,
      Int.cast_add, Int.cast_natCast, Int.cast_one, ih2, Int.cast_ofNat]

Premises used: Int.cast_natCast, Polynomial.eval_X, Int.cast_add, Polynomial.eval_mul, Int.cast_ofNat, Polynomial.Chebyshev.S_add_two, Polynomial.eval_sub, Int.cast_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R) 1
ih2 : eval 2 (S R (↑n : ℤ)) = HAdd.hAdd (α := R) (↑(↑n : ℤ) : R) 1
⊢ 2 * (HAdd.hAdd (α := R) (↑n : R) 1 + 1) - HAdd.hAdd (α := R) (↑n : R) 1 = HAdd.hAdd (α := R) (↑n : R) 2 + 1

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

Tactic:
simp only [S_sub_one, eval_sub, eval_mul, eval_X,
      ih1, Int.cast_neg, Int.cast_natCast, ih2, Int.cast_add, Int.cast_one, Int.cast_sub,
      sub_add_cancel]

Premises used: Int.cast_neg, Int.cast_natCast, Int.cast_sub, Polynomial.eval_X, Int.cast_add, Polynomial.Chebyshev.S_sub_one, Polynomial.eval_mul, Polynomial.eval_sub, sub_add_cancel, Int.cast_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval 2 (S R (-(↑n : ℤ))) = HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1
ih2 : eval 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R) 1
⊢ 2 * HAdd.hAdd (α := R) (-(↑n : R)) 1 - (HAdd.hAdd (α := R) (-(↑n : R)) 1 + 1) = -(↑n : R)

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero : eval 2 (S R 0) = HAdd.hAdd (α := R) (↑0 : R) 1
one : eval 2 (S R 1) = HAdd.hAdd (α := R) (↑1 : R) 1
add_two :
  ∀ (n : ℕ)
    (ih1 : eval 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R) 1)
    (ih2 : eval 2 (S R (↑n : ℤ)) = HAdd.hAdd (α := R) (↑(↑n : ℤ) : R) 1),
    eval 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : R) 1
neg_add_one :
  ∀ (n : ℕ) (ih1 : eval 2 (S R (-(↑n : ℤ))) = HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1)
    (ih2 :
      eval 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R) 1),
    eval 2 (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = HAdd.hAdd (α := R) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : R) 1
⊢ eval 2 (S R n) = 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 [S_add_two, eval_sub, eval_mul, eval_X, ih1,
      Int.cast_add, Int.cast_natCast, Int.cast_one, ih2, Int.cast_ofNat]
    ring
  | neg_add_one n ih1 ih2 =>
    simp only [S_sub_one, eval_sub, eval_mul, eval_X,
      ih1, Int.cast_neg, Int.cast_natCast, ih2, Int.cast_add, Int.cast_one, Int.cast_sub,
      sub_add_cancel]
    ring

Premises used: Int.cast_neg, Int.cast_natCast, Int.cast_sub, Polynomial.eval_X, Int.cast_add, Polynomial.Chebyshev.S_sub_one, Polynomial.eval_mul, Int.cast_ofNat, Polynomial.Chebyshev.S_add_two, Polynomial.eval_sub, sub_add_cancel, Int.cast_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ eval (-2) (S R 0) = (↑(↑(Int.negOnePow 0) : ℤ) : R) * HAdd.hAdd (α := R) (↑0 : R) 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
one : -2 = HAdd.hAdd (α := R) (-1) (-1)
⊢ eval (-2) (S R 1) = (↑(↑(Int.negOnePow 1) : ℤ) : R) * HAdd.hAdd (α := R) (↑1 : R) 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  eval (-2) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R) 1
ih2 : eval (-2) (S R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * HAdd.hAdd (α := R) (↑(↑n : ℤ) : R) 1
add_two :
  -(2 * ((↑(↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) : R) * (HAdd.hAdd (α := R) (↑n : R) 1 + 1))) -
      (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * HAdd.hAdd (α := R) (↑n : R) 1 =
    (↑(↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℤ) (-1) 2) : ℤ) : R) * (HAdd.hAdd (α := R) (↑n : R) 2 + 1)
⊢ eval (-2) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : R) 1

Tactic:
simp only [S_add_two, eval_sub, eval_mul, eval_X, ih1,
      Int.cast_add, Int.cast_natCast, Int.cast_one, neg_mul, ih2, Int.cast_ofNat, Int.negOnePow_add,
      Int.negOnePow_def 2]

Premises used: Int.cast_natCast, Polynomial.eval_X, Int.negOnePow_add, Int.cast_add, Polynomial.eval_mul, Int.cast_ofNat, Int.negOnePow_def, neg_mul, Polynomial.Chebyshev.S_add_two, OfNat.ofNat, Polynomial.eval_sub, Int.cast_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  eval (-2) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R) 1
ih2 : eval (-2) (S R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * HAdd.hAdd (α := R) (↑(↑n : ℤ) : R) 1
add_two :
  Eq.{u_1 + 1} (α := R)
    (↑(-(2 * ((↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) * (↑(n + 1 + 1) : ℤ))) -
          (↑(Int.negOnePow (↑n : ℤ)) : ℤ) * (↑(n + 1) : ℤ)) :
      R)
    (↑((↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 2) : ℤ) * (↑(n + 2 + 1) : ℤ)) : R)
⊢ -(2 * ((↑(↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) : R) * (HAdd.hAdd (α := R) (↑n : R) 1 + 1))) -
      (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * HAdd.hAdd (α := R) (↑n : R) 1 =
    (↑(↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℤ) (-1) 2) : ℤ) : R) * (HAdd.hAdd (α := R) (↑n : R) 2 + 1)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  eval (-2) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R) 1
ih2 : eval (-2) (S R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * HAdd.hAdd (α := R) (↑(↑n : ℤ) : R) 1
add_two :
  2 * (HPow.hPow (α := R) (-1) n * (HAdd.hAdd (α := R) (↑n : R) 1 + 1)) -
      HPow.hPow (α := R) (-1) n * HAdd.hAdd (α := R) (↑n : R) 1 =
    HPow.hPow (α := R) (-1) n * (HAdd.hAdd (α := R) (↑n : R) 2 + 1)
⊢ Eq.{u_1 + 1} (α := R)
    (↑(-(2 * ((↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) * (↑(n + 1 + 1) : ℤ))) -
          (↑(Int.negOnePow (↑n : ℤ)) : ℤ) * (↑(n + 1) : ℤ)) :
      R)
    (↑((↑(Int.negOnePow (↑n : ℤ) * HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 2) : ℤ) * (↑(n + 2 + 1) : ℤ)) : R)

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  eval (-2) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R) 1
ih2 : eval (-2) (S R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * HAdd.hAdd (α := R) (↑(↑n : ℤ) : R) 1
⊢ 2 * (HPow.hPow (α := R) (-1) n * (HAdd.hAdd (α := R) (↑n : R) 1 + 1)) -
      HPow.hPow (α := R) (-1) n * HAdd.hAdd (α := R) (↑n : R) 1 =
    HPow.hPow (α := R) (-1) n * (HAdd.hAdd (α := R) (↑n : R) 2 + 1)

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval (-2) (S R (-(↑n : ℤ))) = (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) * HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1
ih2 :
  eval (-2) (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R) 1
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 (-2) (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : R) 1

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

Premises used: Int.cast_neg, Int.cast_natCast, Int.cast_sub, Polynomial.eval_X, Int.negOnePow_add, Int.cast_add, Int.negOnePow_neg, Polynomial.Chebyshev.S_sub_one, Polynomial.eval_mul, Int.negOnePow_sub, neg_mul, 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 (-2) (S R (-(↑n : ℤ))) = (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) * HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1
ih2 :
  eval (-2) (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R) 1
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 (-2) (S R (-(↑n : ℤ))) = (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) * HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1
ih2 :
  eval (-2) (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R) 1
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 (-2) (S R (-(↑n : ℤ))) = (↑(↑(Int.negOnePow (-(↑n : ℤ))) : ℤ) : R) * HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1
ih2 :
  eval (-2) (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : R) 1
⊢ -(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