awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
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)
have hi : ∀ (hi : Irreducible p) (a b : K[X]) (hab : map (algebraMap R K) p = a * b), IsUnit a ∨ IsUnit b
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 _ _)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
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
⊢ IsUnit a ∨ IsUnit b
have 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
Tactic: obtain ⟨c, c0, hc⟩ := integerNormalization_spec R⁰ a
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
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
⊢ IsUnit a ∨ IsUnit b
have 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
Tactic: obtain ⟨d, d0, hd⟩ := integerNormalization_spec R⁰ b
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
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
⊢ IsUnit a ∨ IsUnit b
have 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
Tactic: rw [Algebra.smul_def, algebraMap_apply] at hc hd
Cleared hypotheses: hc, d, d0, hd
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
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
⊢ IsUnit a ∨ IsUnit b
have 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
Tactic: rw [mem_nonZeroDivisors_iff_ne_zero] at c0 d0
Cleared hypotheses: c0, hc, d, d0, hd
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (hypothesis)
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
⊢ IsUnit a ∨ IsUnit b
have hcd0 : c * d ≠ 0
Tactic: have hcd0 : c * d ≠ 0 := mul_ne_zero c0 d0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (hypothesis)
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
⊢ IsUnit a ∨ IsUnit b
have hcd0₁ : ¬Eq (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X]) (0 : R[X])
Tactic: rw [Ne, ← C_eq_zero] at hcd0
Cleared hypotheses: hcd0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
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)
have 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)))
Tactic: apply map_injective (algebraMap R K) (IsFractionRing.injective _ _) _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
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])
⊢ 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)))
have 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
Tactic: rw [Polynomial.map_mul, Polynomial.map_mul, Polynomial.map_mul, hc, hd, map_C, map_C, hab]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (hypothesis)
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])
⊢ IsUnit a ∨ IsUnit b
have 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)
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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
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)
⊢ IsUnit a ∨ IsUnit b
have have : ∀ (this : NormalizedGCDMonoid R), IsUnit a ∨ IsUnit b
Tactic: have := Classical.arbitrary (NormalizedGCDMonoid R)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
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
⊢ Associated (c * d) (HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)))
have rw : c * d ∣ HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)) ∧
  HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)) ∣ c * d
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
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
rw :
  c * d ∣ HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)) ∧
    HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)) ∣ c * d
⊢ Associated (c * d) (HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)))
have rw₁ : Eq (α := R) ((normalize : (a : R) → R) (c * d) : R)
  ((normalize : (a : R) → R)
      (HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))) :
    R)
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
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
rw :
  c * d ∣ HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)) ∧
    HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)) ∣ c * d
rw₁ :
  Eq (α := R) ((normalize : (a : R) → R) (c * d) : R)
    ((normalize : (a : R) → R)
        (HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))) :
      R)
⊢ Associated (c * d) (HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)))
have rw₂ : HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) c : R) ((normalize : (a : R) → R) d : R) =
  (normalize : (a : R) → R)
    (HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)))
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
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
rw :
  c * d ∣ HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)) ∧
    HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)) ∣ c * d
rw₁ :
  Eq (α := R) ((normalize : (a : R) → R) (c * d) : R)
    ((normalize : (a : R) → R)
        (HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))) :
      R)
rw₂ :
  HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) c : R) ((normalize : (a : R) → R) d : R) =
    (normalize : (a : R) → R)
      (HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)))
⊢ Associated (c * d) (HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)))
have rw₃ : HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) c : R) ((normalize : (a : R) → R) d : R) =
  HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) (content (integerNormalization R⁰ a)) : R)
    ((normalize : (a : R) → R) (content (integerNormalization R⁰ b)) : R)
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.GaussLemma (goal)
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
rw :
  c * d ∣ HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)) ∧
    HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)) ∣ c * d
rw₁ :
  Eq (α := R) ((normalize : (a : R) → R) (c * d) : R)
    ((normalize : (a : R) → R)
        (HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))) :
      R)
rw₂ :
  HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) c : R) ((normalize : (a : R) → R) d : R) =
    (normalize : (a : R) → R)
      (HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)))
rw₃ :
  HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) c : R) ((normalize : (a : R) → R) d : R) =
    HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) (content (integerNormalization R⁰ a)) : R)
      ((normalize : (a : R) → R) (content (integerNormalization R⁰ b)) : R)
⊢ Associated (c * d) (HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b)))
have rw₄ : HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) c : R) ((normalize : (a : R) → R) d : R) =
  HMul.hMul (α := R) (β := R) (content (integerNormalization R⁰ a) : R)
    ((normalize : (a : R) → R) (content (integerNormalization R⁰ b)) : R)
Tactic: 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]