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])
this : NormalizedGCDMonoid R
u : Rˣ
h1 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X]) (primPart (integerNormalization R⁰ b)) *
        primPart (integerNormalization R⁰ a)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (c * d) : R[X]) p
hu : c * d * (↑u : R) = HMul.hMul (α := R) (content (integerNormalization R⁰ a)) (content (integerNormalization R⁰ b))
h0 : a ≠ 0 ∧ b ≠ 0
inl :
  ∀
    (h :
      IsUnit
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑u : R) : R[X])
          (primPart (integerNormalization R⁰ b)))),
    IsUnit a ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b
have inr : ∀ (h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ a))), IsUnit a ∨ IsUnit b
Tactic: rcases hi.isUnit_or_isUnit (mul_left_cancel₀ hcd0 h1).symm with (h | h)
-- 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
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
have inl : IsUnit b
Tactic: right
-- 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
h : IsUnit.{u_1} (M := R[X]) (primPart (integerNormalization R⁰ a))
⊢ IsUnit a ∨ IsUnit b
have inr : IsUnit a
Tactic: left
-- 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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h_dvd : Dvd.dvd (α := K[X]) (map (algebraMap R K) p) (map (algebraMap R K) q)
⊢ p ∣ q
have rcases : ∀ (r : K[X]) (hr : map (algebraMap R K) q = map (algebraMap R K) p * r), p ∣ q
Tactic: rcases h_dvd with ⟨r, hr⟩
Cleared hypotheses: h_dvd
-- 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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
⊢ p ∣ q
have obtain : ∀ (s : R) (s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s)
  (hs : map (algebraMap R K) (integerNormalization R⁰ r) = s • r), p ∣ q
Tactic: obtain ⟨s, s0, hs⟩ := integerNormalization_spec R⁰ r
-- 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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs : map (algebraMap R K) (integerNormalization R⁰ r) = s • r
⊢ p ∣ q
have hs₁ : map (algebraMap R K) (integerNormalization R⁰ r) =
  HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
Tactic: rw [Algebra.smul_def, algebraMap_apply] at hs
Cleared hypotheses: hs
-- 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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
⊢ p ∣ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])
have h : HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X]) = p * integerNormalization R⁰ r
Tactic: use integerNormalization R⁰ 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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
⊢ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X]) = p * integerNormalization R⁰ r
have h : Eq (α := K[X]) (map (algebraMap R K) (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])))
  (map (algebraMap R K) (p * integerNormalization R⁰ r))
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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
⊢ Eq (α := K[X]) (map (algebraMap R K) (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])))
    (map (algebraMap R K) (p * integerNormalization R⁰ r))
have h : map (algebraMap R K) p * (map (algebraMap R K) ((C : (a : R) → R[X]) s) * r) =
  map (algebraMap R K) p * HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
Tactic: rw [Polynomial.map_mul, Polynomial.map_mul, hs, hr, mul_assoc, mul_comm r]
-- 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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
⊢ p ∣ q
have h : p ∣ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])
Tactic: have h : p ∣ q * C s := by
    use integerNormalization R⁰ r
    apply map_injective (algebraMap R K) (IsFractionRing.injective _ _)
    rw [Polynomial.map_mul, Polynomial.map_mul, hs, hr, mul_assoc, mul_comm r]
    simp
-- 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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
h : p ∣ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])
⊢ p ∣ q
have have : ∀ (this : NormalizedGCDMonoid R), p ∣ q
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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
h : p ∣ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])
this : NormalizedGCDMonoid R
⊢ p ∣ q
have rw : ∀ (h : p ∣ q * primPart ((C : (a : R) → R[X]) s)) (h : p ∣ q), p ∣ q
Tactic: rw [← hp.dvd_primPart_iff_dvd, primPart_mul, hq.primPart_eq, Associated.dvd_iff_dvd_right] at h
Cleared hypotheses: h
-- 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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
h : p ∣ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])
this : NormalizedGCDMonoid R
rw : ∀ (h : p ∣ q * primPart ((C : (a : R) → R[X]) s)) (h : p ∣ q), p ∣ q
⊢ p ∣ q
have rw₁ : ∀ (h : p ∣ q * primPart ((C : (a : R) → R[X]) s)), Associated (q * primPart ((C : (a : R) → R[X]) s)) q
Tactic: rw [← hp.dvd_primPart_iff_dvd, primPart_mul, hq.primPart_eq, Associated.dvd_iff_dvd_right] at h
Cleared hypotheses: h
-- 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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
h : p ∣ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])
this : NormalizedGCDMonoid R
rw : ∀ (h : p ∣ q * primPart ((C : (a : R) → R[X]) s)) (h : p ∣ q), p ∣ q
rw₁ : ∀ (h : p ∣ q * primPart ((C : (a : R) → R[X]) s)), Associated (q * primPart ((C : (a : R) → R[X]) s)) q
⊢ p ∣ q
have rw₂ : (h : p ∣ q * primPart ((C : (a : R) → R[X]) s)) → R[X]
Tactic: rw [← hp.dvd_primPart_iff_dvd, primPart_mul, hq.primPart_eq, Associated.dvd_iff_dvd_right] at h
Cleared hypotheses: h
-- 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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
h : p ∣ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])
this : NormalizedGCDMonoid R
rw : ∀ (h : p ∣ q * primPart ((C : (a : R) → R[X]) s)) (h : p ∣ q), p ∣ q
rw₁ : ∀ (h : p ∣ q * primPart ((C : (a : R) → R[X]) s)), Associated (q * primPart ((C : (a : R) → R[X]) s)) q
rw₂ : (h : p ∣ q * primPart ((C : (a : R) → R[X]) s)) → R[X]
⊢ p ∣ q
have rw₃ : ∀ (h : p ∣ (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])).primPart),
  HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X]) ≠ 0
Tactic: rw [← hp.dvd_primPart_iff_dvd, primPart_mul, hq.primPart_eq, Associated.dvd_iff_dvd_right] at h
Cleared hypotheses: h
-- 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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
h : p ∣ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])
this : NormalizedGCDMonoid R
rw : ∀ (h : p ∣ q * primPart ((C : (a : R) → R[X]) s)) (h : p ∣ q), p ∣ q
rw₁ : ∀ (h : p ∣ q * primPart ((C : (a : R) → R[X]) s)), Associated (q * primPart ((C : (a : R) → R[X]) s)) q
rw₂ : (h : p ∣ q * primPart ((C : (a : R) → R[X]) s)) → R[X]
rw₃ :
  ∀ (h : p ∣ (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])).primPart),
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X]) ≠ 0
⊢ p ∣ q
have rw₄ : HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X]) ≠ 0
Tactic: rw [← hp.dvd_primPart_iff_dvd, primPart_mul, hq.primPart_eq, Associated.dvd_iff_dvd_right] at h
-- 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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
this : NormalizedGCDMonoid R
h : p ∣ q * primPart ((C : (a : R) → R[X]) s)
⊢ Associated (q * primPart ((C : (a : R) → R[X]) s)) q
have symm : Associated q (q * primPart ((C : (a : R) → R[X]) s))
Tactic: symm
-- 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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
this : NormalizedGCDMonoid R
h : p ∣ q * primPart ((C : (a : R) → R[X]) s)
⊢ Associated q (q * primPart ((C : (a : R) → R[X]) s))
have rcases : ∀ (u : R[X]ˣ) (hu : (↑u : R[X]) = primPart ((C : (a : R) → R[X]) s)),
  Associated q (q * primPart ((C : (a : R) → R[X]) s))
Tactic: rcases isUnit_primPart_C s with ⟨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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
this : NormalizedGCDMonoid R
h : p ∣ q * primPart ((C : (a : R) → R[X]) s)
u : R[X]ˣ
hu : (↑u : R[X]) = primPart ((C : (a : R) → R[X]) s)
⊢ Associated q (q * primPart ((C : (a : R) → R[X]) s))
have h₁ : q * (↑u : R[X]) = q * primPart ((C : (a : R) → R[X]) s)
Tactic: use u
-- 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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
this : NormalizedGCDMonoid R
h : p ∣ q * primPart ((C : (a : R) → R[X]) s)
u : R[X]ˣ
hu : (↑u : R[X]) = primPart ((C : (a : R) → R[X]) s)
⊢ q * (↑u : R[X]) = q * primPart ((C : (a : R) → R[X]) s)
have h₁ : q * primPart ((C : (a : R) → R[X]) s) = q * primPart ((C : (a : R) → R[X]) s)
Tactic: rw [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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
this : NormalizedGCDMonoid R
h : p ∣ (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])).primPart
⊢ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X]) ≠ 0
have apply : Ne (α := R[X]) ((C : (a : R) → R[X]) s : R[X]) (0 : R[X])
Tactic: apply mul_ne_zero hq.ne_zero
-- 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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
this : NormalizedGCDMonoid R
h : p ∣ (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])).primPart
⊢ Ne (α := R[X]) ((C : (a : R) → R[X]) s : R[X]) (0 : R[X])
have rw : ¬s = 0
Tactic: rw [Ne, C_eq_zero]
-- 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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
this : NormalizedGCDMonoid R
h : p ∣ (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])).primPart
⊢ ¬s = 0
have contrapose : ∀ (s0 : s = 0), s ∉ (R⁰ : Submonoid R)
Tactic: contrapose s0
Cleared hypotheses: s0
-- 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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
h : p ∣ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])
this : NormalizedGCDMonoid R
⊢ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X]) ≠ 0
have apply : Ne (α := R[X]) ((C : (a : R) → R[X]) s : R[X]) (0 : R[X])
Tactic: apply mul_ne_zero hq.ne_zero
-- 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 q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
s : R
s0 : Membership.mem (γ := Submonoid R) (R⁰ : Submonoid R) s
hs :
  map (algebraMap R K) (integerNormalization R⁰ r) =
    HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((algebraMap R K : (a : R) → K) s) : K[X]) r
h : p ∣ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) s : R[X])
this : NormalizedGCDMonoid R
⊢ Ne (α := R[X]) ((C : (a : R) → R[X]) s : R[X]) (0 : R[X])
have rw : ¬s = 0
Tactic: rw [Ne, C_eq_zero]