awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
m k : ℤ
zero : HMul.hMul (α := R[X]) 2 (T R m) * T R 0 = HAdd.hAdd (α := R[X]) (T R (m + 0)) (T R (m - 0))
one : HMul.hMul (α := R[X]) 2 (T R m) * T R 1 = HAdd.hAdd (α := R[X]) (T R (m + 1)) (T R (m - 1))
add_two :
  ∀ (k : ℕ)
    (ih1 :
      HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) =
        HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)))
    (ih2 :
      HMul.hMul (α := R[X]) 2 (T R m) * T R (↑k : ℤ) = HAdd.hAdd (α := R[X]) (T R (m + (↑k : ℤ))) (T R (m - (↑k : ℤ)))),
    HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (↑k : ℤ) 2) =
      HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) (T R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2))
neg_add_one :
  ∀ (k : ℕ)
    (ih1 :
      HMul.hMul (α := R[X]) 2 (T R m) * T R (-(↑k : ℤ)) =
        HAdd.hAdd (α := R[X]) (T R (m + -(↑k : ℤ))) (T R (m - -(↑k : ℤ))))
    (ih2 :
      HMul.hMul (α := R[X]) 2 (T R m) * T R (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1) =
        HAdd.hAdd (α := R[X]) (T R (m + HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1))
          (T R (m - HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) 1))),
    HMul.hMul (α := R[X]) 2 (T R m) * T R (HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1) =
      HAdd.hAdd (α := R[X]) (T R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) (T R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1))
⊢ HMul.hMul (α := R[X]) 2 (T R m) * T R k = HAdd.hAdd (α := R[X]) (T R (m + k)) (T R (m - k))

Tactic:
induction k using Polynomial.Chebyshev.induct with
  | zero => simp [two_mul]
  | one => rw [T_add_one, T_one]; ring
  | add_two k ih1 ih2 =>
    have h₁ := T_add_two R (m + k)
    have h₂ := T_sub_two R (m - k)
    have h₃ := T_add_two R k
    linear_combination (norm := ring_nf) 2 * T R m * h₃ - h₂ - h₁ - ih2 + 2 * (X : R[X]) * ih1
  | neg_add_one k ih1 ih2 =>
    have h₁ := T_add_two R (m + (-k - 1))
    have h₂ := T_sub_two R (m - (-k - 1))
    have h₃ := T_add_two R (-k - 1)
    linear_combination (norm := ring_nf) 2 * T R m * h₃ - h₂ - h₁ - ih2 + 2 * (X : R[X]) * ih1

Premises used: Polynomial.Chebyshev.T, Polynomial.Chebyshev.T_add_one, two_mul, Polynomial.Chebyshev.T_one, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
⊢ HMul.hMul (α := R[X]) (C R m) (C R 0) = HAdd.hAdd (α := R[X]) (C R (m + 0)) (C R (m - 0))

Tactic:
simp [mul_two]

Premises used: mul_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
one : HMul.hMul (α := R[X]) (C R m) X = HMul.hMul (α := R[X]) X (C R m) - C R (m - 1) + C R (m - 1)
⊢ HMul.hMul (α := R[X]) (C R m) (C R 1) = HAdd.hAdd (α := R[X]) (C R (m + 1)) (C R (m - 1))

Tactic:
rw [C_add_one, C_one]

Premises used: Polynomial.Chebyshev.C_one, Polynomial.Chebyshev.C_add_one
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
m : ℤ
⊢ HMul.hMul (α := R[X]) (C R m) X = HMul.hMul (α := R[X]) X (C R m) - C R (m - 1) + C R (m - 1)

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

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

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

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

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

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

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

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

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

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

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

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

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

Tactic:
induction k using Polynomial.Chebyshev.induct with
  | zero => simp [mul_two]
  | one => rw [C_add_one, C_one]; ring
  | add_two k ih1 ih2 =>
    have h₁ := C_add_two R (m + k)
    have h₂ := C_sub_two R (m - k)
    have h₃ := C_add_two R k
    linear_combination (norm := ring_nf) C R m * h₃ - h₂ - h₁ - ih2 + (X : R[X]) * ih1
  | neg_add_one k ih1 ih2 =>
    have h₁ := C_add_two R (m + (-k - 1))
    have h₂ := C_sub_two R (m - (-k - 1))
    have h₃ := C_add_two R (-k - 1)
    linear_combination (norm := ring_nf) C R m * h₃ - h₂ - h₁ - ih2 + (X : R[X]) * ih1

Premises used: Polynomial.Chebyshev.C_one, Polynomial.Chebyshev.C, Polynomial.Chebyshev.C_add_one, Polynomial.X, mul_two
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ Eq (α := R[X]) (T R (0 * n)) (comp (T R 0) (T R n))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
⊢ Eq (α := R[X]) (T R (1 * n)) (comp (T R 1) (T R n))

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

Tactic:
have h₁ := T_mul_T R ((m + 1) * n) n
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (comp (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (T R n))
ih2 : Eq (α := R[X]) (T R ((↑m : ℤ) * n)) (comp (T R (↑m : ℤ)) (T R n))
h₁ :
  HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) * T R n =
    HAdd.hAdd (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n + n)) (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n - n))
⊢ Eq.{u_1 + 1} (α := R[X]) ((fun (x : R[X]) ↦ x.comp (T R n)) (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)))
    ((fun (x : R[X]) ↦ x.comp (T R n)) (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) - T R (↑m : ℤ)))

Tactic:
have h₂ := congr_arg (comp · (T R n)) <| T_add_two R m
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (comp (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (T R n))
ih2 : Eq (α := R[X]) (T R ((↑m : ℤ) * n)) (comp (T R (↑m : ℤ)) (T R n))
h₁ :
  HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) * T R n =
    HAdd.hAdd (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n + n)) (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n - n))
h₂ :
  Eq.{u_1 + 1} (α := R[X]) ((fun (x : R[X]) ↦ x.comp (T R n)) (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)))
    ((fun (x : R[X]) ↦ x.comp (T R n)) (HMul.hMul (α := R[X]) 2 X * T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) - T R (↑m : ℤ)))
⊢ comp (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (T R n) =
    HMul.hMul (α := R[X]) (↑2 : R[X]) (T R n) * comp (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (T R n) -
      comp (T R (↑m : ℤ)) (T R n)

Tactic:
simp only [sub_comp, mul_comp, ofNat_comp, X_comp] at h₂

Premises used: Polynomial.X_comp, Polynomial.ofNat_comp, Polynomial.mul_comp, Polynomial.sub_comp
-- Module: Mathlib.RingTheory.Polynomial.Chebyshev
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (comp (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (T R n))
ih2 : Eq (α := R[X]) (T R ((↑m : ℤ) * n)) (comp (T R (↑m : ℤ)) (T R n))
h₁ :
  HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) * T R n =
    HAdd.hAdd (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n + n)) (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n - n))
h₂ :
  comp (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (T R n) =
    HMul.hMul (α := R[X]) (↑2 : R[X]) (T R n) * comp (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (T R n) -
      comp (T R (↑m : ℤ)) (T R n)
⊢ T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * n) +
        (HAdd.hAdd (α := R[X]) (T R ((↑m : ℤ) * n)) (comp (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (T R n)) +
            HMul.hMul (α := R[X]) 2 (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) * T R n +
          HMul.hMul (α := R[X]) 2 (T R n) * comp (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (T R n)) -
      (comp (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (T R n) +
        (comp (T R (↑m : ℤ)) (T R n) +
              (HMul.hMul (α := R[X]) (↑2 : R[X]) (T R n) * comp (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (T R n) -
                comp (T R (↑m : ℤ)) (T R n)) +
            HAdd.hAdd (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n + n))
              (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n - n)) +
          HMul.hMul (α := R[X]) 2 (T R n) * T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n))) =
    0

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

Tactic:
linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + 2 * T R n * ih1

Premises used: Polynomial.Chebyshev.T