awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
⊢ ¬(X * p).coeff a = 0 ↔ ∃ (a_1 : ℕ), ¬p.coeff a_1 = 0 ∧ a_1.succ = a
have h : ¬(X * p).coeff 0 = 0 ↔ ∃ (a : ℕ), ¬p.coeff a = 0 ∧ a.succ = 0
Tactic: rcases a with - | a
Cleared hypotheses: 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 : ℕ
h : ¬(X * p).coeff 0 = 0 ↔ ∃ (a : ℕ), ¬p.coeff a = 0 ∧ a.succ = 0
⊢ ¬(X * p).coeff a = 0 ↔ ∃ (a_1 : ℕ), ¬p.coeff a_1 = 0 ∧ a_1.succ = a
have h₁ : ∀ (a : ℕ), ¬(X * p).coeff (a + 1) = 0 ↔ ∃ (a_1 : ℕ), ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1
Tactic: rcases a with - | a
Cleared hypotheses: 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 : ℕ
⊢ ¬(X * p).coeff (a + 1) = 0 ↔ ∃ (a_1 : ℕ), ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1
have h : ¬p.coeff a = 0 ↔ ∃ (a_1 : ℕ), ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1
Tactic: rw [mul_comm, coeff_mul_X]
-- 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 : ℕ
⊢ ¬p.coeff a = 0 ↔ ∃ (a_1 : ℕ), ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1
have h : ¬p.coeff a = 0 → ∃ (a_2 : ℕ), ¬p.coeff a_2 = 0 ∧ a_2.succ = a + 1
Tactic: constructor
-- 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 : ℕ
h : ¬p.coeff a = 0 → ∃ (a_2 : ℕ), ¬p.coeff a_2 = 0 ∧ a_2.succ = a + 1
⊢ ¬p.coeff a = 0 ↔ ∃ (a_1 : ℕ), ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1
have h₁ : (∃ (a_1 : ℕ), ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1) → ¬p.coeff a = 0
Tactic: constructor
-- 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 : ℕ
h : ¬p.coeff a = 0
w : ℕ
⊢ ∃ (a_1 : ℕ), ¬p.coeff a_1 = 0 ∧ a_1.succ = a + 1
have h₁ : ¬p.coeff a = 0 ∧ a.succ = a + 1
Tactic: use a
-- 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]
⊢ Multiset.map (X * p).coeff (X * p).support.val = Multiset.map p.coeff p.support.val
have h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ } p.support
Tactic: have h : (X * p).support = p.support.map ⟨Nat.succ, Nat.succ_injective⟩ := by
    ext a
    simp only [Finset.mem_map, Function.Embedding.coeFn_mk, Ne, mem_support_iff]
    rcases a with - | a
    · simp
    rw [mul_comm, coeff_mul_X]
    constructor
    · intro h
      use a
    · rintro ⟨b, ⟨h1, h2⟩⟩
      rw [← Nat.succ_injective h2]
      apply h1
-- 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]
h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ } p.support
⊢ Multiset.map (X * p).coeff (X * p).support.val = Multiset.map p.coeff p.support.val
have rw : Multiset.map (X * p).coeff (Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ } p.support).val =
  Multiset.map p.coeff p.support.val
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
k : ℕ
hi : (HPow.hPow (α := R[X]) X k).content = 1
⊢ (HPow.hPow (α := R[X]) X (k + 1)).content = 1
have succ : (X * HPow.hPow (α := R[X]) X k).content = 1
Tactic: rw [pow_succ', content_X_mul, hi]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
k : ℕ
hi : (HPow.hPow (α := R[X]) X k).content = 1
succ : (X * HPow.hPow (α := R[X]) X k).content = 1
succ₁ : (HPow.hPow (α := R[X]) X k).content = 1
⊢ (HPow.hPow (α := R[X]) X (k + 1)).content = 1
have succ₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [pow_succ', content_X_mul, hi]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
k : ℕ
⊢ (HPow.hPow (α := R[X]) X k).content = 1
have zero : (HPow.hPow (α := R[X]) (β := ℕ) X 0).content = 1
Tactic: induction k with
  | zero => simp
  | succ k hi => rw [pow_succ', content_X_mul, hi]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
k : ℕ
zero : (HPow.hPow (α := R[X]) (β := ℕ) X 0).content = 1
⊢ (HPow.hPow (α := R[X]) X k).content = 1
have succ : ∀ (k : ℕ) (hi : (HPow.hPow (α := R[X]) X k).content = 1), (HPow.hPow (α := R[X]) X (k + 1)).content = 1
Tactic: induction k with
  | zero => simp
  | succ k hi => rw [pow_succ', content_X_mul, hi]
Cleared hypotheses: k
-- 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 X) 1
have rw : (HMul.hMul (α := R[X]) X 1).content = 1
Tactic: rw [← mul_one X, content_X_mul, content_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
rw : (HMul.hMul (α := R[X]) X 1).content = 1
⊢ Eq.{u_1 + 1} (α := R) (content X) 1
have rw₁ : Eq.{u_1 + 1} (α := R) (content 1) 1
Tactic: rw [← mul_one X, content_X_mul, content_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
rw : (HMul.hMul (α := R[X]) X 1).content = 1
rw₁ : Eq.{u_1 + 1} (α := R) (content 1) 1
⊢ Eq.{u_1 + 1} (α := R) (content X) 1
have rw₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [← mul_one X, content_X_mul, content_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
p : R[X]
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).content =
    HMul.hMul (α := R) ((normalize : (a : R) → R) r : R) p.content
have pos : ∀ (h0 : r = 0),
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).content =
    HMul.hMul (α := R) ((normalize : (a : R) → R) r : R) p.content
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
p : R[X]
pos :
  ∀ (h0 : r = 0),
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).content =
      HMul.hMul (α := R) ((normalize : (a : R) → R) r : R) p.content
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).content =
    HMul.hMul (α := R) ((normalize : (a : R) → R) r : R) p.content
have neg : ∀ (h0 : ¬r = 0),
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).content =
    HMul.hMul (α := R) ((normalize : (a : R) → R) r : R) p.content
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
p : R[X]
h0 : ¬r = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support.gcd
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).coeff =
    HMul.hMul (α := R) ((normalize : (a : R) → R) r : R) p.content
have neg : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support.gcd
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).coeff =
  HMul.hMul (α := R) ((normalize : (a : R) → R) r : R) (p.support.gcd p.coeff)
Tactic: rw [content]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support.gcd
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).coeff =
    HMul.hMul (α := R) ((normalize : (a : R) → R) r : R) (p.support.gcd p.coeff)
have neg : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support.gcd
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).coeff =
  p.support.gcd fun (x : ℕ) ↦ r * p.coeff x
Tactic: rw [← Finset.gcd_mul_left]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support.gcd
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).coeff =
    p.support.gcd fun (x : ℕ) ↦ r * p.coeff x
have neg : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support = p.support
Tactic: refine congr (congr rfl ?_) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
neg : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support = p.support
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support.gcd
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).coeff =
    p.support.gcd fun (x : ℕ) ↦ r * p.coeff x
have neg₁ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).coeff = fun (x : ℕ) ↦ r * p.coeff x
Tactic: refine congr (congr rfl ?_) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support = p.support
have neg : ∀ (a : ℕ), a ∈ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).support ↔ a ∈ p.support
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
p : R[X]
h0 : ¬r = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).coeff = fun (x : ℕ) ↦ r * p.coeff x
have neg : ∀ (x : ℕ), (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).coeff x = r * p.coeff x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
k : ℕ
⊢ Eq (α := R) (content ((monomial k : (a : R) → R[X]) r) : R) ((normalize : (a : R) → R) r : R)
have rw : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X k)).content =
  (normalize : (a : R) → R) r
Tactic: rw [← C_mul_X_pow_eq_monomial, content_C_mul, content_X_pow, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
k : ℕ
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X k)).content =
    (normalize : (a : R) → R) r
⊢ Eq (α := R) (content ((monomial k : (a : R) → R[X]) r) : R) ((normalize : (a : R) → R) r : R)
have rw₁ : HMul.hMul (α := R) ((normalize : (a : R) → R) r : R) (HPow.hPow (α := R[X]) X k).content = (normalize : (a : R) → R) r
Tactic: rw [← C_mul_X_pow_eq_monomial, content_C_mul, content_X_pow, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
k : ℕ
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X k)).content =
    (normalize : (a : R) → R) r
rw₁ :
  HMul.hMul (α := R) ((normalize : (a : R) → R) r : R) (HPow.hPow (α := R[X]) X k).content = (normalize : (a : R) → R) r
⊢ Eq (α := R) (content ((monomial k : (a : R) → R[X]) r) : R) ((normalize : (a : R) → R) r : R)
have rw₂ : HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) r : R) (1 : R) = (normalize : (a : R) → R) r
Tactic: rw [← C_mul_X_pow_eq_monomial, content_C_mul, content_X_pow, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
r : R
k : ℕ
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X k)).content =
    (normalize : (a : R) → R) r
rw₁ :
  HMul.hMul (α := R) ((normalize : (a : R) → R) r : R) (HPow.hPow (α := R[X]) X k).content = (normalize : (a : R) → R) r
rw₂ : HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) r : R) (1 : R) = (normalize : (a : R) → R) r
⊢ Eq (α := R) (content ((monomial k : (a : R) → R[X]) r) : R) ((normalize : (a : R) → R) r : R)
have rw₃ : Eq (α := R) ((normalize : (a : R) → R) r : R) ((normalize : (a : R) → R) r : R)
Tactic: rw [← C_mul_X_pow_eq_monomial, content_C_mul, content_X_pow, mul_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]
⊢ p.content = 0 ↔ p = 0
have rw : (∀ x ∈ p.support, p.coeff x = 0) ↔ p = 0
Tactic: rw [content, Finset.gcd_eq_zero_iff]
-- 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, p.coeff x = 0) ↔ p = 0
have mp : (∀ x ∈ p.support, p.coeff x = 0) → p = 0
Tactic: constructor
-- 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]
mp : (∀ x ∈ p.support, p.coeff x = 0) → p = 0
⊢ (∀ x ∈ p.support, p.coeff x = 0) ↔ p = 0
have mpr : p = 0 → ∀ x ∈ p.support, p.coeff x = 0
Tactic: constructor
-- 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]
h : ∀ x ∈ p.support, p.coeff x = 0
⊢ p = 0
have mp : ∀ (n : ℕ), p.coeff n = coeff 0 n
Tactic: ext n
-- 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]
⊢ Eq (α := Rˣ) (normUnit p.content) 1
have pos : ∀ (hp0 : p.content = 0), Eq (α := Rˣ) (normUnit p.content) 1
Tactic: by_cases hp0 : p.content = 0
-- 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]
pos : ∀ (hp0 : p.content = 0), Eq (α := Rˣ) (normUnit p.content) 1
⊢ Eq (α := Rˣ) (normUnit p.content) 1
have neg : ∀ (hp0 : ¬p.content = 0), Eq (α := Rˣ) (normUnit p.content) 1
Tactic: by_cases hp0 : p.content = 0
-- 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]
hp0 : ¬p.content = 0
⊢ Eq (α := Rˣ) (normUnit p.content) 1
have neg : (↑(normUnit p.content) : R) = (↑1 : R)
Tactic: ext
-- 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]
hp0 : ¬p.content = 0
⊢ (↑(normUnit p.content) : R) = (↑1 : R)
have neg : p.content * (↑(normUnit p.content) : R) = p.content * (↑1 : R)
Tactic: apply mul_left_cancel₀ hp0
-- 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]
hp0 : ¬p.content = 0
⊢ p.content * (↑(normUnit p.content) : R) = p.content * (↑1 : R)
have neg : (normalize : (a : R) → R) p.content = p.content * (↑1 : R)
Tactic: rw [← normalize_apply, normalize_content, Units.val_one, mul_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]
hp0 : ¬p.content = 0
neg : (normalize : (a : R) → R) p.content = p.content * (↑1 : R)
⊢ p.content * (↑(normUnit p.content) : R) = p.content * (↑1 : R)
have neg₁ : p.content = p.content * (↑1 : R)
Tactic: rw [← normalize_apply, normalize_content, Units.val_one, mul_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]
hp0 : ¬p.content = 0
neg : (normalize : (a : R) → R) p.content = p.content * (↑1 : R)
neg₁ : p.content = p.content * (↑1 : R)
⊢ p.content * (↑(normUnit p.content) : R) = p.content * (↑1 : R)
have neg₂ : p.content = p.content * 1
Tactic: rw [← normalize_apply, normalize_content, Units.val_one, mul_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]
hp0 : ¬p.content = 0
neg : (normalize : (a : R) → R) p.content = p.content * (↑1 : R)
neg₁ : p.content = p.content * (↑1 : R)
neg₂ : p.content = p.content * 1
⊢ p.content * (↑(normUnit p.content) : R) = p.content * (↑1 : R)
have neg₃ : p.content = p.content
Tactic: rw [← normalize_apply, normalize_content, Units.val_one, mul_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]
n : ℕ
h : p.natDegree < n
⊢ p.content = (Finset.range n).gcd p.coeff
have hab : p.content ∣ (Finset.range n).gcd p.coeff
Tactic: apply dvd_antisymm_of_normalize_eq normalize_content Finset.normalize_gcd
-- 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.natDegree < n
hab : p.content ∣ (Finset.range n).gcd p.coeff
⊢ p.content = (Finset.range n).gcd p.coeff
have hba : (Finset.range n).gcd p.coeff ∣ p.content
Tactic: apply dvd_antisymm_of_normalize_eq normalize_content Finset.normalize_gcd
-- 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.natDegree < n
⊢ p.content ∣ (Finset.range n).gcd p.coeff
have hab : ∀ b ∈ Finset.range n, p.content ∣ p.coeff b
Tactic: rw [Finset.dvd_gcd_iff]
-- 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]
⊢ p.content = @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff p.eraseLead.content
have pos : ∀ (h : p = 0), p.content = @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff p.eraseLead.content
Tactic: by_cases h : p = 0
-- 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]
pos : ∀ (h : p = 0), p.content = @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff p.eraseLead.content
⊢ p.content = @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff p.eraseLead.content
have neg : ∀ (h : ¬p = 0), p.content = @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff p.eraseLead.content
Tactic: by_cases h : p = 0
-- 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]
h : ¬p = 0
⊢ p.content = @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff p.eraseLead.content
have h₁ : p.natDegree ∈ p.support
Tactic: rw [← leadingCoeff_eq_zero, leadingCoeff, ← Ne, ← mem_support_iff] 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]
h : p.natDegree ∈ p.support
⊢ p.content = @gcd _ CommSemiring.toCommMonoidWithZero _ p.leadingCoeff p.eraseLead.content
have neg : @gcd _ CommSemiring.toCommMonoidWithZero _ (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.coeff) =
  @gcd _ CommSemiring.toCommMonoidWithZero _ (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.eraseLead.coeff)
Tactic: rw [content, ← Finset.insert_erase h, Finset.gcd_insert, leadingCoeff, content,
    eraseLead_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]
h : p.natDegree ∈ p.support
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ (p.coeff p.natDegree) ((p.support.erase p.natDegree).gcd p.coeff) =
    @gcd _ CommSemiring.toCommMonoidWithZero _ (p.coeff p.natDegree)
      ((p.support.erase p.natDegree).gcd p.eraseLead.coeff)
have neg : ∀ (i : ℕ) (hi : i ∈ p.support.erase p.natDegree), p.coeff i = p.eraseLead.coeff i
Tactic: refine congr rfl (Finset.gcd_congr rfl fun i hi => ?_)
-- 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]
h : p.natDegree ∈ p.support
i : ℕ
hi : i ∈ p.support.erase p.natDegree
⊢ p.coeff i = p.eraseLead.coeff i
have hi₁ : i ≠ p.natDegree ∧ i ∈ p.support
Tactic: rw [Finset.mem_erase] at hi
Cleared hypotheses: hi
-- 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]
h : p.natDegree ∈ p.support
i : ℕ
hi : i ≠ p.natDegree ∧ i ∈ p.support
⊢ p.coeff i = p.eraseLead.coeff i
have neg : p.coeff i = if i = p.natDegree then 0 else p.coeff i
Tactic: rw [eraseLead_coeff, if_neg hi.1]
-- 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]
h : p.natDegree ∈ p.support
i : ℕ
hi : i ≠ p.natDegree ∧ i ∈ p.support
neg : p.coeff i = if i = p.natDegree then 0 else p.coeff i
⊢ p.coeff i = p.eraseLead.coeff i
have neg₁ : p.coeff i = p.coeff i
Tactic: rw [eraseLead_coeff, if_neg hi.1]
-- 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]
r : R
⊢ r ∣ p.content ↔ (C : (a : R) → R[X]) r ∣ p
have rw : r ∣ p.content ↔ ∀ (i : ℕ), r ∣ p.coeff i
Tactic: rw [C_dvd_iff_dvd_coeff]
-- 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]
r : R
⊢ r ∣ p.content ↔ ∀ (i : ℕ), r ∣ p.coeff i
have mp : r ∣ p.content → ∀ (i : ℕ), r ∣ p.coeff i
Tactic: constructor
-- 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]
r : R
mp : r ∣ p.content → ∀ (i : ℕ), r ∣ p.coeff i
⊢ r ∣ p.content ↔ ∀ (i : ℕ), r ∣ p.coeff i
have mpr : (∀ (i : ℕ), r ∣ p.coeff i) → r ∣ p.content
Tactic: constructor
-- 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]
r : R
h : ∀ (i : ℕ), r ∣ p.coeff i
⊢ r ∣ p.content
have mpr : ∀ b ∈ p.support, r ∣ p.coeff b
Tactic: rw [content, Finset.dvd_gcd_iff]
-- 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]
⊢ p.IsPrimitive ↔ p.content = 1
have rw : (∀ (r : R), (C : (a : R) → R[X]) r ∣ p → IsUnit r) ↔ IsUnit p.content
Tactic: rw [← normalize_content, normalize_eq_one, IsPrimitive]
-- 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]
⊢ (∀ (r : R), (C : (a : R) → R[X]) r ∣ p → IsUnit r) ↔ IsUnit p.content
have simp_rw : (∀ (r : R), r ∣ p.content → IsUnit r) ↔ IsUnit p.content
Tactic: simp_rw [← dvd_content_iff_C_dvd]
-- 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]
⊢ p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart
have pos : ∀ (h : p = 0), p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart
Tactic: by_cases h : p = 0
-- 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]
pos : ∀ (h : p = 0), p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart
⊢ p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart
have neg : ∀ (h : ¬p = 0), p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart
Tactic: by_cases h : p = 0
-- 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]
h : ¬p = 0
⊢ p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart
have neg : p =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X])
    (if p = 0 then 1
    else Classical.choose (p := fun (x : R[X]) ↦ p = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) x) sorry)
Tactic: rw [primPart, if_neg h, ← Classical.choose_spec (C_content_dvd p)]