-- Mathlib/Dynamics/OmegaLimit.lean
theorem nonempty_omegaLimit_of_isCompact_absorbing [NeBot f] {c : Set β} (hc₁ : IsCompact c)
    (hc₂ : ∃ v ∈ f, closure (image2 ϕ v s) ⊆ c) (hs : s.Nonempty) : (ω f ϕ s).Nonempty

Proof state:
case intro.intro.htn
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u : ↑f.sets
hn : (image2 ϕ (↑u ∩ v) s).Nonempty
⊢ (closure (image2 ϕ (↑u ∩ v) s)).Nonempty

Tactic:
exact hn.mono subset_closure

Result:
no goals

Proof state:
case h
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x1 x2 => x1 ⊇ x2) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) ⟨u₁, hu₁⟩)
      ((fun i => closure (image2 ϕ (↑i ∩ v) s)) ⟨u₁ ∩ u₂, ⋯⟩) ∧
    (fun x1 x2 => x1 ⊇ x2) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) ⟨u₂, hu₂⟩)
      ((fun i => closure (image2 ϕ (↑i ∩ v) s)) ⟨u₁ ∩ u₂, ⋯⟩)

Tactic:
constructor

Result:
case h.left
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x1 x2 => x1 ⊇ x2) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) ⟨u₁, hu₁⟩)
    ((fun i => closure (image2 ϕ (↑i ∩ v) s)) ⟨u₁ ∩ u₂, ⋯⟩)

case h.right
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x1 x2 => x1 ⊇ x2) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) ⟨u₂, hu₂⟩)
    ((fun i => closure (image2 ϕ (↑i ∩ v) s)) ⟨u₁ ∩ u₂, ⋯⟩)

Proof state:
case intro.intro.htn
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), (closure (image2 ϕ (↑i ∩ v) s)).Nonempty

Tactic:
intro u

Result:
case intro.intro.htn
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u : ↑f.sets
⊢ (closure (image2 ϕ (↑u ∩ v) s)).Nonempty

Proof state:
case intro.intro.htc
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsCompact (closure (image2 ϕ (↑i ∩ v) s))

Tactic:
intro

Result:
case intro.intro.htc
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
i✝ : ↑f.sets
⊢ IsCompact (closure (image2 ϕ (↑i✝ ∩ v) s))

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ ↑⟨u₁ ∩ u₂, ⋯⟩ ⊆ ↑⟨u₂, hu₂⟩

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.htc
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
i✝ : ↑f.sets
⊢ IsCompact (closure (image2 ϕ (↑i✝ ∩ v) s))

Tactic:
apply hc₁.of_isClosed_subset isClosed_closure

Result:
case intro.intro.htc
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
i✝ : ↑f.sets
⊢ closure (image2 ϕ (↑i✝ ∩ v) s) ⊆ c

Proof state:
case intro.intro.htd.mk.mk
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ ∃ z,
    (fun x1 x2 => x1 ⊇ x2) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) ⟨u₁, hu₁⟩)
        ((fun i => closure (image2 ϕ (↑i ∩ v) s)) z) ∧
      (fun x1 x2 => x1 ⊇ x2) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) ⟨u₂, hu₂⟩)
        ((fun i => closure (image2 ϕ (↑i ∩ v) s)) z)

Tactic:
use ⟨u₁ ∩ u₂, inter_mem hu₁ hu₂⟩

Result:
case h
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x1 x2 => x1 ⊇ x2) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) ⟨u₁, hu₁⟩)
      ((fun i => closure (image2 ϕ (↑i ∩ v) s)) ⟨u₁ ∩ u₂, ⋯⟩) ∧
    (fun x1 x2 => x1 ⊇ x2) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) ⟨u₂, hu₂⟩)
      ((fun i => closure (image2 ϕ (↑i ∩ v) s)) ⟨u₁ ∩ u₂, ⋯⟩)

Proof state:
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ (⋂ u, closure (image2 ϕ (↑u ∩ v) s)).Nonempty

Tactic:
apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed

Result:
case intro.intro.htd
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ Directed (fun x1 x2 => x1 ⊇ x2) fun i => closure (image2 ϕ (↑i ∩ v) s)

case intro.intro.htn
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), (closure (image2 ϕ (↑i ∩ v) s)).Nonempty

case intro.intro.htc
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsCompact (closure (image2 ϕ (↑i ∩ v) s))

case intro.intro.htcl
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsClosed (closure (image2 ϕ (↑i ∩ v) s))

Proof state:
case intro.intro.htn
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u : ↑f.sets
⊢ (closure (image2 ϕ (↑u ∩ v) s)).Nonempty

Tactic:
have hn : (image2 ϕ (u ∩ v) s).Nonempty :=
  Nonempty.image2 (Filter.nonempty_of_mem (inter_mem u.prop hv₁)) hs

Result:
case intro.intro.htn
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u : ↑f.sets
hn : (image2 ϕ (↑u ∩ v) s).Nonempty
⊢ (closure (image2 ϕ (↑u ∩ v) s)).Nonempty