awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ :
  ∀ (f : C(X, Y)) (x : X),
    ∀ V ∈ T, Membership.mem (α := Y) V ((f : (a : X) → Y) x : Y) → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst_1] U
hfKU : MapsTo (⇑f : (a : X) → Y) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ (⇑f : (a : X) → Y) ⁻¹' ⋃₀ t
s : Set (Set X)
hsS : s ⊆ S
hsf : s.Finite
hKs : K ⊆ ⋃₀ s
hst : MapsTo (⇑f : (a : X) → Y) (⋃₀ s) (⋃₀ t)
hsub :
  Subset (α := Set C(X, Y)) (⋂ L ∈ s, {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) L (⋃₀ t)})
    {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U}
L : Set X
hL : L ∈ s
a :
  Membership.mem (γ := Set (Set C(X, Y)))
    {s : Set C(X, Y) |
      f ∈ s ∧
        Membership.mem (γ := Set (Set C(X, Y)))
          (image2 (fun (K : Set X) (t : Set (Set Y)) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K (⋃₀ t)}) S
            {t : Set (Set Y) | t.Finite ∧ t ⊆ T})
          s}
    {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) L (⋃₀ t)}
⊢ Membership.mem (γ := Filter C(X, Y))
    (⨅ (s : Set C(X, Y)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set C(X, Y)))
          {s : Set C(X, Y) |
            f ∈ s ∧
              Membership.mem (γ := Set (Set C(X, Y)))
                (image2 (fun (K : Set X) (t : Set (Set Y)) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K (⋃₀ t)}) S
                  {t : Set (Set Y) | t.Finite ∧ t ⊆ T})
                s}
          s),
        𝓟 s)
    {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) L (⋃₀ t)}

Tactic:
refine mem_iInf_of_mem _ <| mem_iInf_of_mem ?_ <| mem_principal_self _

Premises used: Filter.mem_principal_self, Filter.mem_iInf_of_mem
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ :
  ∀ (f : C(X, Y)) (x : X),
    ∀ V ∈ T, Membership.mem (α := Y) V ((f : (a : X) → Y) x : Y) → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst_1] U
hfKU : MapsTo (⇑f : (a : X) → Y) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ (⇑f : (a : X) → Y) ⁻¹' ⋃₀ t
s : Set (Set X)
hsS : s ⊆ S
hsf : s.Finite
hKs : K ⊆ ⋃₀ s
hst : MapsTo (⇑f : (a : X) → Y) (⋃₀ s) (⋃₀ t)
hsub :
  Subset (α := Set C(X, Y)) (⋂ L ∈ s, {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) L (⋃₀ t)})
    {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U}
L : Set X
hL : L ∈ s
⊢ Membership.mem (γ := Set (Set C(X, Y)))
    {s : Set C(X, Y) |
      f ∈ s ∧
        Membership.mem (γ := Set (Set C(X, Y)))
          (image2 (fun (K : Set X) (t : Set (Set Y)) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K (⋃₀ t)}) S
            {t : Set (Set Y) | t.Finite ∧ t ⊆ T})
          s}
    {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) L (⋃₀ t)}

Tactic:
⟨hst.mono_left (subset_sUnion_of_mem hL), mem_image2_of_mem (hsS hL) ⟨htf, htT⟩⟩

Premises used: Set.Mem, setOf, Set.MapsTo.mono_left, And.intro, Set.subset_sUnion_of_mem, Set.mem_image2_of_mem
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ :
  ∀ (f : C(X, Y)) (x : X),
    ∀ V ∈ T, Membership.mem (α := Y) V ((f : (a : X) → Y) x : Y) → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst_1] U
hfKU : MapsTo (⇑f : (a : X) → Y) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ (⇑f : (a : X) → Y) ⁻¹' ⋃₀ t
s : Set (Set X)
hsS : s ⊆ S
hsf : s.Finite
hKs : K ⊆ ⋃₀ s
hst : MapsTo (⇑f : (a : X) → Y) (⋃₀ s) (⋃₀ t)
hsub :
  Subset (α := Set C(X, Y)) (⋂ L ∈ s, {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) L (⋃₀ t)})
    {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U}
L : Set X
hL : L ∈ s
⊢ Membership.mem (γ := Set (Set C(X, Y)))
    {s : Set C(X, Y) |
      f ∈ s ∧
        Membership.mem (γ := Set (Set C(X, Y)))
          (image2 (fun (K : Set X) (t : Set (Set Y)) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K (⋃₀ t)}) S
            {t : Set (Set Y) | t.Finite ∧ t ⊆ T})
          s}
    {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) L (⋃₀ t)}

Tactic:
exact ⟨hst.mono_left (subset_sUnion_of_mem hL), mem_image2_of_mem (hsS hL) ⟨htf, htT⟩⟩
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology Y
hX :
  ∃ (S : Set (Set X)),
    S.Countable ∧
      (∀ K ∈ S, IsCompact K) ∧
        ∀ (f : C(X, Y)) (V : Set Y),
          IsOpen[inst_1] V →
            ∀ (x : X),
              Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x →
                ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K V
rcases :
  ∀ (S : Set (Set X)) (hScount : S.Countable) (hScomp : ∀ K ∈ S, IsCompact K)
    (hS :
      ∀ (f : C(X, Y)) (V : Set Y),
        IsOpen[inst_1] V →
          ∀ (x : X),
            Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x →
              ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K V),
    ∃ (b : Set (Set C(X, Y))), b.Countable ∧ compactOpen = generateFrom b
⊢ ∃ (b : Set (Set C(X, Y))), b.Countable ∧ compactOpen = generateFrom b

Tactic:
rcases hX with ⟨S, hScount, hScomp, hS⟩
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology Y
S : Set (Set X)
hScount : S.Countable
hScomp : ∀ K ∈ S, IsCompact K
hS :
  ∀ (f : C(X, Y)) (V : Set Y),
    IsOpen[inst_1] V →
      ∀ (x : X),
        Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K V
⊢ ∃ (b : Set (Set C(X, Y))), b.Countable ∧ compactOpen = generateFrom b

Tactic:
⟨_, ?_, compactOpen_eq_generateFrom (S := S) hScomp (isBasis_countableBasis _) ?_⟩

Premises used: And.intro, Exists.intro, TopologicalSpace.isBasis_countableBasis, ContinuousMap.compactOpen_eq_generateFrom
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology Y
S : Set (Set X)
hScount : S.Countable
hScomp : ∀ K ∈ S, IsCompact K
hS :
  ∀ (f : C(X, Y)) (V : Set Y),
    IsOpen[inst_1] V →
      ∀ (x : X),
        Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K V
refine_1 :
  Set.Countable (α := Set C(X, Y))
    (image2 (fun (K : Set X) (t : Set (Set Y)) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K (⋃₀ t)}) S
      {t : Set (Set Y) | t.Finite ∧ t ⊆ countableBasis Y})
refine_2 :
  ∀ (f : C(X, Y)) (x : X),
    ∀ V ∈ countableBasis Y,
      Membership.mem (α := Y) V ((f : (a : X) → Y) x : Y) → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K V
⊢ ∃ (b : Set (Set C(X, Y))), b.Countable ∧ compactOpen = generateFrom b

Tactic:
refine ⟨_, ?_, compactOpen_eq_generateFrom (S := S) hScomp (isBasis_countableBasis _) ?_⟩
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology Y
S : Set (Set X)
hScount : S.Countable
hScomp : ∀ K ∈ S, IsCompact K
hS :
  ∀ (f : C(X, Y)) (V : Set Y),
    IsOpen[inst_1] V →
      ∀ (x : X),
        Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K V
⊢ Set.Countable (α := Set C(X, Y))
    (image2 (fun (K : Set X) (t : Set (Set Y)) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K (⋃₀ t)}) S
      {t : Set (Set Y) | t.Finite ∧ t ⊆ countableBasis Y})

Tactic:
.image2 hScount (countable_setOf_finite_subset (countable_countableBasis Y)) _

Premises used: Set.Countable.image2, TopologicalSpace.countable_countableBasis, Set.countable_setOf_finite_subset
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology Y
S : Set (Set X)
hScount : S.Countable
hScomp : ∀ K ∈ S, IsCompact K
hS :
  ∀ (f : C(X, Y)) (V : Set Y),
    IsOpen[inst_1] V →
      ∀ (x : X),
        Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K V
⊢ Set.Countable (α := Set C(X, Y))
    (image2 (fun (K : Set X) (t : Set (Set Y)) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K (⋃₀ t)}) S
      {t : Set (Set Y) | t.Finite ∧ t ⊆ countableBasis Y})

Tactic:
exact .image2 hScount (countable_setOf_finite_subset (countable_countableBasis Y)) _
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology Y
S : Set (Set X)
hScount : S.Countable
hScomp : ∀ K ∈ S, IsCompact K
hS :
  ∀ (f : C(X, Y)) (V : Set Y),
    IsOpen[inst_1] V →
      ∀ (x : X),
        Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K V
f : C(X, Y)
x : X
V : Set Y
hV : V ∈ countableBasis Y
hx : Membership.mem (α := Y) V ((f : (a : X) → Y) x : Y)
refine_2 : IsOpen[inst_1] V
refine_2₁ : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x
⊢ ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K V

Tactic:
apply hS
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology Y
S : Set (Set X)
hScount : S.Countable
hScomp : ∀ K ∈ S, IsCompact K
hS :
  ∀ (f : C(X, Y)) (V : Set Y),
    IsOpen[inst_1] V →
      ∀ (x : X),
        Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K V
f : C(X, Y)
x : X
V : Set Y
hV : V ∈ countableBasis Y
hx : Membership.mem (α := Y) V ((f : (a : X) → Y) x : Y)
⊢ IsOpen[inst_1] V

Tactic:
isOpen_of_mem_countableBasis hV

Premises used: TopologicalSpace.isOpen_of_mem_countableBasis
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology Y
S : Set (Set X)
hScount : S.Countable
hScomp : ∀ K ∈ S, IsCompact K
hS :
  ∀ (f : C(X, Y)) (V : Set Y),
    IsOpen[inst_1] V →
      ∀ (x : X),
        Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K V
f : C(X, Y)
x : X
V : Set Y
hV : V ∈ countableBasis Y
hx : Membership.mem (α := Y) V ((f : (a : X) → Y) x : Y)
⊢ Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x

Tactic:
hx

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology Y
S : Set (Set X)
hScount : S.Countable
hScomp : ∀ K ∈ S, IsCompact K
hS :
  ∀ (f : C(X, Y)) (V : Set Y),
    IsOpen[inst_1] V →
      ∀ (x : X),
        Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K V
f : C(X, Y)
x : X
V : Set Y
hV : V ∈ countableBasis Y
hx : Membership.mem (α := Y) V ((f : (a : X) → Y) x : Y)
⊢ IsOpen[inst_1] V

Tactic:
exacts [isOpen_of_mem_countableBasis hV, hx]

Premises used: TopologicalSpace.isOpen_of_mem_countableBasis
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology X
inst_3 : LocallyCompactSpace X
inst_4 : SecondCountableTopology Y
hX :
  ∃ (S : Set (Set X)),
    S.Countable ∧
      (∀ K ∈ S, IsCompact K) ∧
        ∀ (f : C(X, Y)) (V : Set Y),
          IsOpen[inst_1] V →
            ∀ (x : X),
              Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x →
                ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K V
⊢ SecondCountableTopology C(X, Y)

Tactic:
apply secondCountableTopology

Premises used: ContinuousMap.secondCountableTopology
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology X
inst_3 : LocallyCompactSpace X
inst_4 : SecondCountableTopology Y
⊢ ∀ (U : (↑(countableBasis X) : Type u_1)), LocallyCompactSpace.{u_1} (↑(↑U : Set X) : Type u_1)

Tactic:
have (U : countableBasis X) : LocallyCompactSpace U.1 :=
    (isOpen_of_mem_countableBasis U.2).locallyCompactSpace
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology X
inst_3 : LocallyCompactSpace X
inst_4 : SecondCountableTopology Y
this : ∀ (U : (↑(countableBasis X) : Type u_1)), LocallyCompactSpace.{u_1} (↑(↑U : Set X) : Type u_1)
K : (U : (↑(countableBasis X) : Type u_1)) → CompactExhaustion (↑(↑U : Set X) : Type u_1) :=
  fun (U : (↑(countableBasis X) : Type u_1)) ↦ CompactExhaustion.choice (↑(↑U : Set X) : Type u_1)
h :
  Set.Countable.{u_1} (α := Set X)
      (⋃ (U : (↑(countableBasis X) : Type u_1)),
        range fun (n : ℕ) ↦
          image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
            ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n)) ∧
    (∀ (K_1 : Set X),
        Membership.mem (γ := Set (Set X))
            (⋃ (U : (↑(countableBasis X) : Type u_1)),
              range fun (n : ℕ) ↦
                image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
                  ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n))
            K_1 →
          IsCompact K_1) ∧
      ∀ (f : C(X, Y)) (V : Set Y),
        IsOpen[inst_1] V →
          ∀ (x : X),
            Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x →
              ∃ (K_1 : Set X),
                Membership.mem (γ := Set (Set X))
                    (⋃ (U : (↑(countableBasis X) : Type u_1)),
                      range fun (n : ℕ) ↦
                        image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
                          ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n))
                    K_1 ∧
                  K_1 ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K_1 V
⊢ ∃ (S : Set (Set X)),
    S.Countable ∧
      (∀ K ∈ S, IsCompact K) ∧
        ∀ (f : C(X, Y)) (V : Set Y),
          IsOpen[inst_1] V →
            ∀ (x : X),
              Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x →
                ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K V

Tactic:
use ⋃ U : countableBasis X, Set.range fun n ↦ K U n

Premises used: TopologicalSpace.countableBasis
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology X
inst_3 : LocallyCompactSpace X
inst_4 : SecondCountableTopology Y
this : ∀ (U : (↑(countableBasis X) : Type u_1)), LocallyCompactSpace.{u_1} (↑(↑U : Set X) : Type u_1)
K : (U : (↑(countableBasis X) : Type u_1)) → CompactExhaustion (↑(↑U : Set X) : Type u_1) :=
  fun (U : (↑(countableBasis X) : Type u_1)) ↦ CompactExhaustion.choice (↑(↑U : Set X) : Type u_1)
⊢ Set.Countable.{u_1} (α := Set X)
      (⋃ (U : (↑(countableBasis X) : Type u_1)),
        range fun (n : ℕ) ↦
          image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
            ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n)) ∧
    (∀ (K_1 : Set X),
        Membership.mem (γ := Set (Set X))
            (⋃ (U : (↑(countableBasis X) : Type u_1)),
              range fun (n : ℕ) ↦
                image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
                  ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n))
            K_1 →
          IsCompact K_1) ∧
      ∀ (f : C(X, Y)) (V : Set Y),
        IsOpen[inst_1] V →
          ∀ (x : X),
            Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x →
              ∃ (K_1 : Set X),
                Membership.mem (γ := Set (Set X))
                    (⋃ (U : (↑(countableBasis X) : Type u_1)),
                      range fun (n : ℕ) ↦
                        image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
                          ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n))
                    K_1 ∧
                  K_1 ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K_1 V

Tactic:
⟨countable_iUnion fun _ ↦ countable_range _, ?_, ?_⟩

Premises used: Set.countable_range, Set.countable_iUnion, And.intro, Set.image, Subtype.val, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology X
inst_3 : LocallyCompactSpace X
inst_4 : SecondCountableTopology Y
this : ∀ (U : (↑(countableBasis X) : Type u_1)), LocallyCompactSpace.{u_1} (↑(↑U : Set X) : Type u_1)
K : (U : (↑(countableBasis X) : Type u_1)) → CompactExhaustion (↑(↑U : Set X) : Type u_1) :=
  fun (U : (↑(countableBasis X) : Type u_1)) ↦ CompactExhaustion.choice (↑(↑U : Set X) : Type u_1)
h :
  ∀ (K_1 : Set X),
    Membership.mem (γ := Set (Set X))
        (⋃ (U : (↑(countableBasis X) : Type u_1)),
          range fun (n : ℕ) ↦
            image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
              ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n))
        K_1 →
      IsCompact K_1
h₁ :
  ∀ (f : C(X, Y)) (V : Set Y),
    IsOpen[inst_1] V →
      ∀ (x : X),
        Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x →
          ∃ (K_1 : Set X),
            Membership.mem (γ := Set (Set X))
                (⋃ (U : (↑(countableBasis X) : Type u_1)),
                  range fun (n : ℕ) ↦
                    image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
                      ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n))
                K_1 ∧
              K_1 ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K_1 V
⊢ Set.Countable.{u_1} (α := Set X)
      (⋃ (U : (↑(countableBasis X) : Type u_1)),
        range fun (n : ℕ) ↦
          image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
            ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n)) ∧
    (∀ (K_1 : Set X),
        Membership.mem (γ := Set (Set X))
            (⋃ (U : (↑(countableBasis X) : Type u_1)),
              range fun (n : ℕ) ↦
                image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
                  ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n))
            K_1 →
          IsCompact K_1) ∧
      ∀ (f : C(X, Y)) (V : Set Y),
        IsOpen[inst_1] V →
          ∀ (x : X),
            Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x →
              ∃ (K_1 : Set X),
                Membership.mem (γ := Set (Set X))
                    (⋃ (U : (↑(countableBasis X) : Type u_1)),
                      range fun (n : ℕ) ↦
                        image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
                          ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n))
                    K_1 ∧
                  K_1 ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K_1 V

Tactic:
refine ⟨countable_iUnion fun _ ↦ countable_range _, ?_, ?_⟩
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology X
inst_3 : LocallyCompactSpace X
inst_4 : SecondCountableTopology Y
this : ∀ (U : (↑(countableBasis X) : Type u_1)), LocallyCompactSpace.{u_1} (↑(↑U : Set X) : Type u_1)
K : (U : (↑(countableBasis X) : Type u_1)) → CompactExhaustion (↑(↑U : Set X) : Type u_1) :=
  fun (U : (↑(countableBasis X) : Type u_1)) ↦ CompactExhaustion.choice (↑(↑U : Set X) : Type u_1)
h :
  ∀ (K_1 : Set X),
    (∃ (i : (↑(countableBasis X) : Type u_1)) (y : ℕ),
        image (α := { x : X // x ∈ (↑i : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑i : Set X)))
            ((K i : (a : ℕ) → Set (↑(↑i : Set X) : Type u_1)) y) =
          K_1) →
      IsCompact K_1
⊢ ∀ (K_1 : Set X),
    Membership.mem (γ := Set (Set X))
        (⋃ (U : (↑(countableBasis X) : Type u_1)),
          range fun (n : ℕ) ↦
            image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
              ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n))
        K_1 →
      IsCompact K_1

Tactic:
simp only [mem_iUnion, mem_range]

Premises used: Set.mem_range, Set.mem_iUnion
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology X
inst_3 : LocallyCompactSpace X
inst_4 : SecondCountableTopology Y
this : ∀ (U : (↑(countableBasis X) : Type u_1)), LocallyCompactSpace.{u_1} (↑(↑U : Set X) : Type u_1)
K : (U : (↑(countableBasis X) : Type u_1)) → CompactExhaustion (↑(↑U : Set X) : Type u_1) :=
  fun (U : (↑(countableBasis X) : Type u_1)) ↦ CompactExhaustion.choice (↑(↑U : Set X) : Type u_1)
U : (↑(countableBasis X) : Type u_1)
n : ℕ
⊢ IsCompact.{u_1} (X := X)
    (image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
      ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n))

Tactic:
((K U).isCompact _).image continuous_subtype_val

Premises used: continuous_subtype_val, CompactExhaustion.isCompact, IsCompact.image
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology X
inst_3 : LocallyCompactSpace X
inst_4 : SecondCountableTopology Y
this : ∀ (U : (↑(countableBasis X) : Type u_1)), LocallyCompactSpace.{u_1} (↑(↑U : Set X) : Type u_1)
K : (U : (↑(countableBasis X) : Type u_1)) → CompactExhaustion (↑(↑U : Set X) : Type u_1) :=
  fun (U : (↑(countableBasis X) : Type u_1)) ↦ CompactExhaustion.choice (↑(↑U : Set X) : Type u_1)
U : (↑(countableBasis X) : Type u_1)
n : ℕ
⊢ IsCompact.{u_1} (X := X)
    (image (α := { x : X // x ∈ (↑U : Set X) }) (Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
      ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n))

Tactic:
exact ((K U).isCompact _).image continuous_subtype_val

Premises used: continuous_subtype_val, CompactExhaustion.isCompact, IsCompact.image
-- Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SecondCountableTopology X
inst_3 : LocallyCompactSpace X
inst_4 : SecondCountableTopology Y
this : ∀ (U : (↑(countableBasis X) : Type u_1)), LocallyCompactSpace.{u_1} (↑(↑U : Set X) : Type u_1)
K : (U : (↑(countableBasis X) : Type u_1)) → CompactExhaustion (↑(↑U : Set X) : Type u_1) :=
  fun (U : (↑(countableBasis X) : Type u_1)) ↦ CompactExhaustion.choice (↑(↑U : Set X) : Type u_1)
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst_1] V
x : X
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x
rw : (⇑f : (a : X) → Y) ⁻¹' V ∈ 𝓝 x
⊢ ∃ U ∈ countableBasis X, x ∈ U ∧ U ⊆ (⇑f : (a : X) → Y) ⁻¹' V

Tactic:
rw [← (isBasis_countableBasis _).mem_nhds_iff]

Premises used: TopologicalSpace.isBasis_countableBasis, TopologicalSpace.IsTopologicalBasis.mem_nhds_iff