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 : IsIntegrallyClosed R
p q : R[X]
hp : p.Monic
hq : q.Monic
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
d' : R[X]
hr' : Polynomial.map (algebraMap R K) d' = r
⊢ Eq (α := K[X]) (Polynomial.map (algebraMap R K) p) (Polynomial.map (algebraMap R K) (q * d'))

Tactic:
rw [← hr', ← Polynomial.map_mul] at hr

Premises used: Polynomial.map_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 : IsIntegrallyClosed R
p q : R[X]
hp : p.Monic
hq : q.Monic
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
d' : R[X]
hr' : Polynomial.map (algebraMap R K) d' = r
hr₁ : Eq (α := K[X]) (Polynomial.map (algebraMap R K) p) (Polynomial.map (algebraMap R K) (q * d'))
⊢ Polynomial.map (algebraMap R K) d' = r

Tactic:
rw [← hr', ← Polynomial.map_mul] at hr

Premises used: Polynomial.map_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 : IsIntegrallyClosed R
p q : R[X]
hp : p.Monic
hq : q.Monic
r : K[X]
d' : R[X]
hr : Eq (α := K[X]) (Polynomial.map (algebraMap R K) p) (Polynomial.map (algebraMap R K) (q * d'))
hr' : Polynomial.map (algebraMap R K) d' = r
⊢ q ∣ p

Tactic:
dvd_of_mul_right_eq _ (Polynomial.map_injective _ (IsFractionRing.injective R K) hr.symm)

Premises used: dvd_of_mul_right_eq, IsFractionRing.injective, Polynomial.map_injective, 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 : IsIntegrallyClosed R
p q : R[X]
hp : p.Monic
hq : q.Monic
r : K[X]
d' : R[X]
hr : Eq (α := K[X]) (Polynomial.map (algebraMap R K) p) (Polynomial.map (algebraMap R K) (q * d'))
hr' : Polynomial.map (algebraMap R K) d' = r
⊢ q ∣ p

Tactic:
exact dvd_of_mul_right_eq _ (Polynomial.map_injective _ (IsFractionRing.injective R K) hr.symm)

Premises used: dvd_of_mul_right_eq, IsFractionRing.injective, Polynomial.map_injective, 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 : IsIntegrallyClosed R
p q : R[X]
hp : p.Monic
hq : q.Monic
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
d' : R[X]
hr' :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) d') ((C : (a : K) → K[X]) r.leadingCoeff : K[X]) =
    r
⊢ (Polynomial.map (algebraMap R K) q * r).Monic

Tactic:
simpa [← hr] using hp.map _

Premises used: Polynomial.Monic.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 : IsIntegrallyClosed R
p q : R[X]
hp : p.Monic
hq : q.Monic
r : K[X]
hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r
d' : R[X]
hr' :
  HMul.hMul (α := K[X]) (β := K[X]) (Polynomial.map (algebraMap R K) d') ((C : (a : K) → K[X]) r.leadingCoeff : K[X]) =
    r
⊢ r.Monic

Tactic:
exact Monic.of_mul_monic_left (hq.map (algebraMap R K)) (by simpa [← hr] using hp.map _)

Premises used: Algebra.algebraMap, Polynomial.Monic.of_mul_monic_left, Polynomial.Monic.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 : IsIntegrallyClosed R
p q : R[X]
hp : p.Monic
hq : q.Monic
⊢ Dvd.dvd (α := K[X]) (Polynomial.map (algebraMap R K) q) (Polynomial.map (algebraMap R K) p) ↔ q ∣ p

Tactic:
⟨fun h => hp.dvd_of_fraction_map_dvd_fraction_map hq h, fun ⟨a, b⟩ =>
    ⟨a.map (algebraMap R K), b.symm ▸ Polynomial.map_mul (algebraMap R K)⟩⟩

Premises used: Polynomial.map_mul, Dvd.dvd, Algebra.algebraMap, Eq.rec, Polynomial.Monic.dvd_of_fraction_map_dvd_fraction_map, Iff.intro, Exists.intro, Polynomial.map, _private.0.Polynomial.Monic.dvd_iff_fraction_map_dvd_fraction_map.match_1, 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 : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ p))
rcases :
  ∀ (u : Rˣ) (hu : Eq (α := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ p) : R[X])),
    IsUnit p
⊢ IsUnit p

Tactic:
rcases isUnit_iff.1 h with ⟨_, ⟨u, rfl⟩, hu⟩

Premises used: Polynomial.isUnit_iff, Iff.mp, rfl
-- 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 : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : Eq (α := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ p) : R[X])
obtain :
  ∀ (c : R) (c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c)
    (hc : map (algebraMap R K) (integerNormalization R⁰ p) = c • p), IsUnit p
⊢ IsUnit p

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

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 : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : Eq (α := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ p) : R[X])
c : R
c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c
hc : map (algebraMap R K) (integerNormalization R⁰ p) = c • p
⊢ map (algebraMap R K) (integerNormalization R⁰ p) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) p

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

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 : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : Eq (α := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ p) : R[X])
c : R
c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c
hc :
  map (algebraMap R K) (integerNormalization R⁰ p) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) p
hu₁ : IsUnit (HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) p)
x : K[X]
⊢ IsUnit p

Tactic:
apply isUnit_of_mul_isUnit_right

Premises used: isUnit_of_mul_isUnit_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 : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : Eq (α := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ p) : R[X])
c : R
c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c
hc :
  map (algebraMap R K) (integerNormalization R⁰ p) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) p
⊢ Eq.{u_2 + 1} (α := K[X])
    ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) (content (integerNormalization R⁰ p) * (↑u : R))) : K[X])
    (map (algebraMap R K) ((C : (a : R) → R[X]) (content (integerNormalization R⁰ p) * (↑u : R))) : K[X])

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 : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : Eq (α := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ p) : R[X])
c : R
c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c
hc :
  map (algebraMap R K) (integerNormalization R⁰ p) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) p
hu₁ :
  ∀
    (con :
      Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (content (integerNormalization R⁰ p) * (↑u : R)) : K)
        (0 : K)),
    False
⊢ ∃ (r : K),
    IsUnit r ∧
      Eq (α := K[X]) ((C : (a : K) → K[X]) r : K[X])
        (map (algebraMap R K) ((C : (a : R) → R[X]) (content (integerNormalization R⁰ p) * (↑u : R))) : K[X])

Tactic:
refine
    ⟨algebraMap R K ((integerNormalization R⁰ p).content * ↑u), isUnit_iff_ne_zero.2 fun con => ?_,
      by 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 : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : Eq (α := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ p) : R[X])
c : R
c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c
hc :
  map (algebraMap R K) (integerNormalization R⁰ p) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) p
con :
  Eq.{u_2 + 1} (α := K) ((algebraMap R K : (a : R) → K) (content (integerNormalization R⁰ p) * (↑u : R)) : K) (0 : K)
⊢ content (integerNormalization R⁰ p) * (↑u : R) = 0

Tactic:
replace con := (injective_iff_map_eq_zero (algebraMap R K)).1 (IsFractionRing.injective _ _) _ 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 : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : Eq (α := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ p) : R[X])
c : R
c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c
hc :
  map (algebraMap R K) (integerNormalization R⁰ p) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) p
con : content (integerNormalization R⁰ p) * (↑u : R) = 0
⊢ p = 0 ∨ (↑u : R) = 0

Tactic:
rw [mul_eq_zero, content_eq_zero_iff, IsFractionRing.integerNormalization_eq_zero_iff] at con

Premises used: Polynomial.content_eq_zero_iff, IsFractionRing.integerNormalization_eq_zero_iff, mul_eq_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 : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : Eq (α := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ p) : R[X])
c : R
c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c
hc :
  map (algebraMap R K) (integerNormalization R⁰ p) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) p
con : p = 0 ∨ (↑u : R) = 0
hu₁ : ∀ (con : p = 0), False
hu₂ : ∀ (con : (↑u : R) = 0), False
⊢ False

Tactic:
rcases con with (con | 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 : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : Eq (α := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ p) : R[X])
c : R
c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c
hc :
  map (algebraMap R K) (integerNormalization R⁰ p) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) p
con : p = 0
⊢ False

Tactic:
apply h0 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 : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ p))
u : Rˣ
hu : Eq (α := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ p) : R[X])
c : R
c0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) c
hc :
  map (algebraMap R K) (integerNormalization R⁰ p) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) c) : K[X]) p
con : (↑u : R) = 0
⊢ False

Tactic:
apply Units.ne_zero _ con

Premises used: Units.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)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := Nonempty.some ⋯
⊢ 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

Tactic:
⟨?_, fun h ↦ Subsemiring.mul_mem _ h ⟨_, rfl⟩⟩

Premises used: Algebra.algebraMap, Subsemiring.mul_mem, Iff.intro, Exists.intro, Polynomial.lifts, rfl
-- 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 : NormalizedGCDMonoid R := Nonempty.some ⋯
refine :
  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
⊢ 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

Tactic:
refine ⟨?_, fun h ↦ Subsemiring.mul_mem _ h ⟨_, rfl⟩⟩
-- 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 : 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
obtain :
  ∀ (b : R) (hb₁ : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) b) (hb₂ : map (algebraMap R K) g' = b • g),
    Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) g
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) g

Tactic:
obtain ⟨b, hb₁, (hb₂ : Polynomial.map _ g' = _)⟩ :=
    integerNormalization_spec (nonZeroDivisors R) g

Premises used: nonZeroDivisors, Polynomial.map, 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)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : 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
a : Eq (α := K[X]) (map (algebraMap R K) (g' * f)) (map (algebraMap R K) (b • k))
⊢ g' * f = b • k

Tactic:
apply Polynomial.map_injective (algebraMap R K) (FaithfulSMul.algebraMap_injective R K)

Premises used: Algebra.algebraMap, Polynomial.map_injective, FaithfulSMul.algebraMap_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)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : 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
a :
  map (algebraMap R K) (g' * f) =
    HSMul.hSMul (α := K) (β := K[X]) ((algebraMap R K : (a : R) → K) b : K) (map (algebraMap R K) k)
a₁ : map (algebraMap R K) (g' * f) = HSMul.hSMul (β := K[X]) b (map (algebraMap R K) k)
a₂ : map (algebraMap R K) (g' * f) = b • (g * map (algebraMap R K) f)
a₃ : map (algebraMap R K) (g' * f) = b • g * map (algebraMap R K) f
a₄ : map (algebraMap R K) (g' * f) = HMul.hMul (α := K[X]) (map (algebraMap R K) g') (map (algebraMap R K) f)
a₅ a₆ :
  HMul.hMul (α := K[X]) (map (algebraMap R K) g') (map (algebraMap R K) f) =
    HMul.hMul (α := K[X]) (map (algebraMap R K) g') (map (algebraMap R K) f)
⊢ Eq (α := K[X]) (map (algebraMap R K) (g' * f)) (map (algebraMap R K) (b • k))

Tactic:
rw [Polynomial.map_smul, algebraMap_smul, hk, ← smul_mul_assoc, ← hb₂, Polynomial.map_mul]

Premises used: Polynomial.map_mul, smul_mul_assoc, algebraMap_smul, Polynomial.map_smul
-- 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 : 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' * f = b • k

Tactic:
have g'_mul_f : g' * f = b • k := by
    apply Polynomial.map_injective (algebraMap R K) (FaithfulSMul.algebraMap_injective R K)
    rw [Polynomial.map_smul, algebraMap_smul, hk, ← smul_mul_assoc, ← hb₂, Polynomial.map_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)
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : 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
h :
  ((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) =
    g
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (algebraMap R K)) g

Tactic:
use C (normUnit b : R) * C k.content * g'.primPart

Premises used: Units.val, Polynomial.C, Polynomial.content, Polynomial.primPart, DFunLike.coe, NormalizationMonoid.normUnit
-- 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 : 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
⊢ (g' * f).content = (b • k).content

Tactic:
have := congr($(g'_mul_f).content)
-- 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' * f).content = (b • k).content
⊢ g'.content = b * (↑(normUnit b) : R) * k.content

Tactic:
simp only [content_mul, hf.content_eq_one, mul_one, smul_eq_C_mul, content_C,
    normalize_apply] at this

Premises used: Polynomial.smul_eq_C_mul, Polynomial.IsPrimitive.content_eq_one, normalize_apply, Polynomial.content_mul, Polynomial.content_C, mul_one
-- 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
h :
  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) g'
⊢ ((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) =
    g

Tactic:
rw [← smul_right_inj (nonZeroDivisors.ne_zero hb₁), ← hb₂]

Premises used: nonZeroDivisors.ne_zero, smul_right_inj
-- 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
h :
  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)
⊢ 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) g'

Tactic:
rw (occs := [2]) [eq_C_content_mul_primPart g']

Premises used: Polynomial.eq_C_content_mul_primPart