-- Mathlib/Topology/Sets/Opens.lean
theorem isCompactElement_iff (s : Opens α) :
    CompleteLattice.IsCompactElement s ↔ IsCompact (s : Set α)

Proof state:
case refine_1.intro
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ i, U i
t : Finset ι
ht : s ≤ t.sup fun i => { carrier := U i, is_open' := ⋯ }
⊢ ∃ t, ↑s ⊆ ⋃ i ∈ t, U i

Tactic:
refine ⟨t, Set.Subset.trans ht ?_⟩

Result:
case refine_1.intro
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ i, U i
t : Finset ι
ht : s ≤ t.sup fun i => { carrier := U i, is_open' := ⋯ }
⊢ ↑(t.sup fun i => { carrier := U i, is_open' := ⋯ }) ⊆ ⋃ i ∈ t, U i

Proof state:
case refine_2.intro
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ i ∈ t, ↑(U i)
⊢ ∀ i ∈ t, ↑(U i) ⊆ ↑(t.sup U)

Tactic:
show ∀ i ∈ t, U i ≤ t.sup U

Result:
case refine_2.intro
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ i ∈ t, ↑(U i)
⊢ ∀ i ∈ t, U i ≤ t.sup U

Proof state:
case refine_2.intro
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ i ∈ t, ↑(U i)
⊢ ∃ t, s ≤ t.sup U

Tactic:
refine ⟨t, Set.Subset.trans ht ?_⟩

Result:
case refine_2.intro
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ i ∈ t, ↑(U i)
⊢ ⋃ i ∈ t, ↑(U i) ⊆ ↑(t.sup U)

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ i, U i
⊢ s ≤ ⨆ i, { carrier := U i, is_open' := ⋯ }

Tactic:
simpa

Result:
no goals

Proof state:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
⊢ (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1) →
    ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i

Tactic:
introv H hU hU'

Result:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ i, U i
⊢ ∃ t, ↑s ⊆ ⋃ i ∈ t, U i

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
⊢ ↑s ⊆ ⋃ i, (fun i => ↑(U i)) i

Tactic:
simpa using show (s : Set α) ⊆ ↑(iSup U) from hU

Result:
no goals

Proof state:
case refine_2.intro
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ i ∈ t, ↑(U i)
⊢ ⋃ i ∈ t, ↑(U i) ⊆ ↑(t.sup U)

Tactic:
simp only [Set.iUnion_subset_iff]

Result:
case refine_2.intro
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ i ∈ t, ↑(U i)
⊢ ∀ i ∈ t, ↑(U i) ⊆ ↑(t.sup U)

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
⊢ CompleteLattice.IsCompactElement s ↔ IsCompact ↑s

Tactic:
rw [isCompact_iff_finite_subcover, CompleteLattice.isCompactElement_iff]

Result:
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
⊢ (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1) ↔
    ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i

Proof state:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ i, U i
⊢ ∃ t, ↑s ⊆ ⋃ i ∈ t, U i

Tactic:
obtain ⟨t, ht⟩ := H ι (fun i => ⟨U i, hU i⟩) (by simpa)

Result:
case refine_1.intro
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ i, U i
t : Finset ι
ht : s ≤ t.sup fun i => { carrier := U i, is_open' := ⋯ }
⊢ ∃ t, ↑s ⊆ ⋃ i ∈ t, U i

Proof state:
case refine_2.intro
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ i ∈ t, ↑(U i)
⊢ ∀ i ∈ t, U i ≤ t.sup U

Tactic:
exact fun i => Finset.le_sup

Result:
no goals

Proof state:
case refine_1.intro
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ i, U i
t : Finset ι
ht : s ≤ t.sup fun i => { carrier := U i, is_open' := ⋯ }
⊢ ↑(t.sup fun i => { carrier := U i, is_open' := ⋯ }) ⊆ ⋃ i ∈ t, U i

Tactic:
rw [coe_finset_sup, Finset.sup_eq_iSup]

Result:
case refine_1.intro
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ i, U i
t : Finset ι
ht : s ≤ t.sup fun i => { carrier := U i, is_open' := ⋯ }
⊢ ⨆ a ∈ t, (SetLike.coe ∘ fun i => { carrier := U i, is_open' := ⋯ }) a ⊆ ⋃ i ∈ t, U i

Proof state:
case refine_1.intro
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen (U i)
hU' : ↑s ⊆ ⋃ i, U i
t : Finset ι
ht : s ≤ t.sup fun i => { carrier := U i, is_open' := ⋯ }
⊢ ⨆ a ∈ t, (SetLike.coe ∘ fun i => { carrier := U i, is_open' := ⋯ }) a ⊆ ⋃ i ∈ t, U i

Tactic:
rfl

Result:
no goals

Proof state:
case refine_2
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
⊢ ∃ t, s ≤ t.sup U

Tactic:
obtain ⟨t, ht⟩ :=
  H (fun i => U i) (fun i => (U i).isOpen) (by simpa using show (s : Set α) ⊆ ↑(iSup U) from hU)

Result:
case refine_2.intro
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i
ι : Type u_2
U : ι → Opens α
hU : s ≤ iSup U
t : Finset ι
ht : ↑s ⊆ ⋃ i ∈ t, ↑(U i)
⊢ ∃ t, s ≤ t.sup U