awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
a :
  U R (n + 1) + (HMul.hMul (α := R[X]) 2 X * U R (n - 1 + 1) - U R (n - 1)) -
      (HMul.hMul (α := R[X]) 2 X * U R n - U R (n - 1) + U R (n - 1 + 2)) =
    0
⊢ U R (n + 1) = HMul.hMul (α := R[X]) 2 X * U R n - U R (n - 1)

Tactic:
linear_combination (norm := ring_nf) U_add_two R (n - 1)

Premises used: HSub.hSub, Polynomial.Chebyshev.U_add_two, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ U R (n - 2) + (HMul.hMul (α := R[X]) 2 X * U R (n - 2 + 1) - U R (n - 2)) -
      (HMul.hMul (α := R[X]) 2 X * U R (n - 1) - U R n + U R (n - 2 + 2)) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
a :
  U R (n - 2) + (HMul.hMul (α := R[X]) 2 X * U R (n - 2 + 1) - U R (n - 2)) -
      (HMul.hMul (α := R[X]) 2 X * U R (n - 1) - U R n + U R (n - 2 + 2)) =
    0
⊢ U R (n - 2) = HMul.hMul (α := R[X]) 2 X * U R (n - 1) - U R n

Tactic:
linear_combination (norm := ring_nf) U_add_two R (n - 2)

Premises used: HSub.hSub, Polynomial.Chebyshev.U_add_two, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ U R (n - 1) + (HMul.hMul (α := R[X]) 2 X * U R (n - 1 + 1) - U R (n - 1)) -
      (HMul.hMul (α := R[X]) 2 X * U R n - U R (n + 1) + U R (n - 1 + 2)) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
a :
  U R (n - 1) + (HMul.hMul (α := R[X]) 2 X * U R (n - 1 + 1) - U R (n - 1)) -
      (HMul.hMul (α := R[X]) 2 X * U R n - U R (n + 1) + U R (n - 1 + 2)) =
    0
⊢ U R (n - 1) = HMul.hMul (α := R[X]) 2 X * U R n - U R (n + 1)

Tactic:
linear_combination (norm := ring_nf) U_add_two R (n - 1)

Premises used: HSub.hSub, Polynomial.Chebyshev.U_add_two, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ U R n + (HMul.hMul (α := R[X]) 2 X * U R (n - 2 + 1) - U R (n - 2)) -
      (HMul.hMul (α := R[X]) 2 X * U R (n - 1) - U R (n - 2) + U R (n - 2 + 2)) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
a :
  U R n + (HMul.hMul (α := R[X]) 2 X * U R (n - 2 + 1) - U R (n - 2)) -
      (HMul.hMul (α := R[X]) 2 X * U R (n - 1) - U R (n - 2) + U R (n - 2 + 2)) =
    0
⊢ U R n = HMul.hMul (α := R[X]) 2 X * U R (n - 1) - U R (n - 2)

Tactic:
linear_combination (norm := ring_nf) U_add_two R (n - 2)

Premises used: HSub.hSub, Polynomial.Chebyshev.U_add_two, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (U R 0) 1

Tactic:
simp [U]

Premises used: Polynomial.Chebyshev.U
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ U R 1 = HMul.hMul (α := R[X]) 2 X

Tactic:
simp [U]

Premises used: Polynomial.Chebyshev.U
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (U R (-1)) 0

Tactic:
simpa using U_sub_one R 0

Premises used: Polynomial.Chebyshev.U_sub_one, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ U R (HAdd.hAdd (α := ℤ) 0 2) = HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) 0 1) - U R 0

Tactic:
have := U_add_two R 0
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
this : U R (HAdd.hAdd (α := ℤ) 0 2) = HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) 0 1) - U R 0
⊢ U R 2 = HMul.hMul (α := R[X]) 2 X * HMul.hMul (α := R[X]) 2 X - 1

Tactic:
simp only [zero_add, U_one, U_zero] at this

Premises used: Polynomial.Chebyshev.U_one, Polynomial.Chebyshev.U_zero, zero_add
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
this : U R 2 = HMul.hMul (α := R[X]) 2 X * HMul.hMul (α := R[X]) 2 X - 1
⊢ U R 2 = 4 * 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]) (U R (-2)) (-1)

Tactic:
simpa [zero_sub, Int.reduceNeg, U_neg_one, mul_zero, U_zero] using U_sub_two R 0

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

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (-1) 1)) (-U 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]) (U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)) (-U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (-U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
⊢ U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) 2 X * U R (↑n : ℤ) - U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)

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

Tactic:
have h₂ := U_sub_two R (-n - 1)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)) (-U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (-U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
h₁ :
  U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) 2 X * U R (↑n : ℤ) - U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)
h₂ :
  U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 2) =
    HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1) - U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
⊢ U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1) +
        (HMul.hMul (α := R[X]) 2 X * -U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1) + U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) +
            (HMul.hMul (α := R[X]) 2 X * U R (↑n : ℤ) - U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) +
          (HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1) -
            U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))) -
      (-U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1) +
        (HMul.hMul (α := R[X]) 2 X * U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1) + -U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) +
            U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) +
          U 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]) (U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)) (-U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1))
ih2 : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (-U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
h₁ :
  U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) 2 X * U R (↑n : ℤ) - U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)
h₂ :
  U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 2) =
    HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1) - U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
a :
  U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1) +
        (HMul.hMul (α := R[X]) 2 X * -U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1) + U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) +
            (HMul.hMul (α := R[X]) 2 X * U R (↑n : ℤ) - U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) +
          (HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1) -
            U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))) -
      (-U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1) +
        (HMul.hMul (α := R[X]) 2 X * U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1) + -U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) +
            U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) +
          U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 2))) =
    0
⊢ Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1)) (-U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1))

Tactic:
linear_combination (norm := ring_nf) 2 * (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]) (U R (HSub.hSub (α := ℤ) (- -(↑n : ℤ)) 1)) (-U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
ih2 : Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1))
⊢ U R (↑n : ℤ) = HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) - U R (HSub.hSub (α := ℤ) (↑n : ℤ) 2)

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

Tactic:
have h₂ := U_sub_two R (-n)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (- -(↑n : ℤ)) 1)) (-U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
ih2 : Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1))
h₁ :
  U R (↑n : ℤ) = HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) - U R (HSub.hSub (α := ℤ) (↑n : ℤ) 2)
h₂ :
  U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) - U R (-(↑n : ℤ))
⊢ U R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1) +
        (HMul.hMul (α := R[X]) 2 X * -U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) +
              U R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1) +
            (HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) - U R (HSub.hSub (α := ℤ) (↑n : ℤ) 2)) +
          (HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) - U R (-(↑n : ℤ)))) -
      (-U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1) +
        (HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (- -(↑n : ℤ)) 1) +
              -U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1) +
            U R (↑n : ℤ) +
          U 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]) (U R (HSub.hSub (α := ℤ) (- -(↑n : ℤ)) 1)) (-U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1))
ih2 : Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1))
h₁ :
  U R (↑n : ℤ) = HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) - U R (HSub.hSub (α := ℤ) (↑n : ℤ) 2)
h₂ :
  U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) - U R (-(↑n : ℤ))
a :
  U R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1) +
        (HMul.hMul (α := R[X]) 2 X * -U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) +
              U R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1) +
            (HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1) - U R (HSub.hSub (α := ℤ) (↑n : ℤ) 2)) +
          (HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) - U R (-(↑n : ℤ)))) -
      (-U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1) +
        (HMul.hMul (α := R[X]) 2 X * U R (HSub.hSub (α := ℤ) (- -(↑n : ℤ)) 1) +
              -U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1) +
            U R (↑n : ℤ) +
          U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 2))) =
    0
⊢ Eq (α := R[X]) (U R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1))

Tactic:
linear_combination (norm := ring_nf) 2 * (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]) (U R (HSub.hSub (α := ℤ) (-0) 1)) (-U R (HSub.hSub (α := ℤ) 0 1))
one : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (-1) 1)) (-U R (HSub.hSub (α := ℤ) 1 1))
add_two :
  ∀ (n : ℕ) (ih1 : Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)) (-U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1)))
    (ih2 : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (-U R (HSub.hSub (α := ℤ) (↑n : ℤ) 1))),
    Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1)) (-U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 - 1))
neg_add_one :
  ∀ (n : ℕ) (ih1 : Eq (α := R[X]) (U R (HSub.hSub (α := ℤ) (- -(↑n : ℤ)) 1)) (-U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)))
    (ih2 : Eq (α := R[X]) (U R (-HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 - 1))),
    Eq (α := R[X]) (U R (-HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1)) (-U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 - 1))
⊢ Eq (α := R[X]) (U R (-n - 1)) (-U R (n - 1))

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    have h₁ := U_add_one R n
    have h₂ := U_sub_two R (-n - 1)
    linear_combination (norm := ring_nf) 2 * (X : R[X]) * ih1 - ih2 + h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := U_eq R n
    have h₂ := U_sub_two R (-n)
    linear_combination (norm := ring_nf) 2 * (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]) (U R (-n)) (-U R (n - 2))

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

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

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

Premises used: sub_eq_add_neg, add_comm, Polynomial.Chebyshev.U_neg, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ eval 1 (U 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 1 (U R 1) = HAdd.hAdd (α := R) (↑1 : R) 1

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

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

Tactic:
simp only [U_add_two, eval_sub, eval_mul, eval_ofNat, eval_X, mul_one, 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.U_add_two, Polynomial.eval_ofNat, mul_one, Polynomial.eval_sub, Int.cast_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : eval 1 (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : R) 1
ih2 : eval 1 (U 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 1 (U R (-(↑n : ℤ))) = HAdd.hAdd (α := R) (↑(-(↑n : ℤ)) : R) 1
ih2 : eval 1 (U 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 1 (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = HAdd.hAdd (α := R) (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : R) 1

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

Tactic:
norm_num
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
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
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 (-1) (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) =
    (↑(↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2).negOnePow : ℤ) : R) *
      HAdd.hAdd (α := R) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : R) 1

Tactic:
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]

Premises used: Int.cast_natCast, Polynomial.eval_X, Int.negOnePow_add, Int.cast_add, Polynomial.eval_mul, Int.cast_ofNat, Int.negOnePow_def, Polynomial.Chebyshev.U_add_two, neg_mul, Polynomial.eval_ofNat, mul_one, OfNat.ofNat, Polynomial.eval_sub, Int.cast_one, mul_neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
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
add_two :
  -HMul.hMul (α := R) 2 (↑((↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) * (↑(n + 1 + 1) : ℤ)) : R) -
      (↑((↑(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 (-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
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)
⊢ -HMul.hMul (α := R) 2 (↑((↑(Int.negOnePow (↑n : ℤ) * Int.negOnePow 1) : ℤ) * (↑(n + 1 + 1) : ℤ)) : R) -
      (↑((↑(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 (-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
⊢ 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