-- 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.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))

Tactic:
exact fun _ ↦ isClosed_closure

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
⊢ closure (image2 ϕ (↑i✝ ∩ v) s) ⊆ c

Tactic:
calc
  _ ⊆ closure (image2 ϕ v s) := closure_mono (image2_subset inter_subset_right Subset.rfl)
  _ ⊆ c := hv₂

Result:
no goals

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
⊢ (ω f ϕ s).Nonempty

Tactic:
rw [omegaLimit_eq_iInter_inter _ _ _ hv₁]

Result:
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

Proof state:
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)

Tactic:
rintro ⟨u₁, hu₁⟩ ⟨u₂, hu₂⟩

Result:
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)

Proof state:
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₂, ⋯⟩)

Tactic:
exact closure_mono (image2_subset (inter_subset_inter_left _ (by simp)) Subset.rfl)

Result:
no goals

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
hc₂ : ∃ v ∈ f, closure (image2 ϕ v s) ⊆ c
hs : s.Nonempty
⊢ (ω f ϕ s).Nonempty

Tactic:
rcases hc₂ with ⟨v, hv₁, hv₂⟩

Result:
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
⊢ (ω f ϕ s).Nonempty

Proof state:
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₂, ⋯⟩)

Tactic:
all_goals exact closure_mono (image2_subset (inter_subset_inter_left _ (by simp)) Subset.rfl)

Result:
no goals