awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)) =
    HAdd.hAdd (α := R[X]) (C R (m + HAdd.hAdd (α := ℤ) (↑k : ℤ) 2)) (C R (m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 2))
have 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
Tactic: linear_combination (norm := ring_nf) C R m * h₃ - h₂ - h₁ - ih2 + (X : R[X]) * ih1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
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))
⊢ 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))
have 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)
Tactic: have h₁ := C_add_two R (m + (-k - 1))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
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)
⊢ 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))
have 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)
Tactic: have h₂ := C_sub_two R (m - (-k - 1))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
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)
⊢ 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))
have 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)
Tactic: have h₃ := C_add_two R (-k - 1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)) =
    HAdd.hAdd (α := R[X]) (C R (m + HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1)) (C R (m - HSub.hSub (α := ℤ) (-(↑k : ℤ)) 1))
have 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
Tactic: linear_combination (norm := ring_nf) C R m * h₃ - h₂ - h₁ - ih2 + (X : R[X]) * ih1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
m k : ℤ
⊢ HMul.hMul (α := R[X]) (C R m) (C R k) = HAdd.hAdd (α := R[X]) (C R (m + k)) (C R (m - k))
have zero : HMul.hMul (α := R[X]) (C R m) (C R 0) = HAdd.hAdd (α := R[X]) (C R (m + 0)) (C R (m - 0))
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
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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))
⊢ HMul.hMul (α := R[X]) (C R m) (C R k) = HAdd.hAdd (α := R[X]) (C R (m + k)) (C R (m - k))
have one : HMul.hMul (α := R[X]) (C R m) (C R 1) = HAdd.hAdd (α := R[X]) (C R (m + 1)) (C R (m - 1))
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
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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))
⊢ HMul.hMul (α := R[X]) (C R m) (C R k) = HAdd.hAdd (α := R[X]) (C R (m + k)) (C R (m - k))
have 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))
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
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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))
⊢ HMul.hMul (α := R[X]) (C R m) (C R k) = HAdd.hAdd (α := R[X]) (C R (m + k)) (C R (m - k))
have 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))
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
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
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))
⊢ Eq (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * n)) (comp (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (T R n))
have 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))
Tactic: have h₁ := T_mul_T R ((m + 1) * n) n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
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 (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * n)) (comp (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (T R n))
have 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 : ℤ)))
Tactic: have h₂ := congr_arg (comp · (T R n)) <| T_add_two R m
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
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 : ℤ)))
⊢ Eq (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * n)) (comp (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (T R n))
have 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)
Tactic: simp only [sub_comp, mul_comp, ofNat_comp, X_comp] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
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)
⊢ Eq (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * n)) (comp (T R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (T R n))
have 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
Tactic: linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + 2 * T R n * ih1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (T R (-(↑m : ℤ) * n)) (comp (T R (-(↑m : ℤ))) (T R n))
ih2 :
  Eq (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (T R n))
⊢ Eq (α := R[X]) (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (T R n))
have h₁ : HMul.hMul (α := R[X]) 2 (T R (-(↑m : ℤ) * n)) * T R n =
  HAdd.hAdd (α := R[X]) (T R (-(↑m : ℤ) * n + n)) (T R (-(↑m : ℤ) * n - n))
Tactic: have h₁ := T_mul_T R ((-m) * n) n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (T R (-(↑m : ℤ) * n)) (comp (T R (-(↑m : ℤ))) (T R n))
ih2 :
  Eq (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (T R n))
h₁ :
  HMul.hMul (α := R[X]) 2 (T R (-(↑m : ℤ) * n)) * T R n =
    HAdd.hAdd (α := R[X]) (T R (-(↑m : ℤ) * n + n)) (T R (-(↑m : ℤ) * n - n))
⊢ Eq (α := R[X]) (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (T R n))
have h₂ : Eq.{u_1 + 1} (α := R[X]) ((fun (x : R[X]) ↦ x.comp (T R n)) (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)))
  ((fun (x : R[X]) ↦ x.comp (T R n))
    (HMul.hMul (α := R[X]) 2 X * T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1) - T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)))
Tactic: have h₂ := congr_arg (comp · (T R n)) <| T_add_two R (-m - 1)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (T R (-(↑m : ℤ) * n)) (comp (T R (-(↑m : ℤ))) (T R n))
ih2 :
  Eq (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (T R n))
h₁ :
  HMul.hMul (α := R[X]) 2 (T R (-(↑m : ℤ) * n)) * T R n =
    HAdd.hAdd (α := R[X]) (T R (-(↑m : ℤ) * n + n)) (T R (-(↑m : ℤ) * n - n))
h₂ :
  Eq.{u_1 + 1} (α := R[X]) ((fun (x : R[X]) ↦ x.comp (T R n)) (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)))
    ((fun (x : R[X]) ↦ x.comp (T R n))
      (HMul.hMul (α := R[X]) 2 X * T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1) - T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)))
⊢ Eq (α := R[X]) (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (T R n))
have h₃ : comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)) (T R n) =
  HMul.hMul (α := R[X]) (↑2 : R[X]) (T R n) * comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) (T R n) -
    comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (T R n)
Tactic: simp only [sub_comp, mul_comp, ofNat_comp, X_comp] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (T R (-(↑m : ℤ) * n)) (comp (T R (-(↑m : ℤ))) (T R n))
ih2 :
  Eq (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (T R n))
h₁ :
  HMul.hMul (α := R[X]) 2 (T R (-(↑m : ℤ) * n)) * T R n =
    HAdd.hAdd (α := R[X]) (T R (-(↑m : ℤ) * n + n)) (T R (-(↑m : ℤ) * n - n))
h₂ :
  comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)) (T R n) =
    HMul.hMul (α := R[X]) (↑2 : R[X]) (T R n) * comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) (T R n) -
      comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (T R n)
⊢ Eq (α := R[X]) (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (T R n))
have a : T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 * n) +
      (HAdd.hAdd (α := R[X]) (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n))
            (comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)) (T R n)) +
          HMul.hMul (α := R[X]) 2 (T R (-(↑m : ℤ) * n)) * T R n +
        HMul.hMul (α := R[X]) 2 (T R n) * comp (T R (-(↑m : ℤ))) (T R n)) -
    (comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (T R n) +
      (comp (T R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (T R n) +
            (HMul.hMul (α := R[X]) (↑2 : R[X]) (T R n) * comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) (T R n) -
              comp (T R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (T R n)) +
          HAdd.hAdd (α := R[X]) (T R (-(↑m : ℤ) * n + n)) (T R (-(↑m : ℤ) * n - n)) +
        HMul.hMul (α := R[X]) 2 (T R n) * T R (-(↑m : ℤ) * n))) =
  0
Tactic: linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + 2 * T R n * ih1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
m n : ℤ
⊢ Eq (α := R[X]) (T R (m * n)) (comp (T R m) (T R n))
have zero : Eq (α := R[X]) (T R (0 * n)) (comp (T R 0) (T R n))
Tactic: induction m using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two m ih1 ih2 =>
    have h₁ := T_mul_T R ((m + 1) * n) n
    have h₂ := congr_arg (comp · (T R n)) <| T_add_two R m
    simp only [sub_comp, mul_comp, ofNat_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + 2 * T R n * ih1
  | neg_add_one m ih1 ih2 =>
    have h₁ := T_mul_T R ((-m) * n) n
    have h₂ := congr_arg (comp · (T R n)) <| T_add_two R (-m - 1)
    simp only [sub_comp, mul_comp, ofNat_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + 2 * T R n * ih1
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Chebyshev (goal)
Goal:
R : Type u_1
inst : CommRing R
m n : ℤ
zero : Eq (α := R[X]) (T R (0 * n)) (comp (T R 0) (T R n))
⊢ Eq (α := R[X]) (T R (m * n)) (comp (T R m) (T R n))
have one : Eq (α := R[X]) (T R (1 * n)) (comp (T R 1) (T R n))
Tactic: induction m using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two m ih1 ih2 =>
    have h₁ := T_mul_T R ((m + 1) * n) n
    have h₂ := congr_arg (comp · (T R n)) <| T_add_two R m
    simp only [sub_comp, mul_comp, ofNat_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + 2 * T R n * ih1
  | neg_add_one m ih1 ih2 =>
    have h₁ := T_mul_T R ((-m) * n) n
    have h₂ := congr_arg (comp · (T R n)) <| T_add_two R (-m - 1)
    simp only [sub_comp, mul_comp, ofNat_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + 2 * T R n * ih1
Cleared hypotheses: m