-- Mathlib/Topology/UniformSpace/CompactConvergence.lean
theorem tendsto_iff_forall_isCompact_tendstoUniformlyOn
    {ι : Type u₃} {p : Filter ι} {F : ι → C(α, β)} {f} :
    Tendsto F p (𝓝 f) ↔ ∀ K, IsCompact K → TendstoUniformlyOn (fun i a => F i a) f p K

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → ∀ (U : Set β), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
a✝ : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen V
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed W
hWU : W ⊆ V
s : Set α := K ∩ ⇑f ⁻¹' ball (f x) W
hnhds : s ∈ 𝓝[K] x
hcomp : IsCompact s
hmaps : MapsTo (⇑f) s (ball (f x) V)
⊢ ∃ t ∈ 𝓝[K] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a => (F i) a) n y) ∈ U

Tactic:
use s, hnhds

Result:
case right
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → ∀ (U : Set β), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
a✝ : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen V
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed W
hWU : W ⊆ V
s : Set α := K ∩ ⇑f ⁻¹' ball (f x) W
hnhds : s ∈ 𝓝[K] x
hcomp : IsCompact s
hmaps : MapsTo (⇑f) s (ball (f x) V)
⊢ ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, (fun i a => (F i) a) n y) ∈ U

Proof state:
case mpr.intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen U
hf : MapsTo (⇑f) K U
V : Set (β × β)
hV : V ∈ 𝓤 β
hVf : ∀ x ∈ ⇑f '' K, ball x V ⊆ U
⊢ ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U

Tactic:
filter_upwards [h K hK V hV] with g hg x hx using hVf _ (mem_image_of_mem f hx) (hg x hx)

Result:
no goals

Proof state:
case right
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → ∀ (U : Set β), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
a✝ : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen V
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed W
hWU : W ⊆ V
s : Set α := K ∩ ⇑f ⁻¹' ball (f x) W
hnhds : s ∈ 𝓝[K] x
hcomp : IsCompact s
hmaps : MapsTo (⇑f) s (ball (f x) V)
⊢ ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, (fun i a => (F i) a) n y) ∈ U

Tactic:
refine (h s hcomp _ (isOpen_ball _ hVo) hmaps).mono fun g hg y hy ↦ ?_

Result:
case right
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → ∀ (U : Set β), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
a✝ : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen V
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed W
hWU : W ⊆ V
s : Set α := K ∩ ⇑f ⁻¹' ball (f x) W
hnhds : s ∈ 𝓝[K] x
hcomp : IsCompact s
hmaps : MapsTo (⇑f) s (ball (f x) V)
g : ι
hg : MapsTo (⇑(F g)) s (ball (f x) V)
y : α
hy : y ∈ s
⊢ (f y, (fun i a => (F i) a) g y) ∈ U

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → ∀ (U : Set β), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
a✝ : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen V
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed W
hWU : W ⊆ V
s : Set α := K ∩ ⇑f ⁻¹' ball (f x) W
hnhds : s ∈ 𝓝[K] x
hcomp : IsCompact s
⊢ ∃ t ∈ 𝓝[K] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a => (F i) a) n y) ∈ U

Tactic:
have hmaps : MapsTo f s (ball (f x) V) := fun x hx ↦ hWU hx.2

Result:
case mp.intro.intro.intro.intro.intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → ∀ (U : Set β), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
a✝ : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen V
hVsymm : SymmetricRel V
hVU : V ○ V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed W
hWU : W ⊆ V
s : Set α := K ∩ ⇑f ⁻¹' ball (f x) W
hnhds : s ∈ 𝓝[K] x
hcomp : IsCompact s
hmaps : MapsTo (⇑f) s (ball (f x) V)
⊢ ∃ t ∈ 𝓝[K] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a => (F i) a) n y) ∈ U

Proof state:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
⊢ Tendsto F p (𝓝 f) ↔ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K

Tactic:
rw [tendsto_nhds_compactOpen]

Result:
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
⊢ (∀ (K : Set α), IsCompact K → ∀ (U : Set β), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U) ↔
    ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K

Proof state:
case mp
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → ∀ (U : Set β), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
⊢ TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K

Tactic:
rw [← tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK]

Result:
case mp
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → ∀ (U : Set β), IsOpen U → MapsTo (⇑f) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U
K : Set α
hK : IsCompact K
⊢ TendstoLocallyUniformlyOn (fun i a => (F i) a) (⇑f) p K

Proof state:
case mpr
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen U
hf : MapsTo (⇑f) K U
⊢ ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U

Tactic:
rcases lebesgue_number_of_compact_open (hK.image (map_continuous f)) hU hf.image_subset
    with ⟨V, hV, -, hVf⟩

Result:
case mpr.intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen U
hf : MapsTo (⇑f) K U
V : Set (β × β)
hV : V ∈ 𝓤 β
hVf : ∀ x ∈ ⇑f '' K, ball x V ⊆ U
⊢ ∀ᶠ (a : ι) in p, MapsTo (⇑(F a)) K U