awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℤ)
h₃ :
  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)
⊢ HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)) +
        (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2) + HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) +
              2 *
                (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) -
                  S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) +
            X *
              (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) +
                C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) +
          HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))) -
      (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) +
        (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) - C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) +
                X * (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)) +
              HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2)) +
            X * HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) +
          (HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))) =
    0

Tactic:
ring_nf
-- 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 : ℤ)
h₃ :
  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)
a :
  HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)) +
        (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2) + HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) +
              2 *
                (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) -
                  S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) +
            X *
              (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) +
                C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) +
          HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))) -
      (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1) +
        (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) - C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) +
                X * (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - S R (↑n : ℤ)) +
              HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 2)) +
            X * HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) +
          (HMul.hMul (α := R[X]) X (S R (↑n : ℤ)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))) =
    0
⊢ HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)

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

Premises used: Polynomial.X
-- 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)) =
    HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) + C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
ih2 :
  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)
⊢ 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_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)) =
    HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) + C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
ih2 :
  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)
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) =
    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)) =
    HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) + C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
ih2 :
  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)
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)
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 : ℤ)) 2) =
    HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) - C R (-(↑n : ℤ))

Tactic:
have h₃ := C_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)) =
    HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) + C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
ih2 :
  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)
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)
h₂ :
  S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) - S R (-(↑n : ℤ))
h₃ :
  C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) - C R (-(↑n : ℤ))
⊢ HMul.hMul (α := R[X]) 2 (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) +
        (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2) +
                2 * (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) - S R (-(↑n : ℤ))) +
              HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 2)) +
            HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)) +
          X * (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) + C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))) -
      (HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) + C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) +
        (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) - C R (-(↑n : ℤ)) +
                HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2)) +
              X *
                (HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) -
                  S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) +
            (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) +
              C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)) +
          X * HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)))) =
    0

Tactic:
ring_nf
-- 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)) =
    HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) + C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
ih2 :
  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)
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)
h₂ :
  S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) - S R (-(↑n : ℤ))
h₃ :
  C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2) =
    HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) - C R (-(↑n : ℤ))
a :
  HMul.hMul (α := R[X]) 2 (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) +
        (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2) +
                2 * (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) - S R (-(↑n : ℤ))) +
              HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 2)) +
            HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)) +
          X * (HMul.hMul (α := R[X]) X (S R (-(↑n : ℤ))) + C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1))) -
      (HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) + C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1) +
        (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) - C R (-(↑n : ℤ)) +
                HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 2)) +
              X *
                (HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) -
                  S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) +
            (HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) +
              C R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1 + 1)) +
          X * HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)))) =
    0
⊢ HMul.hMul (α := R[X]) 2 (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) =
    HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) + C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)

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

Premises used: Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
zero :
  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)
one :
  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)
add_two :
  ∀ (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)),
    HMul.hMul (α := R[X]) 2 (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)) =
      HMul.hMul (α := R[X]) X (S R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) + C R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2 + 1)
neg_add_one :
  ∀ (n : ℕ)
    (ih1 :
      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))
    (ih2 :
      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)),
    HMul.hMul (α := R[X]) 2 (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)) =
      HMul.hMul (α := R[X]) X (S R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) + C R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 + 1)
⊢ HMul.hMul (α := R[X]) 2 (S R (n + 1)) = HMul.hMul (α := R[X]) X (S R n) + C R (n + 1)

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

Premises used: two_mul, Polynomial.Chebyshev.S_two, Polynomial.X, Polynomial.Chebyshev.C_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ C R n + HMul.hMul (α := R[X]) 2 (S R (n - 1 + 1)) -
      (HMul.hMul (α := R[X]) 2 (S R n) - HMul.hMul (α := R[X]) X (S R (n - 1)) +
        (HMul.hMul (α := R[X]) X (S R (n - 1)) + C R (n - 1 + 1))) =
    0

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

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

Premises used: Polynomial.Chebyshev.S_eq_X_mul_S_add_C, HSub.hSub, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
⊢ map f (T R 0) = T R' 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
⊢ map f (T R 1) = T R' 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (T R (↑n : ℤ)) = T R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
add_two₁ :
  map f (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
add_two₂ :
  map f 2 * map f X * map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
add_two₃ :
  2 * map f X * map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
add_two₄ :
  HMul.hMul (α := R'[X]) 2 X * map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
add_two₅ :
  HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - map f (T R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - T R' (↑n : ℤ)
⊢ map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)

Tactic:
simp_rw [T_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X,
      ih1, ih2]

Premises used: Polynomial.map_mul, Polynomial.map_X, Polynomial.map_ofNat, Polynomial.map_sub, Polynomial.Chebyshev.T_add_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (T R (-(↑n : ℤ))) = T R' (-(↑n : ℤ))
ih2 : map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ)) - T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  map f (HMul.hMul (α := R[X]) 2 X * T R (-(↑n : ℤ))) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₂ :
  map f 2 * map f X * map f (T R (-(↑n : ℤ))) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₃ :
  2 * map f X * map f (T R (-(↑n : ℤ))) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₄ :
  HMul.hMul (α := R'[X]) 2 X * map f (T R (-(↑n : ℤ))) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₅ :
  HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * T R' (-(↑n : ℤ)) - T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = T R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)

Tactic:
simp_rw [T_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]

Premises used: Polynomial.map_mul, Polynomial.map_X, Polynomial.map_ofNat, Polynomial.Chebyshev.T_sub_one, Polynomial.map_sub
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℤ
zero : map f (T R 0) = T R' 0
one : map f (T R 1) = T R' 1
add_two :
  ∀ (n : ℕ) (ih1 : map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1))
    (ih2 : map f (T R (↑n : ℤ)) = T R' (↑n : ℤ)),
    map f (T R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = T R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)
neg_add_one :
  ∀ (n : ℕ) (ih1 : map f (T R (-(↑n : ℤ))) = T R' (-(↑n : ℤ)))
    (ih2 : map f (T R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = T R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)),
    map f (T R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = T R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (T R n) = T R' n

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [T_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X,
      ih1, ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [T_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]

Premises used: Polynomial.map_mul, Polynomial.map_X, Polynomial.map_ofNat, Polynomial.Chebyshev.T_sub_one, Polynomial.map_sub, Polynomial.Chebyshev.T_add_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
⊢ map f (U R 0) = U R' 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
⊢ map f (U R 1) = U R' 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
ih2 : map f (U R (↑n : ℤ)) = U R' (↑n : ℤ)
add_two :
  map f (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R' (↑n : ℤ)
add_two₁ :
  map f (HMul.hMul (α := R[X]) 2 X * U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (U R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R' (↑n : ℤ)
add_two₂ :
  map f 2 * map f X * map f (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (U R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R' (↑n : ℤ)
add_two₃ :
  2 * map f X * map f (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (U R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R' (↑n : ℤ)
add_two₄ :
  HMul.hMul (α := R'[X]) 2 X * map f (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) - map f (U R (↑n : ℤ)) =
    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) - map f (U R (↑n : ℤ)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) - U R' (↑n : ℤ)
⊢ map f (U R (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = U R' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)

Tactic:
simp_rw [U_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]

Premises used: Polynomial.map_mul, Polynomial.map_X, Polynomial.map_ofNat, Polynomial.Chebyshev.U_add_two, Polynomial.map_sub
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommRing R'
f : R →+* R'
n : ℕ
ih1 : map f (U R (-(↑n : ℤ))) = U R' (-(↑n : ℤ))
ih2 : map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one :
  map f (HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ)) - U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₁ :
  map f (HMul.hMul (α := R[X]) 2 X * U R (-(↑n : ℤ))) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₂ :
  map f 2 * map f X * map f (U R (-(↑n : ℤ))) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₃ :
  2 * map f X * map f (U R (-(↑n : ℤ))) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
neg_add_one₄ :
  HMul.hMul (α := R'[X]) 2 X * map f (U R (-(↑n : ℤ))) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    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 : ℤ)) - map f (U R (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) =
    HMul.hMul (α := R'[X]) 2 X * U R' (-(↑n : ℤ)) - U R' (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)
⊢ map f (U R (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = U R' (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)

Tactic:
simp_rw [U_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1,
      ih2]

Premises used: Polynomial.map_mul, Polynomial.Chebyshev.U_sub_one, Polynomial.map_X, Polynomial.map_ofNat, Polynomial.map_sub