[GOAL]
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
⊢ IsProper IF.I
[PROOFSTEP]
cases' IF.F.nonempty with w h
[GOAL]
case intro
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
w : P
h : w ∈ ↑IF.F
⊢ IsProper IF.I
[PROOFSTEP]
apply isProper_of_not_mem (_ : w ∉ IF.I)
[GOAL]
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
w : P
h : w ∈ ↑IF.F
⊢ ¬w ∈ IF.I
[PROOFSTEP]
rwa [← IF.compl_I_eq_F] at h 
[GOAL]
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
src✝ : IsProper IF.I := I_isProper IF
⊢ IsPFilter (↑IF.I)ᶜ
[PROOFSTEP]
rw [IF.compl_I_eq_F]
[GOAL]
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
src✝ : IsProper IF.I := I_isProper IF
⊢ IsPFilter ↑IF.F
[PROOFSTEP]
exact IF.F.isPFilter
[GOAL]
P : Type u_1
inst✝ : SemilatticeInf P
x✝ y✝ : P
I : Ideal P
hI : IsPrime I
x y : P
⊢ x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
[PROOFSTEP]
contrapose!
[GOAL]
P : Type u_1
inst✝ : SemilatticeInf P
x✝ y✝ : P
I : Ideal P
hI : IsPrime I
x y : P
⊢ ¬x ∈ I ∧ ¬y ∈ I → ¬x ⊓ y ∈ I
[PROOFSTEP]
let F := hI.compl_filter.toPFilter
[GOAL]
P : Type u_1
inst✝ : SemilatticeInf P
x✝ y✝ : P
I : Ideal P
hI : IsPrime I
x y : P
F : PFilter P := IsPFilter.toPFilter (_ : IsPFilter (↑I)ᶜ)
⊢ ¬x ∈ I ∧ ¬y ∈ I → ¬x ⊓ y ∈ I
[PROOFSTEP]
show x ∈ F ∧ y ∈ F → x ⊓ y ∈ F
[GOAL]
P : Type u_1
inst✝ : SemilatticeInf P
x✝ y✝ : P
I : Ideal P
hI : IsPrime I
x y : P
F : PFilter P := IsPFilter.toPFilter (_ : IsPFilter (↑I)ᶜ)
⊢ x ∈ F ∧ y ∈ F → x ⊓ y ∈ F
[PROOFSTEP]
exact fun h => inf_mem h.1 h.2
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ IsPrime I
[PROOFSTEP]
rw [IsPrime_iff]
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ IsProper I ∧ IsPFilter (↑I)ᶜ
[PROOFSTEP]
use‹_›
[GOAL]
case right
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ IsPFilter (↑I)ᶜ
[PROOFSTEP]
refine .of_def ?_ ?_ ?_
[GOAL]
case right.refine_1
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ Set.Nonempty (↑I)ᶜ
[PROOFSTEP]
exact Set.nonempty_compl.2 (I.IsProper_iff.1 ‹_›)
[GOAL]
case right.refine_2
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ DirectedOn (fun x x_1 => x ≥ x_1) (↑I)ᶜ
[PROOFSTEP]
intro x hx y hy
[GOAL]
case right.refine_2
P : Type u_1
inst✝¹ : SemilatticeInf P
x✝ y✝ : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
x : P
hx : x ∈ (↑I)ᶜ
y : P
hy : y ∈ (↑I)ᶜ
⊢ ∃ z, z ∈ (↑I)ᶜ ∧ (fun x x_1 => x ≥ x_1) x z ∧ (fun x x_1 => x ≥ x_1) y z
[PROOFSTEP]
exact ⟨x ⊓ y, fun h => (hI h).elim hx hy, inf_le_left, inf_le_right⟩
[GOAL]
case right.refine_3
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ ∀ {x y : P}, x ≤ y → x ∈ (↑I)ᶜ → y ∈ (↑I)ᶜ
[PROOFSTEP]
exact @mem_compl_of_ge _ _ _
[GOAL]
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
⊢ IsPrime I
[PROOFSTEP]
rw [isPrime_iff_mem_or_mem]
[GOAL]
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
⊢ ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
[PROOFSTEP]
intro x y
[GOAL]
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
⊢ x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
[PROOFSTEP]
contrapose!
[GOAL]
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
⊢ ¬x ∈ I ∧ ¬y ∈ I → ¬x ⊓ y ∈ I
[PROOFSTEP]
rintro ⟨hx, hynI⟩ hxy
[GOAL]
case intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
⊢ False
[PROOFSTEP]
apply hynI
[GOAL]
case intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
⊢ y ∈ I
[PROOFSTEP]
let J := I ⊔ principal x
[GOAL]
case intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
⊢ y ∈ I
[PROOFSTEP]
have hJuniv : (J : Set P) = Set.univ := IsMaximal.maximal_proper (lt_sup_principal_of_not_mem ‹_›)
[GOAL]
case intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
⊢ y ∈ I
[PROOFSTEP]
have hyJ : y ∈ ↑J := Set.eq_univ_iff_forall.mp hJuniv y
[GOAL]
case intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
hyJ : y ∈ ↑J
⊢ y ∈ I
[PROOFSTEP]
rw [coe_sup_eq] at hyJ 
[GOAL]
case intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
hyJ : y ∈ {x_1 | ∃ i, i ∈ I ∧ ∃ j, j ∈ principal x ∧ x_1 = i ⊔ j}
⊢ y ∈ I
[PROOFSTEP]
rcases hyJ with ⟨a, ha, b, hb, hy⟩
[GOAL]
case intro.intro.intro.intro.intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
a : P
ha : a ∈ I
b : P
hb : b ∈ principal x
hy : y = a ⊔ b
⊢ y ∈ I
[PROOFSTEP]
rw [hy]
[GOAL]
case intro.intro.intro.intro.intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
a : P
ha : a ∈ I
b : P
hb : b ∈ principal x
hy : y = a ⊔ b
⊢ a ⊔ b ∈ I
[PROOFSTEP]
refine' sup_mem ha (I.lower (le_inf hb _) hxy)
[GOAL]
case intro.intro.intro.intro.intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
a : P
ha : a ∈ I
b : P
hb : b ∈ principal x
hy : y = a ⊔ b
⊢ b ≤ y
[PROOFSTEP]
rw [hy]
[GOAL]
case intro.intro.intro.intro.intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
a : P
ha : a ∈ I
b : P
hb : b ∈ principal x
hy : y = a ⊔ b
⊢ b ≤ a ⊔ b
[PROOFSTEP]
exact le_sup_right
[GOAL]
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsPrime I
⊢ x ∈ I ∨ xᶜ ∈ I
[PROOFSTEP]
apply hI.mem_or_mem
[GOAL]
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsPrime I
⊢ x ⊓ xᶜ ∈ I
[PROOFSTEP]
rw [inf_compl_eq_bot]
[GOAL]
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsPrime I
⊢ ⊥ ∈ I
[PROOFSTEP]
exact I.bot_mem
[GOAL]
P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : IsProper I
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
⊢ IsPrime I
[PROOFSTEP]
simp only [isPrime_iff_mem_or_mem, or_iff_not_imp_left]
[GOAL]
P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : IsProper I
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
⊢ ∀ {x y : P}, x ⊓ y ∈ I → ¬x ∈ I → y ∈ I
[PROOFSTEP]
intro x y hxy hxI
[GOAL]
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsProper I
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : ¬x ∈ I
⊢ y ∈ I
[PROOFSTEP]
have hxcI : xᶜ ∈ I := h.resolve_left hxI
[GOAL]
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsProper I
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : ¬x ∈ I
hxcI : xᶜ ∈ I
⊢ y ∈ I
[PROOFSTEP]
have ass : x ⊓ y ⊔ y ⊓ xᶜ ∈ I := sup_mem hxy (I.lower inf_le_right hxcI)
[GOAL]
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsProper I
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : ¬x ∈ I
hxcI : xᶜ ∈ I
ass : x ⊓ y ⊔ y ⊓ xᶜ ∈ I
⊢ y ∈ I
[PROOFSTEP]
rwa [inf_comm, sup_inf_inf_compl] at ass 
[GOAL]
P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : IsPrime I
⊢ IsMaximal I
[PROOFSTEP]
simp only [IsMaximal_iff, Set.eq_univ_iff_forall, IsPrime.toIsProper, true_and]
[GOAL]
P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : IsPrime I
⊢ ∀ ⦃J : Ideal P⦄, I < J → ∀ (x : P), x ∈ ↑J
[PROOFSTEP]
intro J hIJ x
[GOAL]
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsPrime I
J : Ideal P
hIJ : I < J
x : P
⊢ x ∈ ↑J
[PROOFSTEP]
rcases Set.exists_of_ssubset hIJ with ⟨y, hyJ, hyI⟩
[GOAL]
case intro.intro
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsPrime I
J : Ideal P
hIJ : I < J
x y : P
hyJ : y ∈ ↑J
hyI : ¬y ∈ ↑I
⊢ x ∈ ↑J
[PROOFSTEP]
suffices ass : x ⊓ y ⊔ x ⊓ yᶜ ∈ J
[GOAL]
case intro.intro
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsPrime I
J : Ideal P
hIJ : I < J
x y : P
hyJ : y ∈ ↑J
hyI : ¬y ∈ ↑I
ass : x ⊓ y ⊔ x ⊓ yᶜ ∈ J
⊢ x ∈ ↑J
[PROOFSTEP]
rwa [sup_inf_inf_compl] at ass 
[GOAL]
case ass
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsPrime I
J : Ideal P
hIJ : I < J
x y : P
hyJ : y ∈ ↑J
hyI : ¬y ∈ ↑I
⊢ x ⊓ y ⊔ x ⊓ yᶜ ∈ J
[PROOFSTEP]
exact sup_mem (J.lower inf_le_right hyJ) (hIJ.le <| I.lower inf_le_right <| IsPrime.mem_compl_of_not_mem ‹_› hyI)
[GOAL]
P : Type u_1
inst✝ : Preorder P
IF : Ideal.PrimePair P
⊢ IsIdeal (↑IF.F)ᶜ
[PROOFSTEP]
rw [IF.compl_F_eq_I]
[GOAL]
P : Type u_1
inst✝ : Preorder P
IF : Ideal.PrimePair P
⊢ IsIdeal ↑IF.I
[PROOFSTEP]
exact IF.I.isIdeal
