-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem inf_sSup_eq_iSup_inf_sup_finset :
    a ⊓ sSup s = ⨆ (t : Finset α) (_ : ↑t ⊆ s), a ⊓ t.sup id :=
  le_antisymm
    (by
      rw [le_iff_compact_le_imp]
      intro c hc hcinf
      rw [le_inf_iff] at hcinf
      rcases hc s hcinf.2 with ⟨t, ht1, ht2⟩
      refine (le_inf hcinf.1 ht2).trans (le_trans ?_ (le_iSup₂ t ht1))
      rfl)
    (iSup_le fun t =>
      iSup_le fun h => inf_le_inf_left _ ((Finset.sup_id_eq_sSup t).symm ▸ sSup_le_sSup h))

Proof state:
case intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : CompleteLattice.IsCompactElement c
hcinf : c ≤ a ∧ c ≤ sSup s
t : Finset α
ht1 : ↑t ⊆ s
ht2 : c ≤ t.sup id
⊢ a ⊓ t.sup id ≤ a ⊓ t.sup id

Tactic:
rfl

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : CompleteLattice.IsCompactElement c
hcinf : c ≤ a ∧ c ≤ sSup s
t : Finset α
ht1 : ↑t ⊆ s
ht2 : c ≤ t.sup id
⊢ c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id

Tactic:
refine (le_inf hcinf.1 ht2).trans (le_trans ?_ (le_iSup₂ t ht1))

Result:
case intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : CompleteLattice.IsCompactElement c
hcinf : c ≤ a ∧ c ≤ sSup s
t : Finset α
ht1 : ↑t ⊆ s
ht2 : c ≤ t.sup id
⊢ a ⊓ t.sup id ≤ a ⊓ t.sup id

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
⊢ a ⊓ sSup s ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id

Tactic:
rw [le_iff_compact_le_imp]

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
⊢ ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : CompleteLattice.IsCompactElement c
hcinf : c ≤ a ⊓ sSup s
⊢ c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id

Tactic:
rw [le_inf_iff] at hcinf

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : CompleteLattice.IsCompactElement c
hcinf : c ≤ a ∧ c ≤ sSup s
⊢ c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : CompleteLattice.IsCompactElement c
hcinf : c ≤ a ∧ c ≤ sSup s
⊢ c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id

Tactic:
rcases hc s hcinf.2 with ⟨t, ht1, ht2⟩

Result:
case intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : CompleteLattice.IsCompactElement c
hcinf : c ≤ a ∧ c ≤ sSup s
t : Finset α
ht1 : ↑t ⊆ s
ht2 : c ≤ t.sup id
⊢ c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
⊢ ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id

Tactic:
intro c hc hcinf

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
c : α
hc : CompleteLattice.IsCompactElement c
hcinf : c ≤ a ⊓ sSup s
⊢ c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id