R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ∃ m,
    m ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} ∧
      ↑OrderDual.toDual J ≤ m ∧ ∀ (z : (Ideal R)ᵒᵈ), z ∈ {p | IsPrime p ∧ I ≤ p} → m ≤ z → z = m
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ∃ p, p ∈ Ideal.minimalPrimes I ∧ p ≤ J
suffices
  ∃ m ∈ { p : (Ideal R)ᵒᵈ | Ideal.IsPrime p ∧ I ≤ OrderDual.ofDual p },
    OrderDual.toDual J ≤ m ∧ ∀ z ∈ { p : (Ideal R)ᵒᵈ | Ideal.IsPrime p ∧ I ≤ p }, m ≤ z → z = m by
  obtain ⟨p, h₁, h₂, h₃⟩ := this
  simp_rw [← @eq_comm _ p] at h₃
  exact ⟨p, ⟨h₁, fun a b c => le_of_eq (h₃ a b c)⟩, h₂⟩
case ih
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ∀ (c : Set (Ideal R)ᵒᵈ),
    c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : (Ideal R)ᵒᵈ),
          y ∈ c → ∃ ub, ub ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} ∧ ∀ (z : (Ideal R)ᵒᵈ), z ∈ c → z ≤ ub

case hxs
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ↑OrderDual.toDual J ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ∃ m,
    m ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} ∧
      ↑OrderDual.toDual J ≤ m ∧ ∀ (z : (Ideal R)ᵒᵈ), z ∈ {p | IsPrime p ∧ I ≤ p} → m ≤ z → z = m
apply zorn_nonempty_partialOrder₀
case hxs
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ↑OrderDual.toDual J ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}

case ih
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ∀ (c : Set (Ideal R)ᵒᵈ),
    c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : (Ideal R)ᵒᵈ),
          y ∈ c → ∃ ub, ub ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} ∧ ∀ (z : (Ideal R)ᵒᵈ), z ∈ c → z ≤ ub
case ih
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ∀ (c : Set (Ideal R)ᵒᵈ),
    c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : (Ideal R)ᵒᵈ),
          y ∈ c → ∃ ub, ub ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} ∧ ∀ (z : (Ideal R)ᵒᵈ), z ∈ c → z ≤ ub

case hxs
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ↑OrderDual.toDual J ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
swap
case ih
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ ∃ ub, ub ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} ∧ ∀ (z : (Ideal R)ᵒᵈ), z ∈ c → z ≤ ub
case ih
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ∀ (c : Set (Ideal R)ᵒᵈ),
    c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} →
      IsChain (fun x x_1 => x ≤ x_1) c →
        ∀ (y : (Ideal R)ᵒᵈ),
          y ∈ c → ∃ ub, ub ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} ∧ ∀ (z : (Ideal R)ᵒᵈ), z ∈ c → z ≤ ub
rintro (c : Set (Ideal R)) hc hc' J' hJ'
case ih.refine'_1
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ I ≤ ↑OrderDual.ofDual (↑OrderDual.toDual (sInf c))

case ih.refine'_2
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ ∀ (z : (Ideal R)ᵒᵈ), z ∈ c → z ≤ ↑OrderDual.toDual (sInf c)
case ih
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ ∃ ub, ub ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} ∧ ∀ (z : (Ideal R)ᵒᵈ), z ∈ c → z ≤ ub
refine'
  ⟨OrderDual.toDual (sInf c),
    ⟨Ideal.sInf_isPrime_of_isChain ⟨J', hJ'⟩ hc'.symm fun x hx => (hc hx).1, _⟩, _⟩
case intro.intro.intro
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
p : (Ideal R)ᵒᵈ
h₁ : p ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
h₂ : ↑OrderDual.toDual J ≤ p
h₃ : ∀ (z : (Ideal R)ᵒᵈ), z ∈ {p | IsPrime p ∧ I ≤ p} → p ≤ z → z = p
⊢ ∃ p, p ∈ Ideal.minimalPrimes I ∧ p ≤ J
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
this :
  ∃ m,
    m ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p} ∧
      ↑OrderDual.toDual J ≤ m ∧ ∀ (z : (Ideal R)ᵒᵈ), z ∈ {p | IsPrime p ∧ I ≤ p} → m ≤ z → z = m
⊢ ∃ p, p ∈ Ideal.minimalPrimes I ∧ p ≤ J
obtain ⟨p, h₁, h₂, h₃⟩ := this
case intro.intro.intro
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
p : (Ideal R)ᵒᵈ
h₁ : p ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
h₂ : ↑OrderDual.toDual J ≤ p
h₃ : ∀ (z : (Ideal R)ᵒᵈ), z ∈ {p | IsPrime p ∧ I ≤ p} → p ≤ z → p = z
⊢ ∃ p, p ∈ Ideal.minimalPrimes I ∧ p ≤ J
case intro.intro.intro
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
p : (Ideal R)ᵒᵈ
h₁ : p ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
h₂ : ↑OrderDual.toDual J ≤ p
h₃ : ∀ (z : (Ideal R)ᵒᵈ), z ∈ {p | IsPrime p ∧ I ≤ p} → p ≤ z → z = p
⊢ ∃ p, p ∈ Ideal.minimalPrimes I ∧ p ≤ J
simp_rw [← @eq_comm _ p] at h₃
no goals
case intro.intro.intro
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
p : (Ideal R)ᵒᵈ
h₁ : p ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
h₂ : ↑OrderDual.toDual J ≤ p
h₃ : ∀ (z : (Ideal R)ᵒᵈ), z ∈ {p | IsPrime p ∧ I ≤ p} → p ≤ z → p = z
⊢ ∃ p, p ∈ Ideal.minimalPrimes I ∧ p ≤ J
exact ⟨p, ⟨h₁, fun a b c => le_of_eq (h₃ a b c)⟩, h₂⟩
no goals
case hxs
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ ↑OrderDual.toDual J ∈ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
refine' ⟨show J.IsPrime by infer_instance, e⟩
no goals
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
⊢ IsPrime J
infer_instance
case ih.refine'_1
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ ∀ (b : Ideal R), b ∈ c → I ≤ b
case ih.refine'_1
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ I ≤ ↑OrderDual.ofDual (↑OrderDual.toDual (sInf c))
rw [OrderDual.ofDual_toDual, le_sInf_iff]
no goals
case ih.refine'_1
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ ∀ (b : Ideal R), b ∈ c → I ≤ b
exact fun _ hx => (hc hx).2
case ih.refine'_2
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
z : (Ideal R)ᵒᵈ
hz : z ∈ c
⊢ z ≤ ↑OrderDual.toDual (sInf c)
case ih.refine'_2
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
⊢ ∀ (z : (Ideal R)ᵒᵈ), z ∈ c → z ≤ ↑OrderDual.toDual (sInf c)
rintro z hz
case ih.refine'_2
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
z : (Ideal R)ᵒᵈ
hz : z ∈ c
⊢ sInf c ≤ ↑OrderDual.ofDual z
case ih.refine'_2
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
z : (Ideal R)ᵒᵈ
hz : z ∈ c
⊢ z ≤ ↑OrderDual.toDual (sInf c)
rw [OrderDual.le_toDual]
no goals
case ih.refine'_2
R : Type u_1
S : Type ?u.1440
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime J
e : I ≤ J
c : Set (Ideal R)
hc : c ⊆ {p | IsPrime p ∧ I ≤ ↑OrderDual.ofDual p}
hc' : IsChain (fun x x_1 => x ≤ x_1) c
J' : (Ideal R)ᵒᵈ
hJ' : J' ∈ c
z : (Ideal R)ᵒᵈ
hz : z ∈ c
⊢ sInf c ≤ ↑OrderDual.ofDual z
exact sInf_le hz