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 n : ℤ
zero : Eq (α := R[X]) (T R (0 * n)) (comp (T R 0) (T R n))
one : Eq (α := R[X]) (T R (1 * n)) (comp (T R 1) (T R n))
⊢ Eq (α := R[X]) (T R (m * n)) (comp (T R m) (T R n))
have add_two : ∀ (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))
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))
one : Eq (α := R[X]) (T R (1 * n)) (comp (T R 1) (T R n))
add_two :
  ∀ (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))
⊢ Eq (α := R[X]) (T R (m * n)) (comp (T R m) (T R n))
have neg_add_one : ∀ (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))
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 (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℤ
m : ℕ
ih1 : Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n))
ih2 : Eq (α := R[X]) (C R ((↑m : ℤ) * n)) (comp (C R (↑m : ℤ)) (C R n))
⊢ Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (C R n))
have h₁ : HMul.hMul (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (C R n) =
  HAdd.hAdd (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n + n)) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n - n))
Tactic: have h₁ := C_mul_C 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]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n))
ih2 : Eq (α := R[X]) (C R ((↑m : ℤ) * n)) (comp (C R (↑m : ℤ)) (C R n))
h₁ :
  HMul.hMul (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (C R n) =
    HAdd.hAdd (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n + n)) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n - n))
⊢ Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (C R n))
have h₂ : Eq.{u_1 + 1} (α := R[X]) ((fun (x : R[X]) ↦ x.comp (C R n)) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)))
  ((fun (x : R[X]) ↦ x.comp (C R n)) (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) - C R (↑m : ℤ)))
Tactic: have h₂ := congr_arg (comp · (C R n)) <| C_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]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n))
ih2 : Eq (α := R[X]) (C R ((↑m : ℤ) * n)) (comp (C R (↑m : ℤ)) (C R n))
h₁ :
  HMul.hMul (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (C R n) =
    HAdd.hAdd (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n + n)) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n - n))
h₂ :
  Eq.{u_1 + 1} (α := R[X]) ((fun (x : R[X]) ↦ x.comp (C R n)) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)))
    ((fun (x : R[X]) ↦ x.comp (C R n)) (HMul.hMul (α := R[X]) X (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) - C R (↑m : ℤ)))
⊢ Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (C R n))
have h₃ : comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (C R n) =
  HMul.hMul (α := R[X]) (C R n) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n)) - comp (C R (↑m : ℤ)) (C R n)
Tactic: simp only [sub_comp, mul_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]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n))
ih2 : Eq (α := R[X]) (C R ((↑m : ℤ) * n)) (comp (C R (↑m : ℤ)) (C R n))
h₁ :
  HMul.hMul (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (C R n) =
    HAdd.hAdd (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n + n)) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n - n))
h₂ :
  comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (C R n) =
    HMul.hMul (α := R[X]) (C R n) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n)) - comp (C R (↑m : ℤ)) (C R n)
⊢ Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (C R n))
have a : C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * n) +
      (HAdd.hAdd (α := R[X]) (C R ((↑m : ℤ) * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (C R n)) +
          HMul.hMul (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (C R n) +
        HMul.hMul (α := R[X]) (C R n) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n))) -
    (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (C R n) +
      (comp (C R (↑m : ℤ)) (C R n) +
            (HMul.hMul (α := R[X]) (C R n) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n)) -
              comp (C R (↑m : ℤ)) (C R n)) +
          HAdd.hAdd (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n + n))
            (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n - n)) +
        HMul.hMul (α := R[X]) (C R n) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)))) =
  0
Tactic: linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + C 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]) (C R (-(↑m : ℤ) * n)) (comp (C R (-(↑m : ℤ))) (C R n))
ih2 :
  Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (C R n))
⊢ Eq (α := R[X]) (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (C R n))
have h₁ : HMul.hMul (α := R[X]) (C R (-(↑m : ℤ) * n)) (C R n) =
  HAdd.hAdd (α := R[X]) (C R (-(↑m : ℤ) * n + n)) (C R (-(↑m : ℤ) * n - n))
Tactic: have h₁ := C_mul_C 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]) (C R (-(↑m : ℤ) * n)) (comp (C R (-(↑m : ℤ))) (C R n))
ih2 :
  Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (C R n))
h₁ :
  HMul.hMul (α := R[X]) (C R (-(↑m : ℤ) * n)) (C R n) =
    HAdd.hAdd (α := R[X]) (C R (-(↑m : ℤ) * n + n)) (C R (-(↑m : ℤ) * n - n))
⊢ Eq (α := R[X]) (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (C R n))
have h₂ : Eq.{u_1 + 1} (α := R[X]) ((fun (x : R[X]) ↦ x.comp (C R n)) (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)))
  ((fun (x : R[X]) ↦ x.comp (C R n))
    (HMul.hMul (α := R[X]) X (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) - C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)))
Tactic: have h₂ := congr_arg (comp · (C R n)) <| C_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]) (C R (-(↑m : ℤ) * n)) (comp (C R (-(↑m : ℤ))) (C R n))
ih2 :
  Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (C R n))
h₁ :
  HMul.hMul (α := R[X]) (C R (-(↑m : ℤ) * n)) (C R n) =
    HAdd.hAdd (α := R[X]) (C R (-(↑m : ℤ) * n + n)) (C R (-(↑m : ℤ) * n - n))
h₂ :
  Eq.{u_1 + 1} (α := R[X]) ((fun (x : R[X]) ↦ x.comp (C R n)) (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)))
    ((fun (x : R[X]) ↦ x.comp (C R n))
      (HMul.hMul (α := R[X]) X (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) - C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)))
⊢ Eq (α := R[X]) (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (C R n))
have h₃ : comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)) (C R n) =
  HMul.hMul (α := R[X]) (C R n) (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) (C R n)) -
    comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (C R n)
Tactic: simp only [sub_comp, mul_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]) (C R (-(↑m : ℤ) * n)) (comp (C R (-(↑m : ℤ))) (C R n))
ih2 :
  Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (C R n))
h₁ :
  HMul.hMul (α := R[X]) (C R (-(↑m : ℤ) * n)) (C R n) =
    HAdd.hAdd (α := R[X]) (C R (-(↑m : ℤ) * n + n)) (C R (-(↑m : ℤ) * n - n))
h₂ :
  comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)) (C R n) =
    HMul.hMul (α := R[X]) (C R n) (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) (C R n)) -
      comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (C R n)
⊢ Eq (α := R[X]) (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (C R n))
have a : C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 * n) +
      (HAdd.hAdd (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n))
            (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 2)) (C R n)) +
          HMul.hMul (α := R[X]) (C R (-(↑m : ℤ) * n)) (C R n) +
        HMul.hMul (α := R[X]) (C R n) (comp (C R (-(↑m : ℤ))) (C R n))) -
    (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (C R n) +
      (comp (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (C R n) +
            (HMul.hMul (α := R[X]) (C R n) (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 + 1)) (C R n)) -
              comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (C R n)) +
          HAdd.hAdd (α := R[X]) (C R (-(↑m : ℤ) * n + n)) (C R (-(↑m : ℤ) * n - n)) +
        HMul.hMul (α := R[X]) (C R n) (C R (-(↑m : ℤ) * n)))) =
  0
Tactic: linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + C 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]) (C R (m * n)) (comp (C R m) (C R n))
have zero : Eq (α := R[X]) (C R (0 * n)) (comp (C R 0) (C R n))
Tactic: induction m using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two m ih1 ih2 =>
    have h₁ := C_mul_C R ((m + 1) * n) n
    have h₂ := congr_arg (comp · (C R n)) <| C_add_two R m
    simp only [sub_comp, mul_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + C R n * ih1
  | neg_add_one m ih1 ih2 =>
    have h₁ := C_mul_C R ((-m) * n) n
    have h₂ := congr_arg (comp · (C R n)) <| C_add_two R (-m - 1)
    simp only [sub_comp, mul_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + C 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]) (C R (0 * n)) (comp (C R 0) (C R n))
⊢ Eq (α := R[X]) (C R (m * n)) (comp (C R m) (C R n))
have one : Eq (α := R[X]) (C R (1 * n)) (comp (C R 1) (C R n))
Tactic: induction m using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two m ih1 ih2 =>
    have h₁ := C_mul_C R ((m + 1) * n) n
    have h₂ := congr_arg (comp · (C R n)) <| C_add_two R m
    simp only [sub_comp, mul_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + C R n * ih1
  | neg_add_one m ih1 ih2 =>
    have h₁ := C_mul_C R ((-m) * n) n
    have h₂ := congr_arg (comp · (C R n)) <| C_add_two R (-m - 1)
    simp only [sub_comp, mul_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + C 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]) (C R (0 * n)) (comp (C R 0) (C R n))
one : Eq (α := R[X]) (C R (1 * n)) (comp (C R 1) (C R n))
⊢ Eq (α := R[X]) (C R (m * n)) (comp (C R m) (C R n))
have add_two : ∀ (m : ℕ)
  (ih1 : Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n)))
  (ih2 : Eq (α := R[X]) (C R ((↑m : ℤ) * n)) (comp (C R (↑m : ℤ)) (C R n))),
  Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (C R n))
Tactic: induction m using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two m ih1 ih2 =>
    have h₁ := C_mul_C R ((m + 1) * n) n
    have h₂ := congr_arg (comp · (C R n)) <| C_add_two R m
    simp only [sub_comp, mul_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + C R n * ih1
  | neg_add_one m ih1 ih2 =>
    have h₁ := C_mul_C R ((-m) * n) n
    have h₂ := congr_arg (comp · (C R n)) <| C_add_two R (-m - 1)
    simp only [sub_comp, mul_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + C 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]) (C R (0 * n)) (comp (C R 0) (C R n))
one : Eq (α := R[X]) (C R (1 * n)) (comp (C R 1) (C R n))
add_two :
  ∀ (m : ℕ)
    (ih1 :
      Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) (C R n)))
    (ih2 : Eq (α := R[X]) (C R ((↑m : ℤ) * n)) (comp (C R (↑m : ℤ)) (C R n))),
    Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * n)) (comp (C R (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2)) (C R n))
⊢ Eq (α := R[X]) (C R (m * n)) (comp (C R m) (C R n))
have neg_add_one : ∀ (m : ℕ) (ih1 : Eq (α := R[X]) (C R (-(↑m : ℤ) * n)) (comp (C R (-(↑m : ℤ))) (C R n)))
  (ih2 :
    Eq (α := R[X]) (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * n))
      (comp (C R (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) (C R n))),
  Eq (α := R[X]) (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1 * n)) (comp (C R (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1)) (C R n))
Tactic: induction m using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two m ih1 ih2 =>
    have h₁ := C_mul_C R ((m + 1) * n) n
    have h₂ := congr_arg (comp · (C R n)) <| C_add_two R m
    simp only [sub_comp, mul_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + C R n * ih1
  | neg_add_one m ih1 ih2 =>
    have h₁ := C_mul_C R ((-m) * n) n
    have h₂ := congr_arg (comp · (C R n)) <| C_add_two R (-m - 1)
    simp only [sub_comp, mul_comp, X_comp] at h₂
    linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + C R n * ih1
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Monic
r : R
q : R[X]
h : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) q
⊢ r * q.coeff p.natDegree = 1
have rwa : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) q).coeff p.natDegree = 1
Tactic: rwa [← coeff_C_mul, ← h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Monic
r : R
q : R[X]
h : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) q
rwa : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) q).coeff p.natDegree = 1
⊢ r * q.coeff p.natDegree = 1
have rwa₁ : p.coeff p.natDegree = 1
Tactic: rwa [← coeff_C_mul, ← h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
r : R
q : R[X]
hq : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) q
⊢ IsUnit r
have suffices : ¬IsUnit q
Tactic: suffices ¬IsUnit q by simpa using ((hp.2 hq).resolve_right this).map Polynomial.constantCoeff
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
r : R
q : R[X]
hq : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) q
H : IsUnit q
⊢ False
have hr : r ≠ 0
Tactic: have hr : r ≠ 0 := by rintro rfl; simp_all
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : NoZeroDivisors R
p : R[X]
hp : Irreducible p
hp' : p.natDegree ≠ 0
r : R
q : R[X]
hq : p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) q
H : IsUnit q
hr : r ≠ 0
⊢ False
have obtain : ∀ (s : R) (hs : IsUnit s)
  (hq : p = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) ((C : (a : R) → R[X]) s : R[X]))
  (H : IsUnit (M := R[X]) ((C : (a : R) → R[X]) s : R[X])), False
Tactic: obtain ⟨s, hs, rfl⟩ := Polynomial.isUnit_iff.mp H
Cleared hypotheses: q, hq, H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
n : ℕ
⊢ p.content ∣ p.coeff n
have pos : ∀ (h : n ∈ p.support), p.content ∣ p.coeff n
Tactic: by_cases h : n ∈ p.support
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
n : ℕ
pos : ∀ (h : n ∈ p.support), p.content ∣ p.coeff n
⊢ p.content ∣ p.coeff n
have neg : ∀ (h : n ∉ p.support), p.content ∣ p.coeff n
Tactic: by_cases h : n ∈ p.support
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : n ∉ p.support
⊢ p.content ∣ p.coeff n
have h₁ : p.coeff n = 0
Tactic: rw [mem_support_iff, Classical.not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ p.content ∣ p.coeff n
have neg : p.content ∣ 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
⊢ Eq (α := R) ((support.{u_1} (R := R) ((C : (a : R) → R[X]) r)).gcd (coeff ((C : (a : R) → R[X]) r)) : R)
    ((normalize : (a : R) → R) r : R)
have pos : ∀ (h0 : r = 0),
  Eq (α := R) ((support.{u_1} (R := R) ((C : (a : R) → R[X]) r)).gcd (coeff ((C : (a : R) → R[X]) r)) : R)
    ((normalize : (a : R) → R) r : R)
Tactic: by_cases h0 : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
pos :
  ∀ (h0 : r = 0),
    Eq (α := R) ((support.{u_1} (R := R) ((C : (a : R) → R[X]) r)).gcd (coeff ((C : (a : R) → R[X]) r)) : R)
      ((normalize : (a : R) → R) r : R)
⊢ Eq (α := R) ((support.{u_1} (R := R) ((C : (a : R) → R[X]) r)).gcd (coeff ((C : (a : R) → R[X]) r)) : R)
    ((normalize : (a : R) → R) r : R)
have neg : ∀ (h0 : ¬r = 0),
  Eq (α := R) ((support.{u_1} (R := R) ((C : (a : R) → R[X]) r)).gcd (coeff ((C : (a : R) → R[X]) r)) : R)
    ((normalize : (a : R) → R) r : R)
Tactic: by_cases h0 : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ Eq (α := R) ((support.{u_1} (R := R) ((C : (a : R) → R[X]) r)).gcd (coeff ((C : (a : R) → R[X]) r)) : R)
    ((normalize : (a : R) → R) r : R)
have h : support.{u_1} (R := R) ((C : (a : R) → R[X]) r) = {0}
Tactic: have h : (C r).support = {0} := support_monomial _ h0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
⊢ Eq.{u_1 + 1} (α := R) (content 0) 0
have rw : Eq.{u_1 + 1} (α := R) (content ((C : (a : R) → R[X]) 0)) 0
Tactic: rw [← C_0, content_C, normalize_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
rw : Eq.{u_1 + 1} (α := R) (content ((C : (a : R) → R[X]) 0)) 0
⊢ Eq.{u_1 + 1} (α := R) (content 0) 0
have rw₁ : Eq.{u_1 + 1} (α := R) ((normalize : (a : R) → R) 0 : R) (0 : R)
Tactic: rw [← C_0, content_C, normalize_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
rw : Eq.{u_1 + 1} (α := R) (content ((C : (a : R) → R[X]) 0)) 0
rw₁ : Eq.{u_1 + 1} (α := R) ((normalize : (a : R) → R) 0 : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) (content 0) 0
have rw₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← C_0, content_C, normalize_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
⊢ Eq.{u_1 + 1} (α := R) (content 1) 1
have rw : Eq.{u_1 + 1} (α := R) (content ((C : (a : R) → R[X]) 1)) 1
Tactic: rw [← C_1, content_C, normalize_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
rw : Eq.{u_1 + 1} (α := R) (content ((C : (a : R) → R[X]) 1)) 1
⊢ Eq.{u_1 + 1} (α := R) (content 1) 1
have rw₁ : Eq.{u_1 + 1} (α := R) ((normalize : (a : R) → R) 1 : R) (1 : R)
Tactic: rw [← C_1, content_C, normalize_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
rw : Eq.{u_1 + 1} (α := R) (content ((C : (a : R) → R[X]) 1)) 1
rw₁ : Eq.{u_1 + 1} (α := R) ((normalize : (a : R) → R) 1 : R) (1 : R)
⊢ Eq.{u_1 + 1} (α := R) (content 1) 1
have rw₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [← C_1, content_C, normalize_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
⊢ (Multiset.map (X * p).coeff (X * p).support.val).gcd = (Multiset.map p.coeff p.support.val).gcd
have refine : Multiset.map (X * p).coeff (X * p).support.val = Multiset.map p.coeff p.support.val
Tactic: refine congr rfl ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
⊢ (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ } p.support
have h : ∀ (a : ℕ), a ∈ (X * p).support ↔ a ∈ Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ } p.support
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
a : ℕ
⊢ a ∈ (X * p).support ↔ a ∈ Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ } p.support
have h : ¬(X * p).coeff a = 0 ↔ ∃ (a_1 : ℕ), ¬p.coeff a_1 = 0 ∧ a_1.succ = a
Tactic: simp only [Finset.mem_map, Function.Embedding.coeFn_mk, Ne, mem_support_iff]