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
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
⊢ (⇑f : (a : X) → Y) ⁻¹' V ∈ 𝓝 x

Tactic:
(hVo.preimage (map_continuous f)).mem_nhds hxV

Premises used: Set.Mem, IsOpen.mem_nhds, ContinuousMapClass.map_continuous, IsOpen.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 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
⊢ (⇑f : (a : X) → Y) ⁻¹' V ∈ 𝓝 x

Tactic:
exact (hVo.preimage (map_continuous f)).mem_nhds hxV

Premises used: IsOpen.mem_nhds, ContinuousMapClass.map_continuous, IsOpen.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 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
h :
  ∀ (U : Set X) (hU : U ∈ countableBasis X) (hxU : x ∈ U) (hUV : U ⊆ (⇑f : (a : X) → Y) ⁻¹' V),
    ∃ (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
⊢ ∃ (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:
obtain ⟨U, hU, hxU, hUV⟩ : ∃ U ∈ countableBasis X, x ∈ U ∧ U ⊆ f ⁻¹' V := by
      rw [← (isBasis_countableBasis _).mem_nhds_iff]
      exact (hVo.preimage (map_continuous f)).mem_nhds hxV

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)
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
U : Set X
hU : U ∈ countableBasis X
hxU : x ∈ U
hUV : U ⊆ (⇑f : (a : X) → Y) ⁻¹' V
⊢ x ∈ U

Tactic:
hxU
-- 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
U : Set X
hU : U ∈ countableBasis X
hxU : x ∈ U
hUV : U ⊆ (⇑f : (a : X) → Y) ⁻¹' V
h :
  ∀ (x : { x : X // x ∈ U }) (hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : 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 : X) ∧ MapsTo (⇑f : (a : X) → Y) K_1 V
⊢ ∃ (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:
lift x to U using hxU
-- 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
U : Set X
hU : U ∈ countableBasis X
hUV : U ⊆ (⇑f : (a : X) → Y) ⁻¹' V
x : { x : X // x ∈ U }
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)
⊢ U ∈ countableBasis X

Tactic:
hU
-- 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
U : Set X
hU : U ∈ countableBasis X
hUV : U ⊆ (⇑f : (a : X) → Y) ⁻¹' V
x : { x : X // x ∈ U }
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)
h :
  ∀ (U : { x : Set X // x ∈ countableBasis X }) (hUV : (↑U : Set X) ⊆ (⇑f : (a : X) → Y) ⁻¹' V)
    (x : { x : X // x ∈ (↑U : Set X) }) (hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : 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 : X) ∧ MapsTo (⇑f : (a : X) → Y) K_1 V
⊢ ∃ (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 : X) ∧ MapsTo (⇑f : (a : X) → Y) K_1 V

Tactic:
lift U to countableBasis X using hU

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)
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst_1] V
U : { x : Set X // x ∈ countableBasis X }
hUV : (↑U : Set X) ⊆ (⇑f : (a : X) → Y) ⁻¹' V
x : { x : X // x ∈ (↑U : Set X) }
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)
h :
  ∀ (n : ℕ)
    (hn :
      Membership.mem (α := Set (↑(↑U : Set X) : Type u_1)) (𝓝 x)
        ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n : Set (↑(↑U : Set X) : Type u_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 ∧
        K_1 ∈ 𝓝 (↑x : X) ∧ MapsTo (⇑f : (a : X) → Y) K_1 V
⊢ ∃ (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 : X) ∧ MapsTo (⇑f : (a : X) → Y) K_1 V

Tactic:
rcases (K U).exists_mem_nhds x with ⟨n, hn⟩

Premises used: CompactExhaustion.exists_mem_nhds
-- 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
U : { x : Set X // x ∈ countableBasis X }
hUV : (↑U : Set X) ⊆ (⇑f : (a : X) → Y) ⁻¹' V
x : { x : X // x ∈ (↑U : Set X) }
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)
n : ℕ
hn :
  Membership.mem (α := Set (↑(↑U : Set X) : Type u_1)) (𝓝 x)
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n : Set (↑(↑U : Set X) : Type u_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 ∧
      K_1 ∈ 𝓝 (↑x : X) ∧ MapsTo (⇑f : (a : X) → Y) K_1 V

Tactic:
⟨K U n, mem_iUnion.2 ⟨U, mem_range_self _⟩, ?_, ?_⟩

Premises used: Set.mem_range_self, Iff.mpr, Set.mem_iUnion, And.intro, Exists.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)
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst_1] V
U : { x : Set X // x ∈ countableBasis X }
hUV : (↑U : Set X) ⊆ (⇑f : (a : X) → Y) ⁻¹' V
x : { x : X // x ∈ (↑U : Set X) }
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)
n : ℕ
hn :
  Membership.mem (α := Set (↑(↑U : Set X) : Type u_1)) (𝓝 x)
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n : Set (↑(↑U : Set X) : Type u_1))
h :
  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) ∈
    𝓝 (↑x : X)
h₁ :
  MapsTo.{u_1, u_2} (α := X) (⇑f : (a : X) → Y)
    (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))
    V
⊢ ∃ (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 : X) ∧ MapsTo (⇑f : (a : X) → Y) K_1 V

Tactic:
refine ⟨K U n, mem_iUnion.2 ⟨U, mem_range_self _⟩, ?_, ?_⟩
-- 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
U : { x : Set X // x ∈ countableBasis X }
hUV : (↑U : Set X) ⊆ (⇑f : (a : X) → Y) ⁻¹' V
x : { x : X // x ∈ (↑U : Set X) }
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)
n : ℕ
hn :
  Membership.mem (α := Set (↑(↑U : Set X) : Type u_1)) (𝓝 x)
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n : Set (↑(↑U : Set X) : Type u_1))
h :
  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) ∈
    map (Subtype.val (p := Membership.mem (↑U : Set X))) (𝓝 (Subtype.mk (p := Membership.mem (↑U : Set X)) (↑x : X) ⋯))
h₁ : ∀ᶠ (x : X) in 𝓝 (↑x : X), x ∈ (↑U : Set 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) ∈
    𝓝 (↑x : X)

Tactic:
rw [← map_nhds_subtype_coe_eq_nhds x.2]

Premises used: map_nhds_subtype_coe_eq_nhds, Subtype.property
-- 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
U : { x : Set X // x ∈ countableBasis X }
hUV : (↑U : Set X) ⊆ (⇑f : (a : X) → Y) ⁻¹' V
x : { x : X // x ∈ (↑U : Set X) }
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)
n : ℕ
hn :
  Membership.mem (α := Set (↑(↑U : Set X) : Type u_1)) (𝓝 x)
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n : Set (↑(↑U : Set X) : Type u_1))
⊢ 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) ∈
    map (Subtype.val (p := Membership.mem (↑U : Set X))) (𝓝 (Subtype.mk (p := Membership.mem (↑U : Set X)) (↑x : X) ⋯))

Tactic:
image_mem_map hn

Premises used: Set.Mem, Filter.image_mem_map
-- 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
U : { x : Set X // x ∈ countableBasis X }
hUV : (↑U : Set X) ⊆ (⇑f : (a : X) → Y) ⁻¹' V
x : { x : X // x ∈ (↑U : Set X) }
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)
n : ℕ
hn :
  Membership.mem (α := Set (↑(↑U : Set X) : Type u_1)) (𝓝 x)
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n : Set (↑(↑U : Set X) : Type u_1))
⊢ ∀ᶠ (x : X) in 𝓝 (↑x : X), x ∈ (↑U : Set X)

Tactic:
(isOpen_of_mem_countableBasis U.2).mem_nhds x.2

Premises used: Set.Mem, Filter.Eventually, setOf, IsOpen.mem_nhds, TopologicalSpace.isOpen_of_mem_countableBasis, Subtype.property
-- 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
U : { x : Set X // x ∈ countableBasis X }
hUV : (↑U : Set X) ⊆ (⇑f : (a : X) → Y) ⁻¹' V
x : { x : X // x ∈ (↑U : Set X) }
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)
n : ℕ
hn :
  Membership.mem (α := Set (↑(↑U : Set X) : Type u_1)) (𝓝 x)
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n : Set (↑(↑U : Set X) : Type u_1))
⊢ 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) ∈
    map (Subtype.val (p := Membership.mem (↑U : Set X))) (𝓝 (Subtype.mk (p := Membership.mem (↑U : Set X)) (↑x : X) ⋯))

Tactic:
exacts [image_mem_map hn, (isOpen_of_mem_countableBasis U.2).mem_nhds x.2]

Premises used: Filter.image_mem_map, IsOpen.mem_nhds, TopologicalSpace.isOpen_of_mem_countableBasis, Subtype.property
-- 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
U : { x : Set X // x ∈ countableBasis X }
hUV : (↑U : Set X) ⊆ (⇑f : (a : X) → Y) ⁻¹' V
x : { x : X // x ∈ (↑U : Set X) }
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)
n : ℕ
hn :
  Membership.mem (α := Set (↑(↑U : Set X) : Type u_1)) (𝓝 x)
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n : Set (↑(↑U : Set X) : Type u_1))
h :
  MapsTo.{u_1, u_2} (α := { x : X // x ∈ (↑U : Set X) })
    ((⇑f : (a : X) → Y) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n) V
⊢ MapsTo.{u_1, u_2} (α := X) (⇑f : (a : X) → Y)
    (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))
    V

Tactic:
rw [mapsTo_image_iff]

Premises used: Set.mapsTo_image_iff
-- 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
U : { x : Set X // x ∈ countableBasis X }
hUV : (↑U : Set X) ⊆ (⇑f : (a : X) → Y) ⁻¹' V
x : { x : X // x ∈ (↑U : Set X) }
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)
n : ℕ
hn :
  Membership.mem (α := Set (↑(↑U : Set X) : Type u_1)) (𝓝 x)
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n : Set (↑(↑U : Set X) : Type u_1))
⊢ MapsTo.{u_1, u_2} (α := { x : X // x ∈ (↑U : Set X) })
    ((⇑f : (a : X) → Y) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n) V

Tactic:
fun y _ ↦ hUV y.2

Premises used: Set.Mem, setOf, Set.preimage, Set.MapsTo, Subtype.property
-- 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
U : { x : Set X // x ∈ countableBasis X }
hUV : (↑U : Set X) ⊆ (⇑f : (a : X) → Y) ⁻¹' V
x : { x : X // x ∈ (↑U : Set X) }
hxV : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) (↑x : X)
n : ℕ
hn :
  Membership.mem (α := Set (↑(↑U : Set X) : Type u_1)) (𝓝 x)
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n : Set (↑(↑U : Set X) : Type u_1))
⊢ MapsTo.{u_1, u_2} (α := { x : X // x ∈ (↑U : Set X) })
    ((⇑f : (a : X) → Y) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ (↑U : Set X)))
    ((K U : (a : ℕ) → Set (↑(↑U : Set X) : Type u_1)) n) V

Tactic:
exact fun y _ ↦ hUV y.2
-- 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
⊢ SeparableSpace C(X, Y)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.ContinuousMap.Sigma
Goal:
X : Type u_1
ι : Type u_2
Y : ι → Type u_3
inst : TopologicalSpace X
inst_1 : (i : ι) → TopologicalSpace (Y i)
inst_2 : Nonempty X
i : ι
g : ContinuousMap.{u_1, u_3} X (Y i)
i' : ι
g' : ContinuousMap.{u_1, u_3} X (Y i')
h :
  Eq (α := C(X, (i : ι) × Y i))
    ((fun (g : (i : ι) × ContinuousMap.{u_1, u_3} X (Y i)) ↦
        comp (sigmaMk (X := Y) (g.fst (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i))))
          (g.snd (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i))))
      (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i)) i g))
    ((fun (g : (i : ι) × ContinuousMap.{u_1, u_3} X (Y i)) ↦
        comp (sigmaMk (X := Y) (g.fst (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i))))
          (g.snd (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i))))
      (Sigma.mk (β := fun (i : ι) ↦ ContinuousMap.{u_1, u_3} X (Y i)) i' g'))
⊢ i = i' ∧ HEq (α := (a : X) → Y i) (⇑g : (a : X) → Y i) (β := (a : X) → Y i') (⇑g' : (a : X) → Y i')

Tactic:
Function.eq_of_sigmaMk_comp <| congr_arg DFunLike.coe h

Premises used: congr_arg, Function.eq_of_sigmaMk_comp, DFunLike.coe