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
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)
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)
⊢ 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) (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)))
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)
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)
rw₅ :
  HMul.hMul (α := R) (β := R) ((normalize : (a : R) → R) c : R) ((normalize : (a : R) → R) d : 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) * 1 =
  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
⊢ IsUnit a ∨ IsUnit b
have obtain : ∀ (u : Rˣ)
  (hu :
    c * d * (↑u : R) = HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ 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]
-- 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
u : Rˣ
hu : c * d * (↑u : R) = HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))
⊢ IsUnit a ∨ IsUnit b
have 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
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
Cleared hypotheses: h1, this, u, hu
-- 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])
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
have rw : ¬Eq (α := K[X]) (map (algebraMap R K) p) 0
Tactic: rw [Ne, Ne, ← not_or, ← mul_eq_zero, ← hab]
-- 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])
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
⊢ False
have apply : Eq (α := K[X]) (map (algebraMap R K) p) (map (algebraMap R K) 0)
Tactic: apply hp.ne_zero (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])
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
have rw : ¬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]
-- 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])
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
⊢ a ≠ 0 ∧ b ≠ 0
have rw₁ : ¬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]
-- 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])
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
⊢ a ≠ 0 ∧ b ≠ 0
have rw₂ : ¬(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]
-- 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])
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)
⊢ a ≠ 0 ∧ b ≠ 0
have rw₃ : ¬a * 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]
-- 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])
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
⊢ a ≠ 0 ∧ b ≠ 0
have rw₄ : ¬Eq (α := K[X]) (map (algebraMap R K) p) 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]
-- 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])
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
⊢ a ≠ 0 ∧ b ≠ 0
have rw₈ : ∀ (con : Eq (α := K[X]) (map (algebraMap R K) p) 0), Eq (α := K[X]) (map (algebraMap R K) p) (map (algebraMap R K) 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]
-- 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])
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
have h0 : 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]
-- 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])
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
⊢ IsUnit a ∨ IsUnit b
have 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
Tactic: rcases hi.isUnit_or_isUnit (mul_left_cancel₀ hcd0 h1).symm with (h | h)