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
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
⊢ (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
have mp₃ : p.content ∣ s.content →
  p.primPart ∣ s.primPart → q.content ∣ s.content → q.primPart ∣ s.primPart → p.content ∣ s.content
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
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
⊢ (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
have mp₄ : p.content ∣ s.content →
  p.primPart ∣ s.primPart → q.content ∣ s.content → q.primPart ∣ s.primPart → q.content ∣ s.content
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
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
⊢ (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
have mp₅ : p.content ∣ s.content →
  p.primPart ∣ s.primPart → q.content ∣ s.content → q.primPart ∣ s.primPart → p.primPart ∣ s.primPart
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
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
⊢ (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
have mp₆ : p.content ∣ s.content →
  p.primPart ∣ s.primPart → q.content ∣ s.content → q.primPart ∣ s.primPart → q.primPart ∣ s.primPart
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
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
⊢ (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
have 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
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
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
⊢ (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
have mpr₃ : p.content ∣ s.content →
  q.content ∣ s.content → p.primPart ∣ s.primPart → q.primPart ∣ s.primPart → p.content ∣ s.content
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
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
⊢ (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
have mpr₄ : p.content ∣ s.content →
  q.content ∣ s.content → p.primPart ∣ s.primPart → q.primPart ∣ s.primPart → p.primPart ∣ s.primPart
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
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
⊢ (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
have mpr₅ : p.content ∣ s.content →
  q.content ∣ s.content → p.primPart ∣ s.primPart → q.primPart ∣ s.primPart → q.content ∣ s.content
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
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
⊢ (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
have mpr₆ : p.content ∣ s.content →
  q.content ∣ s.content → p.primPart ∣ s.primPart → q.primPart ∣ s.primPart → q.primPart ∣ s.primPart
Tactic: tauto
-- 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]
hp : p ≠ 0
q : R[X]
⊢ (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).degree ≤ p.degree
have this : (@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)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Content (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
⊢ (@gcd _ CommSemiring.toCommMonoidWithZero _ p q).degree ≤ q.degree
have rw : (@gcd _ CommSemiring.toCommMonoidWithZero _ q p).degree ≤ q.degree
Tactic: rw [gcd_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ p.contentIdeal = ⊥ ↔ p = 0
have simp : (∀ x ∈ (↑p.coeffs : Set R), x = 0) ↔ p = 0
Tactic: simp only [contentIdeal_def, span_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ (∀ x ∈ (↑p.coeffs : Set R), x = 0) ↔ p = 0
have refine : (∀ x ∈ (↑p.coeffs : Set R), x = 0) → p = 0
Tactic: refine ⟨?_, fun h ↦ by simp [h]⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ (∀ x ∈ (↑p.coeffs : Set R), x = 0) → p = 0
have contrapose! : p ≠ 0 → ∃ x ∈ (↑p.coeffs : Set R), x ≠ 0
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
⊢ p.coeff n ∈ p.contentIdeal
have pos : ∀ (h : p.coeff n = 0), p.coeff n ∈ p.contentIdeal
Tactic: by_cases h : p.coeff n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
pos : ∀ (h : p.coeff n = 0), p.coeff n ∈ p.contentIdeal
⊢ p.coeff n ∈ p.contentIdeal
have neg : ∀ (h : ¬p.coeff n = 0), p.coeff n ∈ p.contentIdeal
Tactic: by_cases h : p.coeff n = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h : ¬p.coeff n = 0
⊢ p.coeff n ∈ p.contentIdeal
have neg : p.coeff n ∈ (↑p.coeffs : Set R)
Tactic: apply subset_span
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
r : R
⊢ Eq (α := Ideal R) (contentIdeal ((monomial n : (a : R) → R[X]) r)) (span {r})
have pos : ∀ (h : r = 0), Eq (α := Ideal R) (contentIdeal ((monomial n : (a : R) → R[X]) r)) (span {r})
Tactic: by_cases h : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
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})
⊢ Eq (α := Ideal R) (contentIdeal ((monomial n : (a : R) → R[X]) r)) (span {r})
have neg : ∀ (h : ¬r = 0), Eq (α := Ideal R) (contentIdeal ((monomial n : (a : R) → R[X]) r)) (span {r})
Tactic: by_cases h : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := Ideal R) (contentIdeal 1) ⊤
have rw : Eq (α := Ideal R) (contentIdeal 1) (span {1})
Tactic: rw [← span_singleton_one, ← contentIdeal_C 1, C_1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_1
inst : Semiring R
rw : Eq (α := Ideal R) (contentIdeal 1) (span {1})
⊢ Eq.{u_1 + 1} (α := Ideal R) (contentIdeal 1) ⊤
have rw₁ : Eq.{u_1 + 1} (α := Ideal R) (contentIdeal 1) (contentIdeal ((C : (a : R) → R[X]) 1))
Tactic: rw [← span_singleton_one, ← contentIdeal_C 1, C_1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
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))
⊢ Eq.{u_1 + 1} (α := Ideal R) (contentIdeal 1) ⊤
have rw₂ : Eq.{u_1 + 1} (α := Ideal R) (contentIdeal 1) (contentIdeal 1)
Tactic: rw [← span_singleton_one, ← contentIdeal_C 1, C_1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
⊢ (map f p).contentIdeal = Ideal.map f p.contentIdeal
have suffices : Eq (α := Ideal S) (span ((↑(map f p).coeffs : Set S) ∪ {0})) (span ((⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}))
Tactic: suffices span ((map f p).coeffs ∪ {0}) = span (f '' p.coeffs ∪ {0}) by
    simpa [contentIdeal_def, map_span]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
⊢ Eq (α := Ideal S) (span ((↑(map f p).coeffs : Set S) ∪ {0})) (span ((⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}))
have e_s : (↑(map f p).coeffs : Set S) ∪ {0} = (⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.ContentIdeal (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
⊢ (↑(map f p).coeffs : Set S) ∪ {0} = (⇑f : (a : R) → S) '' (↑p.coeffs : Set R) ∪ {0}
have 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
Tactic: ext s