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
x : X
hx : x ∈ K
rcases :
  ∀ (V : Set Y) (hVt : V ∈ t) (hxV : Membership.mem (α := Y) V ((f : (a : X) → Y) x : Y)),
    ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) L (⋃₀ t)
⊢ ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) L (⋃₀ t)

Tactic:
rcases hKT hx with ⟨V, hVt, hxV⟩
-- 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
x : X
hx : x ∈ K
V : Set Y
hVt : V ∈ t
hxV : Membership.mem (α := Y) V ((f : (a : X) → Y) x : Y)
rcases :
  ∀ (L : Set X) (hLS : L ∈ S) (hLx : L ∈ 𝓝 x) (hLV : MapsTo (⇑f : (a : X) → Y) L V),
    ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) L (⋃₀ t)
⊢ ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) L (⋃₀ t)

Tactic:
rcases hS₂ f x V (htT hVt) hxV with ⟨L, hLS, hLx, hLV⟩
-- 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
x : X
hx : x ∈ K
V : Set Y
hVt : V ∈ t
hxV : Membership.mem (α := Y) V ((f : (a : X) → Y) x : Y)
L : Set X
hLS : L ∈ S
hLx : L ∈ 𝓝 x
hLV : MapsTo (⇑f : (a : X) → Y) L V
⊢ ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) L (⋃₀ t)

Tactic:
⟨L, hLS, hLx, hLV.mono_right <| subset_sUnion_of_mem hVt⟩

Premises used: Set.MapsTo.mono_right, And.intro, Exists.intro, Set.subset_sUnion_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
x : X
hx : x ∈ K
V : Set Y
hVt : V ∈ t
hxV : Membership.mem (α := Y) V ((f : (a : X) → Y) x : Y)
L : Set X
hLS : L ∈ S
hLx : L ∈ 𝓝 x
hLV : MapsTo (⇑f : (a : X) → Y) L V
⊢ ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) L (⋃₀ t)

Tactic:
exact ⟨L, hLS, hLx, hLV.mono_right <| subset_sUnion_of_mem hVt⟩
-- 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
⊢ ∀ x ∈ K, ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) L (⋃₀ t)

Tactic:
have : ∀ x ∈ K, ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo f L (⋃₀ t) := by
        intro x hx
        rcases hKT hx with ⟨V, hVt, hxV⟩
        rcases hS₂ f x V (htT hVt) hxV with ⟨L, hLS, hLx, hLV⟩
        exact ⟨L, hLS, hLx, hLV.mono_right <| subset_sUnion_of_mem hVt⟩
-- 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
this : ∀ x ∈ K, ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) L (⋃₀ t)
choose! :
  ∀ (L : (x : X) → Set X) (hLS : ∀ x ∈ K, L x ∈ S) (hLmem : ∀ x ∈ K, L x ∈ 𝓝 x)
    (hLt : ∀ x ∈ K, MapsTo (⇑f : (a : X) → Y) (L x) (⋃₀ t)),
    ∃ s ⊆ S, s.Finite ∧ K ⊆ ⋃₀ s ∧ MapsTo (⇑f : (a : X) → Y) (⋃₀ s) (⋃₀ t)
⊢ ∃ s ⊆ S, s.Finite ∧ K ⊆ ⋃₀ s ∧ MapsTo (⇑f : (a : X) → Y) (⋃₀ s) (⋃₀ t)

Tactic:
choose! L hLS hLmem hLt using this
-- 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
L : (x : X) → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f : (a : X) → Y) (L x) (⋃₀ t)
rcases :
  ∀ (s : Finset X) (hsK : ∀ x ∈ s, x ∈ K) (hs : K ⊆ ⋃ x ∈ s, L x),
    ∃ s ⊆ S, s.Finite ∧ K ⊆ ⋃₀ s ∧ MapsTo (⇑f : (a : X) → Y) (⋃₀ s) (⋃₀ t)
⊢ ∃ s ⊆ S, s.Finite ∧ K ⊆ ⋃₀ s ∧ MapsTo (⇑f : (a : X) → Y) (⋃₀ s) (⋃₀ t)

Tactic:
rcases hK.elim_nhds_subcover L hLmem with ⟨s, hsK, hs⟩

Premises used: IsCompact.elim_nhds_subcover
-- 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
L : (x : X) → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f : (a : X) → Y) (L x) (⋃₀ t)
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hs : K ⊆ ⋃ x ∈ s, L x
rwa rwa₁ rwa₂ rwa₃ : K ⊆ ⋃ a ∈ (↑s : Set X), L a
⊢ K ⊆ ⋃₀ (L '' (↑s : Set X))

Tactic:
rwa [sUnion_image]

Premises used: Set.sUnion_image
-- 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
L : (x : X) → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f : (a : X) → Y) (L x) (⋃₀ t)
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hs : K ⊆ ⋃ x ∈ s, L x
refine : MapsTo (⇑f : (a : X) → Y) (⋃₀ (L '' (↑s : Set X))) (⋃₀ t)
⊢ ∃ s ⊆ S, s.Finite ∧ K ⊆ ⋃₀ s ∧ MapsTo (⇑f : (a : X) → Y) (⋃₀ s) (⋃₀ t)

Tactic:
refine ⟨L '' s, image_subset_iff.2 fun x hx ↦ hLS x <| hsK x hx, s.finite_toSet.image _,
        by rwa [sUnion_image], ?_⟩
-- 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
L : (x : X) → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f : (a : X) → Y) (L x) (⋃₀ t)
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hs : K ⊆ ⋃ x ∈ s, L x
rw : ∀ ⦃x : X⦄, x ∈ (↑s : Set X) → MapsTo (⇑f : (a : X) → Y) (L x) (⋃₀ t)
⊢ MapsTo (⇑f : (a : X) → Y) (⋃₀ (L '' (↑s : Set X))) (⋃₀ t)

Tactic:
rw [mapsTo_sUnion, forall_mem_image]

Premises used: Set.mapsTo_sUnion, Set.forall_mem_image
-- 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
L : (x : X) → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f : (a : X) → Y) (L x) (⋃₀ t)
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hs : K ⊆ ⋃ x ∈ s, L x
⊢ ∀ ⦃x : X⦄, x ∈ (↑s : Set X) → MapsTo (⇑f : (a : X) → Y) (L x) (⋃₀ t)

Tactic:
fun x hx ↦ hLt x <| hsK x hx
-- 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
L : (x : X) → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f : (a : X) → Y) (L x) (⋃₀ t)
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hs : K ⊆ ⋃ x ∈ s, L x
⊢ ∀ ⦃x : X⦄, x ∈ (↑s : Set X) → MapsTo (⇑f : (a : X) → Y) (L x) (⋃₀ t)

Tactic:
exact fun x hx ↦ hLt x <| hsK x hx
-- 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
a :
  ∀ (s : Set (Set X)) (hsS : s ⊆ S) (hsf : s.Finite) (hKs : K ⊆ ⋃₀ s) (hst : MapsTo (⇑f : (a : X) → Y) (⋃₀ s) (⋃₀ 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) K U}
⊢ 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) K U}

Tactic:
obtain ⟨s, hsS, hsf, hKs, hst⟩ : ∃ s ⊆ S, s.Finite ∧ K ⊆ ⋃₀ s ∧ MapsTo f (⋃₀ s) (⋃₀ t) := by
      have : ∀ x ∈ K, ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo f L (⋃₀ t) := by
        intro x hx
        rcases hKT hx with ⟨V, hVt, hxV⟩
        rcases hS₂ f x V (htT hVt) hxV with ⟨L, hLS, hLx, hLV⟩
        exact ⟨L, hLS, hLx, hLV.mono_right <| subset_sUnion_of_mem hVt⟩
      choose! L hLS hLmem hLt using this
      rcases hK.elim_nhds_subcover L hLmem with ⟨s, hsK, hs⟩
      refine ⟨L '' s, image_subset_iff.2 fun x hx ↦ hLS x <| hsK x hx, s.finite_toSet.image _,
        by rwa [sUnion_image], ?_⟩
      rw [mapsTo_sUnion, forall_mem_image]
      exact fun x hx ↦ hLt x <| hsK x hx
-- 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)
simp :
  Subset (α := Set C(X, Y)) {x : C(X, Y) | MapsTo (⇑x : (a : X) → Y) (⋃₀ s) (⋃₀ t)}
    {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U}
⊢ 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}

Tactic:
simp only [← setOf_forall, ← mapsTo_iUnion, ← sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion, Set.mapsTo_iUnion, Set.setOf_forall
-- 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)
⊢ Subset (α := Set C(X, Y)) {x : C(X, Y) | MapsTo (⇑x : (a : X) → Y) (⋃₀ s) (⋃₀ t)}
    {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U}

Tactic:
fun g hg ↦ hg.mono hKs (sUnion_subset hTU)

Premises used: Set.Mem, setOf, Set.MapsTo.mono, Set.sUnion_subset, Set.Subset, Set.MapsTo
-- 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)
⊢ Subset (α := Set C(X, Y)) {x : C(X, Y) | MapsTo (⇑x : (a : X) → Y) (⋃₀ s) (⋃₀ t)}
    {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U}

Tactic:
exact fun g hg ↦ hg.mono hKs (sUnion_subset hTU)
-- 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)
⊢ 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}

Tactic:
have hsub : (⋂ L ∈ s, {g : C(X, Y) | MapsTo g L (⋃₀ t)}) ⊆ {g | MapsTo g K U} := by
      simp only [← setOf_forall, ← mapsTo_iUnion, ← sUnion_eq_biUnion]
      exact fun g hg ↦ hg.mono hKs (sUnion_subset hTU)
-- 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}
⊢ 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) K U}

Tactic:
mem_of_superset ((biInter_mem hsf).2 fun L hL ↦ ?_) hsub

Premises used: Iff.mpr, Filter.biInter_mem, Filter.mem_of_superset
-- 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}
a :
  ∀ (L : Set X) (hL : L ∈ s),
    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)}
⊢ 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) K U}

Tactic:
refine mem_of_superset ((biInter_mem hsf).2 fun L hL ↦ ?_) hsub

Premises used: Iff.mpr, Filter.biInter_mem, Filter.mem_of_superset
-- 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 (γ := 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:
mem_iInf_of_mem _ <| mem_iInf_of_mem ?_ <| mem_principal_self _

Premises used: Filter.mem_principal_self, Set.Mem, setOf, Filter.mem_iInf_of_mem