awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsPrincipalIdealRing α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
P : Ideal α
rw : P = ⊥ → P.IsPrime
⊢ P.IsPrime ↔ P = ⊥ ∨ ∃ (p : α), Prime p ∧ P = span {p}

Tactic:
rw [or_iff_not_imp_left, ← forall_congr' isPrime_iff_of_isPrincipalIdealRing,
    ← or_iff_not_imp_left, or_iff_right_of_imp]

Premises used: Classical.or_iff_not_imp_left, forall_congr', Ideal.isPrime_iff_of_isPrincipalIdealRing, or_iff_right_of_imp
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsPrincipalIdealRing α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
⊢ IsPrime.{u} (α := α) ⊥

Tactic:
isPrime_bot

Premises used: Ideal.isPrime_bot
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
α : Type u
inst : CommSemiring α
inst_1 : IsPrincipalIdealRing α
inst_2 : NoZeroDivisors α
inst_3 : Nontrivial α
⊢ IsPrime.{u} (α := α) ⊥

Tactic:
exact isPrime_bot

Premises used: Ideal.isPrime_bot
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
K : Type u
inst : DivisionSemiring K
h : Eq.{u + 1} (α := Ideal K) ⊥ ⊤
rw : 1 ∉ ⊥
⊢ 1 ∉ ⊤

Tactic:
rw [← h]
-- Module: Mathlib.RingTheory.Ideal.Maximal
Goal:
K : Type u
inst : DivisionSemiring K
h : Eq.{u + 1} (α := Ideal K) ⊥ ⊤
⊢ 1 ∉ ⊥

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
h : I.IsMinimalPrime p
⊢ p.IsPrime

Tactic:
h.1.1

Premises used: And.left
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
h : I.IsMinimalPrime p
⊢ I ≤ p

Tactic:
h.1.2

Premises used: And.right, And.left
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
h : IsMinimalPrime p
⊢ p.IsPrime

Tactic:
h.1.1

Premises used: And.left
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
⊢ IsMinimalPrime p ↔ Minimal Ideal.IsPrime p

Tactic:
simp [Ideal.IsMinimalPrime]

Premises used: Ideal.IsMinimalPrime
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := Ideal R → Prop) (fun (q : Ideal R) ↦ q.IsPrime ∧ ⊥ ≤ q) Ideal.IsPrime

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
p : Ideal R
h : Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) p
⊢ p.IsPrime

Tactic:
h.1.1

Premises used: And.left
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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
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
⊢ ∃ p ∈ I.minimalPrimes, p ≤ J

Tactic:
obtain ⟨p, hJp, hp⟩ := h
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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 : (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:
⟨p, ⟨hp.prop, fun q hq hle ↦ hp.le_of_ge hq hle⟩, hJp⟩

Premises used: Maximal.le_of_ge, Maximal.prop, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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 : (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:
exact ⟨p, ⟨hp.prop, fun q hq hle ↦ hp.le_of_ge hq hle⟩, hJp⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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}
suffices :
  ∃ (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

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⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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
hxs : Membership.mem (α := (Ideal R)ᵒᵈ) S ((OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) J : (Ideal R)ᵒᵈ)
⊢ ∃ (m : (Ideal R)ᵒᵈ),
    (OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) J ≤ m ∧ Maximal (fun (x : (Ideal R)ᵒᵈ) ↦ x ∈ S) m

Tactic:
apply zorn_le_nonempty₀

Premises used: zorn_le_nonempty₀
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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}
⊢ J.IsPrime

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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}
⊢ Membership.mem (α := (Ideal R)ᵒᵈ) S ((OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) J : (Ideal R)ᵒᵈ)

Tactic:
refine ⟨show J.IsPrime by infer_instance, e⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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

Tactic:
⟨OrderDual.toDual (sInf c),
      ⟨Ideal.sInf_isPrime_of_isChain ⟨J', hJ'⟩ hc'.symm fun x hx => (hc hx).1, ?_⟩, ?_⟩

Premises used: OrderDual.toDual, IsChain.symm, Ideal.sInf_isPrime_of_isChain, And.left, And.intro, Exists.intro, DFunLike.coe, InfSet.sInf
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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))
ih₁ : ∀ z ∈ c, z ≤ (OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) (sInf c)
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub

Tactic:
refine
    ⟨OrderDual.toDual (sInf c),
      ⟨Ideal.sInf_isPrime_of_isChain ⟨J', hJ'⟩ hc'.symm fun x hx => (hc hx).1, ?_⟩, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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 : ∀ b ∈ c, I ≤ b
⊢ I ≤ (OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R) ((OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) (sInf c))

Tactic:
rw [OrderDual.ofDual_toDual, le_sInf_iff]

Premises used: le_sInf_iff, OrderDual.ofDual_toDual
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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
⊢ ∀ b ∈ c, I ≤ b

Tactic:
fun _ hx => (hc hx).2

Premises used: Set.Mem, And.right
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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
⊢ ∀ b ∈ c, I ≤ b

Tactic:
exact fun _ hx => (hc hx).2

Premises used: And.right
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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
ih : sInf c ≤ (OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R) z
⊢ z ≤ (OrderDual.toDual : (a : Ideal R) → (Ideal R)ᵒᵈ) (sInf c)

Tactic:
rw [OrderDual.le_toDual]

Premises used: OrderDual.le_toDual
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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
⊢ sInf c ≤ (OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R) z

Tactic:
sInf_le hz

Premises used: Set.Mem, sInf_le
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
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
⊢ sInf c ≤ (OrderDual.ofDual : (a : (Ideal R)ᵒᵈ) → Ideal R) z

Tactic:
exact sInf_le hz

Premises used: sInf_le
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
h : I ≠ ⊤
obtain : ∀ (m : Ideal R) (hm : m.IsMaximal) (hle : I ≤ m), Nonempty.{u_1 + 1} (↑I.minimalPrimes : Type u_1)
⊢ Nonempty.{u_1 + 1} (↑I.minimalPrimes : Type u_1)

Tactic:
obtain ⟨m, hm, hle⟩ := Ideal.exists_le_maximal I h

Premises used: Ideal.exists_le_maximal
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
h : I ≠ ⊤
m : Ideal R
hm : m.IsMaximal
hle : I ≤ m
obtain : ∀ (p : Ideal R) (hp : p ∈ I.minimalPrimes), Nonempty.{u_1 + 1} (↑I.minimalPrimes : Type u_1)
⊢ Nonempty.{u_1 + 1} (↑I.minimalPrimes : Type u_1)

Tactic:
obtain ⟨p, hp, -⟩ := Ideal.exists_minimalPrimes_le hle

Premises used: Ideal.exists_minimalPrimes_le
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
h : I ≠ ⊤
m : Ideal R
hm : m.IsMaximal
hle : I ≤ m
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ Nonempty.{u_1 + 1} (↑I.minimalPrimes : Type u_1)

Tactic:
⟨p, hp⟩

Premises used: Nonempty.intro, Subtype.mk
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
h : I ≠ ⊤
m : Ideal R
hm : m.IsMaximal
hle : I ≤ m
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ Nonempty.{u_1 + 1} (↑I.minimalPrimes : Type u_1)

Tactic:
exact ⟨p, hp⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
h : I.minimalPrimes = ∅
by_contra : ∀ (hI : ¬I = ⊤), False
⊢ I = ⊤

Tactic:
by_contra hI
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
h : I.minimalPrimes = ∅
hI : ¬I = ⊤
obtain : ∀ (p : Ideal R) (hp : p ∈ I.minimalPrimes), False
⊢ False

Tactic:
obtain ⟨p, hp⟩ := Ideal.nonempty_minimalPrimes hI

Premises used: Ideal.nonempty_minimalPrimes
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
h : I.minimalPrimes = ∅
hI : ¬I = ⊤
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ False

Tactic:
Set.notMem_empty p (h ▸ hp)

Premises used: Eq.rec, Set.notMem_empty
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
h : I.minimalPrimes = ∅
hI : ¬I = ⊤
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ False

Tactic:
exact Set.notMem_empty p (h ▸ hp)

Premises used: Eq.rec, Set.notMem_empty
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
h :
  ∀ (p : Ideal R),
    Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.radical.IsMinimalPrime p} p ↔
      Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.IsMinimalPrime p} p
⊢ Eq.{u_1 + 1} (α := Set (Ideal R)) {p : Ideal R | I.radical.IsMinimalPrime p} {p : Ideal R | I.IsMinimalPrime p}

Tactic:
ext p
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
⊢ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.radical.IsMinimalPrime p} p ↔
    Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.IsMinimalPrime p} p

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
h :
  Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.radical.IsMinimalPrime p} p →
    Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.IsMinimalPrime p} p
h₁ :
  Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.IsMinimalPrime p} p →
    Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.radical.IsMinimalPrime p} p
⊢ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.radical.IsMinimalPrime p} p ↔
    Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.IsMinimalPrime p} p

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I.radical ≤ p
⊢ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.IsMinimalPrime p} p

Tactic:
⟨⟨a, a.radical_le_iff.1 ha⟩, ?_⟩

Premises used: Set.Mem, setOf, Ideal.IsMinimalPrime, And.intro, Iff.mp, Minimal, Ideal.IsPrime.radical_le_iff
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I.radical ≤ p
h : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
⊢ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.IsMinimalPrime p} p

Tactic:
refine ⟨⟨a, a.radical_le_iff.1 ha⟩, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I.radical ≤ p
h : ∀ (b : ∀ ⦃y : Ideal R⦄, y.IsPrime → I.radical ≤ y → y ≤ p → p ≤ y) ⦃y : Ideal R⦄, y.IsPrime → I ≤ y → y ≤ p → p ≤ y
⊢ ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y

Tactic:
simp only [and_imp] at *

Premises used: and_imp
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
a : p.IsPrime
ha : I.radical ≤ p
b : ∀ ⦃y : Ideal R⦄, y.IsPrime → I.radical ≤ y → y ≤ p → p ≤ y
⊢ ∀ ⦃y : Ideal R⦄, y.IsPrime → I ≤ y → y ≤ p → p ≤ y

Tactic:
fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.2 h3) h4

Premises used: Iff.mpr, Ideal.IsPrime.radical_le_iff
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
a : p.IsPrime
ha : I.radical ≤ p
b : ∀ ⦃y : Ideal R⦄, y.IsPrime → I.radical ≤ y → y ≤ p → p ≤ y
⊢ ∀ ⦃y : Ideal R⦄, y.IsPrime → I ≤ y → y ≤ p → p ≤ y

Tactic:
exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.2 h3) h4

Premises used: Iff.mpr, Ideal.IsPrime.radical_le_iff
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I ≤ p
⊢ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.radical.IsMinimalPrime p} p

Tactic:
⟨⟨a, a.radical_le_iff.2 ha⟩, ?_⟩

Premises used: Iff.mpr, Set.Mem, setOf, Ideal.IsMinimalPrime, And.intro, Minimal, Ideal.IsPrime.radical_le_iff
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I ≤ p
h : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y
⊢ Membership.mem (γ := Set (Ideal R)) {p : Ideal R | I.radical.IsMinimalPrime p} p

Tactic:
refine ⟨⟨a, a.radical_le_iff.2 ha⟩, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I ≤ p
h : ∀ (b : ∀ ⦃y : Ideal R⦄, y.IsPrime → I ≤ y → y ≤ p → p ≤ y) ⦃y : Ideal R⦄, y.IsPrime → I.radical ≤ y → y ≤ p → p ≤ y
⊢ ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y

Tactic:
simp only [and_imp] at *

Premises used: and_imp
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
a : p.IsPrime
ha : I ≤ p
b : ∀ ⦃y : Ideal R⦄, y.IsPrime → I ≤ y → y ≤ p → p ≤ y
⊢ ∀ ⦃y : Ideal R⦄, y.IsPrime → I.radical ≤ y → y ≤ p → p ≤ y

Tactic:
fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.1 h3) h4

Premises used: Iff.mp, Ideal.IsPrime.radical_le_iff
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I p : Ideal R
a : p.IsPrime
ha : I ≤ p
b : ∀ ⦃y : Ideal R⦄, y.IsPrime → I ≤ y → y ≤ p → p ≤ y
⊢ ∀ ⦃y : Ideal R⦄, y.IsPrime → I.radical ≤ y → y ≤ p → p ≤ y

Tactic:
exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.1 h3) h4

Premises used: Iff.mp, Ideal.IsPrime.radical_le_iff
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
rw : sInf I.minimalPrimes = sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}
⊢ sInf I.minimalPrimes = I.radical

Tactic:
rw [I.radical_eq_sInf]

Premises used: Ideal.radical_eq_sInf
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a : sInf I.minimalPrimes ≤ sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}
a₁ : sInf {J : Ideal R | I ≤ J ∧ J.IsPrime} ≤ sInf I.minimalPrimes
⊢ sInf I.minimalPrimes = sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
hx : x ∈ sInf I.minimalPrimes
a :
  ∀ (hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ I.minimalPrimes → x ∈ I_1) ⦃I_1 : Ideal R⦄,
    Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} I_1 → x ∈ I_1
⊢ Membership.mem (γ := Submodule R R) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}) x

Tactic:
rw [Ideal.mem_sInf] at hx ⊢

Premises used: Ideal.mem_sInf
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ I.minimalPrimes → x ∈ I_1
J : Ideal R
e : I ≤ J
hJ : J.IsPrime
a : ∀ (p : Ideal R) (hp : p ∈ I.minimalPrimes) (hp' : p ≤ J), x ∈ J
⊢ x ∈ J

Tactic:
obtain ⟨p, hp, hp'⟩ := Ideal.exists_minimalPrimes_le e

Premises used: Ideal.exists_minimalPrimes_le
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ I.minimalPrimes → x ∈ I_1
J : Ideal R
e : I ≤ J
hJ : J.IsPrime
p : Ideal R
hp : p ∈ I.minimalPrimes
hp' : p ≤ J
⊢ x ∈ J

Tactic:
hp' (hx hp)

Premises used: Set.Mem
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ I.minimalPrimes → x ∈ I_1
J : Ideal R
e : I ≤ J
hJ : J.IsPrime
p : Ideal R
hp : p ∈ I.minimalPrimes
hp' : p ≤ J
⊢ x ∈ J

Tactic:
exact hp' (hx hp)
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
apply : I.minimalPrimes ⊆ {J : Ideal R | I ≤ J ∧ J.IsPrime}
⊢ sInf {J : Ideal R | I ≤ J ∧ J.IsPrime} ≤ sInf I.minimalPrimes

Tactic:
apply sInf_le_sInf _

Premises used: sInf_le_sInf
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I_1 I : Ideal R
hI : I ∈ I_1.minimalPrimes
⊢ Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I_1 ≤ J ∧ J.IsPrime} I

Tactic:
hI.1.symm

Premises used: Set.Mem, setOf, And.left, And.symm
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I_1 I : Ideal R
hI : I ∈ I_1.minimalPrimes
⊢ Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I_1 ≤ J ∧ J.IsPrime} I

Tactic:
exact hI.1.symm

Premises used: And.left, And.symm
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hI : I.IsPrimary
h : ∀ (J : Ideal R), J ∈ I.minimalPrimes ↔ Membership.mem (γ := Set (Ideal R)) {I.radical} J
⊢ I.minimalPrimes = {I.radical}

Tactic:
ext J
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
h : J ∈ I.minimalPrimes → Membership.mem (γ := Set (Ideal R)) {I.radical} J
h₁ : Membership.mem (γ := Set (Ideal R)) {I.radical} J → J ∈ I.minimalPrimes
⊢ J ∈ I.minimalPrimes ↔ Membership.mem (γ := Set (Ideal R)) {I.radical} J

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
H : J ∈ I.minimalPrimes
⊢ I.radical ≤ J

Tactic:
have le := H.out.isPrime.radical_le_iff.mpr H.le
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
H : J ∈ I.minimalPrimes
le : I.radical ≤ J
⊢ Membership.mem (γ := Set (Ideal R)) {I.radical} J

Tactic:
(H.2 ⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩ le).antisymm le

Premises used: Set.Mem, Ideal.le_radical, setOf, LE.le.antisymm, And.right, And.intro, Set.singleton, Ideal.isPrime_radical
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hI : I.IsPrimary
J : Ideal R
H : J ∈ I.minimalPrimes
le : I.radical ≤ J
⊢ Membership.mem (γ := Set (Ideal R)) {I.radical} J

Tactic:
exact (H.2 ⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩ le).antisymm le

Premises used: Ideal.le_radical, LE.le.antisymm, And.right, And.intro, Ideal.isPrime_radical
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hI : I.IsPrimary
⊢ I.radical ∈ I.minimalPrimes

Tactic:
⟨⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩, fun _ H _ => H.1.radical_le_iff.mpr H.2⟩

Premises used: Iff.mpr, Set.Mem, Ideal.le_radical, setOf, And.right, And.left, Ideal.IsMinimalPrime, And.intro, Ideal.isPrime_radical, Minimal, Ideal.IsPrime.radical_le_iff
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hI : I.IsPrimary
⊢ I.radical ∈ I.minimalPrimes

Tactic:
exact ⟨⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩, fun _ H _ => H.1.radical_le_iff.mpr H.2⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsPrime
h : ∀ (J : Ideal R), J ∈ I.minimalPrimes ↔ Membership.mem (γ := Set (Ideal R)) {I} J
⊢ I.minimalPrimes = {I}

Tactic:
ext J