awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
contrapose! : p ≠ 0 → ∃ x ∈ (↑p.coeffs : Set R), x ≠ 0
⊢ (∀ x ∈ (↑p.coeffs : Set R), x = 0) → p = 0

Tactic:
contrapose!
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ p ≠ 0 → ∃ x ∈ (↑p.coeffs : Set R), x ≠ 0

Tactic:
fun h ↦ ⟨p.leadingCoeff, coeff_mem_coeffs (leadingCoeff_ne_zero.mpr h),
    leadingCoeff_ne_zero.mpr h⟩

Premises used: Iff.mpr, Polynomial.coeff_mem_coeffs, Polynomial.leadingCoeff, Polynomial.leadingCoeff_ne_zero, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ p ≠ 0 → ∃ x ∈ (↑p.coeffs : Set R), x ≠ 0

Tactic:
exact fun h ↦ ⟨p.leadingCoeff, coeff_mem_coeffs (leadingCoeff_ne_zero.mpr h),
    leadingCoeff_ne_zero.mpr h⟩
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
pos : ∀ (h : p.coeff n = 0), p.coeff n ∈ p.contentIdeal
neg : ∀ (h : ¬p.coeff n = 0), p.coeff n ∈ p.contentIdeal
⊢ p.coeff n ∈ p.contentIdeal

Tactic:
by_cases h : p.coeff n = 0

Premises used: Polynomial.coeff
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ p.coeff n ∈ p.contentIdeal

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h : ¬p.coeff n = 0
neg : p.coeff n ∈ (↑p.coeffs : Set R)
⊢ p.coeff n ∈ p.contentIdeal

Tactic:
apply subset_span

Premises used: Ideal.subset_span
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h : ¬p.coeff n = 0
⊢ p.coeff n ∈ (↑p.coeffs : Set R)

Tactic:
simpa using coeff_mem_coeffs h

Premises used: Polynomial.coeff_mem_coeffs
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
r : R
pos : ∀ (h : r = 0), Eq (α := Ideal R) (contentIdeal ((monomial n : (a : R) → R[X]) r)) (span {r})
neg : ∀ (h : ¬r = 0), Eq (α := Ideal R) (contentIdeal ((monomial n : (a : R) → R[X]) r)) (span {r})
⊢ Eq (α := Ideal R) (contentIdeal ((monomial n : (a : R) → R[X]) r)) (span {r})

Tactic:
by_cases h : r = 0
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
r : R
h : r = 0
⊢ Eq (α := Ideal R) (contentIdeal ((monomial n : (a : R) → R[X]) r)) (span {r})

Tactic:
simp [h, Set.singleton_zero, contentIdeal_def, coeffs_monomial]

Premises used: Polynomial.coeffs_monomial, Polynomial.contentIdeal_def, Set.singleton_zero
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
r : R
h : ¬r = 0
⊢ Eq (α := Ideal R) (contentIdeal ((monomial n : (a : R) → R[X]) r)) (span {r})

Tactic:
simp [h, Set.singleton_zero, contentIdeal_def, coeffs_monomial]

Premises used: Polynomial.coeffs_monomial, Polynomial.contentIdeal_def, Set.singleton_zero
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
r : R
⊢ Eq (α := Ideal R) (contentIdeal ((monomial 0 : (a : R) → R[X]) r)) (span {r})

Tactic:
contentIdeal_monomial 0 r

Premises used: Polynomial.contentIdeal_monomial, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
r : R
⊢ Eq (α := Ideal R) (contentIdeal ((monomial 0 : (a : R) → R[X]) r)) (span {r})

Tactic:
exact contentIdeal_monomial 0 r

Premises used: Polynomial.contentIdeal_monomial, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
rw : Eq (α := Ideal R) (contentIdeal 1) (span {1})
rw₁ : Eq.{u_1 + 1} (α := Ideal R) (contentIdeal 1) (contentIdeal ((C : (a : R) → R[X]) 1))
rw₂ rw₃ : Eq.{u_1 + 1} (α := Ideal R) (contentIdeal 1) (contentIdeal 1)
⊢ Eq.{u_1 + 1} (α := Ideal R) (contentIdeal 1) ⊤

Tactic:
rw [← span_singleton_one, ← contentIdeal_C 1, C_1]

Premises used: Polynomial.C_1, Ideal.span_singleton_one, Polynomial.contentIdeal_C, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ p.contentIdeal.FG

Tactic:
⟨p.coeffs, rfl⟩

Premises used: Ideal.FG, Polynomial.coeffs, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
this :
  Eq (α := Ideal S) (span ((↑(map f p).coeffs : Set S) ∪ {0})) (span ((⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}))
⊢ (map f p).contentIdeal = Ideal.map f p.contentIdeal

Tactic:
simpa [contentIdeal_def, map_span]

Premises used: Polynomial.contentIdeal_def, Ideal.map_span
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
suffices :
  Eq (α := Ideal S) (span ((↑(map f p).coeffs : Set S) ∪ {0})) (span ((⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}))
⊢ (map f p).contentIdeal = Ideal.map f p.contentIdeal

Tactic:
suffices span ((map f p).coeffs ∪ {0}) = span (f '' p.coeffs ∪ {0}) by
    simpa [contentIdeal_def, map_span]
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
e_s : (↑(map f p).coeffs : Set S) ∪ {0} = (⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}
⊢ Eq (α := Ideal S) (span ((↑(map f p).coeffs : Set S) ∪ {0})) (span ((⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}))

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
e_s :
  ∀ (s : S),
    s ∈ (↑(map f p).coeffs : Set S) ∪ {0} ↔
      Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}) s
⊢ (↑(map f p).coeffs : Set S) ∪ {0} = (⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}

Tactic:
ext s
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
s : S
pos :
  ∀ (hs : s = 0),
    s ∈ (↑(map f p).coeffs : Set S) ∪ {0} ↔
      Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}) s
neg :
  ∀ (hs : ¬s = 0),
    s ∈ (↑(map f p).coeffs : Set S) ∪ {0} ↔
      Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}) s
⊢ s ∈ (↑(map f p).coeffs : Set S) ∪ {0} ↔
    Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}) s

Tactic:
by_cases hs : s = 0
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
s : S
hs : s = 0
⊢ s ∈ (↑(map f p).coeffs : Set S) ∪ {0} ↔
    Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}) s

Tactic:
simp [hs]
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
s : S
hs : ¬s = 0
⊢ s ∈ (↑(map f p).coeffs : Set S) ∪ {0} ↔
    Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}) s

Tactic:
aesop (add simp mem_coeffs_iff)

Premises used: Polynomial.mem_coeffs_iff
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
rw : (↑(p * q).coeffs : Set R) ⊆ (↑(p.contentIdeal * q.contentIdeal) : Set R)
⊢ (p * q).contentIdeal ≤ p.contentIdeal * q.contentIdeal

Tactic:
rw [contentIdeal_def, span_le]

Premises used: Ideal.span_le, Polynomial.contentIdeal_def
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
simp : ∀ (x : R), (∃ n ∈ (p * q).support, x = (p * q).coeff n) → x ∈ (↑(p.contentIdeal * q.contentIdeal) : Set R)
⊢ (↑(p * q).coeffs : Set R) ⊆ (↑(p.contentIdeal * q.contentIdeal) : Set R)

Tactic:
simp only [Set.subset_def, Finset.mem_coe, mem_coeffs_iff]

Premises used: Set.subset_def, Polynomial.mem_coeffs_iff, Finset.mem_coe
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
n : ℕ
left : n ∈ (p * q).support
⊢ (p * q).coeff n ∈ (↑(p.contentIdeal * q.contentIdeal) : Set R)

Tactic:
simp [coeff_mul, _root_.sum_mem, Submodule.mul_mem_mul, coeff_mem_contentIdeal]

Premises used: Submodule.mul_mem_mul, Polynomial.coeff_mul, Polynomial.coeff_mem_contentIdeal, sum_mem
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p q : R[X]
hpq : p ∣ q
obtain : ∀ (p' : R[X]), (p * p').contentIdeal ≤ p.contentIdeal
⊢ q.contentIdeal ≤ p.contentIdeal

Tactic:
obtain ⟨p', rfl⟩ := hpq

Premises used: rfl
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p p' : R[X]
⊢ (p * p').contentIdeal ≤ p.contentIdeal

Tactic:
le_trans (p.contentIdeal_mul_le_mul_contentIdeal p') mul_le_right

Premises used: Ideal.mul_le_right, Polynomial.contentIdeal_mul_le_mul_contentIdeal, le_trans
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p p' : R[X]
⊢ (p * p').contentIdeal ≤ p.contentIdeal

Tactic:
exact le_trans (p.contentIdeal_mul_le_mul_contentIdeal p') mul_le_right

Premises used: Ideal.mul_le_right, Polynomial.contentIdeal_mul_le_mul_contentIdeal, le_trans
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
n : ℕ
⊢ p.coeff n ∈ p.contentIdeal

Tactic:
have := p.coeff_mem_contentIdeal n
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
n : ℕ
this : p.coeff n ∈ p.contentIdeal
⊢ ∃ (s : R), p.coeff n = s • Submodule.IsPrincipal.generator p.contentIdeal

Tactic:
rw [Submodule.IsPrincipal.mem_iff_eq_smul_generator] at this

Premises used: Submodule.IsPrincipal.mem_iff_eq_smul_generator
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
n : ℕ
this : ∃ (s : R), p.coeff n = s • Submodule.IsPrincipal.generator p.contentIdeal
obtain :
  ∀ (w : R) (ha : p.coeff n = w • Submodule.IsPrincipal.generator p.contentIdeal),
    Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff n
⊢ Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff n

Tactic:
obtain ⟨_, ha⟩ := this
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
n : ℕ
w : R
ha : p.coeff n = w • Submodule.IsPrincipal.generator p.contentIdeal
⊢ Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff n

Tactic:
simp [ha]
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
rw : ∀ (i : ℕ), Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff i
⊢ (C : (a : R) → R[X]) (Submodule.IsPrincipal.generator p.contentIdeal) ∣ p

Tactic:
rw [C_dvd_iff_dvd_coeff]

Premises used: Polynomial.C_dvd_iff_dvd_coeff
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ ∀ (i : ℕ), Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff i

Tactic:
fun i ↦ h_prin.contentIdeal_generator_dvd_coeff i

Premises used: Submodule.IsPrincipal.contentIdeal_generator_dvd_coeff
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ ∀ (i : ℕ), Submodule.IsPrincipal.generator p.contentIdeal ∣ p.coeff i

Tactic:
exact fun i ↦ h_prin.contentIdeal_generator_dvd_coeff i

Premises used: Submodule.IsPrincipal.contentIdeal_generator_dvd_coeff
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
mp : p.contentIdeal ≤ span {r} → (C : (a : R) → R[X]) r ∣ p
mpr : (C : (a : R) → R[X]) r ∣ p → p.contentIdeal ≤ span {r}
⊢ p.contentIdeal ≤ span {r} ↔ (C : (a : R) → R[X]) r ∣ p

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
mp :
  LE.le (α := Ideal R) (span {Submodule.IsPrincipal.generator p.contentIdeal}) (span {r}) → (C : (a : R) → R[X]) r ∣ p
⊢ p.contentIdeal ≤ span {r} → (C : (a : R) → R[X]) r ∣ p

Tactic:
rw [← p.contentIdeal.span_singleton_generator]

Premises used: Polynomial.contentIdeal, Ideal.span_singleton_generator
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
h : LE.le (α := Ideal R) (span {Submodule.IsPrincipal.generator p.contentIdeal}) (span {r})
apply : r ∣ Submodule.IsPrincipal.generator p.contentIdeal
⊢ Dvd.dvd (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
    ((C : (a : R) → R[X]) (Submodule.IsPrincipal.generator p.contentIdeal) : R[X])

Tactic:
apply _root_.map_dvd C

Premises used: Polynomial.C, map_dvd
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
h rwa rwa₁ rwa₂ rwa₃ : LE.le (α := Ideal R) (span {Submodule.IsPrincipal.generator p.contentIdeal}) (span {r})
⊢ r ∣ Submodule.IsPrincipal.generator p.contentIdeal

Tactic:
rwa [← span_singleton_le_span_singleton]

Premises used: Ideal.span_singleton_le_span_singleton
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
h : LE.le (α := Ideal R) (span {Submodule.IsPrincipal.generator p.contentIdeal}) (span {r})
⊢ (C : (a : R) → R[X]) (Submodule.IsPrincipal.generator p.contentIdeal) ∣ p

Tactic:
h_prin.contentIdeal_generator_dvd

Premises used: Submodule.IsPrincipal.contentIdeal_generator_dvd
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
h : LE.le (α := Ideal R) (span {Submodule.IsPrincipal.generator p.contentIdeal}) (span {r})
C :
  Dvd.dvd (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X])
    ((Polynomial.C : (a : R) → R[X]) (Submodule.IsPrincipal.generator p.contentIdeal) : R[X])
⊢ (Polynomial.C : (a : R) → R[X]) r ∣ p

Tactic:
calc
    C r ∣ C h_prin.generator := by
      apply _root_.map_dvd C
      rwa [← span_singleton_le_span_singleton]
     _ ∣ p := h_prin.contentIdeal_generator_dvd

Premises used: Polynomial.C, Submodule.IsPrincipal.generator, Submodule.IsPrincipal.contentIdeal_generator_dvd, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
mpr : (C : (a : R) → R[X]) r ∣ p → p.contentIdeal ≤ contentIdeal ((C : (a : R) → R[X]) r)
⊢ (C : (a : R) → R[X]) r ∣ p → p.contentIdeal ≤ span {r}

Tactic:
rw [← contentIdeal_C r]

Premises used: Polynomial.contentIdeal_C
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
⊢ (C : (a : R) → R[X]) r ∣ p → p.contentIdeal ≤ contentIdeal ((C : (a : R) → R[X]) r)

Tactic:
fun h ↦ contentIdeal_le_contentIdeal_of_dvd h

Premises used: Polynomial.contentIdeal_le_contentIdeal_of_dvd
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
⊢ (C : (a : R) → R[X]) r ∣ p → p.contentIdeal ≤ contentIdeal ((C : (a : R) → R[X]) r)

Tactic:
exact fun h ↦ contentIdeal_le_contentIdeal_of_dvd h

Premises used: Polynomial.contentIdeal_le_contentIdeal_of_dvd
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h : p.contentIdeal = ⊤
rw : Submodule.IsPrincipal.{u_3, u_3} (R := R) (M := R) ⊤
⊢ Submodule.IsPrincipal p.contentIdeal

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h : p.contentIdeal = ⊤
⊢ Submodule.IsPrincipal.{u_3, u_3} (R := R) (M := R) ⊤

Tactic:
top_isPrincipal

Premises used: top_isPrincipal
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h : p.contentIdeal = ⊤
⊢ Submodule.IsPrincipal.{u_3, u_3} (R := R) (M := R) ⊤

Tactic:
exact top_isPrincipal

Premises used: top_isPrincipal
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h : p.contentIdeal = ⊤
⊢ Submodule.IsPrincipal p.contentIdeal

Tactic:
have h_prin : p.contentIdeal.IsPrincipal := by
    rw [h]
    exact top_isPrincipal
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h : p.contentIdeal = ⊤
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
⊢ (C : (a : R) → R[X]) r ∣ p → IsUnit r

Tactic:
simp [← h_prin.contentIdeal_le_span_iff_dvd r, h]

Premises used: Submodule.IsPrincipal.contentIdeal_le_span_iff_dvd
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ p.IsPrimitive ↔ p.contentIdeal = ⊤

Tactic:
⟨?_, fun h ↦ isPrimitive_of_contentIdeal_eq_top h⟩

Premises used: Polynomial.isPrimitive_of_contentIdeal_eq_top, Iff.intro
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
refine : p.IsPrimitive → p.contentIdeal = ⊤
⊢ p.IsPrimitive ↔ p.contentIdeal = ⊤

Tactic:
refine ⟨?_, fun h ↦ isPrimitive_of_contentIdeal_eq_top h⟩
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
contrapose! : p.contentIdeal ≠ ⊤ → ¬p.IsPrimitive
⊢ p.IsPrimitive → p.contentIdeal = ⊤

Tactic:
contrapose!
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
simp : p.contentIdeal ≠ ⊤ → ∃ (x : R) (_ : (C : (a : R) → R[X]) x ∣ p), ¬IsUnit x
⊢ p.contentIdeal ≠ ⊤ → ¬p.IsPrimitive

Tactic:
simp only [IsPrimitive, not_forall]

Premises used: Polynomial.IsPrimitive, Classical.not_forall
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
h_1 : p.contentIdeal ≠ ⊤
h : ¬IsUnit (Submodule.IsPrincipal.generator p.contentIdeal)
⊢ ∃ (x : R) (_ : (C : (a : R) → R[X]) x ∣ p), ¬IsUnit x

Tactic:
use h_prin.generator, h_prin.contentIdeal_generator_dvd

Premises used: Submodule.IsPrincipal.generator, Submodule.IsPrincipal.contentIdeal_generator_dvd
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
h : p.contentIdeal ≠ ⊤
⊢ ¬IsUnit (Submodule.IsPrincipal.generator p.contentIdeal)

Tactic:
simp_all [← Ideal.span_singleton_eq_top]

Premises used: Ideal.span_singleton_eq_top
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p q : R[X]
h : (p * q).contentIdeal = ⊤
apply : ⊤ ≤ p.contentIdeal
⊢ p.contentIdeal = ⊤

Tactic:
apply le_antisymm le_top

Premises used: le_antisymm, le_top
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p q : R[X]
h : (p * q).contentIdeal = ⊤
⊢ ⊤ = (p * q).contentIdeal

Tactic:
h.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p q : R[X]
h : (p * q).contentIdeal = ⊤
⊢ (p * q).contentIdeal ≤ p.contentIdeal * q.contentIdeal

Tactic:
contentIdeal_mul_le_mul_contentIdeal p q

Premises used: Set.Mem, Polynomial.contentIdeal_mul_le_mul_contentIdeal
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p q : R[X]
h : (p * q).contentIdeal = ⊤
⊢ p.contentIdeal * q.contentIdeal ≤ p.contentIdeal

Tactic:
mul_le_right

Premises used: Ideal.mul_le_right, Set.Mem
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommSemiring R
p q : R[X]
h : (p * q).contentIdeal = ⊤
⊢ ⊤ ≤ p.contentIdeal

Tactic:
calc
  ⊤ = (p * q).contentIdeal := h.symm
  _ ≤ p.contentIdeal * q.contentIdeal := contentIdeal_mul_le_mul_contentIdeal p q
  _ ≤ p.contentIdeal := mul_le_right

Premises used: Polynomial.contentIdeal, Ideal.mul_le_right, HMul.hMul, Polynomial.contentIdeal_mul_le_mul_contentIdeal, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
p q : R[X]
rw :
  ∀ (b : Ideal R),
    Membership.mem (γ := Set (Ideal R)) {J : Ideal R | (p * q).contentIdeal ≤ J ∧ J.IsPrime} b →
      p.contentIdeal * q.contentIdeal ≤ b
⊢ p.contentIdeal * q.contentIdeal ≤ (p * q).contentIdeal.radical

Tactic:
rw [radical_eq_sInf, le_sInf_iff]

Premises used: le_sInf_iff, Ideal.radical_eq_sInf
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
p q : R[X]
P : Ideal R
this : ∀ (hpq : (p * q).contentIdeal ≤ P) (hPprime : P.IsPrime), p.contentIdeal * q.contentIdeal ≤ P
⊢ Membership.mem (γ := Set (Ideal R)) {J : Ideal R | (p * q).contentIdeal ≤ J ∧ J.IsPrime} P →
    p.contentIdeal * q.contentIdeal ≤ P

Tactic:
⟨hpq, hPprime⟩
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
p q : R[X]
P : Ideal R
hpq : (p * q).contentIdeal ≤ P
hPprime : P.IsPrime
rw : p.contentIdeal ≤ P ∨ q.contentIdeal ≤ P
⊢ p.contentIdeal * q.contentIdeal ≤ P

Tactic:
rw [hPprime.mul_le]

Premises used: Ideal.IsPrime.mul_le
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
p q : R[X]
P : Ideal R
hpq : (p * q).contentIdeal ≤ P
hPprime : P.IsPrime
rw :
  ∀ (hpq : (p * q).contentIdeal ≤ RingHom.ker (F := R →+* R ⧸ P) (Ideal.Quotient.mk P)) (hPprime : P.IsPrime),
    p.contentIdeal ≤ RingHom.ker (F := R →+* R ⧸ P) (Ideal.Quotient.mk P) ∨
      q.contentIdeal ≤ RingHom.ker (F := R →+* R ⧸ P) (Ideal.Quotient.mk P)
⊢ p.contentIdeal ≤ P ∨ q.contentIdeal ≤ P

Tactic:
rw [← Ideal.mk_ker (I := P)] at hpq ⊢

Premises used: Ideal.mk_ker
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
p q : R[X]
P : Ideal R
hpq : (p * q).contentIdeal ≤ RingHom.ker (F := R →+* R ⧸ P) (Ideal.Quotient.mk P)
hPprime : P.IsPrime
⊢ p.contentIdeal ≤ RingHom.ker (F := R →+* R ⧸ P) (Ideal.Quotient.mk P) ∨
    q.contentIdeal ≤ RingHom.ker (F := R →+* R ⧸ P) (Ideal.Quotient.mk P)

Tactic:
simpa only [← map_eq_bot_iff_le_ker, ← contentIdeal_map_eq_map_contentIdeal, Polynomial.map_mul,
    contentIdeal_eq_bot_iff, mul_eq_zero] using hpq

Premises used: Polynomial.map_mul, mul_eq_zero, Polynomial.contentIdeal_map_eq_map_contentIdeal, Polynomial.contentIdeal_eq_bot_iff, Ideal.map_eq_bot_iff_le_ker
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
p q : R[X]
hp : p.contentIdeal = ⊤
hq : q.contentIdeal = ⊤
rw : (p * q).contentIdeal.radical = ⊤
⊢ (p * q).contentIdeal = ⊤

Tactic:
rw [← Ideal.radical_eq_top]

Premises used: Ideal.radical_eq_top
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
p q : R[X]
hp : p.contentIdeal = ⊤
hq : q.contentIdeal = ⊤
apply : ⊤ ≤ (p * q).contentIdeal.radical
⊢ (p * q).contentIdeal.radical = ⊤

Tactic:
apply le_antisymm le_top

Premises used: le_antisymm, le_top
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
p q : R[X]
hp : p.contentIdeal = ⊤
hq : q.contentIdeal = ⊤
⊢ ⊤ = p.contentIdeal * q.contentIdeal

Tactic:
simp [hp, hq]
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_3
inst : CommRing R
p q : R[X]
hp : p.contentIdeal = ⊤
hq : q.contentIdeal = ⊤
⊢ p.contentIdeal * q.contentIdeal ≤ (p * q).contentIdeal.radical

Tactic:
mul_contentIdeal_le_radical_contentIdeal_mul

Premises used: Polynomial.mul_contentIdeal_le_radical_contentIdeal_mul