case h₀.intro.mk.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V✝ : Set (β × β)
f g : C(α, β)
K : Set α
V : Set (β × β)
hK : IsCompact (K, V).fst
hV : (K, V).snd ∈ 𝓤 β
⊢ g ∈ (fun KV => compactConvNhd KV.fst KV.snd g) (K, V)

case h₁.intro.mk.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V✝ : Set (β × β)
f g : C(α, β)
K : Set α
V : Set (β × β)
hK : IsCompact (K, V).fst
hV : (K, V).snd ∈ 𝓤 β
⊢ ∃ n₁,
    n₁ ∈ compactConvergenceFilterBasis g ∧
      n₁ ⊆ (fun KV => compactConvNhd KV.fst KV.snd g) (K, V) ∧
        ∀ (x' : C(α, β)),
          x' ∈ n₁ → ∃ n₂, n₂ ∈ compactConvergenceFilterBasis x' ∧ n₂ ⊆ (fun KV => compactConvNhd KV.fst KV.snd g) (K, V)
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
⊢ 𝓝 f = FilterBasis.filter (compactConvergenceFilterBasis f)
rw [TopologicalSpace.nhds_mkOfNhds_filterBasis] <;> rintro g - ⟨⟨K, V⟩, ⟨hK, hV⟩, rfl⟩
no goals
case h₀.intro.mk.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V✝ : Set (β × β)
f g : C(α, β)
K : Set α
V : Set (β × β)
hK : IsCompact (K, V).fst
hV : (K, V).snd ∈ 𝓤 β
⊢ g ∈ (fun KV => compactConvNhd KV.fst KV.snd g) (K, V)
exact self_mem_compactConvNhd g hV
case h₁.intro.mk.intro.intro.intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V✝ : Set (β × β)
f g : C(α, β)
K : Set α
V : Set (β × β)
hK : IsCompact (K, V).fst
hV : (K, V).snd ∈ 𝓤 β
V' : Set (β × β)
hV' : V' ∈ 𝓤 β
h₁ : V' ⊆ (K, V).snd
h₂ :
  ∀ (g_1 : C(α, β)),
    g_1 ∈ compactConvNhd ?m.4915 V' g → compactConvNhd ?m.4915 V' g_1 ⊆ compactConvNhd ?m.4915 (K, V).snd g
⊢ ∃ n₁,
    n₁ ∈ compactConvergenceFilterBasis g ∧
      n₁ ⊆ (fun KV => compactConvNhd KV.fst KV.snd g) (K, V) ∧
        ∀ (x' : C(α, β)),
          x' ∈ n₁ → ∃ n₂, n₂ ∈ compactConvergenceFilterBasis x' ∧ n₂ ⊆ (fun KV => compactConvNhd KV.fst KV.snd g) (K, V)
case h₁.intro.mk.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V✝ : Set (β × β)
f g : C(α, β)
K : Set α
V : Set (β × β)
hK : IsCompact (K, V).fst
hV : (K, V).snd ∈ 𝓤 β
⊢ ∃ n₁,
    n₁ ∈ compactConvergenceFilterBasis g ∧
      n₁ ⊆ (fun KV => compactConvNhd KV.fst KV.snd g) (K, V) ∧
        ∀ (x' : C(α, β)),
          x' ∈ n₁ → ∃ n₂, n₂ ∈ compactConvergenceFilterBasis x' ∧ n₂ ⊆ (fun KV => compactConvNhd KV.fst KV.snd g) (K, V)
obtain ⟨V', hV', h₁, h₂⟩ := compactConvNhd_nhd_basis g hV
no goals
case h₁.intro.mk.intro.intro.intro.intro.intro
α : Type u₁
β : Type u₂
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
K✝ : Set α
V✝ : Set (β × β)
f g : C(α, β)
K : Set α
V : Set (β × β)
hK : IsCompact (K, V).fst
hV : (K, V).snd ∈ 𝓤 β
V' : Set (β × β)
hV' : V' ∈ 𝓤 β
h₁ : V' ⊆ (K, V).snd
h₂ :
  ∀ (g_1 : C(α, β)),
    g_1 ∈ compactConvNhd ?m.4915 V' g → compactConvNhd ?m.4915 V' g_1 ⊆ compactConvNhd ?m.4915 (K, V).snd g
⊢ ∃ n₁,
    n₁ ∈ compactConvergenceFilterBasis g ∧
      n₁ ⊆ (fun KV => compactConvNhd KV.fst KV.snd g) (K, V) ∧
        ∀ (x' : C(α, β)),
          x' ∈ n₁ → ∃ n₂, n₂ ∈ compactConvergenceFilterBasis x' ∧ n₂ ⊆ (fun KV => compactConvNhd KV.fst KV.snd g) (K, V)
exact
  ⟨compactConvNhd K V' g, ⟨⟨K, V'⟩, ⟨hK, hV'⟩, rfl⟩, compactConvNhd_mono g h₁, fun g' hg' =>
    ⟨compactConvNhd K V' g', ⟨⟨K, V'⟩, ⟨hK, hV'⟩, rfl⟩, h₂ g' hg'⟩⟩