case h
R : Type u_1
S : Type ?u.122062
inst✝² : CommRing R
inst✝¹ : CommRing S
I J✝ : Ideal R
inst✝ : IsPrime I
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes I ↔ J ∈ {I}
R : Type u_1
S : Type ?u.122062
inst✝² : CommRing R
inst✝¹ : CommRing S
I J : Ideal R
inst✝ : IsPrime I
⊢ Ideal.minimalPrimes I = {I}
ext J
case h.mp
R : Type u_1
S : Type ?u.122062
inst✝² : CommRing R
inst✝¹ : CommRing S
I J✝ : Ideal R
inst✝ : IsPrime I
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes I → J ∈ {I}

case h.mpr
R : Type u_1
S : Type ?u.122062
inst✝² : CommRing R
inst✝¹ : CommRing S
I J✝ : Ideal R
inst✝ : IsPrime I
J : Ideal R
⊢ J ∈ {I} → J ∈ Ideal.minimalPrimes I
case h
R : Type u_1
S : Type ?u.122062
inst✝² : CommRing R
inst✝¹ : CommRing S
I J✝ : Ideal R
inst✝ : IsPrime I
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes I ↔ J ∈ {I}
constructor
no goals
case h.mp
R : Type u_1
S : Type ?u.122062
inst✝² : CommRing R
inst✝¹ : CommRing S
I J✝ : Ideal R
inst✝ : IsPrime I
J : Ideal R
⊢ J ∈ Ideal.minimalPrimes I → J ∈ {I}
exact fun H => (H.2 ⟨inferInstance, rfl.le⟩ H.1.2).antisymm H.1.2
case h.mpr
R : Type u_1
S : Type ?u.122062
inst✝² : CommRing R
inst✝¹ : CommRing S
J✝ J : Ideal R
inst✝ : IsPrime J
⊢ J ∈ Ideal.minimalPrimes J
case h.mpr
R : Type u_1
S : Type ?u.122062
inst✝² : CommRing R
inst✝¹ : CommRing S
I J✝ : Ideal R
inst✝ : IsPrime I
J : Ideal R
⊢ J ∈ {I} → J ∈ Ideal.minimalPrimes I
rintro (rfl : J = I)
no goals
case h.mpr
R : Type u_1
S : Type ?u.122062
inst✝² : CommRing R
inst✝¹ : CommRing S
J✝ J : Ideal R
inst✝ : IsPrime J
⊢ J ∈ Ideal.minimalPrimes J
refine' ⟨⟨inferInstance, rfl.le⟩, fun _ h _ => h.2⟩