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)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this_1 : NormalizedGCDMonoid R := Nonempty.some ⋯
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) b
hb₂ : map (algebraMap R K) g' = b • g
g'_mul_f : g' * f = b • k
this : g'.content = b * (↑(normUnit b) : R) * k.content
⊢ HSMul.hSMul (β := K[X]) b
      (((mapRingHom (algebraMap R K) : RingHom.{u_1, u_2} R[X] K[X]) : (a : R[X]) → K[X])
          (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit b) : R) : R[X])
              ((C : (a : R) → R[X]) k.content : R[X]) *
            g'.primPart) :
        K[X]) =
    map (algebraMap R K) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g'.content : R[X]) g'.primPart)

Tactic:
simp [this, Polynomial.map_mul, map_C, Algebra.smul_def, algebraMap_apply,
    mul_assoc]

Premises used: Polynomial.map_mul, Polynomial.algebraMap_apply, mul_assoc, Algebra.smul_def, Polynomial.map_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)
f : R[X]
hf : f.IsPrimitive
g : K[X]
rw :
  Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) (g * map (algebraMap R K) f) ↔
    Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) g
rw₁ rw₂ :
  Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) g ↔
    Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) g
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) (map (algebraMap R K) f * g) ↔
    Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) g

Tactic:
rw [mul_comm, hf.mul_map_mem_lifts_iff]

Premises used: Polynomial.IsPrimitive.mul_map_mem_lifts_iff, 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 : R[X]
hp : p.IsPrimitive
⊢ Irreducible p ↔ Irreducible (M := K[X]) (map (algebraMap R K) p)

Tactic:
⟨fun hi => ⟨fun h => hi.not_isUnit (hp.isUnit_iff_isUnit_map.2 h), fun a b hab => ?_⟩,
      hp.irreducible_of_irreducible_map_of_injective (IsFractionRing.injective _ _)⟩

Premises used: Iff.mpr, IsFractionRing.injective, Polynomial.IsPrimitive.irreducible_of_irreducible_map_of_injective, Irreducible.not_isUnit, Irreducible.mk, Iff.intro, Polynomial.IsPrimitive.isUnit_iff_isUnit_map
-- 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 : ∀ (hi : Irreducible p) (a b : K[X]) (hab : map (algebraMap R K) p = a * b), IsUnit a ∨ IsUnit b
⊢ Irreducible p ↔ Irreducible (M := K[X]) (map (algebraMap R K) p)

Tactic:
refine
    ⟨fun hi => ⟨fun h => hi.not_isUnit (hp.isUnit_iff_isUnit_map.2 h), fun a b hab => ?_⟩,
      hp.irreducible_of_irreducible_map_of_injective (IsFractionRing.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 : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
obtain :
  ∀ (c : R) (c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c)
    (hc : map (algebraMap R K) (integerNormalization R⁰ a) = c • a), IsUnit a ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
obtain ⟨c, c0, hc⟩ := integerNormalization_spec R⁰ a

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 : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c
hc : map (algebraMap R K) (integerNormalization R⁰ a) = c • a
obtain :
  ∀ (d : R) (d0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) d)
    (hd : map (algebraMap R K) (integerNormalization R⁰ b) = d • b), IsUnit a ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
obtain ⟨d, d0, hd⟩ := integerNormalization_spec R⁰ b

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 : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c
hc : map (algebraMap R K) (integerNormalization R⁰ a) = c • a
d : R
d0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) d
hd : map (algebraMap R K) (integerNormalization R⁰ b) = d • b
rw :
  ∀
    (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 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) d)
    (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),
    IsUnit a ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
rw [Algebra.smul_def, algebraMap_apply] at hc hd

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 : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c
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 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) d
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
rw :
  ∀ (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),
    IsUnit a ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
rw [mem_nonZeroDivisors_iff_ne_zero] at c0 d0

Premises used: mem_nonZeroDivisors_iff_ne_zero
-- 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
⊢ c * d ≠ 0

Tactic:
have hcd0 : c * d ≠ 0 := mul_ne_zero c0 d0
-- 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 : c * d ≠ 0
⊢ ¬Eq (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X]) (0 : R[X])

Tactic:
rw [Ne, ← C_eq_zero] at hcd0

Premises used: Polynomial.C_eq_zero, Ne
-- 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])
apply :
  Eq (α := K[X])
    (map (algebraMap R K)
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) ((C : (a : R) → R[X]) d : R[X]) * p))
    (map (algebraMap R K) (HMul.hMul (α := R[X]) (integerNormalization R⁰ a) (integerNormalization R⁰ b)))
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) ((C : (a : R) → R[X]) d : R[X]) * p =
    HMul.hMul (α := R[X]) (integerNormalization R⁰ a) (integerNormalization R⁰ b)

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 : 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])
rw :
  HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X])
        ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) d) : K[X]) *
      (a * b) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) a *
      HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) d) : K[X]) b
⊢ Eq (α := K[X])
    (map (algebraMap R K)
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) ((C : (a : R) → R[X]) d : R[X]) * p))
    (map (algebraMap R K) (HMul.hMul (α := R[X]) (integerNormalization R⁰ a) (integerNormalization R⁰ b)))

Tactic:
rw [Polynomial.map_mul, Polynomial.map_mul, Polynomial.map_mul, hc, hd, map_C, map_C, hab]

Premises used: Polynomial.map_mul, Polynomial.map_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 : 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])
⊢ HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X])
        ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) d) : K[X]) *
      (a * b) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) a *
      HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) d) : K[X]) b

Tactic:
ring
-- 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])
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) ((C : (a : R) → R[X]) d : R[X]) * p =
    HMul.hMul (α := R[X]) (integerNormalization R⁰ a) (integerNormalization R⁰ b)

Tactic:
have h1 : C c * C d * p = integerNormalization R⁰ a * integerNormalization R⁰ b := by
    apply map_injective (algebraMap R K) (IsFractionRing.injective _ _) _
    rw [Polynomial.map_mul, Polynomial.map_mul, Polynomial.map_mul, hc, hd, map_C, map_C, hab]
    ring
-- 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])
h1 :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) ((C : (a : R) → R[X]) d : R[X]) * p =
    HMul.hMul (α := R[X]) (integerNormalization R⁰ a) (integerNormalization R⁰ b)
have : ∀ (this : NormalizedGCDMonoid R), IsUnit a ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b

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 : 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])
h1 :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) ((C : (a : R) → R[X]) d : R[X]) * p =
    HMul.hMul (α := R[X]) (integerNormalization R⁰ a) (integerNormalization R⁰ b)
this : NormalizedGCDMonoid R
obtain :
  ∀ (u : Rˣ)
    (hu :
      c * d * (↑u : R) =
        HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))),
    IsUnit a ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
obtain ⟨u, hu⟩ :
    Associated (c * d)
      (content (integerNormalization R⁰ a) * content (integerNormalization R⁰ b)) := by
    rw [← dvd_dvd_iff_associated, ← normalize_eq_normalize_iff, normalize.map_mul,
      normalize.map_mul, normalize_content, normalize_content, ←
      mul_one (normalize c * normalize d), ← hp.content_eq_one, ← content_C, ← content_C, ←
      content_mul, ← content_mul, ← content_mul, h1]

Premises used: HMul.hMul, nonZeroDivisors, Polynomial.content, Associated, 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 : 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])
h1 :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) ((C : (a : R) → R[X]) d : R[X]) * p =
    HMul.hMul (α := R[X]) (integerNormalization R⁰ a) (integerNormalization R⁰ b)
this : NormalizedGCDMonoid R
u : Rˣ
hu : c * d * (↑u : R) = HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))
rw :
  ∀ (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))),
    IsUnit a ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
rw [← map_mul, eq_comm, (integerNormalization R⁰ a).eq_C_content_mul_primPart,
    (integerNormalization R⁰ b).eq_C_content_mul_primPart, mul_assoc, mul_comm _ (C _ * _), ←
    mul_assoc, ← mul_assoc, ← map_mul, ← hu, map_mul, mul_assoc, mul_assoc, ←
    mul_assoc (C (u : R))] at h1

Premises used: Units.val, Polynomial.C, HMul.hMul, mul_assoc, nonZeroDivisors, Polynomial.eq_C_content_mul_primPart, eq_comm, map_mul, mul_comm, DFunLike.coe, 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 : 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 : ¬Eq (α := K[X]) (map (algebraMap R K) p) 0
⊢ a ≠ 0 ∧ b ≠ 0

Tactic:
rw [Ne, Ne, ← not_or, ← mul_eq_zero, ← hab]

Premises used: Ne, 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))
con : Eq (α := K[X]) (map (algebraMap R K) p) 0
apply : Eq (α := K[X]) (map (algebraMap R K) p) (map (algebraMap R K) 0)
⊢ False

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

Premises used: Algebra.algebraMap, IsFractionRing.injective, Polynomial.map_injective, Polynomial.IsPrimitive.ne_zero
-- 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))
con : Eq (α := K[X]) (map (algebraMap R K) p) 0
⊢ Eq (α := K[X]) (map (algebraMap R K) p) (map (algebraMap R K) 0)

Tactic:
simp [con]