awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
a : α
⊢ Quot.out (r := (⇑(Associated.setoid α) : α → α → Prop)) (Associates.mk a ⊔ Associates.mk 0) = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
rw : a ∣ c ∧ a ∣ b
⊢ a ∣ Associates.out (Associates.mk c ⊓ Associates.mk b)

Tactic:
rw [dvd_out_iff, le_inf_iff, mk_le_mk_iff_dvd, mk_le_mk_iff_dvd]

Premises used: Associates.mk_le_mk_iff_dvd, le_inf_iff, Associates.dvd_out_iff
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ a ∣ c ∧ a ∣ b

Tactic:
⟨hac, hab⟩

Premises used: And.intro
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ a ∣ c ∧ a ∣ b

Tactic:
exact ⟨hac, hab⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
a b : α
rw : (normalize : (a : α) → α) (a * b) ~ᵤ a * b
⊢ Associates.out (Associates.mk a ⊓ Associates.mk b) * Associates.out (Associates.mk a ⊔ Associates.mk b) ~ᵤ a * b

Tactic:
rw [← out_mul, mul_comm, sup_mul_inf, mk_mul_mk, out_mk]

Premises used: Associates.out_mk, Associates.mk_mul_mk, Associates.sup_mul_inf, mul_comm, Associates.out_mul
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
a b : α
⊢ (normalize : (a : α) → α) (a * b) ~ᵤ a * b

Tactic:
normalize_associated (a * b)

Premises used: HMul.hMul, normalize_associated
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
a b : α
⊢ (normalize : (a : α) → α) (a * b) ~ᵤ a * b

Tactic:
exact normalize_associated (a * b)

Premises used: HMul.hMul, normalize_associated
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
a : α
⊢ Associates.out (⊤ ⊔ Associates.mk a) = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
a : α
⊢ Associates.out (Associates.mk a ⊔ ⊤) = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
a b : α
⊢ (normalize : (a : α) → α) (Associates.out (Associates.mk a ⊓ Associates.mk b)) =
    Associates.out (Associates.mk a ⊓ Associates.mk b)

Tactic:
apply normalize_out _

Premises used: Associates.normalize_out
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
a b : α
⊢ (normalize : (a : α) → α) (Associates.out (Associates.mk a ⊔ Associates.mk b)) =
    Associates.out (Associates.mk a ⊔ Associates.mk b)

Tactic:
apply normalize_out _

Premises used: Associates.normalize_out
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ Nonempty.{u_2 + 1} (NormalizedGCDMonoid α)

Tactic:
⟨UniqueFactorizationMonoid.toNormalizedGCDMonoid α⟩

Premises used: UniqueFactorizationMonoid.toNormalizedGCDMonoid, Nonempty.intro
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ Nonempty.{u_2 + 1} (NormalizedGCDMonoid α)

Tactic:
exact ⟨UniqueFactorizationMonoid.toNormalizedGCDMonoid α⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
⊢ Nonempty.{u_2 + 1} (NormalizedGCDMonoid α)

Tactic:
classical exact ⟨UniqueFactorizationMonoid.toNormalizedGCDMonoid α⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
obtain : ∀ (a : R) (ha₁ : a ∈ I) (ha₂ : a ≠ 0), ∃ x ∈ I, Prime x
⊢ ∃ x ∈ I, Prime x

Tactic:
obtain ⟨a : R, ha₁ : a ∈ I, ha₂ : a ≠ 0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hI

Premises used: Submodule.exists_mem_ne_zero_of_ne_bot
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₁ : a ∈ I
ha₂ : a ≠ 0
obtain : ∀ (u : Rˣ) (hu : (factors a).prod * (↑u : R) = a), (factors a).prod ∈ I
⊢ (factors a).prod ∈ I

Tactic:
obtain ⟨u : Rˣ, hu : (factors a).prod * u = a⟩ := factors_prod ha₂

Premises used: Multiset.prod, UniqueFactorizationMonoid.factors, UniqueFactorizationMonoid.factors_prod
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₁ : a ∈ I
ha₂ : a ≠ 0
u : Rˣ
hu : (factors a).prod * (↑u : R) = a
rwa : ∀ (ha₁ : (factors a).prod * (↑u : R) ∈ I) (hu : (factors a).prod * (↑u : R) = a), (factors a).prod ∈ I
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (ha₁ : (factors a).prod ∈ I) (hu : (factors a).prod * (↑u : R) = a), (factors a).prod ∈ I
⊢ (factors a).prod ∈ I

Tactic:
rwa [← hu, mul_unit_mem_iff_mem _ u.isUnit] at ha₁

Premises used: Ideal.mul_unit_mem_iff_mem, Units.isUnit
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₁ : a ∈ I
ha₂ : a ≠ 0
⊢ (factors a).prod ∈ I

Tactic:
replace ha₁ : (factors a).prod ∈ I := by
    obtain ⟨u : Rˣ, hu : (factors a).prod * u = a⟩ := factors_prod ha₂
    rwa [← hu, mul_unit_mem_iff_mem _ u.isUnit] at ha₁
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₂ : a ≠ 0
ha₁ : (factors a).prod ∈ I
obtain : ∀ (p : R) (hp₁ : p ∈ factors a) (hp₂ : p ∈ I), ∃ x ∈ I, Prime x
⊢ ∃ x ∈ I, Prime x

Tactic:
obtain ⟨p : R, hp₁ : p ∈ factors a, hp₂ : p ∈ I⟩ :=
    (hI₂.multiset_prod_mem_iff_exists_mem <| factors a).1 ha₁

Premises used: UniqueFactorizationMonoid.factors, Ideal.IsPrime.multiset_prod_mem_iff_exists_mem, Iff.mp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₂ : a ≠ 0
ha₁ : (factors a).prod ∈ I
p : R
hp₁ : p ∈ factors a
hp₂ : p ∈ I
⊢ ∃ x ∈ I, Prime x

Tactic:
⟨p, hp₂, prime_of_factor p hp₁⟩

Premises used: UniqueFactorizationMonoid.prime_of_factor, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
a : R
ha₂ : a ≠ 0
ha₁ : (factors a).prod ∈ I
p : R
hp₁ : p ∈ factors a
hp₂ : p ∈ I
⊢ ∃ x ∈ I, Prime x

Tactic:
exact ⟨p, hp₂, prime_of_factor p hp₁⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : UniqueFactorizationMonoid R
I : Ideal R
hI₂ : I.IsPrime
hI : I ≠ ⊥
obtain : ∀ (a : R) (ha₁ : a ∈ I) (ha₂ : a ≠ 0), ∃ x ∈ I, Prime x
obtain₁ : ∀ (a : R) (ha₂ : a ≠ 0) (ha₁ : (factors a).prod ∈ I), ∃ x ∈ I, Prime x
obtain₂ :
  ∀ (a : R) (ha₂ : a ≠ 0) (ha₁ : (factors a).prod ∈ I) (p : R) (hp₁ : p ∈ factors a) (hp₂ : p ∈ I), ∃ x ∈ I, Prime x
⊢ ∃ x ∈ I, Prime x

Tactic:
classical
  obtain ⟨a : R, ha₁ : a ∈ I, ha₂ : a ≠ 0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hI
  replace ha₁ : (factors a).prod ∈ I := by
    obtain ⟨u : Rˣ, hu : (factors a).prod * u = a⟩ := factors_prod ha₂
    rwa [← hu, mul_unit_mem_iff_mem _ u.isUnit] at ha₁
  obtain ⟨p : R, hp₁ : p ∈ factors a, hp₂ : p ∈ I⟩ :=
    (hI₂.multiset_prod_mem_iff_exists_mem <| factors a).1 ha₁
  exact ⟨p, hp₂, prime_of_factor p hp₁⟩

Premises used: Submodule.exists_mem_ne_zero_of_ne_bot
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : WfDvdMonoid α
inst_2 : IsDomain α
h :
  ∀ (x : Ideal α),
    Membership.mem (γ := Set (Ideal α)) {I : Ideal α | Submodule.IsPrincipal I} x ↔
      Membership.mem (γ := Set (Ideal α)) ((fun (a : α) ↦ span {a}) '' Set.univ) x
⊢ Eq.{u_1 + 1} (α := Set (Ideal α)) {I : Ideal α | Submodule.IsPrincipal I} ((fun (a : α) ↦ span {a}) '' Set.univ)

Tactic:
ext
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : WfDvdMonoid α
inst_2 : IsDomain α
x : Ideal α
⊢ Membership.mem (γ := Set (Ideal α)) {I : Ideal α | Submodule.IsPrincipal I} x ↔
    Membership.mem (γ := Set (Ideal α)) ((fun (a : α) ↦ span {a}) '' Set.univ) x

Tactic:
simp [Submodule.isPrincipal_iff, eq_comm]

Premises used: eq_comm, Submodule.isPrincipal_iff
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : WfDvdMonoid α
inst_2 : IsDomain α
⊢ Eq.{u_1 + 1} (α := Set (Ideal α)) {I : Ideal α | Submodule.IsPrincipal I} ((fun (a : α) ↦ span {a}) '' Set.univ)

Tactic:
have : {I : Ideal α | I.IsPrincipal} = ((fun a ↦ Ideal.span {a}) '' Set.univ) := by
    ext
    simp [Submodule.isPrincipal_iff, eq_comm]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : WfDvdMonoid α
inst_2 : IsDomain α
this : Eq.{u_1 + 1} (α := Set (Ideal α)) {I : Ideal α | Submodule.IsPrincipal I} ((fun (a : α) ↦ span {a}) '' Set.univ)
rw : WellFounded.{u_1 + 1} (α := α) (Function.onFun (fun (x1 x2 : Ideal α) ↦ x1 > x2) fun (a : α) ↦ span {a})
⊢ Set.WellFoundedOn {I : Ideal α | Submodule.IsPrincipal I} fun (x1 x2 : Ideal α) ↦ x1 > x2

Tactic:
rw [this, Set.wellFoundedOn_image, Set.wellFoundedOn_univ]

Premises used: Set.wellFoundedOn_univ, Set.wellFoundedOn_image
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : WfDvdMonoid α
inst_2 : IsDomain α
this : Eq.{u_1 + 1} (α := Set (Ideal α)) {I : Ideal α | Submodule.IsPrincipal I} ((fun (a : α) ↦ span {a}) '' Set.univ)
⊢ WellFounded.{u_1 + 1} (α := α) DvdNotUnit

Tactic:
wellFounded_dvdNotUnit (α := α)

Premises used: wellFounded_dvdNotUnit
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : WfDvdMonoid α
inst_2 : IsDomain α
this : Eq.{u_1 + 1} (α := Set (Ideal α)) {I : Ideal α | Submodule.IsPrincipal I} ((fun (a : α) ↦ span {a}) '' Set.univ)
h :
  Eq.{u_1 + 1} (α := α → α → Prop) (Function.onFun (fun (x1 x2 : Ideal α) ↦ x1 > x2) fun (a : α) ↦ span {a}) DvdNotUnit
⊢ WellFounded.{u_1 + 1} (α := α) (Function.onFun (fun (x1 x2 : Ideal α) ↦ x1 > x2) fun (a : α) ↦ span {a})

Tactic:
convert! wellFounded_dvdNotUnit (α := α)

Premises used: wellFounded_dvdNotUnit
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : WfDvdMonoid α
inst_2 : IsDomain α
this : Eq.{u_1 + 1} (α := Set (Ideal α)) {I : Ideal α | Submodule.IsPrincipal I} ((fun (a : α) ↦ span {a}) '' Set.univ)
h : ∀ (x x_1 : α), Function.onFun (fun (x1 x2 : Ideal α) ↦ x1 > x2) (fun (a : α) ↦ span {a}) x x_1 ↔ DvdNotUnit x x_1
⊢ Eq.{u_1 + 1} (α := α → α → Prop) (Function.onFun (fun (x1 x2 : Ideal α) ↦ x1 > x2) fun (a : α) ↦ span {a}) DvdNotUnit

Tactic:
ext
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : WfDvdMonoid α
inst_2 : IsDomain α
this : Eq.{u_1 + 1} (α := Set (Ideal α)) {I : Ideal α | Submodule.IsPrincipal I} ((fun (a : α) ↦ span {a}) '' Set.univ)
x x_1 : α
⊢ Function.onFun (fun (x1 x2 : Ideal α) ↦ x1 > x2) (fun (a : α) ↦ span {a}) x x_1 ↔ DvdNotUnit x x_1

Tactic:
Ideal.span_singleton_lt_span_singleton

Premises used: Ideal.span_singleton_lt_span_singleton
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : WfDvdMonoid α
inst_2 : IsDomain α
this : Eq.{u_1 + 1} (α := Set (Ideal α)) {I : Ideal α | Submodule.IsPrincipal I} ((fun (a : α) ↦ span {a}) '' Set.univ)
x x_1 : α
⊢ Function.onFun (fun (x1 x2 : Ideal α) ↦ x1 > x2) (fun (a : α) ↦ span {a}) x x_1 ↔ DvdNotUnit x x_1

Tactic:
exact Ideal.span_singleton_lt_span_singleton

Premises used: Ideal.span_singleton_lt_span_singleton
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : IsDomain α
h : Set.WellFoundedOn {I : Ideal α | Submodule.IsPrincipal I} fun (x1 x2 : Ideal α) ↦ x1 > x2
⊢ WellFounded fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2

Tactic:
have : WellFounded (α := {I : Ideal α // I.IsPrincipal}) (· > ·) := h
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : IsDomain α
h : Set.WellFoundedOn {I : Ideal α | Submodule.IsPrincipal I} fun (x1 x2 : Ideal α) ↦ x1 > x2
this : WellFounded fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2
wf : WellFounded.{u_1 + 1} (α := α) DvdNotUnit
⊢ WfDvdMonoid α

Tactic:
constructor
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : IsDomain α
h : Set.WellFoundedOn {I : Ideal α | Submodule.IsPrincipal I} fun (x1 x2 : Ideal α) ↦ x1 > x2
this : WellFounded fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2
⊢ WellFounded.{u_1 + 1} (α := α)
    (InvImage (fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2) fun (a : α) ↦
      Subtype.mk (p := fun (I : Ideal α) ↦ Submodule.IsPrincipal I) (Ideal.span {a}) ⋯)

Tactic:
InvImage.wf (fun a => ⟨Ideal.span ({ a } : Set α), _, rfl⟩) this

Premises used: InvImage.wf
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : IsDomain α
h : Set.WellFoundedOn {I : Ideal α | Submodule.IsPrincipal I} fun (x1 x2 : Ideal α) ↦ x1 > x2
this : WellFounded fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2
h₁ :
  Eq.{u_1 + 1} (α := α → α → Prop) DvdNotUnit
    (InvImage (fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2) fun (a : α) ↦
      Subtype.mk (p := fun (I : Ideal α) ↦ Submodule.IsPrincipal I) (Ideal.span {a}) ⋯)
⊢ WellFounded.{u_1 + 1} (α := α) DvdNotUnit

Tactic:
convert! InvImage.wf (fun a => ⟨Ideal.span ({ a } : Set α), _, rfl⟩) this

Premises used: InvImage.wf
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : IsDomain α
h : Set.WellFoundedOn {I : Ideal α | Submodule.IsPrincipal I} fun (x1 x2 : Ideal α) ↦ x1 > x2
this : WellFounded fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2
h₁ :
  ∀ (x x_1 : α),
    DvdNotUnit x x_1 ↔
      InvImage (fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2)
        (fun (a : α) ↦ Subtype.mk (p := fun (I : Ideal α) ↦ Submodule.IsPrincipal I) (Ideal.span {a}) ⋯) x x_1
⊢ Eq.{u_1 + 1} (α := α → α → Prop) DvdNotUnit
    (InvImage (fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2) fun (a : α) ↦
      Subtype.mk (p := fun (I : Ideal α) ↦ Submodule.IsPrincipal I) (Ideal.span {a}) ⋯)

Tactic:
ext
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : IsDomain α
h : Set.WellFoundedOn {I : Ideal α | Submodule.IsPrincipal I} fun (x1 x2 : Ideal α) ↦ x1 > x2
this : WellFounded fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2
x x_1 : α
⊢ DvdNotUnit x x_1 ↔
    InvImage (fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2)
      (fun (a : α) ↦ Subtype.mk (p := fun (I : Ideal α) ↦ Submodule.IsPrincipal I) (Ideal.span {a}) ⋯) x x_1

Tactic:
Ideal.span_singleton_lt_span_singleton.symm

Premises used: InvImage, Ideal.span_singleton_lt_span_singleton, Iff.symm
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
Goal:
α : Type u_1
inst : CommSemiring α
inst_1 : IsDomain α
h : Set.WellFoundedOn {I : Ideal α | Submodule.IsPrincipal I} fun (x1 x2 : Ideal α) ↦ x1 > x2
this : WellFounded fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2
x x_1 : α
⊢ DvdNotUnit x x_1 ↔
    InvImage (fun (x1 x2 : { I : Ideal α // Submodule.IsPrincipal I }) ↦ x1 > x2)
      (fun (a : α) ↦ Subtype.mk (p := fun (I : Ideal α) ↦ Submodule.IsPrincipal I) (Ideal.span {a}) ⋯) x x_1

Tactic:
exact Ideal.span_singleton_lt_span_singleton.symm

Premises used: Ideal.span_singleton_lt_span_singleton, Iff.symm
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
Goal:
R : Type u_1
inst : Semiring R
S : Subsemigroup R
P : Ideal R
⊢ P ∈ kaplanskySet S ↔ (↑P : Set R) ∩ (↑S : Set R) = ∅

Tactic:
disjoint_iff_inter_eq_empty

Premises used: Set.Mem, setOf, Disjoint, _private.0.UniqueFactorizationMonoid.kaplanskySet, Set.disjoint_iff_inter_eq_empty
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
Goal:
R : Type u_1
inst : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
inl :
  ∀ (hC : ∅ ⊆ kaplanskySet S) (hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) ∅),
    ∃ P ∈ kaplanskySet S, ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) ∅ J → J ≤ P
inr : ∀ (w : Ideal R) (hI : w ∈ C), ∃ P ∈ kaplanskySet S, ∀ J ∈ C, J ≤ P
⊢ ∃ P ∈ kaplanskySet S, ∀ J ∈ C, J ≤ P

Tactic:
rcases C.eq_empty_or_nonempty with rfl | ⟨_, hI⟩

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
Goal:
R : Type u_1
inst : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
hC : ∅ ⊆ kaplanskySet S
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) ∅
⊢ ⊥ ∈ kaplanskySet S ∧ ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) ∅ J → J ≤ ⊥

Tactic:
simpa [mem_kaplanskySet_iff, eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem, _private.0.UniqueFactorizationMonoid.mem_kaplanskySet_iff
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
Goal:
R : Type u_1
inst : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
hC : ∅ ⊆ kaplanskySet S
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) ∅
⊢ ∃ P ∈ kaplanskySet S, ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) ∅ J → J ≤ P

Tactic:
exact ⟨⊥, by simpa [mem_kaplanskySet_iff, eq_empty_iff_forall_notMem]⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
Goal:
R : Type u_1
inst : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
w : Ideal R
hI : w ∈ C
⊢ ∃ P ∈ kaplanskySet S, ∀ J ∈ C, J ≤ P

Tactic:
⟨sSup C, ?_, fun _ hz ↦ le_sSup hz⟩

Premises used: And.intro, Exists.intro, le_sSup, SupSet.sSup
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
Goal:
R : Type u_1
inst : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
w : Ideal R
hI : w ∈ C
inr : sSup C ∈ kaplanskySet S
⊢ ∃ P ∈ kaplanskySet S, ∀ J ∈ C, J ≤ P

Tactic:
refine ⟨sSup C, ?_, fun _ hz ↦ le_sSup hz⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
Goal:
R : Type u_1
inst : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
w : Ideal R
hI : w ∈ C
inr : ∀ (x : R), x ∉ (↑(sSup C) : Set R) ∩ (↑S : Set R)
⊢ sSup C ∈ kaplanskySet S

Tactic:
rw [mem_kaplanskySet_iff, eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem, _private.0.UniqueFactorizationMonoid.mem_kaplanskySet_iff
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
Goal:
R : Type u_1
inst : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
w : Ideal R
hI : w ∈ C
x : R
hx : x ∈ (↑(sSup C) : Set R) ∩ (↑S : Set R)
inr : ∀ (J : Submodule R R) (hJ₁ : J ∈ C) (hJ₂ : x ∈ J), False
⊢ False

Tactic:
rcases (Submodule.mem_sSup_of_directed ⟨_, hI⟩ hC₂.directedOn).1 hx.1 with ⟨J, hJ₁, hJ₂⟩

Premises used: IsChain.directedOn, And.left, Exists.intro, Iff.mp, Submodule.mem_sSup_of_directed
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
Goal:
R : Type u_1
inst : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
w : Ideal R
hI : w ∈ C
x : R
hx : x ∈ (↑(sSup C) : Set R) ∩ (↑S : Set R)
J : Submodule R R
hJ₁ : J ∈ C
hJ₂ : x ∈ J
⊢ (↑J : Set R) ∩ (↑S : Set R) ≠ ∅

Tactic:
have hx₂ : (J : Set R) ∩ S ≠ ∅ := nonempty_iff_ne_empty.1 ⟨x, hJ₂, hx.2⟩
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
Goal:
R : Type u_1
inst : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
w : Ideal R
hI : w ∈ C
x : R
hx : x ∈ (↑(sSup C) : Set R) ∩ (↑S : Set R)
J : Submodule R R
hJ₁ : J ∈ C
hJ₂ : x ∈ J
hx₂ : (↑J : Set R) ∩ (↑S : Set R) ≠ ∅
⊢ False

Tactic:
hx₂ (mem_kaplanskySet_iff.mp (hC hJ₁))

Premises used: Iff.mp, _private.0.UniqueFactorizationMonoid.mem_kaplanskySet_iff
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
Goal:
R : Type u_1
inst : Semiring R
S : Subsemigroup R
C : Set (Ideal R)
hS : 0 ∉ S
hC : C ⊆ kaplanskySet S
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
w : Ideal R
hI : w ∈ C
x : R
hx : x ∈ (↑(sSup C) : Set R) ∩ (↑S : Set R)
J : Submodule R R
hJ₁ : J ∈ C
hJ₂ : x ∈ J
hx₂ : (↑J : Set R) ∩ (↑S : Set R) ≠ ∅
⊢ False

Tactic:
exact hx₂ (mem_kaplanskySet_iff.mp (hC hJ₁))

Premises used: Iff.mp, _private.0.UniqueFactorizationMonoid.mem_kaplanskySet_iff
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
Goal:
R : Type u_1
inst : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
obtain :
  ∀ (P : Ideal R) (hP : Maximal (fun (x : Ideal R) ↦ x ∈ kaplanskySet S) P),
    ∃ P ∈ kaplanskySet S, ∀ I ∈ kaplanskySet S, P ≤ I → I = P
⊢ ∃ P ∈ kaplanskySet S, ∀ I ∈ kaplanskySet S, P ≤ I → I = P

Tactic:
obtain ⟨P, hP⟩ := zorn_le₀ (kaplanskySet S) (fun _ ↦ exists_mem_kaplanskySet_le hS)

Premises used: _private.0.UniqueFactorizationMonoid.exists_mem_kaplanskySet_le, zorn_le₀, _private.0.UniqueFactorizationMonoid.kaplanskySet
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
Goal:
R : Type u_1
inst : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
P : Ideal R
hP : Maximal (fun (x : Ideal R) ↦ x ∈ kaplanskySet S) P
⊢ ∃ P ∈ kaplanskySet S, ∀ I ∈ kaplanskySet S, P ≤ I → I = P

Tactic:
⟨P, hP.1, fun _ hI H ↦ le_antisymm (hP.2 hI H) H⟩

Premises used: le_antisymm, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
Goal:
R : Type u_1
inst : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
P : Ideal R
hP : Maximal (fun (x : Ideal R) ↦ x ∈ kaplanskySet S) P
⊢ ∃ P ∈ kaplanskySet S, ∀ I ∈ kaplanskySet S, P ≤ I → I = P

Tactic:
exact ⟨P, hP.1, fun _ hI H ↦ le_antisymm (hP.2 hI H) H⟩