-- Mathlib/Topology/ContinuousMap/SecondCountableSpace.lean
theorem compactOpen_eq_generateFrom {S : Set (Set X)} {T : Set (Set Y)}
    (hS₁ : ∀ K ∈ S, IsCompact K) (hT : IsTopologicalBasis T)
    (hS₂ : ∀ f : C(X, Y), ∀ x, ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo f K V) :
    compactOpen = .generateFrom (.image2 (fun K t ↦
      {f : C(X, Y) | MapsTo f K (⋃₀ t)}) S {t : Set (Set Y) | t.Finite ∧ t ⊆ T})

Proof state:
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : 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, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen U
hfKU : ⇑f '' K ⊆ ⋃ i ∈ {s | s ∈ T ∧ s ⊆ U}, i
t : Set (Set Y)
ht : t ⊆ {s | s ∈ T ∧ s ⊆ U}
hfin : t.Finite
htK : ⇑f '' K ⊆ ⋃ i ∈ t, i
⊢ ∃ t ⊆ T, t.Finite ∧ (∀ V ∈ t, V ⊆ U) ∧ ⇑f '' K ⊆ ⋃₀ t

Tactic:
refine ⟨t, fun _ h ↦ (ht h).1, hfin, fun _ h ↦ (ht h).2, ?_⟩

Result:
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : 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, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen U
hfKU : ⇑f '' K ⊆ ⋃ i ∈ {s | s ∈ T ∧ s ⊆ U}, i
t : Set (Set Y)
ht : t ⊆ {s | s ∈ T ∧ s ⊆ U}
hfin : t.Finite
htK : ⇑f '' K ⊆ ⋃ i ∈ t, i
⊢ ⇑f '' K ⊆ ⋃₀ t

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : 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, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
L : X → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f) (L x) (⋃₀ t)
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hs : K ⊆ ⋃ x ∈ s, L x
⊢ ∀ ⦃x : X⦄, x ∈ ↑s → MapsTo (⇑f) (L x) (⋃₀ t)

Tactic:
exact fun x hx ↦ hLt x <| hsK x hx

Result:
no goals

Proof state:
case a.intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : 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, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
s : Set (Set X)
hsS : s ⊆ S
hsf : s.Finite
hKs : K ⊆ ⋃₀ s
hst : MapsTo (⇑f) (⋃₀ s) (⋃₀ t)
hsub : ⋂ L ∈ s, {g | MapsTo (⇑g) L (⋃₀ t)} ⊆ {g | MapsTo (⇑g) K U}
⊢ {g | MapsTo (⇑g) K U} ∈
    ⨅ s ∈ {s | f ∈ s ∧ s ∈ image2 (fun K t => {f | MapsTo (⇑f) K (⋃₀ t)}) S {t | t.Finite ∧ t ⊆ T}}, 𝓟 s

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

Result:
case a.intro.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : 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, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
s : Set (Set X)
hsS : s ⊆ S
hsf : s.Finite
hKs : K ⊆ ⋃₀ s
hst : MapsTo (⇑f) (⋃₀ s) (⋃₀ t)
hsub : ⋂ L ∈ s, {g | MapsTo (⇑g) L (⋃₀ t)} ⊆ {g | MapsTo (⇑g) K U}
L : Set X
hL : L ∈ s
⊢ {g | MapsTo (⇑g) L (⋃₀ t)} ∈
    ⨅ s ∈ {s | f ∈ s ∧ s ∈ image2 (fun K t => {f | MapsTo (⇑f) K (⋃₀ t)}) S {t | t.Finite ∧ t ⊆ T}}, 𝓟 s

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : 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, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
⊢ ∃ s ⊆ S, s.Finite ∧ K ⊆ ⋃₀ s ∧ MapsTo (⇑f) (⋃₀ s) (⋃₀ 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⟩

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : 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, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
this : ∀ x ∈ K, ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo (⇑f) L (⋃₀ t)
⊢ ∃ s ⊆ S, s.Finite ∧ K ⊆ ⋃₀ s ∧ MapsTo (⇑f) (⋃₀ s) (⋃₀ t)

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : 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, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
x : X
hx : x ∈ K
V : Set Y
hVt : V ∈ t
hxV : f x ∈ V
⊢ ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo (⇑f) L (⋃₀ t)

Tactic:
rcases hS₂ f x V (htT hVt) hxV with ⟨L, hLS, hLx, hLV⟩

Result:
case intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : 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, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
x : X
hx : x ∈ K
V : Set Y
hVt : V ∈ t
hxV : f x ∈ V
L : Set X
hLS : L ∈ S
hLx : L ∈ 𝓝 x
hLV : MapsTo (⇑f) L V
⊢ ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo (⇑f) L (⋃₀ t)

Proof state:
case a
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : 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, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen U
hfKU : MapsTo (⇑f) K U
⊢ {g | MapsTo (⇑g) K U} ∈
    ⨅ s ∈ {s | f ∈ s ∧ s ∈ image2 (fun K t => {f | MapsTo (⇑f) K (⋃₀ t)}) S {t | t.Finite ∧ t ⊆ T}}, 𝓟 s

Tactic:
obtain ⟨t, htT, htf, hTU, hKT⟩ : ∃ t ⊆ T, t.Finite ∧ (∀ V ∈ t, V ⊆ U) ∧ f '' K ⊆ ⋃₀ t := by
  rw [hT.open_eq_sUnion' hU, mapsTo', sUnion_eq_biUnion] at hfKU
  obtain ⟨t, ht, hfin, htK⟩ :=
    (hK.image (map_continuous f)).elim_finite_subcover_image (fun V hV ↦ hT.isOpen hV.1) hfKU
  refine ⟨t, fun _ h ↦ (ht h).1, hfin, fun _ h ↦ (ht h).2, ?_⟩
  rwa [sUnion_eq_biUnion]

Result:
case a.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : 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, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : ⇑f '' K ⊆ ⋃₀ t
⊢ {g | MapsTo (⇑g) K U} ∈
    ⨅ s ∈ {s | f ∈ s ∧ s ∈ image2 (fun K t => {f | MapsTo (⇑f) K (⋃₀ t)}) S {t | t.Finite ∧ t ⊆ T}}, 𝓟 s