awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
x : R
zero : eval (-x) (U R (↑0 : ℤ)) = (↑(↑(Int.negOnePow (↑0 : ℤ)) : ℤ) : R) * eval x (U R (↑0 : ℤ))
one : eval (-x) (U R (↑1 : ℤ)) = (↑(↑(Int.negOnePow (↑1 : ℤ)) : ℤ) : R) * eval x (U R (↑1 : ℤ))
more :
  ∀ (n : ℕ) (ih1 : eval (-x) (U R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (U R (↑n : ℤ)))
    (ih2 : eval (-x) (U R (↑(n + 1) : ℤ)) = (↑(↑(Int.negOnePow (↑(n + 1) : ℤ)) : ℤ) : R) * eval x (U R (↑(n + 1) : ℤ))),
    eval (-x) (U R (↑(n + 2) : ℤ)) = (↑(↑(Int.negOnePow (↑(n + 2) : ℤ)) : ℤ) : R) * eval x (U R (↑(n + 2) : ℤ))
⊢ eval (-x) (U R (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑n : ℤ)) : ℤ) : R) * eval x (U R (↑n : ℤ))

Tactic:
induction n using Nat.twoStepInduction with
  | zero => simp
  | one => simp
  | more n ih1 ih2 =>
    trans (n + 2 : ℤ).negOnePow * (2 * x * (U R (n + 1)).eval x - (U R n).eval x)
    · push_cast; push_cast at ih2
      rw [U_add_two, eval_sub, eval_mul, eval_mul, ih1, ih2,
        Int.negOnePow_succ, Int.negOnePow_add, Int.negOnePow_even 2 even_two]
      simp; ring
    · simp

Premises used: Polynomial.eval, HMul.hMul, Polynomial.Chebyshev.U, even_two, HSub.hSub, Int.negOnePow_add, Polynomial.eval_mul, Nat.cast, Polynomial.Chebyshev.U_add_two, HAdd.hAdd, Int.negOnePow_even, OfNat.ofNat, Polynomial.eval_sub, Int.negOnePow_succ, Int.negOnePow
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
hn : n ≠ -1
⊢ degree (U R n) ≠ ⊥

Tactic:
simp [degree_U_of_ne_neg_one R n hn]

Premises used: Polynomial.Chebyshev.degree_U_of_ne_neg_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
h : Eq (α := R[X]) (U R n) 0
contrapose! : ∀ (h : n ≠ -1), Ne (α := R[X]) (U R n) 0
⊢ n = -1

Tactic:
contrapose! h
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
h : n ≠ -1
⊢ Ne (α := R[X]) (U R n) 0

Tactic:
U_ne_zero R n h

Premises used: Polynomial.Chebyshev.U_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
h : n ≠ -1
⊢ Ne (α := R[X]) (U R n) 0

Tactic:
exact U_ne_zero R n h

Premises used: Polynomial.Chebyshev.U_ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
inst_1 : IsDomain R
inst_2 : NeZero.{u_1} (R := R) 2
h : n = -1
⊢ Eq (α := R[X]) (U R n) 0

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ U R (HAdd.hAdd (α := ℤ) 0 1) = HMul.hMul (α := R[X]) X (U R 0) + T R (HAdd.hAdd (α := ℤ) 0 1)

Tactic:
simp [two_mul]

Premises used: two_mul
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
one :
  4 * HPow.hPow (α := R[X]) (β := ℕ) X 2 - 1 =
    X * HMul.hMul (α := R[X]) 2 X + (2 * HPow.hPow (α := R[X]) (β := ℕ) X 2 - 1)
⊢ U R (HAdd.hAdd (α := ℤ) 1 1) = HMul.hMul (α := R[X]) X (U R 1) + T R (HAdd.hAdd (α := ℤ) 1 1)

Tactic:
simp [U_two, T_two]

Premises used: Polynomial.Chebyshev.T_two, Polynomial.Chebyshev.U_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ 4 * HPow.hPow (α := R[X]) (β := ℕ) X 2 - 1 =
    X * HMul.hMul (α := R[X]) 2 X + (2 * HPow.hPow (α := R[X]) (β := ℕ) X 2 - 1)

Tactic:
ring
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) =
    HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)
ih2 : U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) = HMul.hMul (α := R[X]) X (U R (↑n : ℤ)) + T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
⊢ U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) - U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)

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

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

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

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

Premises used: Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) =
    HMul.hMul (α := R[X]) X (U R (-(↑n : ℤ))) + T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
ih2 :
  U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1) =
    HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) + T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 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_add_two R (-n - 1)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 :
  U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) =
    HMul.hMul (α := R[X]) X (U R (-(↑n : ℤ))) + T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
ih2 :
  U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1) =
    HMul.hMul (α := R[X]) X (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) + T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 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) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) - U R (-(↑n : ℤ))

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

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

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

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

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

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp [two_mul]
  | one => simp [U_two, T_two]; ring
  | add_two n ih1 ih2 =>
    have h₁ := U_add_two R (n + 1)
    have h₂ := U_add_two R n
    have h₃ := T_add_two R (n + 1)
    linear_combination (norm := ring_nf) -h₃ - (X : R[X]) * h₂ + h₁ + 2 * (X : R[X]) * ih1 - ih2
  | neg_add_one n ih1 ih2 =>
    have h₁ := U_add_two R (-n - 1)
    have h₂ := U_add_two R (-n)
    have h₃ := T_add_two R (-n)
    linear_combination (norm := ring_nf) -h₃ + h₂ - (X : R[X]) * h₁ - ih2 + 2 * (X : R[X]) * ih1

Premises used: Polynomial.Chebyshev.T_two, Polynomial.Chebyshev.U_two, two_mul, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ HAdd.hAdd (α := R[X]) (T R n) (U R (n - 1 + 1)) -
      (U R n - HMul.hMul (α := R[X]) X (U R (n - 1)) + (HMul.hMul (α := R[X]) X (U R (n - 1)) + T R (n - 1 + 1))) =
    0

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

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

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

Tactic:
have h₁ := U_eq_X_mul_U_add_T R n
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h₁ : U R (n + 1) = HMul.hMul (α := R[X]) X (U R n) + T R (n + 1)
⊢ U R (n + 1 + 1) = HMul.hMul (α := R[X]) X (U R (n + 1)) + T R (n + 1 + 1)

Tactic:
have h₂ := U_eq_X_mul_U_add_T R (n + 1)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h₁ : U R (n + 1) = HMul.hMul (α := R[X]) X (U R n) + T R (n + 1)
h₂ : U R (n + 1 + 1) = HMul.hMul (α := R[X]) X (U R (n + 1)) + T R (n + 1 + 1)
⊢ U R (n + 2) = HMul.hMul (α := R[X]) 2 X * U R (n + 1) - U R n

Tactic:
have h₃ := U_add_two R n
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h₁ : U R (n + 1) = HMul.hMul (α := R[X]) X (U R n) + T R (n + 1)
h₂ : U R (n + 1 + 1) = HMul.hMul (α := R[X]) X (U R (n + 1)) + T R (n + 1 + 1)
h₃ : U R (n + 2) = HMul.hMul (α := R[X]) 2 X * U R (n + 1) - U R n
⊢ T R (n + 2) +
        (HMul.hMul (α := R[X]) 2 X * U R (n + 1) - U R n + U R (n + 1 + 1) +
          X * (HMul.hMul (α := R[X]) X (U R n) + T R (n + 1))) -
      (HMul.hMul (α := R[X]) X (T R (n + 1)) - (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n +
        (U R (n + 2) + (HMul.hMul (α := R[X]) X (U R (n + 1)) + T R (n + 1 + 1)) +
          HMul.hMul (α := R[X]) X (U R (n + 1)))) =
    0

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h₁ : U R (n + 1) = HMul.hMul (α := R[X]) X (U R n) + T R (n + 1)
h₂ : U R (n + 1 + 1) = HMul.hMul (α := R[X]) X (U R (n + 1)) + T R (n + 1 + 1)
h₃ : U R (n + 2) = HMul.hMul (α := R[X]) 2 X * U R (n + 1) - U R n
a :
  T R (n + 2) +
        (HMul.hMul (α := R[X]) 2 X * U R (n + 1) - U R n + U R (n + 1 + 1) +
          X * (HMul.hMul (α := R[X]) X (U R n) + T R (n + 1))) -
      (HMul.hMul (α := R[X]) X (T R (n + 1)) - (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n +
        (U R (n + 2) + (HMul.hMul (α := R[X]) X (U R (n + 1)) + T R (n + 1 + 1)) +
          HMul.hMul (α := R[X]) X (U R (n + 1)))) =
    0
⊢ T R (n + 2) = HMul.hMul (α := R[X]) X (T R (n + 1)) - (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n

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

Premises used: Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ (1 - HPow.hPow (α := R[X]) (β := ℕ) X 2) * U R n = HMul.hMul (α := R[X]) X (T R (n + 1)) - T R (n + 2)

Tactic:
linear_combination T_eq_X_mul_T_sub_pol_U R n

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

Tactic:
have h := T_eq_U_sub_X_mul_U (R := R) (-(n + 2))
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h : T R (n + 2) = -U R n - HMul.hMul (α := R[X]) X (-U R (n + 2 + 1 - 2))
⊢ n + 2 + 1 - 2 = n + 1

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

Tactic:
rw [T_neg, U_neg, Int.add_sub_cancel, ← neg_add' _ 1, U_neg,
    show n + 2 + 1 - 2 = n + 1 by ring] at h

Premises used: Int.add_sub_cancel, neg_add', Polynomial.Chebyshev.U_neg, Polynomial.Chebyshev.T_neg, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
h : T R (n + 2) = -U R n - HMul.hMul (α := R[X]) X (-U R (n + 1))
⊢ T R (n + 2) + (-U R n - HMul.hMul (α := R[X]) X (-U R (n + 1))) -
      (HMul.hMul (α := R[X]) X (U R (n + 1)) - U R n + T R (n + 2)) =
    0

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

Tactic:
linear_combination (norm := ring_nf) h
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ HMul.hMul (α := R[X]) 2 (T R (n + 2)) +
        (U R (n + 2) - HMul.hMul (α := R[X]) X (U R (n + 2 - 1)) + (HMul.hMul (α := R[X]) X (U R (n + 1)) - U R n)) -
      (HSub.hSub (α := R[X]) (U R (n + 2)) (U R n) + HAdd.hAdd (α := R[X]) (T R (n + 2)) (T R (n + 2))) =
    0

Tactic:
ring_nf