ι : Sort ?u.103797
α : Type u_1
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
ι : Sort ?u.103797
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
⊢ a ⊓ sSup s ≤ ⨆ (t : Finset α) (_ : ↑t ⊆ s), a ⊓ Finset.sup t id
rw [le_iff_compact_le_imp]
ι : Sort ?u.103797
α : Type u_1
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
ι : Sort ?u.103797
α : Type u_1
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
intro c hc hcinf
ι : Sort ?u.103797
α : Type u_1
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
ι : Sort ?u.103797
α : Type u_1
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
rw [le_inf_iff] at hcinf
case intro.intro
ι : Sort ?u.103797
α : Type u_1
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
ι : Sort ?u.103797
α : Type u_1
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
rcases hc s hcinf.2 with ⟨t, ht1, ht2⟩
case intro.intro
ι : Sort ?u.103797
α : Type u_1
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
case intro.intro
ι : Sort ?u.103797
α : Type u_1
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
refine' (le_inf hcinf.1 ht2).trans (le_trans _ (le_iSup₂ t ht1))
no goals
case intro.intro
ι : Sort ?u.103797
α : Type u_1
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
rfl