[GOAL]
P : Type u_1
inst✝ : LE P
I J s✝ t✝ : Ideal P
x y : P
s t : Ideal P
x✝ : s.toLowerSet = t.toLowerSet
⊢ s = t
[PROOFSTEP]
cases s
[GOAL]
case mk
P : Type u_1
inst✝ : LE P
I J s t✝ : Ideal P
x y : P
t : Ideal P
toLowerSet✝ : LowerSet P
nonempty'✝ : Set.Nonempty toLowerSet✝.carrier
directed'✝ : DirectedOn (fun x x_1 => x ≤ x_1) toLowerSet✝.carrier
x✝ : { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }.toLowerSet = t.toLowerSet
⊢ { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ } = t
[PROOFSTEP]
cases t
[GOAL]
case mk.mk
P : Type u_1
inst✝ : LE P
I J s t : Ideal P
x y : P
toLowerSet✝¹ : LowerSet P
nonempty'✝¹ : Set.Nonempty toLowerSet✝¹.carrier
directed'✝¹ : DirectedOn (fun x x_1 => x ≤ x_1) toLowerSet✝¹.carrier
toLowerSet✝ : LowerSet P
nonempty'✝ : Set.Nonempty toLowerSet✝.carrier
directed'✝ : DirectedOn (fun x x_1 => x ≤ x_1) toLowerSet✝.carrier
x✝ :
  { toLowerSet := toLowerSet✝¹, nonempty' := nonempty'✝¹, directed' := directed'✝¹ }.toLowerSet =
    { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }.toLowerSet
⊢ { toLowerSet := toLowerSet✝¹, nonempty' := nonempty'✝¹, directed' := directed'✝¹ } =
    { toLowerSet := toLowerSet✝, nonempty' := nonempty'✝, directed' := directed'✝ }
[PROOFSTEP]
congr
[GOAL]
P : Type u_1
inst✝ : LE P
I✝ J s t : Ideal P
x y : P
I : Ideal P
p : P
nmem : ¬p ∈ I
hp : ↑I = univ
⊢ False
[PROOFSTEP]
have := mem_univ p
[GOAL]
P : Type u_1
inst✝ : LE P
I✝ J s t : Ideal P
x y : P
I : Ideal P
p : P
nmem : ¬p ∈ I
hp : ↑I = univ
this : p ∈ univ
⊢ False
[PROOFSTEP]
rw [← hp] at this 
[GOAL]
P : Type u_1
inst✝ : LE P
I✝ J s t : Ideal P
x y : P
I : Ideal P
p : P
nmem : ¬p ∈ I
hp : ↑I = univ
this : p ∈ ↑I
⊢ False
[PROOFSTEP]
exact nmem this
[GOAL]
P : Type u_1
inst✝¹ : LE P
I✝ J✝ s t : Ideal P
x y : P
inst✝ : IsDirected P fun x x_1 => x ≥ x_1
I J : Ideal P
⊢ Set.Nonempty (↑I ∩ ↑J)
[PROOFSTEP]
obtain ⟨a, ha⟩ := I.nonempty
[GOAL]
case intro
P : Type u_1
inst✝¹ : LE P
I✝ J✝ s t : Ideal P
x y : P
inst✝ : IsDirected P fun x x_1 => x ≥ x_1
I J : Ideal P
a : P
ha : a ∈ ↑I
⊢ Set.Nonempty (↑I ∩ ↑J)
[PROOFSTEP]
obtain ⟨b, hb⟩ := J.nonempty
[GOAL]
case intro.intro
P : Type u_1
inst✝¹ : LE P
I✝ J✝ s t : Ideal P
x y : P
inst✝ : IsDirected P fun x x_1 => x ≥ x_1
I J : Ideal P
a : P
ha : a ∈ ↑I
b : P
hb : b ∈ ↑J
⊢ Set.Nonempty (↑I ∩ ↑J)
[PROOFSTEP]
obtain ⟨c, hac, hbc⟩ := exists_le_le a b
[GOAL]
case intro.intro.intro.intro
P : Type u_1
inst✝¹ : LE P
I✝ J✝ s t : Ideal P
x y : P
inst✝ : IsDirected P fun x x_1 => x ≥ x_1
I J : Ideal P
a : P
ha : a ∈ ↑I
b : P
hb : b ∈ ↑J
c : P
hac : c ≤ a
hbc : c ≤ b
⊢ Set.Nonempty (↑I ∩ ↑J)
[PROOFSTEP]
exact ⟨c, I.lower hac ha, J.lower hbc hb⟩
[GOAL]
P : Type u_1
inst✝² : LE P
inst✝¹ : IsDirected P fun x x_1 => x ≤ x_1
inst✝ : Nonempty P
I : Ideal P
hI : IsCoatom I
src✝ : IsProper I := IsCoatom.isProper hI
x✝ : Ideal P
hJ : I < x✝
⊢ ↑x✝ = univ
[PROOFSTEP]
simp [hI.2 _ hJ]
[GOAL]
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
I : Ideal P
h : ⊤ ∈ I
⊢ I = ⊤
[PROOFSTEP]
ext
[GOAL]
case a.h
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
I : Ideal P
h : ⊤ ∈ I
x✝ : P
⊢ x✝ ∈ ↑I ↔ x✝ ∈ ↑⊤
[PROOFSTEP]
exact iff_of_true (I.lower le_top h) trivial
[GOAL]
P : Type u_1
inst✝¹ : Preorder P
inst✝ : OrderBot P
⊢ ∀ (a : Ideal P), ⊥ ≤ a
[PROOFSTEP]
simp
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsDirected P fun x x_1 => x ≥ x_1
x✝ : P
I✝ J✝ K s t I J : Ideal P
x : P
hx : x ∈ (I.toLowerSet ⊓ J.toLowerSet).carrier
y : P
hy : y ∈ (I.toLowerSet ⊓ J.toLowerSet).carrier
⊢ (fun x x_1 => x ≤ x_1) x (x ⊔ y) ∧ (fun x x_1 => x ≤ x_1) y (x ⊔ y)
[PROOFSTEP]
simp
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsDirected P fun x x_1 => x ≥ x_1
x : P
I✝ J✝ K s t I J : Ideal P
⊢ Set.Nonempty
    { carrier := {x | ∃ i, i ∈ I ∧ ∃ j, j ∈ J ∧ x ≤ i ⊔ j},
        lower' :=
          (_ :
            ∀ (x y : P),
              y ≤ x →
                x ∈ {x | ∃ i, i ∈ I ∧ ∃ j, j ∈ J ∧ x ≤ i ⊔ j} → y ∈ {x | ∃ i, i ∈ I ∧ ∃ j, j ∈ J ∧ x ≤ i ⊔ j}) }.carrier
[PROOFSTEP]
cases' inter_nonempty I J with w h
[GOAL]
case intro
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsDirected P fun x x_1 => x ≥ x_1
x : P
I✝ J✝ K s t I J : Ideal P
w : P
h : w ∈ ↑I ∩ ↑J
⊢ Set.Nonempty
    { carrier := {x | ∃ i, i ∈ I ∧ ∃ j, j ∈ J ∧ x ≤ i ⊔ j},
        lower' :=
          (_ :
            ∀ (x y : P),
              y ≤ x →
                x ∈ {x | ∃ i, i ∈ I ∧ ∃ j, j ∈ J ∧ x ≤ i ⊔ j} → y ∈ {x | ∃ i, i ∈ I ∧ ∃ j, j ∈ J ∧ x ≤ i ⊔ j}) }.carrier
[PROOFSTEP]
exact ⟨w, w, h.1, w, h.2, le_sup_left⟩
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsDirected P fun x x_1 => x ≥ x_1
x : P
I J K s t : Ideal P
hx : ¬x ∈ I
h : I = I ⊔ principal x
⊢ x ∈ I
[PROOFSTEP]
simpa only [left_eq_sup, principal_le_iff] using h
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
I J K : Ideal P
S : Set (Ideal P)
⊢ ⊥ ∈ (⨅ (s : Ideal P) (_ : s ∈ S), s.toLowerSet).carrier
[PROOFSTEP]
rw [LowerSet.carrier_eq_coe, LowerSet.coe_iInf₂, Set.mem_iInter₂]
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
I J K : Ideal P
S : Set (Ideal P)
⊢ ∀ (i : Ideal P), i ∈ S → ⊥ ∈ ↑i.toLowerSet
[PROOFSTEP]
exact fun s _ ↦ s.bot_mem
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
I J K : Ideal P
S : Set (Ideal P)
a : P
ha : a ∈ (⨅ (s : Ideal P) (_ : s ∈ S), s.toLowerSet).carrier
b : P
hb : b ∈ (⨅ (s : Ideal P) (_ : s ∈ S), s.toLowerSet).carrier
⊢ a ⊔ b ∈ (⨅ (s : Ideal P) (_ : s ∈ S), s.toLowerSet).carrier
[PROOFSTEP]
rw [LowerSet.carrier_eq_coe, LowerSet.coe_iInf₂, Set.mem_iInter₂] at ha hb ⊢
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
I J K : Ideal P
S : Set (Ideal P)
a : P
ha : ∀ (i : Ideal P), i ∈ S → a ∈ ↑i.toLowerSet
b : P
hb : ∀ (i : Ideal P), i ∈ S → b ∈ ↑i.toLowerSet
⊢ ∀ (i : Ideal P), i ∈ S → a ⊔ b ∈ ↑i.toLowerSet
[PROOFSTEP]
exact fun s hs ↦ sup_mem (ha _ hs) (hb _ hs)
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
I J K : Ideal P
S : Set (Ideal P)
⊢ x ∈ sInf S ↔ ∀ (s : Ideal P), s ∈ S → x ∈ s
[PROOFSTEP]
simp_rw [← SetLike.mem_coe, coe_sInf, mem_iInter₂]
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
I J K : Ideal P
S✝ : Set (Ideal P)
src✝ : Lattice (Ideal P) := inferInstance
S : Set (Ideal P)
⊢ IsGLB S (sInf S)
[PROOFSTEP]
refine' ⟨fun s hs ↦ _, fun s hs ↦ by rwa [← coe_subset_coe, coe_sInf, subset_iInter₂_iff]⟩
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
I J K : Ideal P
S✝ : Set (Ideal P)
src✝ : Lattice (Ideal P) := inferInstance
S : Set (Ideal P)
s : Ideal P
hs : s ∈ lowerBounds S
⊢ s ≤ sInf S
[PROOFSTEP]
rwa [← coe_subset_coe, coe_sInf, subset_iInter₂_iff]
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
I J K : Ideal P
S✝ : Set (Ideal P)
src✝ : Lattice (Ideal P) := inferInstance
S : Set (Ideal P)
s : Ideal P
hs : s ∈ S
⊢ sInf S ≤ s
[PROOFSTEP]
rw [← coe_subset_coe, coe_sInf]
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
I J K : Ideal P
S✝ : Set (Ideal P)
src✝ : Lattice (Ideal P) := inferInstance
S : Set (Ideal P)
s : Ideal P
hs : s ∈ S
⊢ ⋂ (s : Ideal P) (_ : s ∈ S), ↑s ⊆ ↑s
[PROOFSTEP]
exact biInter_subset_of_mem hs
[GOAL]
P : Type u_1
inst✝ : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
⊢ ∃ i', i' ∈ I ∧ ∃ j', j' ∈ J ∧ x = i' ⊔ j'
[PROOFSTEP]
refine' ⟨x ⊓ i, I.lower inf_le_right hi, x ⊓ j, J.lower inf_le_right hj, _⟩
[GOAL]
P : Type u_1
inst✝ : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
⊢ x = x ⊓ i ⊔ x ⊓ j
[PROOFSTEP]
calc
  x = x ⊓ (i ⊔ j) := left_eq_inf.mpr hx
  _ = x ⊓ i ⊔ x ⊓ j := inf_sup_left
[GOAL]
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
hxc : xᶜ ∈ I
⊢ ¬x ∈ I
[PROOFSTEP]
intro hx
[GOAL]
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
hxc : xᶜ ∈ I
hx : x ∈ I
⊢ False
[PROOFSTEP]
apply hI.top_not_mem
[GOAL]
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
hxc : xᶜ ∈ I
hx : x ∈ I
⊢ ⊤ ∈ I
[PROOFSTEP]
have ht : x ⊔ xᶜ ∈ I := sup_mem ‹_› ‹_›
[GOAL]
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
hxc : xᶜ ∈ I
hx : x ∈ I
ht : x ⊔ xᶜ ∈ I
⊢ ⊤ ∈ I
[PROOFSTEP]
rwa [sup_compl_eq_top] at ht 
[GOAL]
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
⊢ ¬x ∈ I ∨ ¬xᶜ ∈ I
[PROOFSTEP]
have h : xᶜ ∈ I → x ∉ I := hI.not_mem_of_compl_mem
[GOAL]
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsProper I
h : xᶜ ∈ I → ¬x ∈ I
⊢ ¬x ∈ I ∨ ¬xᶜ ∈ I
[PROOFSTEP]
tauto
[GOAL]
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
⊢ Monotone (sequenceOfCofinals p 𝒟)
[PROOFSTEP]
apply monotone_nat_of_le_succ
[GOAL]
case hf
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
⊢ ∀ (n : ℕ), sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 (n + 1)
[PROOFSTEP]
intro n
[GOAL]
case hf
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
⊢ sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 (n + 1)
[PROOFSTEP]
dsimp only [sequenceOfCofinals, Nat.add]
[GOAL]
case hf
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
⊢ sequenceOfCofinals p 𝒟 n ≤
    match Encodable.decode n with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => Cofinal.above (𝒟 i) (sequenceOfCofinals p 𝒟 n)
[PROOFSTEP]
cases (Encodable.decode n : Option ι)
[GOAL]
case hf.none
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
⊢ sequenceOfCofinals p 𝒟 n ≤
    match none with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => Cofinal.above (𝒟 i) (sequenceOfCofinals p 𝒟 n)
[PROOFSTEP]
rfl
[GOAL]
case hf.some
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
val✝ : ι
⊢ sequenceOfCofinals p 𝒟 n ≤
    match some val✝ with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => Cofinal.above (𝒟 i) (sequenceOfCofinals p 𝒟 n)
[PROOFSTEP]
apply Cofinal.le_above
[GOAL]
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ sequenceOfCofinals p 𝒟 (Encodable.encode i + 1) ∈ 𝒟 i
[PROOFSTEP]
dsimp only [sequenceOfCofinals, Nat.add]
[GOAL]
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ (match Encodable.decode (Encodable.encode i) with
    | none => sequenceOfCofinals p 𝒟 (Encodable.encode i)
    | some i_1 => Cofinal.above (𝒟 i_1) (sequenceOfCofinals p 𝒟 (Encodable.encode i))) ∈
    𝒟 i
[PROOFSTEP]
rw [Encodable.encodek]
[GOAL]
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ (match some i with
    | none => sequenceOfCofinals p 𝒟 (Encodable.encode i)
    | some i_1 => Cofinal.above (𝒟 i_1) (sequenceOfCofinals p 𝒟 (Encodable.encode i))) ∈
    𝒟 i
[PROOFSTEP]
apply Cofinal.above_mem
