awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x (↑I : Set α))
IJ : I ≤ J
xJ : x ∈ J
left : 1 ∉ I
oJ : 1 ∈ J
⊢ y ∈ I
have rcases : ∀ (a b : α) (h : Membership.mem (γ := Submodule α α) (Submodule.span α (↑I : Set α)) b) (oe : 1 = a • x + b), y ∈ I
Tactic: rcases Submodule.mem_span_insert.mp oJ with ⟨a, b, h, oe⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (hypothesis)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x (↑I : Set α))
IJ : I ≤ J
xJ : x ∈ J
left : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : Membership.mem (γ := Submodule α α) (Submodule.span α (↑I : Set α)) b
oe : 1 = a • x + b
⊢ y ∈ I
have F : y * 1 = y * (a • x + b)
Tactic: obtain F : y * 1 = y * (a • x + b) := congr_arg (fun g : α => y * g) oe
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x (↑I : Set α))
IJ : I ≤ J
xJ : x ∈ J
left : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : Membership.mem (γ := Submodule α α) (Submodule.span α (↑I : Set α)) b
oe : 1 = a • x + b
F : y * 1 = y * (a • x + b)
⊢ y ∈ I
have rw : a * (x * y) + y * b ∈ I
Tactic: rw [← mul_one y, F, mul_add, mul_comm, smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x (↑I : Set α))
IJ : I ≤ J
xJ : x ∈ J
left : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : Membership.mem (γ := Submodule α α) (Submodule.span α (↑I : Set α)) b
oe : 1 = a • x + b
F : y * 1 = y * (a • x + b)
⊢ a * (x * y) + y * b ∈ I
have refine : b ∈ I
Tactic: refine Submodule.add_mem I (I.mul_mem_left a hxy) (Submodule.smul_mem I y ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x (↑I : Set α))
IJ : I ≤ J
xJ : x ∈ J
left : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : Membership.mem (γ := Submodule α α) (Submodule.span α (↑I : Set α)) b
oe : 1 = a • x + b
F : y * 1 = y * (a • x + b)
⊢ b ∈ I
have rwa : ∀ (h : b ∈ I) (oe : 1 = a • x + b) (F : y * 1 = y * (a • x + b)), b ∈ I
Tactic: rwa [Submodule.span_eq] at h
Cleared hypotheses: h, oe, F
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
s : Set α
hs : Eq (α := Ideal α) (span s) ⊤
I : Ideal α
hI : I ≠ ⊤
⊢ ∃ r ∈ s, Disjoint (↑I : Set α) (↑(Submonoid.powers r) : Set α)
have have : ∀ (M : Ideal α) (hM : M.IsMaximal) (le : I ≤ M), ∃ r ∈ s, Disjoint (↑I : Set α) (↑(Submonoid.powers r) : Set α)
Tactic: have ⟨M, hM, le⟩ := exists_le_maximal I hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (hypothesis)
Goal:
α : Type u
inst : CommSemiring α
s : Set α
hs : Eq (α := Ideal α) (span s) ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
⊢ ∃ r ∈ s, Disjoint (↑I : Set α) (↑(Submonoid.powers r) : Set α)
have this : M ≠ ⊤
Tactic: have := hM.1.1
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (hypothesis)
Goal:
α : Type u
inst : CommSemiring α
s : Set α
hs : Eq (α := Ideal α) (span s) ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : M ≠ ⊤
⊢ ∃ r ∈ s, Disjoint (↑I : Set α) (↑(Submonoid.powers r) : Set α)
have this₁ : ∃ a ∈ s, a ∉ (↑M : Set α)
Tactic: rw [Ne, eq_top_iff, ← hs, span_le, Set.not_subset] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
s : Set α
hs : Eq (α := Ideal α) (span s) ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : ∃ a ∈ s, a ∉ (↑M : Set α)
⊢ ∃ r ∈ s, Disjoint (↑I : Set α) (↑(Submonoid.powers r) : Set α)
have have : ∀ (a : α) (has : a ∈ s) (haM : a ∉ (↑M : Set α)), ∃ r ∈ s, Disjoint (↑I : Set α) (↑(Submonoid.powers r) : Set α)
Tactic: have ⟨a, has, haM⟩ := this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsDomain α
x y : α
⊢ LT.lt (α := Ideal α) (span {x}) (span {y}) ↔ DvdNotUnit y x
have rw : LE.le (α := Ideal α) (span {x}) (span {y}) ∧ ¬LE.le (α := Ideal α) (span {y}) (span {x}) ↔ DvdNotUnit y x
Tactic: rw [lt_iff_le_not_ge, span_singleton_le_span_singleton, span_singleton_le_span_singleton,
    dvd_and_not_dvd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsDomain α
x y : α
rw : LE.le (α := Ideal α) (span {x}) (span {y}) ∧ ¬LE.le (α := Ideal α) (span {y}) (span {x}) ↔ DvdNotUnit y x
⊢ LT.lt (α := Ideal α) (span {x}) (span {y}) ↔ DvdNotUnit y x
have rw₁ : y ∣ x ∧ ¬LE.le (α := Ideal α) (span {y}) (span {x}) ↔ DvdNotUnit y x
Tactic: rw [lt_iff_le_not_ge, span_singleton_le_span_singleton, span_singleton_le_span_singleton,
    dvd_and_not_dvd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsDomain α
x y : α
rw : LE.le (α := Ideal α) (span {x}) (span {y}) ∧ ¬LE.le (α := Ideal α) (span {y}) (span {x}) ↔ DvdNotUnit y x
rw₁ : y ∣ x ∧ ¬LE.le (α := Ideal α) (span {y}) (span {x}) ↔ DvdNotUnit y x
⊢ LT.lt (α := Ideal α) (span {x}) (span {y}) ↔ DvdNotUnit y x
have rw₂ : y ∣ x ∧ ¬x ∣ y ↔ DvdNotUnit y x
Tactic: rw [lt_iff_le_not_ge, span_singleton_le_span_singleton, span_singleton_le_span_singleton,
    dvd_and_not_dvd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsDomain α
x y : α
rw : LE.le (α := Ideal α) (span {x}) (span {y}) ∧ ¬LE.le (α := Ideal α) (span {y}) (span {x}) ↔ DvdNotUnit y x
rw₁ : y ∣ x ∧ ¬LE.le (α := Ideal α) (span {y}) (span {x}) ↔ DvdNotUnit y x
rw₂ : y ∣ x ∧ ¬x ∣ y ↔ DvdNotUnit y x
⊢ LT.lt (α := Ideal α) (span {x}) (span {y}) ↔ DvdNotUnit y x
have rw₃ : DvdNotUnit y x ↔ DvdNotUnit y x
Tactic: rw [lt_iff_le_not_ge, span_singleton_le_span_singleton, span_singleton_le_span_singleton,
    dvd_and_not_dvd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (hypothesis)
Goal:
α : Type u
inst : CommSemiring α
S : Submonoid α
disjoint : Disjoint (↑⊤ : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), ⊤ < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
⊢ False
have this : 1 ∈ (↑S : Set α)
Tactic: have : 1 ∈ (S : Set α) := S.one_mem
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I
have by_contra! : ∀ (rid : x ∉ I ∧ y ∉ I), False
Tactic: by_contra! rid
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (hypothesis)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
⊢ False
have hx : ¬Disjoint (↑(I ⊔ span {x}) : Set α) (↑S : Set α)
Tactic: have hx := maximally_disjoint (I ⊔ span {x}) (Submodule.lt_sup_iff_notMem.mpr rid.1)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (hypothesis)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
hx : ¬Disjoint (↑(I ⊔ span {x}) : Set α) (↑S : Set α)
⊢ False
have hy : ¬Disjoint (↑(I ⊔ span {y}) : Set α) (↑S : Set α)
Tactic: have hy := maximally_disjoint (I ⊔ span {y}) (Submodule.lt_sup_iff_notMem.mpr rid.2)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (hypothesis)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
hx : ¬Disjoint (↑(I ⊔ span {x}) : Set α) (↑S : Set α)
hy : ¬Disjoint (↑(I ⊔ span {y}) : Set α) (↑S : Set α)
⊢ False
have hx₁ : ∃ (x_1 : α), (∃ y ∈ I, ∃ (z : α), x ∣ z ∧ y + z = x_1) ∧ x_1 ∈ S
Tactic: simp only [Set.not_disjoint_iff, SetLike.mem_coe, Submodule.mem_sup,
      mem_span_singleton] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (hypothesis)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
hx : ¬Disjoint (↑(I ⊔ span {x}) : Set α) (↑S : Set α)
hy : ¬Disjoint (↑(I ⊔ span {y}) : Set α) (↑S : Set α)
hx₁ : ∃ (x_1 : α), (∃ y ∈ I, ∃ (z : α), x ∣ z ∧ y + z = x_1) ∧ x_1 ∈ S
⊢ False
have hy₁ : ∃ (x : α), (∃ y_1 ∈ I, ∃ (z : α), y ∣ z ∧ y_1 + z = x) ∧ x ∈ S
Tactic: simp only [Set.not_disjoint_iff, SetLike.mem_coe, Submodule.mem_sup,
      mem_span_singleton] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
hx : ∃ (x_1 : α), (∃ y ∈ I, ∃ (z : α), x ∣ z ∧ y + z = x_1) ∧ x_1 ∈ S
hy : ∃ (x : α), (∃ y_1 ∈ I, ∃ (z : α), y ∣ z ∧ y_1 + z = x) ∧ x ∈ S
⊢ False
have obtain : ∀ (s₁ : α) (hs₁ : s₁ ∈ S) (i₁ : α) (hi₁ : i₁ ∈ I) (r₁ : α) (hr₁ : i₁ + x * r₁ = s₁), False
Tactic: obtain ⟨s₁, ⟨i₁, hi₁, ⟨_, ⟨r₁, rfl⟩, hr₁⟩⟩, hs₁⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
hy : ∃ (x : α), (∃ y_1 ∈ I, ∃ (z : α), y ∣ z ∧ y_1 + z = x) ∧ x ∈ S
s₁ : α
hs₁ : s₁ ∈ S
i₁ : α
hi₁ : i₁ ∈ I
r₁ : α
hr₁ : i₁ + x * r₁ = s₁
⊢ False
have obtain : ∀ (s₂ : α) (hs₂ : s₂ ∈ S) (i₂ : α) (hi₂ : i₂ ∈ I) (r₂ : α) (hr₂ : i₂ + y * r₂ = s₂), False
Tactic: obtain ⟨s₂, ⟨i₂, hi₂, ⟨_, ⟨r₂, rfl⟩, hr₂⟩⟩, hs₂⟩ := hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
s₁ : α
hs₁ : s₁ ∈ S
i₁ : α
hi₁ : i₁ ∈ I
r₁ : α
hr₁ : i₁ + x * r₁ = s₁
s₂ : α
hs₂ : s₂ ∈ S
i₂ : α
hi₂ : i₂ ∈ I
r₂ : α
hr₂ : i₂ + y * r₂ = s₂
⊢ False
have refine : (i₁ + x * r₁) * i₂ + (i₁ * (y * r₂) + x * y * (r₁ * r₂)) = s₁ * s₂
Tactic: refine disjoint.ne_of_mem
      (I.add_mem (I.mul_mem_left (i₁ + x * r₁) hi₂) <| I.add_mem (I.mul_mem_right (y * r₂) hi₁) <|
        I.mul_mem_right (r₁ * r₂) hxy)
      (S.mul_mem hs₁ hs₂) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint (↑J : Set α) (↑S : Set α)
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
s₁ : α
hs₁ : s₁ ∈ S
i₁ : α
hi₁ : i₁ ∈ I
r₁ : α
hr₁ : i₁ + x * r₁ = s₁
s₂ : α
hs₂ : s₂ ∈ S
i₂ : α
hi₂ : i₂ ∈ I
r₂ : α
hr₂ : i₂ + y * r₂ = s₂
⊢ (i₁ + x * r₁) * i₂ + (i₁ * (y * r₂) + x * y * (r₁ * r₂)) = s₁ * s₂
have rw : (i₁ + x * r₁) * i₂ + (i₁ * (y * r₂) + x * y * (r₁ * r₂)) = (i₁ + x * r₁) * (i₂ + y * r₂)
Tactic: rw [← hr₁, ← hr₂]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
⊢ ∃ (p : Ideal α), p.IsPrime ∧ I ≤ p ∧ Disjoint (↑p : Set α) (↑S : Set α)
have refine_2 : ∀ (p : Ideal α) (hIp : I ≤ p)
  (hp :
    Maximal
      (fun (x : Ideal α) ↦ Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} x) p),
  ∃ (p : Ideal α), p.IsPrime ∧ I ≤ p ∧ Disjoint (↑p : Set α) (↑S : Set α)
Tactic: have ⟨p, hIp, hp⟩ := zorn_le_nonempty₀ {p : Ideal α | Disjoint (p : Set α) S}
    (fun c hc hc' x hx ↦ ?_) I disjoint
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
refine_2 :
  ∀ (p : Ideal α) (hIp : I ≤ p)
    (hp :
      Maximal
        (fun (x : Ideal α) ↦ Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} x)
        p),
    ∃ (p : Ideal α), p.IsPrime ∧ I ≤ p ∧ Disjoint (↑p : Set α) (↑S : Set α)
⊢ ∃ (p : Ideal α), p.IsPrime ∧ I ≤ p ∧ Disjoint (↑p : Set α) (↑S : Set α)
have refine_1 : ∀ (c : Set (Ideal α)) (hc : c ⊆ {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)})
  (hc' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) c) (x : Ideal α) (hx : x ∈ c),
  ∃ (ub : Ideal α),
    Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} ub ∧ ∀ z ∈ c, z ≤ ub
Tactic: have ⟨p, hIp, hp⟩ := zorn_le_nonempty₀ {p : Ideal α | Disjoint (p : Set α) S}
    (fun c hc hc' x hx ↦ ?_) I disjoint
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
c : Set (Ideal α)
hc : c ⊆ {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)}
hc' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) c
x : Ideal α
hx : x ∈ c
⊢ ∃ (ub : Ideal α),
    Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} ub ∧ ∀ z ∈ c, z ≤ ub
have refine_1 : IsEmpty.{u + 1} (↑c : Type u) →
  ∃ (ub : Ideal α),
    Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} ub ∧ ∀ z ∈ c, z ≤ ub
Tactic: cases isEmpty_or_nonempty c
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
c : Set (Ideal α)
hc : c ⊆ {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)}
hc' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) c
x : Ideal α
hx : x ∈ c
refine_1 :
  IsEmpty.{u + 1} (↑c : Type u) →
    ∃ (ub : Ideal α),
      Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} ub ∧ ∀ z ∈ c, z ≤ ub
⊢ ∃ (ub : Ideal α),
    Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} ub ∧ ∀ z ∈ c, z ≤ ub
have refine_1₁ : Nonempty.{u + 1} (↑c : Type u) →
  ∃ (ub : Ideal α),
    Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} ub ∧ ∀ z ∈ c, z ≤ ub
Tactic: cases isEmpty_or_nonempty c
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
c : Set (Ideal α)
hc : c ⊆ {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)}
hc' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) c
x : Ideal α
hx : x ∈ c
h : Nonempty.{u + 1} (↑c : Type u)
⊢ ∃ (ub : Ideal α),
    Membership.mem (γ := Set (Ideal α)) {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)} ub ∧ ∀ z ∈ c, z ≤ ub
have refine_1 : ∀ (x : α) (hx : x ∈ (↑(sSup c) : Set α)), x ∉ (↑S : Set α)
Tactic: refine ⟨sSup c, Set.disjoint_left.mpr fun x hx ↦ ?_, fun _ ↦ le_sSup⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint (↑I : Set α) (↑S : Set α)
c : Set (Ideal α)
hc : c ⊆ {p : Ideal α | Disjoint (↑p : Set α) (↑S : Set α)}
hc' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) c
x_1 : Ideal α
hx_1 : x_1 ∈ c
h : Nonempty.{u + 1} (↑c : Type u)
x : α
hx : x ∈ (↑(sSup c) : Set α)
⊢ x ∉ (↑S : Set α)
have refine_1 : ∀ (p : { a : Ideal α // a ∈ c }) (hp : x ∈ (↑p : Ideal α)), x ∉ (↑S : Set α)
Tactic: have ⟨p, hp⟩ := (Submodule.mem_iSup_of_directed _ hc'.directed).mp (sSup_eq_iSup' c ▸ hx)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
a : α
ha : IsIdempotentElem a
haI : a ∉ I
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ (↑(Submonoid.powers a) : Set α) → a_1 ∉ (↑I : Set α)
have rw : ∀ ⦃a_1 : α⦄, Membership.mem (γ := Set α) {1, a} a_1 → a_1 ∉ (↑I : Set α)
Tactic: rw [ha.coe_powers]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsPrincipalIdealRing α
P : Ideal α
hP : P ≠ ⊥
h : P.IsPrime
⊢ ∃ (p : α), Prime p ∧ P = span {p}
have obtain : ∀ (p : α) (hP : Ne (α := Ideal α) (α ∙ p) ⊥) (h : IsPrime (α ∙ p)),
  ∃ (p_1 : α), Prime p_1 ∧ Eq (α := Ideal α) (α ∙ p) (span {p_1})
Tactic: obtain ⟨p, rfl⟩ := Submodule.IsPrincipal.principal P
Cleared hypotheses: P, hP, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsPrincipalIdealRing α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
P : Ideal α
⊢ P.IsPrime ↔ P = ⊥ ∨ ∃ (p : α), Prime p ∧ P = span {p}
have rw : P = ⊥ → P.IsPrime
Tactic: rw [or_iff_not_imp_left, ← forall_congr' isPrime_iff_of_isPrincipalIdealRing,
    ← or_iff_not_imp_left, or_iff_right_of_imp]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
K : Type u
inst : DivisionSemiring K
h : Eq.{u + 1} (α := Ideal K) ⊥ ⊤
⊢ 1 ∉ ⊤
have rw : 1 ∉ ⊥
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I J : Ideal R
inst_1 : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p : (Ideal R)ᵒᵈ | IsPrime p ∧ I ≤ (OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R) p}
h :
  ∃ (m : (Ideal R)ᵒᵈ),
    (OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) J ≤ m ∧ Maximal (fun (x : (Ideal R)ᵒᵈ) ↦ x ∈ S) m
⊢ ∃ p ∈ I.minimalPrimes, p ≤ J
have obtain : ∀ (p : (Ideal R)ᵒᵈ) (hJp : (OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) J ≤ p)
  (hp : Maximal (fun (x : (Ideal R)ᵒᵈ) ↦ x ∈ S) p), ∃ p ∈ I.minimalPrimes, p ≤ J
Tactic: obtain ⟨p, hJp, hp⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I J : Ideal R
inst_1 : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p : (Ideal R)ᵒᵈ | IsPrime p ∧ I ≤ (OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R) p}
⊢ ∃ p ∈ I.minimalPrimes, p ≤ J
have suffices : ∃ (m : (Ideal R)ᵒᵈ), (OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) J ≤ m ∧ Maximal (fun (x : (Ideal R)ᵒᵈ) ↦ x ∈ S) m
Tactic: suffices h : ∃ m, OrderDual.toDual J ≤ m ∧ Maximal (· ∈ S) m by
    obtain ⟨p, hJp, hp⟩ := h
    exact ⟨p, ⟨hp.prop, fun q hq hle ↦ hp.le_of_ge hq hle⟩, hJp⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I J : Ideal R
inst_1 : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p : (Ideal R)ᵒᵈ | IsPrime p ∧ I ≤ (OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R) p}
⊢ ∃ (m : (Ideal R)ᵒᵈ),
    (OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) J ≤ m ∧ Maximal (fun (x : (Ideal R)ᵒᵈ) ↦ x ∈ S) m
have ih : ∀ c ⊆ S, IsChain (fun (x1 x2 : (Ideal R)ᵒᵈ) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
Tactic: apply zorn_le_nonempty₀
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I J : Ideal R
inst_1 : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p : (Ideal R)ᵒᵈ | IsPrime p ∧ I ≤ (OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R) p}
ih : ∀ c ⊆ S, IsChain (fun (x1 x2 : (Ideal R)ᵒᵈ) ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
⊢ ∃ (m : (Ideal R)ᵒᵈ),
    (OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) J ≤ m ∧ Maximal (fun (x : (Ideal R)ᵒᵈ) ↦ x ∈ S) m
have hxs : Membership.mem (α := (Ideal R)ᵒᵈ) S ((OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) J : (Ideal R)ᵒᵈ)
Tactic: apply zorn_le_nonempty₀
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I J : Ideal R
inst_1 : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p : (Ideal R)ᵒᵈ | IsPrime p ∧ I ≤ (OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R) p}
c : Set (Ideal R)
hc : c ⊆ S
hc' : IsChain (fun (x1 x2 : (Ideal R)ᵒᵈ) ↦ x1 ≤ x2) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
have ih : I ≤ (OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R) ((OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) (sInf c))
Tactic: refine
    ⟨OrderDual.toDual (sInf c),
      ⟨Ideal.sInf_isPrime_of_isChain ⟨J', hJ'⟩ hc'.symm fun x hx => (hc hx).1, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I J : Ideal R
inst_1 : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p : (Ideal R)ᵒᵈ | IsPrime p ∧ I ≤ (OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R) p}
c : Set (Ideal R)
hc : c ⊆ S
hc' : IsChain (fun (x1 x2 : (Ideal R)ᵒᵈ) ↦ x1 ≤ x2) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
ih : I ≤ (OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R) ((OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) (sInf c))
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
have ih₁ : ∀ z ∈ c, z ≤ (OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) (sInf c)
Tactic: refine
    ⟨OrderDual.toDual (sInf c),
      ⟨Ideal.sInf_isPrime_of_isChain ⟨J', hJ'⟩ hc'.symm fun x hx => (hc hx).1, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I J : Ideal R
inst_1 : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p : (Ideal R)ᵒᵈ | IsPrime p ∧ I ≤ (OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R) p}
c : Set (Ideal R)
hc : c ⊆ S
hc' : IsChain (fun (x1 x2 : (Ideal R)ᵒᵈ) ↦ x1 ≤ x2) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ I ≤ (OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R) ((OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) (sInf c))
have ih : ∀ b ∈ c, I ≤ b
Tactic: rw [OrderDual.ofDual_toDual, le_sInf_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I J : Ideal R
inst_1 : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := {p : (Ideal R)ᵒᵈ | IsPrime p ∧ I ≤ (OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R) p}
c : Set (Ideal R)
hc : c ⊆ S
hc' : IsChain (fun (x1 x2 : (Ideal R)ᵒᵈ) ↦ x1 ≤ x2) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
z : (Ideal R)ᵒᵈ
hz : z ∈ c
⊢ z ≤ (OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) (sInf c)
have ih : sInf c ≤ (OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R) z
Tactic: rw [OrderDual.le_toDual]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
h : I ≠ ⊤
⊢ Nonempty.{u_1 + 1} (↑I.minimalPrimes : Type u_1)
have obtain : ∀ (m : Ideal R) (hm : m.IsMaximal) (hle : I ≤ m), Nonempty.{u_1 + 1} (↑I.minimalPrimes : Type u_1)
Tactic: obtain ⟨m, hm, hle⟩ := Ideal.exists_le_maximal I h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
h : I ≠ ⊤
m : Ideal R
hm : m.IsMaximal
hle : I ≤ m
⊢ Nonempty.{u_1 + 1} (↑I.minimalPrimes : Type u_1)
have obtain : ∀ (p : Ideal R) (hp : p ∈ I.minimalPrimes), Nonempty.{u_1 + 1} (↑I.minimalPrimes : Type u_1)
Tactic: obtain ⟨p, hp, -⟩ := Ideal.exists_minimalPrimes_le hle
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
h : I.minimalPrimes = ∅
⊢ I = ⊤
have by_contra : ∀ (hI : ¬I = ⊤), False
Tactic: by_contra hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
h : I.minimalPrimes = ∅
hI : ¬I = ⊤
⊢ False
have obtain : ∀ (p : Ideal R) (hp : p ∈ I.minimalPrimes), False
Tactic: obtain ⟨p, hp⟩ := Ideal.nonempty_minimalPrimes hI