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

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp; norm_num
  | add_two n ih1 ih2 =>
    simp only [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]
    norm_cast
    norm_num
    ring
  | neg_add_one n ih1 ih2 =>
    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]
    norm_cast
    norm_num
    ring

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.cast_ofNat, Int.negOnePow_def, Int.negOnePow_sub, neg_mul, Polynomial.Chebyshev.S_add_two, OfNat.ofNat, Polynomial.eval_sub, sub_add_cancel, Int.cast_one, mul_neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ comp (S R 0) (HMul.hMul (α := R[X]) 2 X) = U R 0

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

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) = U R (↑n : ℤ)
add_two :
  comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
add_two₁ :
  (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)).comp (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
add_two₂ :
  (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))).comp (HMul.hMul (α := R[X]) 2 X) -
      comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
add_two₃ :
  comp X (HMul.hMul (α := R[X]) 2 X) * comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) -
      comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
add_two₄ :
  HMul.hMul (α := R[X]) 2 X * comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (HMul.hMul (α := R[X]) 2 X) -
      comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
add_two₅ :
  HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - comp (S R (↑n : ℤ)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)
⊢ comp (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)

Tactic:
simp_rw [U_add_two, S_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]

Premises used: Polynomial.X_comp, Polynomial.Chebyshev.U_add_two, Polynomial.mul_comp, Polynomial.Chebyshev.S_add_two, Polynomial.sub_comp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih1 : comp (S R (-(↑n : ℤ))) (HMul.hMul (α := R[X]) 2 X) = U R (-(↑n : ℤ))
ih2 : comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  comp (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)).comp
      (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₂ :
  (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ)))).comp (HMul.hMul (α := R[X]) 2 X) -
      comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₃ :
  comp X (HMul.hMul (α := R[X]) 2 X) * comp (S R (-(↑n : ℤ))) (HMul.hMul (α := R[X]) 2 X) -
      comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₄ :
  HMul.hMul (α := R[X]) 2 X * comp (S R (-(↑n : ℤ))) (HMul.hMul (α := R[X]) 2 X) -
      comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₅ :
  HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) -
      comp (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) =
    HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ comp (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) (HMul.hMul (α := R[X]) 2 X) = U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)

Tactic:
simp_rw [U_sub_one, S_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]

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

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 => simp_rw [U_add_two, S_add_two, sub_comp, mul_comp, X_comp, ih1, ih2]
  | neg_add_one n ih1 ih2 => simp_rw [U_sub_one, S_sub_one, sub_comp, mul_comp, X_comp, ih1, ih2]

Premises used: Polynomial.X_comp, Polynomial.Chebyshev.U_sub_one, Polynomial.Chebyshev.S_sub_one, Polynomial.Chebyshev.U_add_two, Polynomial.mul_comp, Polynomial.Chebyshev.S_add_two, Polynomial.sub_comp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
zero : 1 + HPow.hPow (α := R[X]) (β := ℕ) X 2 - HMul.hMul (α := R[X]) X X = 1
⊢ HPow.hPow (α := R[X]) (β := ℕ) (S R 0) 2 + HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) 0 1)) 2 -
      HMul.hMul (α := R[X]) X (S R 0) * S R (HAdd.hAdd (α := ℤ) 0 1) =
    1

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

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

Tactic:
have h₁ := S_add_two R n
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih :
  HPow.hPow (α := R[X]) (β := ℕ) (S R (↑n : ℤ)) 2 +
        HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2 -
      HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) * S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    1
h₁ : S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)
⊢ HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2 +
            HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) 2 -
          HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) * S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) +
        (HSub.hSub (α := R[X]) (S R (HAdd.hAdd (α := ℤ) 2 (↑n : ℤ))) (S R (↑n : ℤ)) *
            (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)) +
          1) -
      (1 +
        (HSub.hSub (α := R[X]) (S R (HAdd.hAdd (α := ℤ) 2 (↑n : ℤ))) (S R (↑n : ℤ)) *
            S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) +
          (HPow.hPow (α := R[X]) (β := ℕ) (S R (↑n : ℤ)) 2 +
              HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2 -
            HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) * S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))) =
    0

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

Tactic:
linear_combination (norm := ring_nf) (S R (2 + n) - S R n) * h₁ + ih

Premises used: HSub.hSub, Polynomial.Chebyshev.S, Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih :
  HPow.hPow (α := R[X]) (β := ℕ) (S R (-(↑n : ℤ))) 2 +
        HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) 2 -
      HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) * S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) =
    1
⊢ S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) =
    HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)

Tactic:
have h₁ := S_sub_one R (-n)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
ih :
  HPow.hPow (α := R[X]) (β := ℕ) (S R (-(↑n : ℤ))) 2 +
        HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) 2 -
      HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) * S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) =
    1
h₁ :
  S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) =
    HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ HPow.hPow (α := R[X]) (β := ℕ) (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) 2 +
            HPow.hPow (α := R[X]) (β := ℕ) (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) 2 -
          HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) *
            S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) +
        (HSub.hSub (α := R[X]) (S R (HSub.hSub (α := ℤ) (-1) (↑n : ℤ))) (S R (HSub.hSub (α := ℤ) 1 (↑n : ℤ))) *
            (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) - S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) +
          1) -
      (1 +
        (HSub.hSub (α := R[X]) (S R (HSub.hSub (α := ℤ) (-1) (↑n : ℤ))) (S R (HSub.hSub (α := ℤ) 1 (↑n : ℤ))) *
            S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) +
          (HPow.hPow (α := R[X]) (β := ℕ) (S R (-(↑n : ℤ))) 2 +
              HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) 2 -
            HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) * S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)))) =
    0

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

Tactic:
linear_combination (norm := ring_nf) (S R (-1 - n) - S R (1 - n)) * h₁ + ih

Premises used: HSub.hSub, Polynomial.Chebyshev.S, Nat.cast, OfNat.ofNat, Neg.neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero :
  HPow.hPow (α := R[X]) (β := ℕ) (S R 0) 2 + HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) 0 1)) 2 -
      HMul.hMul (α := R[X]) X (S R 0) * S R (HAdd.hAdd (α := ℤ) 0 1) =
    1
succ :
  ∀ (n : ℕ)
    (ih :
      HPow.hPow (α := R[X]) (β := ℕ) (S R (↑n : ℤ)) 2 +
            HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2 -
          HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) * S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
        1),
    HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2 +
          HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) 2 -
        HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) * S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) =
      1
pred :
  ∀ (n : ℕ)
    (ih :
      HPow.hPow (α := R[X]) (β := ℕ) (S R (-(↑n : ℤ))) 2 +
            HPow.hPow (α := R[X]) (β := ℕ) (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) 2 -
          HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) * S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) =
        1),
    HPow.hPow (α := R[X]) (β := ℕ) (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) 2 +
          HPow.hPow (α := R[X]) (β := ℕ) (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) 2 -
        HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) * S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) =
      1
⊢ HPow.hPow (α := R[X]) (β := ℕ) (S R n) 2 + HPow.hPow (α := R[X]) (β := ℕ) (S R (n + 1)) 2 -
      HMul.hMul (α := R[X]) X (S R n) * S R (n + 1) =
    1

Tactic:
induction n with
  | zero => simp; ring
  | succ n ih =>
    have h₁ := S_add_two R n
    linear_combination (norm := ring_nf) (S R (2 + n) - S R n) * h₁ + ih
  | pred n ih =>
    have h₁ := S_sub_one R (-n)
    linear_combination (norm := ring_nf) (S R (-1 - n) - S R (1 - n)) * h₁ + ih

Premises used: HSub.hSub, Polynomial.Chebyshev.S, HAdd.hAdd, OfNat.ofNat, Neg.neg
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
n : ℤ
⊢ Eq.{u_1 + 1} (α := R[X])
    ((fun (x : R[X]) ↦
        x.comp
          (HMul.hMul (α := R[X])
            ((Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X))
      (comp (S R n) (HMul.hMul (α := R[X]) 2 X)))
    ((fun (x : R[X]) ↦
        x.comp
          (HMul.hMul (α := R[X])
            ((Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X))
      (U R n))

Tactic:
have := congr_arg (·.comp (Polynomial.C ⅟2 * X)) (S_comp_two_mul_X R n)
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
n : ℤ
this :
  Eq.{u_1 + 1} (α := R[X])
    ((fun (x : R[X]) ↦
        x.comp
          (HMul.hMul (α := R[X])
            ((Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X))
      (comp (S R n) (HMul.hMul (α := R[X]) 2 X)))
    ((fun (x : R[X]) ↦
        x.comp
          (HMul.hMul (α := R[X])
            ((Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X))
      (U R n))
⊢ S R n =
    comp (U R n)
      (HMul.hMul (α := R[X])
        ((Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X)

Tactic:
simp_rw [comp_assoc, mul_comp, ofNat_comp, X_comp, ← mul_assoc, ← C_eq_natCast, ← C_mul,
    Nat.cast_ofNat, mul_invOf_self', map_one, one_mul, comp_X] at this

Premises used: Nat.cast_ofNat, Polynomial.comp_assoc, Polynomial.X_comp, Polynomial.C_eq_natCast, mul_assoc, Polynomial.comp_X, map_one, Polynomial.C_mul, Polynomial.ofNat_comp, Polynomial.mul_comp, mul_invOf_self', one_mul
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Invertible (α := R) 2
n : ℤ
this :
  S R n =
    comp (U R n)
      (HMul.hMul (α := R[X])
        ((Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X)
⊢ S R n =
    comp (U R n)
      (HMul.hMul (α := R[X])
        ((Polynomial.C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)) X)

Tactic:
assumption
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
⊢ HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) 0 1)) =
    HMul.hMul (α := R[X]) X (S R 0) + C 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 :
  2 * (HPow.hPow (α := R[X]) (β := ℕ) X 2 - 1) = HMul.hMul (α := R[X]) X X + (HPow.hPow (α := R[X]) (β := ℕ) X 2 - 2)
⊢ HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) 1 1)) =
    HMul.hMul (α := R[X]) X (S R 1) + C R (HAdd.hAdd (α := ℤ) 1 1)

Tactic:
simp [S_two, C_two]

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

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

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

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

Tactic:
have h₃ := C_add_two R (n + 1)