[GOAL]
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
⊢ IsCompactElement k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
[PROOFSTEP]
classical
constructor
· intro H ι s hs
  obtain ⟨t, ht, ht'⟩ := H (Set.range s) hs
  have : ∀ x : t, ∃ i, s i = x := fun x => ht x.prop
  choose f hf using this
  refine' ⟨Finset.univ.image f, ht'.trans _⟩
  · rw [Finset.sup_le_iff]
    intro b hb
    rw [← show s (f ⟨b, hb⟩) = id b from hf _]
    exact Finset.le_sup (Finset.mem_image_of_mem f <| Finset.mem_univ (Subtype.mk b hb))
· intro H s hs
  obtain ⟨t, ht⟩ :=
    H s Subtype.val
      (by
        delta iSup
        rwa [Subtype.range_coe])
  refine' ⟨t.image Subtype.val, by simp, ht.trans _⟩
  rw [Finset.sup_le_iff]
  exact fun x hx => @Finset.le_sup _ _ _ _ _ id _ (Finset.mem_image_of_mem Subtype.val hx)
[GOAL]
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
⊢ IsCompactElement k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
⊢ IsCompactElement k → ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
[PROOFSTEP]
intro H ι s hs
[GOAL]
case mp
ι✝ : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
⊢ ∃ t, k ≤ Finset.sup t s
[PROOFSTEP]
obtain ⟨t, ht, ht'⟩ := H (Set.range s) hs
[GOAL]
case mp.intro.intro
ι✝ : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
⊢ ∃ t, k ≤ Finset.sup t s
[PROOFSTEP]
have : ∀ x : t, ∃ i, s i = x := fun x => ht x.prop
[GOAL]
case mp.intro.intro
ι✝ : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
this : ∀ (x : { x // x ∈ t }), ∃ i, s i = ↑x
⊢ ∃ t, k ≤ Finset.sup t s
[PROOFSTEP]
choose f hf using this
[GOAL]
case mp.intro.intro
ι✝ : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f✝ : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
f : { x // x ∈ t } → ι
hf : ∀ (x : { x // x ∈ t }), s (f x) = ↑x
⊢ ∃ t, k ≤ Finset.sup t s
[PROOFSTEP]
refine' ⟨Finset.univ.image f, ht'.trans _⟩
[GOAL]
case mp.intro.intro
ι✝ : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f✝ : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
f : { x // x ∈ t } → ι
hf : ∀ (x : { x // x ∈ t }), s (f x) = ↑x
⊢ Finset.sup t id ≤ Finset.sup (Finset.image f Finset.univ) s
[PROOFSTEP]
rw [Finset.sup_le_iff]
[GOAL]
case mp.intro.intro
ι✝ : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f✝ : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
f : { x // x ∈ t } → ι
hf : ∀ (x : { x // x ∈ t }), s (f x) = ↑x
⊢ ∀ (b : α), b ∈ t → id b ≤ Finset.sup (Finset.image f Finset.univ) s
[PROOFSTEP]
intro b hb
[GOAL]
case mp.intro.intro
ι✝ : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f✝ : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
f : { x // x ∈ t } → ι
hf : ∀ (x : { x // x ∈ t }), s (f x) = ↑x
b : α
hb : b ∈ t
⊢ id b ≤ Finset.sup (Finset.image f Finset.univ) s
[PROOFSTEP]
rw [← show s (f ⟨b, hb⟩) = id b from hf _]
[GOAL]
case mp.intro.intro
ι✝ : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f✝ : ι✝ → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : IsCompactElement k
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : ↑t ⊆ Set.range s
ht' : k ≤ Finset.sup t id
f : { x // x ∈ t } → ι
hf : ∀ (x : { x // x ∈ t }), s (f x) = ↑x
b : α
hb : b ∈ t
⊢ s (f { val := b, property := hb }) ≤ Finset.sup (Finset.image f Finset.univ) s
[PROOFSTEP]
exact Finset.le_sup (Finset.mem_image_of_mem f <| Finset.mem_univ (Subtype.mk b hb))
[GOAL]
case mpr
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
⊢ (∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s) → IsCompactElement k
[PROOFSTEP]
intro H s hs
[GOAL]
case mpr
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
s : Set α
hs : k ≤ sSup s
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
[PROOFSTEP]
obtain ⟨t, ht⟩ :=
  H s Subtype.val
    (by
      delta iSup
      rwa [Subtype.range_coe])
[GOAL]
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
s : Set α
hs : k ≤ sSup s
⊢ k ≤ iSup Subtype.val
[PROOFSTEP]
delta iSup
[GOAL]
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
s : Set α
hs : k ≤ sSup s
⊢ k ≤ sSup (Set.range Subtype.val)
[PROOFSTEP]
rwa [Subtype.range_coe]
[GOAL]
case mpr.intro
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
s : Set α
hs : k ≤ sSup s
t : Finset ↑s
ht : k ≤ Finset.sup t Subtype.val
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
[PROOFSTEP]
refine' ⟨t.image Subtype.val, by simp, ht.trans _⟩
[GOAL]
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
s : Set α
hs : k ≤ sSup s
t : Finset ↑s
ht : k ≤ Finset.sup t Subtype.val
⊢ ↑(Finset.image Subtype.val t) ⊆ s
[PROOFSTEP]
simp
[GOAL]
case mpr.intro
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
s : Set α
hs : k ≤ sSup s
t : Finset ↑s
ht : k ≤ Finset.sup t Subtype.val
⊢ Finset.sup t Subtype.val ≤ Finset.sup (Finset.image Subtype.val t) id
[PROOFSTEP]
rw [Finset.sup_le_iff]
[GOAL]
case mpr.intro
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u
inst✝ : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ Finset.sup t s
s : Set α
hs : k ≤ sSup s
t : Finset ↑s
ht : k ≤ Finset.sup t Subtype.val
⊢ ∀ (b : ↑s), b ∈ t → ↑b ≤ Finset.sup (Finset.image Subtype.val t) id
[PROOFSTEP]
exact fun x hx => @Finset.le_sup _ _ _ _ _ id _ (Finset.mem_image_of_mem Subtype.val hx)
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
⊢ IsCompactElement k ↔
    ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
[PROOFSTEP]
classical
constructor
· intro hk s hne hdir hsup
  obtain ⟨t, ht⟩ := hk s hsup
  have t_below_s : ∀ x ∈ t, ∃ y ∈ s, x ≤ y := fun x hxt => ⟨x, ht.left hxt, le_rfl⟩
  obtain ⟨x, ⟨hxs, hsupx⟩⟩ := Finset.sup_le_of_le_directed s hne hdir t t_below_s
  exact ⟨x, ⟨hxs, le_trans ht.right hsupx⟩⟩
· intro hk s hsup
  let S : Set α :=
    {x | ∃ t : Finset α, ↑t ⊆ s ∧ x = t.sup id}
      -- S is directed, nonempty, and still has sup above k.
  have dir_US : DirectedOn (· ≤ ·) S := by
    rintro x ⟨c, hc⟩ y ⟨d, hd⟩
    use x ⊔ y
    constructor
    · use c ∪ d
      constructor
      · simp only [hc.left, hd.left, Set.union_subset_iff, Finset.coe_union, and_self_iff]
      · simp only [hc.right, hd.right, Finset.sup_union]
    simp only [and_self_iff, le_sup_left, le_sup_right]
  have sup_S : sSup s ≤ sSup S := by
    apply sSup_le_sSup
    intro x hx
    use{ x }
    simpa only [and_true_iff, id.def, Finset.coe_singleton, eq_self_iff_true, Finset.sup_singleton,
      Set.singleton_subset_iff]
  have Sne : S.Nonempty := by
    suffices : ⊥ ∈ S
    exact Set.nonempty_of_mem this
    use∅
    simp only [Set.empty_subset, Finset.coe_empty, Finset.sup_empty, eq_self_iff_true, and_self_iff]
      -- Now apply the defn of compact and finish.
  obtain ⟨j, ⟨hjS, hjk⟩⟩ := hk S Sne dir_US (le_trans hsup sup_S)
  obtain ⟨t, ⟨htS, htsup⟩⟩ := hjS
  use t
  exact ⟨htS, by rwa [← htsup]⟩
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
⊢ IsCompactElement k ↔
    ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
⊢ IsCompactElement k →
    ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
[PROOFSTEP]
intro hk s hne hdir hsup
[GOAL]
case mp
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : IsCompactElement k
s : Set α
hne : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hsup : k ≤ sSup s
⊢ ∃ x, x ∈ s ∧ k ≤ x
[PROOFSTEP]
obtain ⟨t, ht⟩ := hk s hsup
[GOAL]
case mp.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : IsCompactElement k
s : Set α
hne : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hsup : k ≤ sSup s
t : Finset α
ht : ↑t ⊆ s ∧ k ≤ Finset.sup t id
⊢ ∃ x, x ∈ s ∧ k ≤ x
[PROOFSTEP]
have t_below_s : ∀ x ∈ t, ∃ y ∈ s, x ≤ y := fun x hxt => ⟨x, ht.left hxt, le_rfl⟩
[GOAL]
case mp.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : IsCompactElement k
s : Set α
hne : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hsup : k ≤ sSup s
t : Finset α
ht : ↑t ⊆ s ∧ k ≤ Finset.sup t id
t_below_s : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ x ≤ y
⊢ ∃ x, x ∈ s ∧ k ≤ x
[PROOFSTEP]
obtain ⟨x, ⟨hxs, hsupx⟩⟩ := Finset.sup_le_of_le_directed s hne hdir t t_below_s
[GOAL]
case mp.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : IsCompactElement k
s : Set α
hne : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hsup : k ≤ sSup s
t : Finset α
ht : ↑t ⊆ s ∧ k ≤ Finset.sup t id
t_below_s : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ x ≤ y
x : α
hxs : x ∈ s
hsupx : Finset.sup t id ≤ x
⊢ ∃ x, x ∈ s ∧ k ≤ x
[PROOFSTEP]
exact ⟨x, ⟨hxs, le_trans ht.right hsupx⟩⟩
[GOAL]
case mpr
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
⊢ (∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x) →
    IsCompactElement k
[PROOFSTEP]
intro hk s hsup
[GOAL]
case mpr
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
[PROOFSTEP]
let S : Set α :=
  {x | ∃ t : Finset α, ↑t ⊆ s ∧ x = t.sup id}
    -- S is directed, nonempty, and still has sup above k.
[GOAL]
case mpr
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
[PROOFSTEP]
have dir_US : DirectedOn (· ≤ ·) S := by
  rintro x ⟨c, hc⟩ y ⟨d, hd⟩
  use x ⊔ y
  constructor
  · use c ∪ d
    constructor
    · simp only [hc.left, hd.left, Set.union_subset_iff, Finset.coe_union, and_self_iff]
    · simp only [hc.right, hd.right, Finset.sup_union]
  simp only [and_self_iff, le_sup_left, le_sup_right]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
⊢ DirectedOn (fun x x_1 => x ≤ x_1) S
[PROOFSTEP]
rintro x ⟨c, hc⟩ y ⟨d, hd⟩
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ ∃ z, z ∈ S ∧ (fun x x_1 => x ≤ x_1) x z ∧ (fun x x_1 => x ≤ x_1) y z
[PROOFSTEP]
use x ⊔ y
[GOAL]
case h
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ x ⊔ y ∈ S ∧ (fun x x_1 => x ≤ x_1) x (x ⊔ y) ∧ (fun x x_1 => x ≤ x_1) y (x ⊔ y)
[PROOFSTEP]
constructor
[GOAL]
case h.left
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ x ⊔ y ∈ S
[PROOFSTEP]
use c ∪ d
[GOAL]
case h
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ ↑(c ∪ d) ⊆ s ∧ x ⊔ y = Finset.sup (c ∪ d) id
[PROOFSTEP]
constructor
[GOAL]
case h.left
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ ↑(c ∪ d) ⊆ s
[PROOFSTEP]
simp only [hc.left, hd.left, Set.union_subset_iff, Finset.coe_union, and_self_iff]
[GOAL]
case h.right
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ x ⊔ y = Finset.sup (c ∪ d) id
[PROOFSTEP]
simp only [hc.right, hd.right, Finset.sup_union]
[GOAL]
case h.right
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ (fun x x_1 => x ≤ x_1) x (x ⊔ y) ∧ (fun x x_1 => x ≤ x_1) y (x ⊔ y)
[PROOFSTEP]
simp only [and_self_iff, le_sup_left, le_sup_right]
[GOAL]
case mpr
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
[PROOFSTEP]
have sup_S : sSup s ≤ sSup S := by
  apply sSup_le_sSup
  intro x hx
  use{ x }
  simpa only [and_true_iff, id.def, Finset.coe_singleton, eq_self_iff_true, Finset.sup_singleton,
    Set.singleton_subset_iff]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
⊢ sSup s ≤ sSup S
[PROOFSTEP]
apply sSup_le_sSup
[GOAL]
case h
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
⊢ s ⊆ S
[PROOFSTEP]
intro x hx
[GOAL]
case h
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
x : α
hx : x ∈ s
⊢ x ∈ S
[PROOFSTEP]
use{ x }
[GOAL]
case h
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
x : α
hx : x ∈ s
⊢ ↑{x} ⊆ s ∧ x = Finset.sup {x} id
[PROOFSTEP]
simpa only [and_true_iff, id.def, Finset.coe_singleton, eq_self_iff_true, Finset.sup_singleton,
  Set.singleton_subset_iff]
[GOAL]
case mpr
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
[PROOFSTEP]
have Sne : S.Nonempty := by
  suffices : ⊥ ∈ S
  exact Set.nonempty_of_mem this
  use∅
  simp only [Set.empty_subset, Finset.coe_empty, Finset.sup_empty, eq_self_iff_true, and_self_iff]
    -- Now apply the defn of compact and finish.
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
⊢ Set.Nonempty S
[PROOFSTEP]
suffices : ⊥ ∈ S
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
this : ⊥ ∈ S
⊢ Set.Nonempty S
case this
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
⊢ ⊥ ∈ S
[PROOFSTEP]
exact Set.nonempty_of_mem this
[GOAL]
case this
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
⊢ ⊥ ∈ S
[PROOFSTEP]
use∅
[GOAL]
case h
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
⊢ ↑∅ ⊆ s ∧ ⊥ = Finset.sup ∅ id
[PROOFSTEP]
simp only [Set.empty_subset, Finset.coe_empty, Finset.sup_empty, eq_self_iff_true, and_self_iff]
  -- Now apply the defn of compact and finish.
[GOAL]
case mpr
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
Sne : Set.Nonempty S
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
[PROOFSTEP]
obtain ⟨j, ⟨hjS, hjk⟩⟩ := hk S Sne dir_US (le_trans hsup sup_S)
[GOAL]
case mpr.intro.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
Sne : Set.Nonempty S
j : α
hjS : j ∈ S
hjk : k ≤ j
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
[PROOFSTEP]
obtain ⟨t, ⟨htS, htsup⟩⟩ := hjS
[GOAL]
case mpr.intro.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
Sne : Set.Nonempty S
j : α
hjk : k ≤ j
t : Finset α
htS : ↑t ⊆ s
htsup : j = Finset.sup t id
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
[PROOFSTEP]
use t
[GOAL]
case h
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
Sne : Set.Nonempty S
j : α
hjk : k ≤ j
t : Finset α
htS : ↑t ⊆ s
htsup : j = Finset.sup t id
⊢ ↑t ⊆ s ∧ k ≤ Finset.sup t id
[PROOFSTEP]
exact ⟨htS, by rwa [← htsup]⟩
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
Sne : Set.Nonempty S
j : α
hjk : k ≤ j
t : Finset α
htS : ↑t ⊆ s
htsup : j = Finset.sup t id
⊢ k ≤ Finset.sup t id
[PROOFSTEP]
rwa [← htsup]
[GOAL]
ι✝ : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f✝ : ι✝ → α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ (i : ι), f i
⊢ ∃ s, k ≤ ⨆ (i : ι) (_ : i ∈ s), f i
[PROOFSTEP]
classical
let g : Finset ι → α := fun s => ⨆ i ∈ s, f i
have h1 : DirectedOn (· ≤ ·) (Set.range g) :=
  by
  rintro - ⟨s, rfl⟩ - ⟨t, rfl⟩
  exact
    ⟨g (s ∪ t), ⟨s ∪ t, rfl⟩, iSup_le_iSup_of_subset (Finset.subset_union_left s t),
      iSup_le_iSup_of_subset (Finset.subset_union_right s t)⟩
have h2 : k ≤ sSup (Set.range g) :=
  h.trans
    (iSup_le fun i => le_sSup_of_le ⟨{ i }, rfl⟩ (le_iSup_of_le i (le_iSup_of_le (Finset.mem_singleton_self i) le_rfl)))
obtain ⟨-, ⟨s, rfl⟩, hs⟩ :=
  (isCompactElement_iff_le_of_directed_sSup_le α k).mp hk (Set.range g) (Set.range_nonempty g) h1 h2
exact ⟨s, hs⟩
[GOAL]
ι✝ : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f✝ : ι✝ → α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ (i : ι), f i
⊢ ∃ s, k ≤ ⨆ (i : ι) (_ : i ∈ s), f i
[PROOFSTEP]
let g : Finset ι → α := fun s => ⨆ i ∈ s, f i
[GOAL]
ι✝ : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f✝ : ι✝ → α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun s => ⨆ (i : ι) (_ : i ∈ s), f i
⊢ ∃ s, k ≤ ⨆ (i : ι) (_ : i ∈ s), f i
[PROOFSTEP]
have h1 : DirectedOn (· ≤ ·) (Set.range g) :=
  by
  rintro - ⟨s, rfl⟩ - ⟨t, rfl⟩
  exact
    ⟨g (s ∪ t), ⟨s ∪ t, rfl⟩, iSup_le_iSup_of_subset (Finset.subset_union_left s t),
      iSup_le_iSup_of_subset (Finset.subset_union_right s t)⟩
[GOAL]
ι✝ : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f✝ : ι✝ → α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun s => ⨆ (i : ι) (_ : i ∈ s), f i
⊢ DirectedOn (fun x x_1 => x ≤ x_1) (Set.range g)
[PROOFSTEP]
rintro - ⟨s, rfl⟩ - ⟨t, rfl⟩
[GOAL]
case intro.intro
ι✝ : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f✝ : ι✝ → α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun s => ⨆ (i : ι) (_ : i ∈ s), f i
s t : Finset ι
⊢ ∃ z, z ∈ Set.range g ∧ (fun x x_1 => x ≤ x_1) (g s) z ∧ (fun x x_1 => x ≤ x_1) (g t) z
[PROOFSTEP]
exact
  ⟨g (s ∪ t), ⟨s ∪ t, rfl⟩, iSup_le_iSup_of_subset (Finset.subset_union_left s t),
    iSup_le_iSup_of_subset (Finset.subset_union_right s t)⟩
[GOAL]
ι✝ : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f✝ : ι✝ → α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun s => ⨆ (i : ι) (_ : i ∈ s), f i
h1 : DirectedOn (fun x x_1 => x ≤ x_1) (Set.range g)
⊢ ∃ s, k ≤ ⨆ (i : ι) (_ : i ∈ s), f i
[PROOFSTEP]
have h2 : k ≤ sSup (Set.range g) :=
  h.trans
    (iSup_le fun i => le_sSup_of_le ⟨{ i }, rfl⟩ (le_iSup_of_le i (le_iSup_of_le (Finset.mem_singleton_self i) le_rfl)))
[GOAL]
ι✝ : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f✝ : ι✝ → α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun s => ⨆ (i : ι) (_ : i ∈ s), f i
h1 : DirectedOn (fun x x_1 => x ≤ x_1) (Set.range g)
h2 : k ≤ sSup (Set.range g)
⊢ ∃ s, k ≤ ⨆ (i : ι) (_ : i ∈ s), f i
[PROOFSTEP]
obtain ⟨-, ⟨s, rfl⟩, hs⟩ :=
  (isCompactElement_iff_le_of_directed_sSup_le α k).mp hk (Set.range g) (Set.range_nonempty g) h1 h2
[GOAL]
case intro.intro.intro
ι✝ : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f✝ : ι✝ → α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun s => ⨆ (i : ι) (_ : i ∈ s), f i
h1 : DirectedOn (fun x x_1 => x ≤ x_1) (Set.range g)
h2 : k ≤ sSup (Set.range g)
s : Finset ι
hs : k ≤ g s
⊢ ∃ s, k ≤ ⨆ (i : ι) (_ : i ∈ s), f i
[PROOFSTEP]
exact ⟨s, hs⟩
[GOAL]
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_3
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
s : Set α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
⊢ sSup s < k
[PROOFSTEP]
rw [isCompactElement_iff_le_of_directed_sSup_le] at hk
[GOAL]
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_3
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
⊢ sSup s < k
[PROOFSTEP]
by_contra h
[GOAL]
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_3
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
h : ¬sSup s < k
⊢ False
[PROOFSTEP]
have sSup' : sSup s ≤ k := sSup_le s k fun s hs => (hbelow s hs).le
[GOAL]
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_3
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
h : ¬sSup s < k
sSup' : sSup s ≤ k
⊢ False
[PROOFSTEP]
replace sSup : sSup s = k := eq_iff_le_not_lt.mpr ⟨sSup', h⟩
[GOAL]
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_3
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ SupSet.sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
h : ¬SupSet.sSup s < k
sSup' : SupSet.sSup s ≤ k
sSup : SupSet.sSup s = k
⊢ False
[PROOFSTEP]
obtain ⟨x, hxs, hkx⟩ := hk s hemp hdir sSup.symm.le
[GOAL]
case intro.intro
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_3
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ SupSet.sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
h : ¬SupSet.sSup s < k
sSup' : SupSet.sSup s ≤ k
sSup : SupSet.sSup s = k
x : α
hxs : x ∈ s
hkx : k ≤ x
⊢ False
[PROOFSTEP]
obtain hxk := hbelow x hxs
[GOAL]
case intro.intro
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_3
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ SupSet.sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
h : ¬SupSet.sSup s < k
sSup' : SupSet.sSup s ≤ k
sSup : SupSet.sSup s = k
x : α
hxs : x ∈ s
hkx : k ≤ x
hxk : x < k
⊢ False
[PROOFSTEP]
exact hxk.ne (hxk.le.antisymm hkx)
[GOAL]
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
⊢ IsCompactElement (Finset.sup s f)
[PROOFSTEP]
classical
rw [isCompactElement_iff_le_of_directed_sSup_le]
intro d hemp hdir hsup
rw [← Function.comp.left_id f]
rw [← Finset.sup_image]
apply Finset.sup_le_of_le_directed d hemp hdir
rintro x hx
obtain ⟨p, ⟨hps, rfl⟩⟩ := Finset.mem_image.mp hx
specialize h p hps
rw [isCompactElement_iff_le_of_directed_sSup_le] at h
specialize h d hemp hdir (le_trans (Finset.le_sup hps) hsup)
simpa only [exists_prop]
[GOAL]
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
⊢ IsCompactElement (Finset.sup s f)
[PROOFSTEP]
rw [isCompactElement_iff_le_of_directed_sSup_le]
[GOAL]
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
⊢ ∀ (s_1 : Set α),
    Set.Nonempty s_1 →
      DirectedOn (fun x x_1 => x ≤ x_1) s_1 → Finset.sup s f ≤ sSup s_1 → ∃ x, x ∈ s_1 ∧ Finset.sup s f ≤ x
[PROOFSTEP]
intro d hemp hdir hsup
[GOAL]
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
⊢ ∃ x, x ∈ d ∧ Finset.sup s f ≤ x
[PROOFSTEP]
rw [← Function.comp.left_id f]
[GOAL]
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
⊢ ∃ x, x ∈ d ∧ Finset.sup s (id ∘ f) ≤ x
[PROOFSTEP]
rw [← Finset.sup_image]
[GOAL]
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
⊢ ∃ x, x ∈ d ∧ Finset.sup (Finset.image f s) id ≤ x
[PROOFSTEP]
apply Finset.sup_le_of_le_directed d hemp hdir
[GOAL]
case a
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
⊢ ∀ (x : α), x ∈ Finset.image f s → ∃ y, y ∈ d ∧ x ≤ y
[PROOFSTEP]
rintro x hx
[GOAL]
case a
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
x : α
hx : x ∈ Finset.image f s
⊢ ∃ y, y ∈ d ∧ x ≤ y
[PROOFSTEP]
obtain ⟨p, ⟨hps, rfl⟩⟩ := Finset.mem_image.mp hx
[GOAL]
case a.intro.intro
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
⊢ ∃ y, y ∈ d ∧ f p ≤ y
[PROOFSTEP]
specialize h p hps
[GOAL]
case a.intro.intro
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
h : IsCompactElement (f p)
⊢ ∃ y, y ∈ d ∧ f p ≤ y
[PROOFSTEP]
rw [isCompactElement_iff_le_of_directed_sSup_le] at h
[GOAL]
case a.intro.intro
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
h : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → f p ≤ sSup s → ∃ x, x ∈ s ∧ f p ≤ x
⊢ ∃ y, y ∈ d ∧ f p ≤ y
[PROOFSTEP]
specialize h d hemp hdir (le_trans (Finset.le_sup hps) hsup)
[GOAL]
case a.intro.intro
ι : Sort u_1
α✝ : Type u_2
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
h : ∃ x, x ∈ d ∧ f p ≤ x
⊢ ∃ y, y ∈ d ∧ f p ≤ y
[PROOFSTEP]
simpa only [exists_prop]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = Finset.sup t id
[PROOFSTEP]
let S := {x | ∃ t : Finset α, ↑t ⊆ s ∧ t.sup id = x}
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = Finset.sup t id
[PROOFSTEP]
obtain ⟨m, ⟨t, ⟨ht₁, rfl⟩⟩, hm⟩ := h.has_min S ⟨⊥, ∅, by simp⟩
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
⊢ ↑∅ ⊆ s ∧ Finset.sup ∅ id = ⊥
[PROOFSTEP]
simp
[GOAL]
case intro.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ (x : α), x ∈ S → ¬x > Finset.sup t id
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = Finset.sup t id
[PROOFSTEP]
refine' ⟨t, ht₁, (sSup_le _ _ fun y hy => _).antisymm _⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ (x : α), x ∈ S → ¬x > Finset.sup t id
y : α
hy : y ∈ s
⊢ y ≤ Finset.sup t id
[PROOFSTEP]
classical
rw [eq_of_le_of_not_lt (Finset.sup_mono (t.subset_insert y))
    (hm _ ⟨insert y t, by simp [Set.insert_subset_iff, hy, ht₁]⟩)]
simp
[GOAL]
case intro.intro.intro.intro.refine'_1
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ (x : α), x ∈ S → ¬x > Finset.sup t id
y : α
hy : y ∈ s
⊢ y ≤ Finset.sup t id
[PROOFSTEP]
rw [eq_of_le_of_not_lt (Finset.sup_mono (t.subset_insert y))
    (hm _ ⟨insert y t, by simp [Set.insert_subset_iff, hy, ht₁]⟩)]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ (x : α), x ∈ S → ¬x > Finset.sup t id
y : α
hy : y ∈ s
⊢ ↑(insert y t) ⊆ s ∧ Finset.sup (insert y t) id = Finset.sup (insert y t) id
[PROOFSTEP]
simp [Set.insert_subset_iff, hy, ht₁]
[GOAL]
case intro.intro.intro.intro.refine'_1
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ (x : α), x ∈ S → ¬x > Finset.sup t id
y : α
hy : y ∈ s
⊢ y ≤ Finset.sup (insert y t) id
[PROOFSTEP]
simp
[GOAL]
case intro.intro.intro.intro.refine'_2
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ (x : α), x ∈ S → ¬x > Finset.sup t id
⊢ Finset.sup t id ≤ sSup s
[PROOFSTEP]
rw [Finset.sup_id_eq_sSup]
[GOAL]
case intro.intro.intro.intro.refine'_2
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ (x : α), x ∈ S → ¬x > Finset.sup t id
⊢ sSup ↑t ≤ sSup s
[PROOFSTEP]
exact sSup_le_sSup ht₁
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupFiniteCompact α
⊢ IsSupClosedCompact α
[PROOFSTEP]
intro s hne hsc
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupFiniteCompact α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
⊢ sSup s ∈ s
[PROOFSTEP]
obtain ⟨t, ht₁, ht₂⟩ := h s
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupFiniteCompact α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
⊢ sSup s ∈ s
[PROOFSTEP]
clear h
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
⊢ sSup s ∈ s
[PROOFSTEP]
cases' t.eq_empty_or_nonempty with h h
[GOAL]
case intro.intro.inl
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
h : t = ∅
⊢ sSup s ∈ s
[PROOFSTEP]
subst h
[GOAL]
case intro.intro.inl
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = Finset.sup ∅ id
⊢ sSup s ∈ s
[PROOFSTEP]
rw [Finset.sup_empty] at ht₂
[GOAL]
case intro.intro.inl
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ⊥
⊢ sSup s ∈ s
[PROOFSTEP]
rw [ht₂]
[GOAL]
case intro.intro.inl
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ⊥
⊢ ⊥ ∈ s
[PROOFSTEP]
simp [eq_singleton_bot_of_sSup_eq_bot_of_nonempty ht₂ hne]
[GOAL]
case intro.intro.inr
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
h : Finset.Nonempty t
⊢ sSup s ∈ s
[PROOFSTEP]
rw [ht₂]
[GOAL]
case intro.intro.inr
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
h : Finset.Nonempty t
⊢ Finset.sup t id ∈ s
[PROOFSTEP]
exact t.sup_closed_of_sup_closed h ht₁ hsc
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
⊢ WellFounded fun x x_1 => x > x_1
[PROOFSTEP]
refine' RelEmbedding.wellFounded_iff_no_descending_seq.mpr ⟨fun a => _⟩
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ False
[PROOFSTEP]
suffices sSup (Set.range a) ∈ Set.range a
  by
  obtain ⟨n, hn⟩ := Set.mem_range.mp this
  have h' : sSup (Set.range a) < a (n + 1) := by
    change _ > _
    simp [← hn, a.map_rel_iff]
  apply lt_irrefl (a (n + 1))
  apply lt_of_le_of_lt _ h'
  apply le_sSup
  apply Set.mem_range_self
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
⊢ False
[PROOFSTEP]
obtain ⟨n, hn⟩ := Set.mem_range.mp this
[GOAL]
case intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
⊢ False
[PROOFSTEP]
have h' : sSup (Set.range a) < a (n + 1) := by
  change _ > _
  simp [← hn, a.map_rel_iff]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
⊢ sSup (Set.range ↑a) < ↑a (n + 1)
[PROOFSTEP]
change _ > _
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
⊢ ↑a (n + 1) > sSup (Set.range ↑a)
[PROOFSTEP]
simp [← hn, a.map_rel_iff]
[GOAL]
case intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
h' : sSup (Set.range ↑a) < ↑a (n + 1)
⊢ False
[PROOFSTEP]
apply lt_irrefl (a (n + 1))
[GOAL]
case intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
h' : sSup (Set.range ↑a) < ↑a (n + 1)
⊢ ↑a (n + 1) < ↑a (n + 1)
[PROOFSTEP]
apply lt_of_le_of_lt _ h'
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
h' : sSup (Set.range ↑a) < ↑a (n + 1)
⊢ ↑a (n + 1) ≤ sSup (Set.range ↑a)
[PROOFSTEP]
apply le_sSup
[GOAL]
case a
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
this : sSup (Set.range ↑a) ∈ Set.range ↑a
n : ℕ
hn : ↑a n = sSup (Set.range ↑a)
h' : sSup (Set.range ↑a) < ↑a (n + 1)
⊢ ↑a (n + 1) ∈ Set.range ↑a
[PROOFSTEP]
apply Set.mem_range_self
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ sSup (Set.range ↑a) ∈ Set.range ↑a
[PROOFSTEP]
apply h (Set.range a)
[GOAL]
case x
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ Set.Nonempty (Set.range ↑a)
[PROOFSTEP]
use a 37
[GOAL]
case h
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ ↑a 37 ∈ Set.range ↑a
[PROOFSTEP]
apply Set.mem_range_self
[GOAL]
case a
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
⊢ ∀ (a_1 : α), a_1 ∈ Set.range ↑a → ∀ (b : α), b ∈ Set.range ↑a → a_1 ⊔ b ∈ Set.range ↑a
[PROOFSTEP]
rintro x ⟨m, hm⟩ y ⟨n, hn⟩
[GOAL]
case a.intro.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
x : α
m : ℕ
hm : ↑a m = x
y : α
n : ℕ
hn : ↑a n = y
⊢ x ⊔ y ∈ Set.range ↑a
[PROOFSTEP]
use m ⊔ n
[GOAL]
case h
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
x : α
m : ℕ
hm : ↑a m = x
y : α
n : ℕ
hn : ↑a n = y
⊢ ↑a (m ⊔ n) = x ⊔ y
[PROOFSTEP]
rw [← hm, ← hn]
[GOAL]
case h
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupClosedCompact α
a : (fun x x_1 => x > x_1) ↪r fun x x_1 => x > x_1
x : α
m : ℕ
hm : ↑a m = x
y : α
n : ℕ
hn : ↑a n = y
⊢ ↑a (m ⊔ n) = ↑a m ⊔ ↑a n
[PROOFSTEP]
apply RelHomClass.map_sup a
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
⊢ IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k
[PROOFSTEP]
refine' ⟨fun h k s hs => _, fun h s => _⟩
[GOAL]
case refine'_1
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
[PROOFSTEP]
obtain ⟨t, ⟨hts, htsup⟩⟩ := h s
[GOAL]
case refine'_1.intro.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s = Finset.sup t id
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
[PROOFSTEP]
use t, hts
[GOAL]
case right
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s = Finset.sup t id
⊢ k ≤ Finset.sup t id
[PROOFSTEP]
rwa [← htsup]
[GOAL]
case refine'_2
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = Finset.sup t id
[PROOFSTEP]
obtain ⟨t, ⟨hts, htsup⟩⟩ := h (sSup s) s (by rfl)
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
⊢ sSup s ≤ sSup s
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.intro.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = Finset.sup t id
[PROOFSTEP]
have : sSup s = t.sup id := by
  suffices t.sup id ≤ sSup s by apply le_antisymm <;> assumption
  simp only [id.def, Finset.sup_le_iff]
  intro x hx
  exact le_sSup _ _ (hts hx)
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
⊢ sSup s = Finset.sup t id
[PROOFSTEP]
suffices t.sup id ≤ sSup s by apply le_antisymm <;> assumption
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
this : Finset.sup t id ≤ sSup s
⊢ sSup s = Finset.sup t id
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
this : Finset.sup t id ≤ sSup s
⊢ sSup s ≤ Finset.sup t id
[PROOFSTEP]
assumption
[GOAL]
case a
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
this : Finset.sup t id ≤ sSup s
⊢ Finset.sup t id ≤ sSup s
[PROOFSTEP]
assumption
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
⊢ Finset.sup t id ≤ sSup s
[PROOFSTEP]
simp only [id.def, Finset.sup_le_iff]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
⊢ ∀ (b : α), b ∈ t → b ≤ sSup s
[PROOFSTEP]
intro x hx
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
x : α
hx : x ∈ t
⊢ x ≤ sSup s
[PROOFSTEP]
exact le_sSup _ _ (hts hx)
[GOAL]
case refine'_2.intro.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
this : sSup s = Finset.sup t id
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = Finset.sup t id
[PROOFSTEP]
exact ⟨t, hts, this⟩
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
⊢ TFAE [WellFounded fun x x_1 => x > x_1, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k]
[PROOFSTEP]
tfae_have 1 → 2
[GOAL]
case tfae_1_to_2
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
⊢ (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
[PROOFSTEP]
exact WellFounded.isSupFiniteCompact α
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
⊢ TFAE [WellFounded fun x x_1 => x > x_1, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k]
[PROOFSTEP]
tfae_have 2 → 3
[GOAL]
case tfae_2_to_3
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
⊢ IsSupFiniteCompact α → IsSupClosedCompact α
[PROOFSTEP]
exact IsSupFiniteCompact.isSupClosedCompact α
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
⊢ TFAE [WellFounded fun x x_1 => x > x_1, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k]
[PROOFSTEP]
tfae_have 3 → 1
[GOAL]
case tfae_3_to_1
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
⊢ IsSupClosedCompact α → WellFounded fun x x_1 => x > x_1
[PROOFSTEP]
exact IsSupClosedCompact.wellFounded α
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
tfae_3_to_1 : IsSupClosedCompact α → WellFounded fun x x_1 => x > x_1
⊢ TFAE [WellFounded fun x x_1 => x > x_1, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k]
[PROOFSTEP]
tfae_have 2 ↔ 4
[GOAL]
case tfae_2_iff_4
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
tfae_3_to_1 : IsSupClosedCompact α → WellFounded fun x x_1 => x > x_1
⊢ IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k
[PROOFSTEP]
exact isSupFiniteCompact_iff_all_elements_compact α
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
tfae_1_to_2 : (WellFounded fun x x_1 => x > x_1) → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
tfae_3_to_1 : IsSupClosedCompact α → WellFounded fun x x_1 => x > x_1
tfae_2_iff_4 : IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k
⊢ TFAE [WellFounded fun x x_1 => x > x_1, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k]
[PROOFSTEP]
tfae_finish
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
⊢ Set.Finite s
[PROOFSTEP]
classical
refine' Set.not_infinite.mp fun contra => _
obtain ⟨t, ht₁, ht₂⟩ := WellFounded.isSupFiniteCompact α h s
replace contra : ∃ x : α, x ∈ s ∧ x ≠ ⊥ ∧ x ∉ t
· have : (s \ (insert ⊥ t : Finset α)).Infinite := contra.diff (Finset.finite_toSet _)
  obtain ⟨x, hx₁, hx₂⟩ := this.nonempty
  exact ⟨x, hx₁, by simpa [not_or] using hx₂⟩
obtain ⟨x, hx₀, hx₁, hx₂⟩ := contra
replace hs : x ⊓ sSup s = ⊥
· have := hs.mono (by simp [ht₁, hx₀, -Set.union_singleton] : ↑t ∪ { x } ≤ s) (by simp : x ∈ _)
  simpa [Disjoint, hx₂, ← t.sup_id_eq_sSup, ← ht₂] using this.eq_bot
apply hx₁
rw [← hs, eq_comm, inf_eq_left]
exact le_sSup _ _ hx₀
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
⊢ Set.Finite s
[PROOFSTEP]
refine' Set.not_infinite.mp fun contra => _
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
contra : Set.Infinite s
⊢ False
[PROOFSTEP]
obtain ⟨t, ht₁, ht₂⟩ := WellFounded.isSupFiniteCompact α h s
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
contra : Set.Infinite s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
⊢ False
[PROOFSTEP]
replace contra : ∃ x : α, x ∈ s ∧ x ≠ ⊥ ∧ x ∉ t
[GOAL]
case contra
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
contra : Set.Infinite s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
⊢ ∃ x, x ∈ s ∧ x ≠ ⊥ ∧ ¬x ∈ t
[PROOFSTEP]
have : (s \ (insert ⊥ t : Finset α)).Infinite := contra.diff (Finset.finite_toSet _)
[GOAL]
case contra
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
contra : Set.Infinite s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
this : Set.Infinite (s \ ↑(insert ⊥ t))
⊢ ∃ x, x ∈ s ∧ x ≠ ⊥ ∧ ¬x ∈ t
[PROOFSTEP]
obtain ⟨x, hx₁, hx₂⟩ := this.nonempty
[GOAL]
case contra.intro.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
contra : Set.Infinite s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
this : Set.Infinite (s \ ↑(insert ⊥ t))
x : α
hx₁ : x ∈ s
hx₂ : ¬x ∈ ↑(insert ⊥ t)
⊢ ∃ x, x ∈ s ∧ x ≠ ⊥ ∧ ¬x ∈ t
[PROOFSTEP]
exact ⟨x, hx₁, by simpa [not_or] using hx₂⟩
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
contra : Set.Infinite s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
this : Set.Infinite (s \ ↑(insert ⊥ t))
x : α
hx₁ : x ∈ s
hx₂ : ¬x ∈ ↑(insert ⊥ t)
⊢ x ≠ ⊥ ∧ ¬x ∈ t
[PROOFSTEP]
simpa [not_or] using hx₂
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
contra : ∃ x, x ∈ s ∧ x ≠ ⊥ ∧ ¬x ∈ t
⊢ False
[PROOFSTEP]
obtain ⟨x, hx₀, hx₁, hx₂⟩ := contra
[GOAL]
case intro.intro.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
⊢ False
[PROOFSTEP]
replace hs : x ⊓ sSup s = ⊥
[GOAL]
case hs
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
⊢ x ⊓ sSup s = ⊥
[PROOFSTEP]
have := hs.mono (by simp [ht₁, hx₀, -Set.union_singleton] : ↑t ∪ { x } ≤ s) (by simp : x ∈ _)
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
⊢ ↑t ∪ {x} ≤ s
[PROOFSTEP]
simp [ht₁, hx₀, -Set.union_singleton]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
⊢ x ∈ ↑t ∪ {x}
[PROOFSTEP]
simp
[GOAL]
case hs
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
this : Disjoint x (sSup ((↑t ∪ {x}) \ {x}))
⊢ x ⊓ sSup s = ⊥
[PROOFSTEP]
simpa [Disjoint, hx₂, ← t.sup_id_eq_sSup, ← ht₂] using this.eq_bot
[GOAL]
case intro.intro.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
hs : x ⊓ sSup s = ⊥
⊢ False
[PROOFSTEP]
apply hx₁
[GOAL]
case intro.intro.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
hs : x ⊓ sSup s = ⊥
⊢ x = ⊥
[PROOFSTEP]
rw [← hs, eq_comm, inf_eq_left]
[GOAL]
case intro.intro.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
hs : x ⊓ sSup s = ⊥
⊢ x ≤ sSup s
[PROOFSTEP]
exact le_sSup _ _ hx₀
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b✝ : α
s : Set α
b : α
⊢ sSup {c | CompleteLattice.IsCompactElement c ∧ c ≤ b} = b
[PROOFSTEP]
rcases IsCompactlyGenerated.exists_sSup_eq b with ⟨s, hs, rfl⟩
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ s : Set α
hs : ∀ (x : α), x ∈ s → CompleteLattice.IsCompactElement x
⊢ sSup {c | CompleteLattice.IsCompactElement c ∧ c ≤ sSup s} = sSup s
[PROOFSTEP]
exact le_antisymm (sSup_le fun c hc => hc.2) (sSup_le_sSup fun c cs => ⟨hs c cs, le_sSup cs⟩)
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
⊢ sSup {a | CompleteLattice.IsCompactElement a} = ⊤
[PROOFSTEP]
refine' Eq.trans (congr rfl (Set.ext fun x => _)) (sSup_compact_le_eq ⊤)
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
x : α
⊢ x ∈ {a | CompleteLattice.IsCompactElement a} ↔ x ∈ {c | CompleteLattice.IsCompactElement c ∧ c ≤ ⊤}
[PROOFSTEP]
exact (and_iff_left le_top).symm
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a✝ b✝ : α
s : Set α
a b : α
h : ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a → c ≤ b
⊢ a ≤ b
[PROOFSTEP]
rw [← sSup_compact_le_eq a, ← sSup_compact_le_eq b]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a✝ b✝ : α
s : Set α
a b : α
h : ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a → c ≤ b
⊢ sSup {c | CompleteLattice.IsCompactElement c ∧ c ≤ a} ≤ sSup {c | CompleteLattice.IsCompactElement c ∧ c ≤ b}
[PROOFSTEP]
exact sSup_le_sSup fun c hc => ⟨hc.1, h c hc.1 hc.2⟩
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : DirectedOn (fun x x_1 => x ≤ x_1) s
⊢ a ⊓ sSup s ≤ ⨆ (b : α) (_ : b ∈ s), a ⊓ b
[PROOFSTEP]
rw [le_iff_compact_le_imp]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : DirectedOn (fun x x_1 => x ≤ x_1) s
⊢ ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ (b : α) (_ : b ∈ s), a ⊓ b
[PROOFSTEP]
by_cases hs : s.Nonempty
[GOAL]
case pos
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : DirectedOn (fun x x_1 => x ≤ x_1) s
hs : Set.Nonempty s
⊢ ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ (b : α) (_ : b ∈ s), a ⊓ b
[PROOFSTEP]
intro c hc hcinf
[GOAL]
case pos
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : DirectedOn (fun x x_1 => x ≤ x_1) s
hs : Set.Nonempty s
c : α
hc : CompleteLattice.IsCompactElement c
hcinf : c ≤ a ⊓ sSup s
⊢ c ≤ ⨆ (b : α) (_ : b ∈ s), a ⊓ b
[PROOFSTEP]
rw [le_inf_iff] at hcinf
[GOAL]
case pos
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : DirectedOn (fun x x_1 => x ≤ x_1) s
hs : Set.Nonempty s
c : α
hc : CompleteLattice.IsCompactElement c
hcinf : c ≤ a ∧ c ≤ sSup s
⊢ c ≤ ⨆ (b : α) (_ : b ∈ s), a ⊓ b
[PROOFSTEP]
rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le] at hc
[GOAL]
case pos
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : DirectedOn (fun x x_1 => x ≤ x_1) s
hs : Set.Nonempty s
c : α
hc : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → c ≤ sSup s → ∃ x, x ∈ s ∧ c ≤ x
hcinf : c ≤ a ∧ c ≤ sSup s
⊢ c ≤ ⨆ (b : α) (_ : b ∈ s), a ⊓ b
[PROOFSTEP]
rcases hc s hs h hcinf.2 with ⟨d, ds, cd⟩
[GOAL]
case pos.intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : DirectedOn (fun x x_1 => x ≤ x_1) s
hs : Set.Nonempty s
c : α
hc : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → c ≤ sSup s → ∃ x, x ∈ s ∧ c ≤ x
hcinf : c ≤ a ∧ c ≤ sSup s
d : α
ds : d ∈ s
cd : c ≤ d
⊢ c ≤ ⨆ (b : α) (_ : b ∈ s), a ⊓ b
[PROOFSTEP]
refine' (le_inf hcinf.1 cd).trans (le_trans _ (le_iSup₂ d ds))
[GOAL]
case pos.intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : DirectedOn (fun x x_1 => x ≤ x_1) s
hs : Set.Nonempty s
c : α
hc : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → c ≤ sSup s → ∃ x, x ∈ s ∧ c ≤ x
hcinf : c ≤ a ∧ c ≤ sSup s
d : α
ds : d ∈ s
cd : c ≤ d
⊢ a ⊓ d ≤ a ⊓ d
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : DirectedOn (fun x x_1 => x ≤ x_1) s
hs : ¬Set.Nonempty s
⊢ ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ (b : α) (_ : b ∈ s), a ⊓ b
[PROOFSTEP]
rw [Set.not_nonempty_iff_eq_empty] at hs
[GOAL]
case neg
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : DirectedOn (fun x x_1 => x ≤ x_1) s
hs : s = ∅
⊢ ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ (b : α) (_ : b ∈ s), a ⊓ b
[PROOFSTEP]
simp [hs]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : DirectedOn (fun x x_1 => x ≤ x_1) s
⊢ sSup s ⊓ a = ⨆ (b : α) (_ : b ∈ s), b ⊓ a
[PROOFSTEP]
simp_rw [@inf_comm _ _ _ a, h.inf_sSup_eq]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : Directed (fun x x_1 => x ≤ x_1) f
⊢ a ⊓ ⨆ (i : ι), f i = ⨆ (i : ι), a ⊓ f i
[PROOFSTEP]
rw [iSup, h.directedOn_range.inf_sSup_eq, iSup_range]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : Directed (fun x x_1 => x ≤ x_1) f
⊢ (⨆ (i : ι), f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
[PROOFSTEP]
rw [iSup, h.directedOn_range.sSup_inf_eq, iSup_range]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : DirectedOn (fun x x_1 => x ≤ x_1) s
⊢ Disjoint a (sSup s) ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint a b
[PROOFSTEP]
simp_rw [disjoint_iff, h.inf_sSup_eq, iSup_eq_bot]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : DirectedOn (fun x x_1 => x ≤ x_1) s
⊢ Disjoint (sSup s) a ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint b a
[PROOFSTEP]
simp_rw [disjoint_iff, h.sSup_inf_eq, iSup_eq_bot]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : Directed (fun x x_1 => x ≤ x_1) f
⊢ Disjoint a (⨆ (i : ι), f i) ↔ ∀ (i : ι), Disjoint a (f i)
[PROOFSTEP]
simp_rw [disjoint_iff, h.inf_iSup_eq, iSup_eq_bot]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : Directed (fun x x_1 => x ≤ x_1) f
⊢ Disjoint (⨆ (i : ι), f i) a ↔ ∀ (i : ι), Disjoint (f i) a
[PROOFSTEP]
simp_rw [disjoint_iff, h.iSup_inf_eq, iSup_eq_bot]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
⊢ a ⊓ sSup s ≤ ⨆ (t : Finset α) (_ : ↑t ⊆ s), a ⊓ Finset.sup t id
[PROOFSTEP]
rw [le_iff_compact_le_imp]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
⊢ ∀ (c : α),
    CompleteLattice.IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ (t : Finset α) (_ : ↑t ⊆ s), a ⊓ Finset.sup t id
[PROOFSTEP]
intro c hc hcinf
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
c : α
hc : CompleteLattice.IsCompactElement c
hcinf : c ≤ a ⊓ sSup s
⊢ c ≤ ⨆ (t : Finset α) (_ : ↑t ⊆ s), a ⊓ Finset.sup t id
[PROOFSTEP]
rw [le_inf_iff] at hcinf
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
c : α
hc : CompleteLattice.IsCompactElement c
hcinf : c ≤ a ∧ c ≤ sSup s
⊢ c ≤ ⨆ (t : Finset α) (_ : ↑t ⊆ s), a ⊓ Finset.sup t id
[PROOFSTEP]
rcases hc s hcinf.2 with ⟨t, ht1, ht2⟩
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
c : α
hc : CompleteLattice.IsCompactElement c
hcinf : c ≤ a ∧ c ≤ sSup s
t : Finset α
ht1 : ↑t ⊆ s
ht2 : c ≤ Finset.sup t id
⊢ c ≤ ⨆ (t : Finset α) (_ : ↑t ⊆ s), a ⊓ Finset.sup t id
[PROOFSTEP]
refine' (le_inf hcinf.1 ht2).trans (le_trans _ (le_iSup₂ t ht1))
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
c : α
hc : CompleteLattice.IsCompactElement c
hcinf : c ≤ a ∧ c ≤ sSup s
t : Finset α
ht1 : ↑t ⊆ s
ht2 : c ≤ Finset.sup t id
⊢ a ⊓ Finset.sup t id ≤ a ⊓ Finset.sup t id
[PROOFSTEP]
rfl
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a✝ b : α
s✝ s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → SetIndependent ↑t
a : α
ha : a ∈ s
⊢ Disjoint a (sSup (s \ {a}))
[PROOFSTEP]
rw [disjoint_iff, inf_sSup_eq_iSup_inf_sup_finset, iSup_eq_bot]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a✝ b : α
s✝ s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → SetIndependent ↑t
a : α
ha : a ∈ s
⊢ ∀ (i : Finset α), ⨆ (_ : ↑i ⊆ s \ {a}), a ⊓ Finset.sup i id = ⊥
[PROOFSTEP]
intro t
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a✝ b : α
s✝ s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → SetIndependent ↑t
a : α
ha : a ∈ s
t : Finset α
⊢ ⨆ (_ : ↑t ⊆ s \ {a}), a ⊓ Finset.sup t id = ⊥
[PROOFSTEP]
rw [iSup_eq_bot, Finset.sup_id_eq_sSup]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a✝ b : α
s✝ s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → SetIndependent ↑t
a : α
ha : a ∈ s
t : Finset α
⊢ ↑t ⊆ s \ {a} → a ⊓ sSup ↑t = ⊥
[PROOFSTEP]
intro ht
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a✝ b : α
s✝ s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → SetIndependent ↑t
a : α
ha : a ∈ s
t : Finset α
ht : ↑t ⊆ s \ {a}
⊢ a ⊓ sSup ↑t = ⊥
[PROOFSTEP]
classical
have h' := (h (insert a t) ?_ (t.mem_insert_self a)).eq_bot
· rwa [Finset.coe_insert, Set.insert_diff_self_of_not_mem] at h'
  exact fun con => ((Set.mem_diff a).1 (ht con)).2 (Set.mem_singleton a)
· rw [Finset.coe_insert, Set.insert_subset_iff]
  exact ⟨ha, Set.Subset.trans ht (Set.diff_subset _ _)⟩
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a✝ b : α
s✝ s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → SetIndependent ↑t
a : α
ha : a ∈ s
t : Finset α
ht : ↑t ⊆ s \ {a}
⊢ a ⊓ sSup ↑t = ⊥
[PROOFSTEP]
have h' := (h (insert a t) ?_ (t.mem_insert_self a)).eq_bot
[GOAL]
case refine_2
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a✝ b : α
s✝ s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → SetIndependent ↑t
a : α
ha : a ∈ s
t : Finset α
ht : ↑t ⊆ s \ {a}
h' : a ⊓ sSup (↑(insert a t) \ {a}) = ⊥
⊢ a ⊓ sSup ↑t = ⊥
[PROOFSTEP]
rwa [Finset.coe_insert, Set.insert_diff_self_of_not_mem] at h'
[GOAL]
case refine_2
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a✝ b : α
s✝ s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → SetIndependent ↑t
a : α
ha : a ∈ s
t : Finset α
ht : ↑t ⊆ s \ {a}
h' : a ⊓ sSup (insert a ↑t \ {a}) = ⊥
⊢ ¬a ∈ ↑t
[PROOFSTEP]
exact fun con => ((Set.mem_diff a).1 (ht con)).2 (Set.mem_singleton a)
[GOAL]
case refine_1
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a✝ b : α
s✝ s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → SetIndependent ↑t
a : α
ha : a ∈ s
t : Finset α
ht : ↑t ⊆ s \ {a}
⊢ ↑(insert a t) ⊆ s
[PROOFSTEP]
rw [Finset.coe_insert, Set.insert_subset_iff]
[GOAL]
case refine_1
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a✝ b : α
s✝ s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → SetIndependent ↑t
a : α
ha : a ∈ s
t : Finset α
ht : ↑t ⊆ s \ {a}
⊢ a ∈ s ∧ ↑t ⊆ s
[PROOFSTEP]
exact ⟨ha, Set.Subset.trans ht (Set.diff_subset _ _)⟩
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_3
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
⊢ SetIndependent (⋃ (i : η), s i)
[PROOFSTEP]
by_cases hη : Nonempty η
[GOAL]
case pos
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_3
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : Nonempty η
⊢ SetIndependent (⋃ (i : η), s i)
[PROOFSTEP]
rw [CompleteLattice.setIndependent_iff_finite]
[GOAL]
case pos
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_3
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : Nonempty η
⊢ ∀ (t : Finset α), ↑t ⊆ ⋃ (i : η), s i → SetIndependent ↑t
[PROOFSTEP]
intro t ht
[GOAL]
case pos
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_3
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : Nonempty η
t : Finset α
ht : ↑t ⊆ ⋃ (i : η), s i
⊢ SetIndependent ↑t
[PROOFSTEP]
obtain ⟨I, fi, hI⟩ := Set.finite_subset_iUnion t.finite_toSet ht
[GOAL]
case pos.intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_3
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : Nonempty η
t : Finset α
ht : ↑t ⊆ ⋃ (i : η), s i
I : Set η
fi : Set.Finite I
hI : ↑t ⊆ ⋃ (i : η) (_ : i ∈ I), s i
⊢ SetIndependent ↑t
[PROOFSTEP]
obtain ⟨i, hi⟩ := hs.finset_le fi.toFinset
[GOAL]
case pos.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_3
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : Nonempty η
t : Finset α
ht : ↑t ⊆ ⋃ (i : η), s i
I : Set η
fi : Set.Finite I
hI : ↑t ⊆ ⋃ (i : η) (_ : i ∈ I), s i
i : η
hi : ∀ (i_1 : η), i_1 ∈ Set.Finite.toFinset fi → s i_1 ⊆ s i
⊢ SetIndependent ↑t
[PROOFSTEP]
exact (h i).mono (Set.Subset.trans hI <| Set.iUnion₂_subset fun j hj => hi j (fi.mem_toFinset.2 hj))
[GOAL]
case neg
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
η : Type u_3
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : ¬Nonempty η
⊢ SetIndependent (⋃ (i : η), s i)
[PROOFSTEP]
rintro a ⟨_, ⟨i, _⟩, _⟩
[GOAL]
case neg.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a✝ b : α
s✝ : Set α
η : Type u_3
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : ¬Nonempty η
a : α
w✝ : Set α
right✝ : a ∈ w✝
i : η
h✝ : (fun i => s i) i = w✝
⊢ Disjoint a (sSup ((⋃ (i : η), s i) \ {a}))
[PROOFSTEP]
exfalso
[GOAL]
case neg.intro.intro.intro.h
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a✝ b : α
s✝ : Set α
η : Type u_3
s : η → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (i : η), SetIndependent (s i)
hη : ¬Nonempty η
a : α
w✝ : Set α
right✝ : a ∈ w✝
i : η
h✝ : (fun i => s i) i = w✝
⊢ False
[PROOFSTEP]
exact hη ⟨i⟩
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
s : Set (Set α)
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set α), a ∈ s → SetIndependent a
⊢ SetIndependent (⋃₀ s)
[PROOFSTEP]
rw [Set.sUnion_eq_iUnion]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
s : Set (Set α)
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set α), a ∈ s → SetIndependent a
⊢ SetIndependent (⋃ (i : ↑s), ↑i)
[PROOFSTEP]
exact CompleteLattice.setIndependent_iUnion_of_directed hs.directed_val (by simpa using h)
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s✝ : Set α
s : Set (Set α)
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ (a : Set α), a ∈ s → SetIndependent a
⊢ ∀ (i : ↑s), SetIndependent ↑i
[PROOFSTEP]
simpa using h
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
⊢ IsCompactlyGenerated α
[PROOFSTEP]
rw [wellFounded_iff_isSupFiniteCompact, isSupFiniteCompact_iff_all_elements_compact] at h
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
⊢ IsCompactlyGenerated α
[PROOFSTEP]
exact ⟨fun x => ⟨{ x }, ⟨fun x _ => h x, sSup_singleton⟩⟩⟩
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
⊢ IsCoatomic ↑(Set.Iic k)
[PROOFSTEP]
constructor
[GOAL]
case eq_top_or_exists_le_coatom
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
⊢ ∀ (b : ↑(Set.Iic k)), b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a
[PROOFSTEP]
rintro ⟨b, hbk⟩
[GOAL]
case eq_top_or_exists_le_coatom.mk
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
⊢ { val := b, property := hbk } = ⊤ ∨ ∃ a, IsCoatom a ∧ { val := b, property := hbk } ≤ a
[PROOFSTEP]
obtain rfl | H := eq_or_ne b k
[GOAL]
case eq_top_or_exists_le_coatom.mk.inl
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
b : α
h : IsCompactElement b
hbk : b ∈ Set.Iic b
⊢ { val := b, property := hbk } = ⊤ ∨ ∃ a, IsCoatom a ∧ { val := b, property := hbk } ≤ a
[PROOFSTEP]
left
[GOAL]
case eq_top_or_exists_le_coatom.mk.inl.h
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
b : α
h : IsCompactElement b
hbk : b ∈ Set.Iic b
⊢ { val := b, property := hbk } = ⊤
[PROOFSTEP]
ext
[GOAL]
case eq_top_or_exists_le_coatom.mk.inl.h.a
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
b : α
h : IsCompactElement b
hbk : b ∈ Set.Iic b
⊢ ↑{ val := b, property := hbk } = ↑⊤
[PROOFSTEP]
simp only [Set.Iic.coe_top, Subtype.coe_mk]
[GOAL]
case eq_top_or_exists_le_coatom.mk.inr
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
⊢ { val := b, property := hbk } = ⊤ ∨ ∃ a, IsCoatom a ∧ { val := b, property := hbk } ≤ a
[PROOFSTEP]
right
[GOAL]
case eq_top_or_exists_le_coatom.mk.inr.h
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
⊢ ∃ a, IsCoatom a ∧ { val := b, property := hbk } ≤ a
[PROOFSTEP]
have ⟨a, a₀, ba, h⟩ := zorn_nonempty_partialOrder₀ (Set.Iio k) ?_ b (lt_of_le_of_ne hbk H)
[GOAL]
case eq_top_or_exists_le_coatom.mk.inr.h.refine_2
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
a : α
a₀ : a ∈ Set.Iio k
ba : b ≤ a
h : ∀ (z : α), z ∈ Set.Iio k → a ≤ z → z = a
⊢ ∃ a, IsCoatom a ∧ { val := b, property := hbk } ≤ a
[PROOFSTEP]
refine' ⟨⟨a, le_of_lt a₀⟩, ⟨ne_of_lt a₀, fun c hck => by_contradiction fun c₀ => _⟩, ba⟩
[GOAL]
case eq_top_or_exists_le_coatom.mk.inr.h.refine_2
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
a : α
a₀ : a ∈ Set.Iio k
ba : b ≤ a
h : ∀ (z : α), z ∈ Set.Iio k → a ≤ z → z = a
c : ↑(Set.Iic k)
hck : { val := a, property := (_ : a ≤ k) } < c
c₀ : ¬c = ⊤
⊢ False
[PROOFSTEP]
cases h c.1 (lt_of_le_of_ne c.2 fun con => c₀ (Subtype.ext con)) hck.le
[GOAL]
case eq_top_or_exists_le_coatom.mk.inr.h.refine_2.refl
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
c : ↑(Set.Iic k)
c₀ : ¬c = ⊤
a₀ : ↑c ∈ Set.Iio k
ba : b ≤ ↑c
h : ∀ (z : α), z ∈ Set.Iio k → ↑c ≤ z → z = ↑c
hck : { val := ↑c, property := (_ : ↑c ≤ k) } < c
⊢ False
[PROOFSTEP]
exact lt_irrefl _ hck
[GOAL]
case eq_top_or_exists_le_coatom.mk.inr.h.refine_1
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
⊢ ∀ (c : Set α),
    c ⊆ Set.Iio k →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : α), y ∈ c → ∃ ub, ub ∈ Set.Iio k ∧ ∀ (z : α), z ∈ c → z ≤ ub
[PROOFSTEP]
intro S SC cC I _
[GOAL]
case eq_top_or_exists_le_coatom.mk.inr.h.refine_1
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Set.Iio k
cC : IsChain (fun x x_1 => x ≤ x_1) S
I : α
a✝ : I ∈ S
⊢ ∃ ub, ub ∈ Set.Iio k ∧ ∀ (z : α), z ∈ S → z ≤ ub
[PROOFSTEP]
by_cases hS : S.Nonempty
[GOAL]
case pos
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Set.Iio k
cC : IsChain (fun x x_1 => x ≤ x_1) S
I : α
a✝ : I ∈ S
hS : Set.Nonempty S
⊢ ∃ ub, ub ∈ Set.Iio k ∧ ∀ (z : α), z ∈ S → z ≤ ub
[PROOFSTEP]
refine' ⟨sSup S, h.directed_sSup_lt_of_lt hS cC.directedOn SC, _⟩
[GOAL]
case pos
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Set.Iio k
cC : IsChain (fun x x_1 => x ≤ x_1) S
I : α
a✝ : I ∈ S
hS : Set.Nonempty S
⊢ ∀ (z : α), z ∈ S → z ≤ sSup S
[PROOFSTEP]
intro
[GOAL]
case pos
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Set.Iio k
cC : IsChain (fun x x_1 => x ≤ x_1) S
I : α
a✝ : I ∈ S
hS : Set.Nonempty S
z✝ : α
⊢ z✝ ∈ S → z✝ ≤ sSup S
[PROOFSTEP]
apply le_sSup
[GOAL]
case neg
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Set.Iio k
cC : IsChain (fun x x_1 => x ≤ x_1) S
I : α
a✝ : I ∈ S
hS : ¬Set.Nonempty S
⊢ ∃ ub, ub ∈ Set.Iio k ∧ ∀ (z : α), z ∈ S → z ≤ ub
[PROOFSTEP]
exact
  ⟨b, lt_of_le_of_ne hbk H, by
    simp only [Set.not_nonempty_iff_eq_empty.mp hS, Set.mem_empty_iff_false, forall_const, forall_prop_of_false,
      not_false_iff]⟩
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Set.Iio k
cC : IsChain (fun x x_1 => x ≤ x_1) S
I : α
a✝ : I ∈ S
hS : ¬Set.Nonempty S
⊢ ∀ (z : α), z ∈ S → z ≤ b
[PROOFSTEP]
simp only [Set.not_nonempty_iff_eq_empty.mp hS, Set.mem_empty_iff_false, forall_const, forall_prop_of_false,
  not_false_iff]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b
[PROOFSTEP]
by_cases h : {c : α | CompleteLattice.IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
[GOAL]
case pos
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : {c | CompleteLattice.IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b
[PROOFSTEP]
left
[GOAL]
case pos.h
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : {c | CompleteLattice.IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
⊢ b = ⊥
[PROOFSTEP]
rw [← sSup_compact_le_eq b, sSup_eq_bot]
[GOAL]
case pos.h
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : {c | CompleteLattice.IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
⊢ ∀ (a : α), a ∈ {c | CompleteLattice.IsCompactElement c ∧ c ≤ b} → a = ⊥
[PROOFSTEP]
exact h
[GOAL]
case neg
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | CompleteLattice.IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b
[PROOFSTEP]
rcases Set.not_subset.1 h with ⟨c, ⟨hc, hcb⟩, hcbot⟩
[GOAL]
case neg.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | CompleteLattice.IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : ¬c ∈ {⊥}
hc : CompleteLattice.IsCompactElement c
hcb : c ≤ b
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b
[PROOFSTEP]
right
[GOAL]
case neg.intro.intro.intro.h
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | CompleteLattice.IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : ¬c ∈ {⊥}
hc : CompleteLattice.IsCompactElement c
hcb : c ≤ b
⊢ ∃ a, IsAtom a ∧ a ≤ b
[PROOFSTEP]
have hc' := CompleteLattice.Iic_coatomic_of_compact_element hc
[GOAL]
case neg.intro.intro.intro.h
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | CompleteLattice.IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : ¬c ∈ {⊥}
hc : CompleteLattice.IsCompactElement c
hcb : c ≤ b
hc' : IsCoatomic ↑(Set.Iic c)
⊢ ∃ a, IsAtom a ∧ a ≤ b
[PROOFSTEP]
rw [← isAtomic_iff_isCoatomic] at hc'
[GOAL]
case neg.intro.intro.intro.h
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | CompleteLattice.IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : ¬c ∈ {⊥}
hc : CompleteLattice.IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic ↑(Set.Iic c)
⊢ ∃ a, IsAtom a ∧ a ≤ b
[PROOFSTEP]
haveI := hc'
[GOAL]
case neg.intro.intro.intro.h
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | CompleteLattice.IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : ¬c ∈ {⊥}
hc : CompleteLattice.IsCompactElement c
hcb : c ≤ b
hc' this : IsAtomic ↑(Set.Iic c)
⊢ ∃ a, IsAtom a ∧ a ≤ b
[PROOFSTEP]
obtain con | ⟨a, ha, hac⟩ := eq_bot_or_exists_atom_le (⟨c, le_refl c⟩ : Set.Iic c)
[GOAL]
case neg.intro.intro.intro.h.inl
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | CompleteLattice.IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : ¬c ∈ {⊥}
hc : CompleteLattice.IsCompactElement c
hcb : c ≤ b
hc' this : IsAtomic ↑(Set.Iic c)
con : { val := c, property := (_ : c ≤ c) } = ⊥
⊢ ∃ a, IsAtom a ∧ a ≤ b
[PROOFSTEP]
exfalso
[GOAL]
case neg.intro.intro.intro.h.inl.h
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | CompleteLattice.IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : ¬c ∈ {⊥}
hc : CompleteLattice.IsCompactElement c
hcb : c ≤ b
hc' this : IsAtomic ↑(Set.Iic c)
con : { val := c, property := (_ : c ≤ c) } = ⊥
⊢ False
[PROOFSTEP]
apply hcbot
[GOAL]
case neg.intro.intro.intro.h.inl.h
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | CompleteLattice.IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : ¬c ∈ {⊥}
hc : CompleteLattice.IsCompactElement c
hcb : c ≤ b
hc' this : IsAtomic ↑(Set.Iic c)
con : { val := c, property := (_ : c ≤ c) } = ⊥
⊢ c ∈ {⊥}
[PROOFSTEP]
simp only [Subtype.ext_iff, Set.Iic.coe_bot, Subtype.coe_mk] at con
[GOAL]
case neg.intro.intro.intro.h.inl.h
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | CompleteLattice.IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : ¬c ∈ {⊥}
hc : CompleteLattice.IsCompactElement c
hcb : c ≤ b
hc' this : IsAtomic ↑(Set.Iic c)
con : c = ⊥
⊢ c ∈ {⊥}
[PROOFSTEP]
exact con
[GOAL]
case neg.intro.intro.intro.h.inr.intro.intro
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | CompleteLattice.IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : ¬c ∈ {⊥}
hc : CompleteLattice.IsCompactElement c
hcb : c ≤ b
hc' this : IsAtomic ↑(Set.Iic c)
a : { x // x ∈ Set.Iic c }
ha : IsAtom a
hac : a ≤ { val := c, property := (_ : c ≤ c) }
⊢ ∃ a, IsAtom a ∧ a ≤ b
[PROOFSTEP]
rw [← Subtype.coe_le_coe, Subtype.coe_mk] at hac
[GOAL]
case neg.intro.intro.intro.h.inr.intro.intro
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | CompleteLattice.IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : ¬c ∈ {⊥}
hc : CompleteLattice.IsCompactElement c
hcb : c ≤ b
hc' this : IsAtomic ↑(Set.Iic c)
a : { x // x ∈ Set.Iic c }
ha : IsAtom a
hac : ↑a ≤ ↑{ val := c, property := (_ : c ≤ c) }
⊢ ∃ a, IsAtom a ∧ a ≤ b
[PROOFSTEP]
exact ⟨a, ha.of_isAtom_coe_Iic, hac.trans hcb⟩
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
⊢ b = sSup {a | IsAtom a ∧ a ≤ b}
[PROOFSTEP]
symm
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
⊢ sSup {a | IsAtom a ∧ a ≤ b} = b
[PROOFSTEP]
have hle : sSup {a : α | IsAtom a ∧ a ≤ b} ≤ b := sSup_le fun _ => And.right
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
⊢ sSup {a | IsAtom a ∧ a ≤ b} = b
[PROOFSTEP]
apply (lt_or_eq_of_le hle).resolve_left _
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
⊢ ¬sSup {a | IsAtom a ∧ a ≤ b} < b
[PROOFSTEP]
intro con
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a | IsAtom a ∧ a ≤ b} < b
⊢ False
[PROOFSTEP]
obtain ⟨c, hc⟩ := exists_isCompl (⟨sSup {a : α | IsAtom a ∧ a ≤ b}, hle⟩ : Set.Iic b)
[GOAL]
case intro
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a | IsAtom a ∧ a ≤ b} < b
c : { x // x ∈ Set.Iic b }
hc : IsCompl { val := sSup {a | IsAtom a ∧ a ≤ b}, property := hle } c
⊢ False
[PROOFSTEP]
obtain rfl | ⟨a, ha, hac⟩ := eq_bot_or_exists_atom_le c
[GOAL]
case intro.inl
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a | IsAtom a ∧ a ≤ b} < b
hc : IsCompl { val := sSup {a | IsAtom a ∧ a ≤ b}, property := hle } ⊥
⊢ False
[PROOFSTEP]
exact ne_of_lt con (Subtype.ext_iff.1 (eq_top_of_isCompl_bot hc))
[GOAL]
case intro.inr.intro.intro
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a | IsAtom a ∧ a ≤ b} < b
c : { x // x ∈ Set.Iic b }
hc : IsCompl { val := sSup {a | IsAtom a ∧ a ≤ b}, property := hle } c
a : { x // x ∈ Set.Iic b }
ha : IsAtom a
hac : a ≤ c
⊢ False
[PROOFSTEP]
apply ha.1
[GOAL]
case intro.inr.intro.intro
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a | IsAtom a ∧ a ≤ b} < b
c : { x // x ∈ Set.Iic b }
hc : IsCompl { val := sSup {a | IsAtom a ∧ a ≤ b}, property := hle } c
a : { x // x ∈ Set.Iic b }
ha : IsAtom a
hac : a ≤ c
⊢ a = ⊥
[PROOFSTEP]
rw [eq_bot_iff]
[GOAL]
case intro.inr.intro.intro
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a | IsAtom a ∧ a ≤ b} < b
c : { x // x ∈ Set.Iic b }
hc : IsCompl { val := sSup {a | IsAtom a ∧ a ≤ b}, property := hle } c
a : { x // x ∈ Set.Iic b }
ha : IsAtom a
hac : a ≤ c
⊢ a ≤ ⊥
[PROOFSTEP]
apply le_trans (le_inf _ hac) hc.disjoint.le_bot
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a | IsAtom a ∧ a ≤ b} < b
c : { x // x ∈ Set.Iic b }
hc : IsCompl { val := sSup {a | IsAtom a ∧ a ≤ b}, property := hle } c
a : { x // x ∈ Set.Iic b }
ha : IsAtom a
hac : a ≤ c
⊢ a ≤ { val := sSup {a | IsAtom a ∧ a ≤ b}, property := hle }
[PROOFSTEP]
rw [← Subtype.coe_le_coe, Subtype.coe_mk]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
hle : sSup {a | IsAtom a ∧ a ≤ b} ≤ b
con : sSup {a | IsAtom a ∧ a ≤ b} < b
c : { x // x ∈ Set.Iic b }
hc : IsCompl { val := sSup {a | IsAtom a ∧ a ≤ b}, property := hle } c
a : { x // x ∈ Set.Iic b }
ha : IsAtom a
hac : a ≤ c
⊢ ↑a ≤ ↑{ val := sSup {a | IsAtom a ∧ a ≤ b}, property := hle }
[PROOFSTEP]
exact le_sSup ⟨ha.of_isAtom_coe_Iic, a.2⟩
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
⊢ ∃ s, CompleteLattice.SetIndependent s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
[PROOFSTEP]
have :=
  zorn_subset {s : Set α | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a} fun c hc1 hc2 =>
    ⟨⋃₀ c,
      ⟨CompleteLattice.independent_sUnion_of_directed hc2.directedOn fun s hs => (hc1 hs).1, ?_, fun a ⟨s, sc, as⟩ =>
        (hc1 sc).2.2 a as⟩,
      fun _ => Set.subset_sUnion_of_mem⟩
[GOAL]
case refine_2
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
this :
  ∃ m,
    m ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} ∧
      ∀ (a : Set α),
        a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → m ⊆ a → a = m
⊢ ∃ s, CompleteLattice.SetIndependent s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
case refine_1
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ Disjoint b (sSup (⋃₀ c))
[PROOFSTEP]
obtain ⟨s, ⟨s_ind, b_inf_Sup_s, s_atoms⟩, s_max⟩ := this
[GOAL]
case refine_2.intro.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
⊢ ∃ s, CompleteLattice.SetIndependent s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
case refine_1
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ Disjoint b (sSup (⋃₀ c))
[PROOFSTEP]
swap
[GOAL]
case refine_1
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ Disjoint b (sSup (⋃₀ c))
[PROOFSTEP]
rw [sSup_sUnion, ← sSup_image, DirectedOn.disjoint_sSup_right]
[GOAL]
case refine_1
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ ∀ ⦃b_1 : α⦄, b_1 ∈ (fun t => sSup t) '' c → Disjoint b b_1
[PROOFSTEP]
rintro _ ⟨s, hs, rfl⟩
[GOAL]
case refine_1.intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
s : Set α
hs : s ∈ c
⊢ Disjoint b ((fun t => sSup t) s)
[PROOFSTEP]
exact (hc1 hs).2.1
[GOAL]
case refine_1
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ DirectedOn (fun x x_1 => x ≤ x_1) ((fun t => sSup t) '' c)
[PROOFSTEP]
rw [directedOn_image]
[GOAL]
case refine_1
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
c : Set (Set α)
hc1 : c ⊆ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a}
hc2 : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ DirectedOn ((fun t => sSup t) ⁻¹'o fun x x_1 => x ≤ x_1) c
[PROOFSTEP]
exact hc2.directedOn.mono @fun s t => sSup_le_sSup
[GOAL]
case refine_2.intro.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
⊢ ∃ s, CompleteLattice.SetIndependent s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
[PROOFSTEP]
refine' ⟨s, s_ind, ⟨b_inf_Sup_s, _⟩, s_atoms⟩
[GOAL]
case refine_2.intro.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
⊢ Codisjoint b (sSup s)
[PROOFSTEP]
rw [codisjoint_iff_le_sup, ← h, sSup_le_iff]
[GOAL]
case refine_2.intro.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
⊢ ∀ (b_1 : α), b_1 ∈ {a | IsAtom a} → b_1 ≤ b ⊔ sSup s
[PROOFSTEP]
intro a ha
[GOAL]
case refine_2.intro.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
⊢ a ≤ b ⊔ sSup s
[PROOFSTEP]
rw [← inf_eq_left]
[GOAL]
case refine_2.intro.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
⊢ a ⊓ (b ⊔ sSup s) = a
[PROOFSTEP]
refine' (ha.le_iff.mp inf_le_left).resolve_left fun con => ha.1 _
[GOAL]
case refine_2.intro.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : a ⊓ (b ⊔ sSup s) = ⊥
⊢ a = ⊥
[PROOFSTEP]
rw [← con, eq_comm, inf_eq_left]
[GOAL]
case refine_2.intro.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : a ⊓ (b ⊔ sSup s) = ⊥
⊢ a ≤ b ⊔ sSup s
[PROOFSTEP]
refine' (le_sSup _).trans le_sup_right
[GOAL]
case refine_2.intro.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : a ⊓ (b ⊔ sSup s) = ⊥
⊢ a ∈ s
[PROOFSTEP]
rw [← disjoint_iff] at con
[GOAL]
case refine_2.intro.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
⊢ a ∈ s
[PROOFSTEP]
have a_dis_Sup_s : Disjoint a (sSup s) := con.mono_right le_sup_right
[GOAL]
case refine_2.intro.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ a ∈ s
[PROOFSTEP]
rw [← s_max (s ∪ { a }) ⟨fun x hx => _, _, fun x hx => _⟩ (Set.subset_union_left _ _)]
[GOAL]
case refine_2.intro.intro.intro.intro
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ a ∈ s ∪ {a}
[PROOFSTEP]
exact Set.mem_union_right _ (Set.mem_singleton _)
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ ∀ (x : α), x ∈ s ∪ {a} → Disjoint x (sSup ((s ∪ {a}) \ {x}))
[PROOFSTEP]
intro x hx
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∪ {a}
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))
[PROOFSTEP]
rw [Set.mem_union, Set.mem_singleton_iff] at hx
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))
[PROOFSTEP]
obtain rfl | xa := eq_or_ne x a
[GOAL]
case inl
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
x : α
ha : x ∈ {a | IsAtom a}
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
hx : x ∈ s ∨ x = x
⊢ Disjoint x (sSup ((s ∪ {x}) \ {x}))
[PROOFSTEP]
simp only [Set.mem_singleton, Set.insert_diff_of_mem, Set.union_singleton]
[GOAL]
case inl
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
x : α
ha : x ∈ {a | IsAtom a}
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
hx : x ∈ s ∨ x = x
⊢ Disjoint x (sSup (s \ {x}))
[PROOFSTEP]
exact con.mono_right ((sSup_le_sSup <| Set.diff_subset _ _).trans le_sup_right)
[GOAL]
case inr
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))
[PROOFSTEP]
have h : (s ∪ { a }) \ { x } = s \ { x } ∪ { a } :=
  by
  simp only [Set.union_singleton]
  rw [Set.insert_diff_of_not_mem]
  rw [Set.mem_singleton_iff]
  exact Ne.symm xa
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
⊢ (s ∪ {a}) \ {x} = s \ {x} ∪ {a}
[PROOFSTEP]
simp only [Set.union_singleton]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
⊢ insert a s \ {x} = insert a (s \ {x})
[PROOFSTEP]
rw [Set.insert_diff_of_not_mem]
[GOAL]
case h
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
⊢ ¬a ∈ {x}
[PROOFSTEP]
rw [Set.mem_singleton_iff]
[GOAL]
case h
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
⊢ ¬a = x
[PROOFSTEP]
exact Ne.symm xa
[GOAL]
case inr
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h✝ : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a}
⊢ Disjoint x (sSup ((s ∪ {a}) \ {x}))
[PROOFSTEP]
rw [h, sSup_union, sSup_singleton]
[GOAL]
case inr
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h✝ : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a}
⊢ Disjoint x (sSup (s \ {x}) ⊔ a)
[PROOFSTEP]
apply (s_ind (hx.resolve_right xa)).disjoint_sup_right_of_disjoint_sup_left (a_dis_Sup_s.mono_right _).symm
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h✝ : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a}
⊢ x ⊔ sSup (s \ {x}) ≤ sSup s
[PROOFSTEP]
rw [← sSup_insert, Set.insert_diff_singleton, Set.insert_eq_of_mem (hx.resolve_right xa)]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ Disjoint b (sSup (s ∪ {a}))
[PROOFSTEP]
rw [sSup_union, sSup_singleton]
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ Disjoint b (sSup s ⊔ a)
[PROOFSTEP]
exact b_inf_Sup_s.disjoint_sup_right_of_disjoint_sup_left con.symm
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ ∀ (x : α), x ∈ s ∪ {a} → IsAtom x
[PROOFSTEP]
intro x hx
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∪ {a}
⊢ IsAtom x
[PROOFSTEP]
rw [Set.mem_union, Set.mem_singleton_iff] at hx
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
⊢ IsAtom x
[PROOFSTEP]
obtain hx | rfl := hx
[GOAL]
case inl
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
a : α
ha : a ∈ {a | IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s
⊢ IsAtom x
[PROOFSTEP]
exact s_atoms x hx
[GOAL]
case inr
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
s : Set α
s_max :
  ∀ (a : Set α),
    a ∈ {s | CompleteLattice.SetIndependent s ∧ Disjoint b (sSup s) ∧ ∀ (a : α), a ∈ s → IsAtom a} → s ⊆ a → a = s
s_ind : CompleteLattice.SetIndependent s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ (a : α), a ∈ s → IsAtom a
x : α
ha : x ∈ {a | IsAtom a}
con : Disjoint x (b ⊔ sSup s)
a_dis_Sup_s : Disjoint x (sSup s)
⊢ IsAtom x
[PROOFSTEP]
exact ha
[GOAL]
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
⊢ ComplementedLattice α ↔ IsAtomistic α
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
⊢ ComplementedLattice α → IsAtomistic α
[PROOFSTEP]
intros
[GOAL]
case mpr
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
⊢ IsAtomistic α → ComplementedLattice α
[PROOFSTEP]
intros
[GOAL]
case mp
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
a✝ : ComplementedLattice α
⊢ IsAtomistic α
[PROOFSTEP]
exact isAtomistic_of_complementedLattice
[GOAL]
case mpr
ι : Sort u_1
α : Type u_2
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
a✝ : IsAtomistic α
⊢ ComplementedLattice α
[PROOFSTEP]
exact complementedLattice_of_isAtomistic