awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h_1 : ∃ (n : ℕ) (r : R[X]), r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find (p := fun (n : ℕ) ↦ ∃ (r : R[X]), r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r) h_1
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ (n : ℕ) (s : R[X]), s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find (p := fun (n : ℕ) ↦ ∃ (s : R[X]), s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s) con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : 0 < s.natDegree
hcancel :
  (r.cancelLeads s).natDegree <
    Nat.find (p := fun (n : ℕ) ↦ ∃ (s : R[X]), s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s) con
rcs :
  r ∣
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r.leadingCoeff : R[X]) s -
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) s.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (s.natDegree - r.natDegree)) *
        r
h : r ∣ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r.leadingCoeff : R[X]) s).primPart
h_2 : Nontrivial R
hC0 : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) r.leadingCoeff : R[X]) (0 : R[X])
u : R[X]ˣ
hu : (↑u : R[X]) = primPart ((C : (a : R) → R[X]) r.leadingCoeff)
apply : s.primPart * (↑u : R[X]) = (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r.leadingCoeff : R[X]) s).primPart
⊢ r ∣ s.primPart

Tactic:
apply h.trans (Associated.symm ⟨u, _⟩).dvd

Premises used: Associated.dvd, Associated.symm, Exists.intro, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h_1 : ∃ (n : ℕ) (r : R[X]), r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find (p := fun (n : ℕ) ↦ ∃ (r : R[X]), r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r) h_1
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ (n : ℕ) (s : R[X]), s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find (p := fun (n : ℕ) ↦ ∃ (s : R[X]), s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s) con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : 0 < s.natDegree
hcancel :
  (r.cancelLeads s).natDegree <
    Nat.find (p := fun (n : ℕ) ↦ ∃ (s : R[X]), s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s) con
rcs :
  r ∣
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r.leadingCoeff : R[X]) s -
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) s.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (s.natDegree - r.natDegree)) *
        r
h : r ∣ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r.leadingCoeff : R[X]) s).primPart
h_2 : Nontrivial R
hC0 : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) r.leadingCoeff : R[X]) (0 : R[X])
u : R[X]ˣ
hu : (↑u : R[X]) = primPart ((C : (a : R) → R[X]) r.leadingCoeff)
rw : s.primPart * (↑u : R[X]) = primPart ((C : (a : R) → R[X]) r.leadingCoeff) * s.primPart
rw₁ :
  s.primPart * primPart ((C : (a : R) → R[X]) r.leadingCoeff) =
    primPart ((C : (a : R) → R[X]) r.leadingCoeff) * s.primPart
rw₂ rw₃ :
  primPart ((C : (a : R) → R[X]) r.leadingCoeff) * s.primPart =
    primPart ((C : (a : R) → R[X]) r.leadingCoeff) * s.primPart
⊢ s.primPart * (↑u : R[X]) = (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r.leadingCoeff : R[X]) s).primPart

Tactic:
rw [primPart_mul (mul_ne_zero hC0 s0), hu, mul_comm]

Premises used: mul_comm, mul_ne_zero, Polynomial.primPart_mul
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
mp : p ∣ q → p.content ∣ q.content ∧ p.primPart ∣ q.primPart
mpr : p.content ∣ q.content ∧ p.primPart ∣ q.primPart → p ∣ q
⊢ p ∣ q ↔ p.content ∣ q.content ∧ p.primPart ∣ q.primPart

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p r : R[X]
hq : p * r ≠ 0
mp : p.content ∣ p.content * r.content ∧ p.primPart ∣ p * r
⊢ p.content ∣ (p * r).content ∧ p.primPart ∣ (p * r).primPart

Tactic:
rw [content_mul, p.isPrimitive_primPart.dvd_primPart_iff_dvd hq]

Premises used: Polynomial.isPrimitive_primPart, Polynomial.IsPrimitive.dvd_primPart_iff_dvd, Polynomial.content_mul
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p r : R[X]
hq : p * r ≠ 0
⊢ p.content ∣ p.content * r.content ∧ p.primPart ∣ p * r

Tactic:
⟨dvd_mul_right .., dvd_mul_of_dvd_left p.primPart_dvd _⟩

Premises used: dvd_mul_of_dvd_left, Polynomial.primPart_dvd, And.intro, dvd_mul_right
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p r : R[X]
hq : p * r ≠ 0
⊢ p.content ∣ p.content * r.content ∧ p.primPart ∣ p * r

Tactic:
exact ⟨dvd_mul_right .., dvd_mul_of_dvd_left p.primPart_dvd _⟩
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
h₁ : p.content ∣ q.content
h₂ : p.primPart ∣ q.primPart
mpr :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart ∣
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart
⊢ p ∣ q

Tactic:
rw [p.eq_C_content_mul_primPart, q.eq_C_content_mul_primPart]

Premises used: Polynomial.eq_C_content_mul_primPart
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
h₁ : p.content ∣ q.content
h₂ : p.primPart ∣ q.primPart
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.content : R[X]) p.primPart ∣
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.content : R[X]) q.primPart

Tactic:
gcongr
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q : R[X]
rcases :
  ∀ (r : R[X]) (rprim : r.IsPrimitive) (hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s),
    ∃ (c : R[X]), ∀ (d : R[X]), p ∣ d ∧ q ∣ d ↔ c ∣ d
⊢ ∃ (c : R[X]), ∀ (d : R[X]), p ∣ d ∧ q ∣ d ↔ c ∣ d

Tactic:
rcases exists_primitive_lcm_of_isPrimitive p.isPrimitive_primPart
        q.isPrimitive_primPart with
      ⟨r, rprim, hr⟩

Premises used: Polynomial.isPrimitive_primPart, Polynomial.exists_primitive_lcm_of_isPrimitive
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
⊢ ∃ (c : R[X]), ∀ (d : R[X]), p ∣ d ∧ q ∣ d ↔ c ∣ d

Tactic:
⟨C (lcm p.content q.content) * r, fun s => ?_⟩

Premises used: Polynomial.C, HMul.hMul, Polynomial.content, GCDMonoid.lcm, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
refine :
  ∀ (s : R[X]),
    p ∣ s ∧ q ∣ s ↔
      HMul.hMul (α := R[X])
          ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X]) r ∣
        s
⊢ ∃ (c : R[X]), ∀ (d : R[X]), p ∣ d ∧ q ∣ d ↔ c ∣ d

Tactic:
refine ⟨C (lcm p.content q.content) * r, fun s => ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
pos :
  ∀ (hs : s = 0),
    p ∣ s ∧ q ∣ s ↔
      HMul.hMul (α := R[X])
          ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X]) r ∣
        s
neg :
  ∀ (hs : ¬s = 0),
    p ∣ s ∧ q ∣ s ↔
      HMul.hMul (α := R[X])
          ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X]) r ∣
        s
⊢ p ∣ s ∧ q ∣ s ↔
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
        r ∣
      s

Tactic:
by_cases hs : s = 0
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : s = 0
⊢ p ∣ s ∧ q ∣ s ↔
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
        r ∣
      s

Tactic:
simp [hs]
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
pos :
  ∀
    (hpq :
      Eq (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
        (0 : R[X])),
    p ∣ s ∧ q ∣ s ↔
      HMul.hMul (α := R[X])
          ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X]) r ∣
        s
neg :
  ∀
    (hpq :
      ¬Eq (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
          (0 : R[X])),
    p ∣ s ∧ q ∣ s ↔
      HMul.hMul (α := R[X])
          ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X]) r ∣
        s
⊢ p ∣ s ∧ q ∣ s ↔
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
        r ∣
      s

Tactic:
by_cases hpq : C (lcm p.content q.content) = 0

Premises used: Polynomial.C, Polynomial.content, GCDMonoid.lcm, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq :
  Eq (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
    (0 : R[X])
⊢ p = 0 ∨ q = 0

Tactic:
rw [C_eq_zero, lcm_eq_zero_iff, content_eq_zero_iff, content_eq_zero_iff] at hpq

Premises used: lcm_eq_zero_iff, Polynomial.content_eq_zero_iff, Polynomial.C_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : p = 0 ∨ q = 0
pos :
  ∀ (hpq : p = 0),
    p ∣ s ∧ q ∣ s ↔
      HMul.hMul (α := R[X])
          ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X]) r ∣
        s
pos₁ :
  ∀ (hpq : q = 0),
    p ∣ s ∧ q ∣ s ↔
      HMul.hMul (α := R[X])
          ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X]) r ∣
        s
⊢ p ∣ s ∧ q ∣ s ↔
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
        r ∣
      s

Tactic:
rcases hpq with (hpq | hpq)
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : p = 0
⊢ p ∣ s ∧ q ∣ s ↔
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
        r ∣
      s

Tactic:
simp [hpq, hs]
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq : q = 0
⊢ p ∣ s ∧ q ∣ s ↔
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
        r ∣
      s

Tactic:
simp [hpq, hs]
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq :
  ¬Eq (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
      (0 : R[X])
neg :
  (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q ∣ s ↔
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
        r ∣
      s
⊢ p ∣ s ∧ q ∣ s ↔
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
        r ∣
      s

Tactic:
rw [dvd_iff_content_dvd_content_and_primPart_dvd_primPart hs]

Premises used: Polynomial.dvd_iff_content_dvd_content_and_primPart_dvd_primPart
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq :
  ¬Eq (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
      (0 : R[X])
neg :
  (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
        r ∣
      s
⊢ (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q ∣ s ↔
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
        r ∣
      s

Tactic:
rw [dvd_iff_content_dvd_content_and_primPart_dvd_primPart hs]

Premises used: Polynomial.dvd_iff_content_dvd_content_and_primPart_dvd_primPart
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq :
  ¬Eq (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
      (0 : R[X])
neg :
  (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    (HMul.hMul (α := R[X])
            ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X]) r).content ∣
        s.content ∧
      (HMul.hMul (α := R[X])
            ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X]) r).primPart ∣
        s.primPart
⊢ (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
        r ∣
      s

Tactic:
rw [dvd_iff_content_dvd_content_and_primPart_dvd_primPart hs]

Premises used: Polynomial.dvd_iff_content_dvd_content_and_primPart_dvd_primPart
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq :
  ¬Eq (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
      (0 : R[X])
neg :
  (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    (HMul.hMul (α := R[X])
            ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X]) r).content ∣
        s.content ∧
      (HMul.hMul (α := R[X])
            ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X]) r).primPart ∣
        s.primPart
⊢ p ∣ s ∧ q ∣ s ↔
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
        r ∣
      s

Tactic:
iterate 3 rw [dvd_iff_content_dvd_content_and_primPart_dvd_primPart hs]

Premises used: Polynomial.dvd_iff_content_dvd_content_and_primPart_dvd_primPart
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq :
  ¬Eq (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
      (0 : R[X])
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq :
  ¬Eq (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
      (0 : R[X])
h : Nontrivial R
rw :
  (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    (p.content ∣ s.content ∧ q.content ∣ s.content) ∧ p.primPart ∣ s.primPart ∧ q.primPart ∣ s.primPart
⊢ (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    (HMul.hMul (α := R[X])
            ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X]) r).content ∣
        s.content ∧
      (HMul.hMul (α := R[X])
            ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X]) r).primPart ∣
        s.primPart

Tactic:
rw [content_mul, rprim.content_eq_one, mul_one, content_C, normalize_lcm, lcm_dvd_iff,
      primPart_mul (mul_ne_zero hpq rprim.ne_zero), rprim.primPart_eq,
      (isUnit_primPart_C (lcm p.content q.content)).mul_left_dvd, ← hr s.primPart]

Premises used: Polynomial.IsPrimitive.content_eq_one, Polynomial.IsPrimitive.ne_zero, Polynomial.content, lcm_dvd_iff, GCDMonoid.lcm, normalize_lcm, IsUnit.mul_left_dvd, Polynomial.isUnit_primPart_C, Polynomial.IsPrimitive.primPart_eq, Polynomial.primPart, Polynomial.content_mul, Polynomial.content_C, mul_one, mul_ne_zero, Polynomial.primPart_mul
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
this : DecidableEq R := Classical.decEq R
p q r : R[X]
rprim : r.IsPrimitive
hr : ∀ (s : R[X]), p.primPart ∣ s ∧ q.primPart ∣ s ↔ r ∣ s
s : R[X]
hs : ¬s = 0
hpq :
  ¬Eq (α := R[X]) ((C : (a : R) → R[X]) (@lcm _ CommSemiring.toCommMonoidWithZero _ p.content q.content) : R[X])
      (0 : R[X])
h : Nontrivial R
mp :
  (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart →
    (p.content ∣ s.content ∧ q.content ∣ s.content) ∧ p.primPart ∣ s.primPart ∧ q.primPart ∣ s.primPart
mpr :
  (p.content ∣ s.content ∧ q.content ∣ s.content) ∧ p.primPart ∣ s.primPart ∧ q.primPart ∣ s.primPart →
    (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart
mp₁ mp₂ :
  p.content ∣ s.content →
    p.primPart ∣ s.primPart →
      q.content ∣ s.content →
        q.primPart ∣ s.primPart →
          (p.content ∣ s.content ∧ q.content ∣ s.content) ∧ p.primPart ∣ s.primPart ∧ q.primPart ∣ s.primPart
mp₃ :
  p.content ∣ s.content →
    p.primPart ∣ s.primPart → q.content ∣ s.content → q.primPart ∣ s.primPart → p.content ∣ s.content
mp₄ :
  p.content ∣ s.content →
    p.primPart ∣ s.primPart → q.content ∣ s.content → q.primPart ∣ s.primPart → q.content ∣ s.content
mp₅ :
  p.content ∣ s.content →
    p.primPart ∣ s.primPart → q.content ∣ s.content → q.primPart ∣ s.primPart → p.primPart ∣ s.primPart
mp₆ :
  p.content ∣ s.content →
    p.primPart ∣ s.primPart → q.content ∣ s.content → q.primPart ∣ s.primPart → q.primPart ∣ s.primPart
mpr₁ mpr₂ :
  p.content ∣ s.content →
    q.content ∣ s.content →
      p.primPart ∣ s.primPart →
        q.primPart ∣ s.primPart →
          (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart
mpr₃ :
  p.content ∣ s.content →
    q.content ∣ s.content → p.primPart ∣ s.primPart → q.primPart ∣ s.primPart → p.content ∣ s.content
mpr₄ :
  p.content ∣ s.content →
    q.content ∣ s.content → p.primPart ∣ s.primPart → q.primPart ∣ s.primPart → p.primPart ∣ s.primPart
mpr₅ :
  p.content ∣ s.content →
    q.content ∣ s.content → p.primPart ∣ s.primPart → q.primPart ∣ s.primPart → q.content ∣ s.content
mpr₆ :
  p.content ∣ s.content →
    q.content ∣ s.content → p.primPart ∣ s.primPart → q.primPart ∣ s.primPart → q.primPart ∣ s.primPart
⊢ (p.content ∣ s.content ∧ p.primPart ∣ s.primPart) ∧ q.content ∣ s.content ∧ q.primPart ∣ s.primPart ↔
    (p.content ∣ s.content ∧ q.content ∣ s.content) ∧ p.primPart ∣ s.primPart ∧ q.primPart ∣ s.primPart

Tactic:
tauto
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
hp : p ≠ 0
q : R[X]
⊢ (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).degree ≤ (↑p.natDegree : WithBot ℕ)

Tactic:
have := natDegree_le_iff_degree_le.mp (natDegree_le_of_dvd (gcd_dvd_left p q) hp)
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p : R[X]
hp : p ≠ 0
q : R[X]
this : (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).degree ≤ (↑p.natDegree : WithBot ℕ)
rwa rwa₁ rwa₂ rwa₃ : (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).degree ≤ (↑p.natDegree : WithBot ℕ)
⊢ (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).degree ≤ p.degree

Tactic:
rwa [degree_eq_natDegree hp]

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
rw : (@gcd _ CommSemiring.toCommMonoidWithZero _ q p).degree ≤ q.degree
⊢ (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).degree ≤ q.degree

Tactic:
rw [gcd_comm]

Premises used: gcd_comm
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
⊢ (@gcd _ CommSemiring.toCommMonoidWithZero _ q p).degree ≤ q.degree

Tactic:
degree_gcd_le_left hq p

Premises used: Polynomial.degree_gcd_le_left
-- Module: Mathlib.RingTheory.Polynomial.Content
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
⊢ (@gcd _ CommSemiring.toCommMonoidWithZero _ q p).degree ≤ q.degree

Tactic:
exact degree_gcd_le_left hq p

Premises used: Polynomial.degree_gcd_le_left
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ p.contentIdeal = span (↑p.coeffs : Set R)

Tactic:
rfl

Premises used: Polynomial.contentIdeal, rfl
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := Ideal R) (contentIdeal 0) ⊥

Tactic:
simp [contentIdeal_def]

Premises used: Polynomial.contentIdeal_def
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
simp : (∀ x ∈ (↑p.coeffs : Set R), x = 0) ↔ p = 0
⊢ p.contentIdeal = ⊥ ↔ p = 0

Tactic:
simp only [contentIdeal_def, span_eq_bot]

Premises used: Polynomial.contentIdeal_def, Ideal.span_eq_bot
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
h : p = 0
⊢ ∀ x ∈ (↑p.coeffs : Set R), x = 0

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Polynomial.ContentIdeal
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
refine : (∀ x ∈ (↑p.coeffs : Set R), x = 0) → p = 0
⊢ (∀ x ∈ (↑p.coeffs : Set R), x = 0) ↔ p = 0

Tactic:
refine ⟨?_, fun h ↦ by simp [h]⟩