-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoLocallyUniformlyOn_TFAE [LocallyCompactSpace α] (G : ι → α → β) (g : α → β)
    (p : Filter ι) (hs : IsOpen s) :
    List.TFAE [
      TendstoLocallyUniformlyOn G g p s,
      ∀ K, K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K,
      ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v]

Proof state:
case intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
h : ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
x : α
hx : x ∈ s
K : Set α
hK3 : K ⊆ s
hK1 : K ∈ 𝓝 x
hK2 : IsCompact K
⊢ ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v

Tactic:
exact ⟨K, nhdsWithin_le_nhds hK1, h K hK3 hK2⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 : (∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K) → ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
tfae_3_to_1 : (∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v) → TendstoLocallyUniformlyOn G g p s
⊢ [TendstoLocallyUniformlyOn G g p s, ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K,
      ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
h : ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
x : α
hx : x ∈ s
⊢ ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v

Tactic:
obtain ⟨K, ⟨hK1, hK2⟩, hK3⟩ := (compact_basis_nhds x).mem_iff.mp (hs.mem_nhds hx)

Result:
case intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
h : ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
x : α
hx : x ∈ s
K : Set α
hK3 : K ⊆ s
hK1 : K ∈ 𝓝 x
hK2 : IsCompact K
⊢ ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 : (∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K) → ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
h : ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (g y, G n y) ∈ u

Tactic:
obtain ⟨v, hv1, hv2⟩ := h x hx

Result:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 : (∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K) → ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
h : ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
v : Set α
hv1 : v ∈ 𝓝[s] x
hv2 : TendstoUniformlyOn G g p v
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (g y, G n y) ∈ u

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
⊢ [TendstoLocallyUniformlyOn G g p s, ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K,
      ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v].TFAE

Tactic:
tfae_have 2 → 3
| h, x, hx => by
  obtain ⟨K, ⟨hK1, hK2⟩, hK3⟩ := (compact_basis_nhds x).mem_iff.mp (hs.mem_nhds hx)
  exact ⟨K, nhdsWithin_le_nhds hK1, h K hK3 hK2⟩

Result:
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 : (∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K) → ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
⊢ [TendstoLocallyUniformlyOn G g p s, ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K,
      ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v].TFAE

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
⊢ [TendstoLocallyUniformlyOn G g p s, ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K,
      ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v].TFAE

Tactic:
tfae_have 1 → 2
| h, K, hK1, hK2 =>
  (tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK2).mp (h.mono hK1)

Result:
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
⊢ [TendstoLocallyUniformlyOn G g p s, ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K,
      ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v].TFAE

Proof state:
case intro.intro
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 : (∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K) → ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
h : ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
v : Set α
hv1 : v ∈ 𝓝[s] x
hv2 : TendstoUniformlyOn G g p v
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (g y, G n y) ∈ u

Tactic:
exact ⟨v, hv1, hv2 u hu⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 : (∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K) → ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
⊢ [TendstoLocallyUniformlyOn G g p s, ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K,
      ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v].TFAE

Tactic:
tfae_have 3 → 1
| h, u, hu, x, hx => by
  obtain ⟨v, hv1, hv2⟩ := h x hx
  exact ⟨v, hv1, hv2 u hu⟩

Result:
α : Type u
β : Type v
ι : Type x
inst✝² : UniformSpace β
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 : (∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K) → ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
tfae_3_to_1 : (∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v) → TendstoLocallyUniformlyOn G g p s
⊢ [TendstoLocallyUniformlyOn G g p s, ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K,
      ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v].TFAE