awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc :
  map (algebraMap R K) (integerNormalization R⁰ a) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) a
d : R
d0 : d ≠ 0
hd :
  map (algebraMap R K) (integerNormalization R⁰ b) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) d) : K[X]) b
hcd0 : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X]) (0 : R[X])
this : NormalizedGCDMonoid R
u : Rˣ
h1 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ b)) *
        primPart (integerNormalization R⁰ a)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X]) p
hu : c * d * (↑u : R) = HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))
rw : ¬a = 0 ∧ b ≠ 0
rw₁ : ¬a = 0 ∧ ¬b = 0
rw₂ : ¬(a = 0 ∨ b = 0)
rw₃ : ¬a * b = 0
rw₄ rw₅ rw₆ : ¬Eq (α := K[X]) (map (algebraMap R K) p) 0
rw₇ : ∀ (con : Eq (α := K[X]) (map (algebraMap R K) p) 0), False
rw₈ :
  ∀ (con : Eq (α := K[X]) (map (algebraMap R K) p) 0), Eq (α := K[X]) (map (algebraMap R K) p) (map (algebraMap R K) 0)
⊢ a ≠ 0 ∧ b ≠ 0

Tactic:
classical
    rw [Ne, Ne, ← not_or, ← mul_eq_zero, ← hab]
    intro con
    apply hp.ne_zero (map_injective (algebraMap R K) (IsFractionRing.injective _ _) _)
    simp [con]

Premises used: Algebra.algebraMap, IsFractionRing.injective, Polynomial.map_injective, Ne, Polynomial.IsPrimitive.ne_zero, mul_eq_zero, not_or
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc :
  map (algebraMap R K) (integerNormalization R⁰ a) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) a
d : R
d0 : d ≠ 0
hd :
  map (algebraMap R K) (integerNormalization R⁰ b) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) d) : K[X]) b
hcd0 : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X]) (0 : R[X])
this : NormalizedGCDMonoid R
u : Rˣ
h1 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ b)) *
        primPart (integerNormalization R⁰ a)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X]) p
hu : c * d * (↑u : R) = HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))
⊢ a ≠ 0 ∧ b ≠ 0

Tactic:
have h0 : a ≠ 0 ∧ b ≠ 0 := by
    classical
    rw [Ne, Ne, ← not_or, ← mul_eq_zero, ← hab]
    intro con
    apply hp.ne_zero (map_injective (algebraMap R K) (IsFractionRing.injective _ _) _)
    simp [con]
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc :
  map (algebraMap R K) (integerNormalization R⁰ a) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) a
d : R
d0 : d ≠ 0
hd :
  map (algebraMap R K) (integerNormalization R⁰ b) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) d) : K[X]) b
hcd0 : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X]) (0 : R[X])
this : NormalizedGCDMonoid R
u : Rˣ
h1 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ b)) *
        primPart (integerNormalization R⁰ a)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X]) p
hu : c * d * (↑u : R) = HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))
h0 : a ≠ 0 ∧ b ≠ 0
inl :
  ∀
    (h :
      IsUnit
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X])
          (primPart (integerNormalization R⁰ b)))),
    IsUnit a ∨ IsUnit b
inr : ∀ (h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ a))), IsUnit a ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
rcases hi.isUnit_or_isUnit (mul_left_cancel₀ hcd0 h1).symm with (h | h)

Premises used: mul_left_cancel₀, Irreducible.isUnit_or_isUnit, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc :
  map (algebraMap R K) (integerNormalization R⁰ a) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) a
d : R
d0 : d ≠ 0
hd :
  map (algebraMap R K) (integerNormalization R⁰ b) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) d) : K[X]) b
hcd0 : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X]) (0 : R[X])
this : NormalizedGCDMonoid R
u : Rˣ
h1 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ b)) *
        primPart (integerNormalization R⁰ a)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X]) p
hu : c * d * (↑u : R) = HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))
h0 : a ≠ 0 ∧ b ≠ 0
h :
  IsUnit
    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ b)))
inl : IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
right
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc :
  map (algebraMap R K) (integerNormalization R⁰ a) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) a
d : R
d0 : d ≠ 0
hd :
  map (algebraMap R K) (integerNormalization R⁰ b) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) d) : K[X]) b
hcd0 : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X]) (0 : R[X])
this : NormalizedGCDMonoid R
u : Rˣ
h1 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ b)) *
        primPart (integerNormalization R⁰ a)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X]) p
hu : c * d * (↑u : R) = HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))
h0 : a ≠ 0 ∧ b ≠ 0
h :
  IsUnit
    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ b)))
⊢ IsUnit b

Tactic:
apply
      isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart h0.2
        (isUnit_of_mul_isUnit_right h)

Premises used: isUnit_of_mul_isUnit_right, Polynomial.isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart, And.right
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc :
  map (algebraMap R K) (integerNormalization R⁰ a) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) a
d : R
d0 : d ≠ 0
hd :
  map (algebraMap R K) (integerNormalization R⁰ b) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) d) : K[X]) b
hcd0 : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X]) (0 : R[X])
this : NormalizedGCDMonoid R
u : Rˣ
h1 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ b)) *
        primPart (integerNormalization R⁰ a)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X]) p
hu : c * d * (↑u : R) = HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))
h0 : a ≠ 0 ∧ b ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ a))
inr : IsUnit a
⊢ IsUnit a ∨ IsUnit b

Tactic:
left
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc :
  map (algebraMap R K) (integerNormalization R⁰ a) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) a
d : R
d0 : d ≠ 0
hd :
  map (algebraMap R K) (integerNormalization R⁰ b) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) d) : K[X]) b
hcd0 : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X]) (0 : R[X])
this : NormalizedGCDMonoid R
u : Rˣ
h1 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ b)) *
        primPart (integerNormalization R⁰ a)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X]) p
hu : c * d * (↑u : R) = HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))
h0 : a ≠ 0 ∧ b ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ a))
⊢ IsUnit a

Tactic:
apply isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart h0.1 h

Premises used: Polynomial.isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart, And.left
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h_dvd : Dvd.dvd (α := K[X]) (map (algebraMap R K) p) (map (algebraMap R K) q)
rcases : ∀ (r : K[X]) (hr : map (algebraMap R K) q = map (algebraMap R K) p * r), p ∣ q
⊢ p ∣ q

Tactic:
rcases h_dvd with ⟨r, hr⟩
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
obtain :
  ∀ (s : R) (s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s)
    (hs : map (algebraMap R K) (integerNormalization R⁰ r) = s • r), p ∣ q
⊢ p ∣ q

Tactic:
obtain ⟨s, s0, hs⟩ := integerNormalization_spec R⁰ r

Premises used: nonZeroDivisors, IsLocalization.integerNormalization_spec
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs : map (algebraMap R K) (integerNormalization R⁰ r) = s • r
⊢ map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r

Tactic:
rw [Algebra.smul_def, algebraMap_apply] at hs

Premises used: Polynomial.algebraMap_apply, Algebra.smul_def
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
h : HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X]) = p * integerNormalization R⁰ r
⊢ p ∣ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])

Tactic:
use integerNormalization R⁰ r

Premises used: nonZeroDivisors, IsLocalization.integerNormalization
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
h :
  Eq (α := K[X]) (map (algebraMap R K) (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])))
    (map (algebraMap R K) (p * integerNormalization R⁰ r))
⊢ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X]) = p * integerNormalization R⁰ r

Tactic:
apply map_injective (algebraMap R K) (IsFractionRing.injective _ _)

Premises used: Algebra.algebraMap, IsFractionRing.injective, Polynomial.map_injective
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
h :
  map (algebraMap R K) p * (map (algebraMap R K) ((C : (a : R) → R[X]) s) * r) =
    map (algebraMap R K) p * HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
⊢ Eq (α := K[X]) (map (algebraMap R K) (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])))
    (map (algebraMap R K) (p * integerNormalization R⁰ r))

Tactic:
rw [Polynomial.map_mul, Polynomial.map_mul, hs, hr, mul_assoc, mul_comm r]

Premises used: Polynomial.map_mul, mul_assoc, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
⊢ map (algebraMap R K) p * (map (algebraMap R K) ((C : (a : R) → R[X]) s) * r) =
    map (algebraMap R K) p * HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
⊢ p ∣ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])

Tactic:
have h : p ∣ q * C s := by
    use integerNormalization R⁰ r
    apply map_injective (algebraMap R K) (IsFractionRing.injective _ _)
    rw [Polynomial.map_mul, Polynomial.map_mul, hs, hr, mul_assoc, mul_comm r]
    simp
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
h : p ∣ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])
have : ∀ (this : NormalizedGCDMonoid R), p ∣ q
⊢ p ∣ q

Tactic:
have := Classical.arbitrary (NormalizedGCDMonoid R)
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
h : p ∣ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])
this : NormalizedGCDMonoid R
rw : ∀ (h : p ∣ q * primPart ((C : (a : R) → R[X]) s)) (h : p ∣ q), p ∣ q
rw₁ : ∀ (h : p ∣ q * primPart ((C : (a : R) → R[X]) s)), Associated (q * primPart ((C : (a : R) → R[X]) s)) q
rw₂ : (h : p ∣ q * primPart ((C : (a : R) → R[X]) s)) → R[X]
rw₃ :
  ∀ (h : p ∣ (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])).primPart),
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X]) ≠ 0
rw₄ : HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X]) ≠ 0
⊢ p ∣ q

Tactic:
rw [← hp.dvd_primPart_iff_dvd, primPart_mul, hq.primPart_eq, Associated.dvd_iff_dvd_right] at h

Premises used: Polynomial.IsPrimitive.dvd_primPart_iff_dvd, Polynomial.IsPrimitive.primPart_eq, Associated.dvd_iff_dvd_right, Polynomial.primPart_mul
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
this : NormalizedGCDMonoid R
h_1 : p ∣ q * primPart ((C : (a : R) → R[X]) s)
h : p ∣ q
⊢ p ∣ q

Tactic:
h
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
this : NormalizedGCDMonoid R
h_1 : p ∣ q * primPart ((C : (a : R) → R[X]) s)
h : p ∣ q
⊢ p ∣ q

Tactic:
exact h
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
this : NormalizedGCDMonoid R
h : p ∣ q * primPart ((C : (a : R) → R[X]) s)
symm : Associated q (q * primPart ((C : (a : R) → R[X]) s))
⊢ Associated (q * primPart ((C : (a : R) → R[X]) s)) q

Tactic:
symm
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
this : NormalizedGCDMonoid R
h : p ∣ q * primPart ((C : (a : R) → R[X]) s)
rcases :
  ∀ (u : R[X]ˣ) (hu : (↑u : R[X]) = primPart ((C : (a : R) → R[X]) s)),
    Associated q (q * primPart ((C : (a : R) → R[X]) s))
⊢ Associated q (q * primPart ((C : (a : R) → R[X]) s))

Tactic:
rcases isUnit_primPart_C s with ⟨u, hu⟩

Premises used: Polynomial.isUnit_primPart_C
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
this : NormalizedGCDMonoid R
h : p ∣ q * primPart ((C : (a : R) → R[X]) s)
u : R[X]ˣ
hu : (↑u : R[X]) = primPart ((C : (a : R) → R[X]) s)
h₁ : q * (↑u : R[X]) = q * primPart ((C : (a : R) → R[X]) s)
⊢ Associated q (q * primPart ((C : (a : R) → R[X]) s))

Tactic:
use u
-- Module: Mathlib.RingTheory.Polynomial.GaussLemma
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDomain R
inst_5 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
this : NormalizedGCDMonoid R
h : p ∣ q * primPart ((C : (a : R) → R[X]) s)
u : R[X]ˣ
hu : (↑u : R[X]) = primPart ((C : (a : R) → R[X]) s)
h₁ h₂ : q * primPart ((C : (a : R) → R[X]) s) = q * primPart ((C : (a : R) → R[X]) s)
⊢ q * (↑u : R[X]) = q * primPart ((C : (a : R) → R[X]) s)

Tactic:
rw [hu]