-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace [CompactSpace α] :
    TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p

Proof state:
case intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
hU : ∀ᶠ (x : ι) in p, ∀ (i : { x // x ∈ t }), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V
i : ι
hi : ∀ (i_1 : { x // x ∈ t }), ∀ y ∈ U ↑↑i_1, (f y, F i y) ∈ V
x : α
ht : x ∈ ⋃ x ∈ t, U ↑x
⊢ (f x, F i x) ∈ V

Tactic:
simp only [exists_prop, mem_iUnion, SetCoe.exists, exists_and_right, Subtype.coe_mk] at ht

Result:
case intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
hU : ∀ᶠ (x : ι) in p, ∀ (i : { x // x ∈ t }), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V
i : ι
hi : ∀ (i_1 : { x // x ∈ t }), ∀ y ∈ U ↑↑i_1, (f y, F i y) ∈ V
x : α
ht : ∃ x_1, (∃ (x : x_1 ∈ univ), ⟨x_1, ⋯⟩ ∈ t) ∧ x ∈ U x_1
⊢ (f x, F i x) ∈ V

Proof state:
case intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
ht : univ ⊆ ⋃ x ∈ t, U ↑x
hU : ∀ᶠ (x : ι) in p, ∀ (i : { x // x ∈ t }), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V

Tactic:
refine hU.mono fun i hi x => ?_

Result:
case intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
ht : univ ⊆ ⋃ x ∈ t, U ↑x
hU : ∀ᶠ (x : ι) in p, ∀ (i : { x // x ∈ t }), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V
i : ι
hi : ∀ (i_1 : { x // x ∈ t }), ∀ y ∈ U ↑↑i_1, (f y, F i y) ∈ V
x : α
⊢ (f x, F i x) ∈ V

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
hU : ∀ (x : α), U x ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ y ∈ U x, (f y, F n y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V

Tactic:
obtain ⟨t, ht⟩ := isCompact_univ.elim_nhds_subcover' (fun k _ => U k) fun k _ => (hU k).1

Result:
case intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
hU : ∀ (x : α), U x ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ y ∈ U x, (f y, F n y) ∈ V
t : Finset ↑univ
ht : univ ⊆ ⋃ x ∈ t, U ↑x
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V

Proof state:
case intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
hU : ∀ (x : α), U x ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ y ∈ U x, (f y, F n y) ∈ V
t : Finset ↑univ
ht : univ ⊆ ⋃ x ∈ t, U ↑x
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V

Tactic:
replace hU := fun x : t => (hU x).2

Result:
case intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
ht : univ ⊆ ⋃ x ∈ t, U ↑x
hU : ∀ (x : { x // x ∈ t }), ∀ᶠ (n : ι) in p, ∀ y ∈ U ↑↑x, (f y, F n y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V

Proof state:
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
hU : ∀ᶠ (x : ι) in p, ∀ (i : { x // x ∈ t }), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V
i : ι
hi : ∀ (i_1 : { x // x ∈ t }), ∀ y ∈ U ↑↑i_1, (f y, F i y) ∈ V
x y : α
hy₃ : x ∈ U y
hy₁ : y ∈ univ
hy₂ : ⟨y, ⋯⟩ ∈ t
⊢ (f x, F i x) ∈ V

Tactic:
exact hi ⟨⟨y, hy₁⟩, hy₂⟩ x hy₃

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V

Tactic:
choose U hU using h V hV

Result:
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
hU : ∀ (x : α), U x ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ y ∈ U x, (f y, F n y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V

Proof state:
case intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
ht : univ ⊆ ⋃ x ∈ t, U ↑x
hU : ∀ (x : { x // x ∈ t }), ∀ᶠ (n : ι) in p, ∀ y ∈ U ↑↑x, (f y, F n y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V

Tactic:
rw [← eventually_all] at hU

Result:
case intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
ht : univ ⊆ ⋃ x ∈ t, U ↑x
hU : ∀ᶠ (x : ι) in p, ∀ (i : { x // x ∈ t }), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V

Proof state:
case intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
hU : ∀ᶠ (x : ι) in p, ∀ (i : { x // x ∈ t }), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V
i : ι
hi : ∀ (i_1 : { x // x ∈ t }), ∀ y ∈ U ↑↑i_1, (f y, F i y) ∈ V
x : α
ht : ∃ x_1, (∃ (x : x_1 ∈ univ), ⟨x_1, ⋯⟩ ∈ t) ∧ x ∈ U x_1
⊢ (f x, F i x) ∈ V

Tactic:
obtain ⟨y, ⟨hy₁, hy₂⟩, hy₃⟩ := ht

Result:
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
hU : ∀ᶠ (x : ι) in p, ∀ (i : { x // x ∈ t }), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V
i : ι
hi : ∀ (i_1 : { x // x ∈ t }), ∀ y ∈ U ↑↑i_1, (f y, F i y) ∈ V
x y : α
hy₃ : x ∈ U y
hy₁ : y ∈ univ
hy₂ : ⟨y, ⋯⟩ ∈ t
⊢ (f x, F i x) ∈ V

Proof state:
case intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
ht : univ ⊆ ⋃ x ∈ t, U ↑x
hU : ∀ᶠ (x : ι) in p, ∀ (i : { x // x ∈ t }), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V
i : ι
hi : ∀ (i_1 : { x // x ∈ t }), ∀ y ∈ U ↑↑i_1, (f y, F i y) ∈ V
x : α
⊢ (f x, F i x) ∈ V

Tactic:
specialize ht (mem_univ x)

Result:
case intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
hU : ∀ᶠ (x : ι) in p, ∀ (i : { x // x ∈ t }), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V
i : ι
hi : ∀ (i_1 : { x // x ∈ t }), ∀ y ∈ U ↑↑i_1, (f y, F i y) ∈ V
x : α
ht : x ∈ ⋃ x ∈ t, U ↑x
⊢ (f x, F i x) ∈ V