-- Mathlib/Dynamics/OmegaLimit.lean
theorem mapsTo_omegaLimit' {α' β' : Type*} [TopologicalSpace β'] {f : Filter τ} {ϕ : τ → α → β}
    {ϕ' : τ → α' → β'} {ga : α → α'} {s' : Set α'} (hs : MapsTo ga s s') {gb : β → β'}
    (hg : ∀ᶠ t in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s) (hgc : Continuous gb) :
    MapsTo gb (ω f ϕ s) (ω f ϕ' s')

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
s : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous gb
y : β
hy : ∀ i ∈ f, y ∈ closure (image2 ϕ i s)
u : Set τ
hu : u ∈ f
t : τ
ht : t ∈ u ∩ {x | (fun t => EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s) x}
x : α
hx : x ∈ s
⊢ gb (ϕ t x) ∈ image2 ϕ' u s'

Tactic:
calc
  ϕ' t (ga x) ∈ image2 ϕ' u s' := mem_image2_of_mem ht.1 (hs hx)
  _ = gb (ϕ t x) := ht.2 hx |>.symm

Result:
no goals

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
s : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous gb
⊢ MapsTo gb (ω f ϕ s) (ω f ϕ' s')

Tactic:
simp only [omegaLimit_def, mem_iInter, MapsTo]

Result:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
s : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous gb
⊢ ∀ ⦃x : β⦄, (∀ i ∈ f, x ∈ closure (image2 ϕ i s)) → ∀ i ∈ f, gb x ∈ closure (image2 ϕ' i s')

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
s : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous gb
⊢ ∀ ⦃x : β⦄, (∀ i ∈ f, x ∈ closure (image2 ϕ i s)) → ∀ i ∈ f, gb x ∈ closure (image2 ϕ' i s')

Tactic:
intro y hy u hu

Result:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
s : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous gb
y : β
hy : ∀ i ∈ f, y ∈ closure (image2 ϕ i s)
u : Set τ
hu : u ∈ f
⊢ gb y ∈ closure (image2 ϕ' u s')

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
s : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous gb
y : β
hy : ∀ i ∈ f, y ∈ closure (image2 ϕ i s)
u : Set τ
hu : u ∈ f
⊢ gb y ∈ closure (image2 ϕ' u s')

Tactic:
refine map_mem_closure hgc (hy _ (inter_mem hu hg)) (forall_mem_image2.2 fun t ht x hx ↦ ?_)

Result:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
s : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous gb
y : β
hy : ∀ i ∈ f, y ∈ closure (image2 ϕ i s)
u : Set τ
hu : u ∈ f
t : τ
ht : t ∈ u ∩ {x | (fun t => EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s) x}
x : α
hx : x ∈ s
⊢ gb (ϕ t x) ∈ image2 ϕ' u s'