awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (hypothesis)
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)
⊢ 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}
have 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}
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)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
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}
have 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)}
Tactic: refine mem_of_superset ((biInter_mem hsf).2 fun L hL ↦ ?_) hsub
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
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)}
have 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)}
Tactic: refine mem_iInf_of_mem _ <| mem_iInf_of_mem ?_ <| mem_principal_self _
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
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
⊢ ∃ (b : Set (Set C(X, Y))), b.Countable ∧ compactOpen = generateFrom b
have 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
Tactic: rcases hX with ⟨S, hScount, hScomp, hS⟩
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
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
have 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})
Tactic: refine ⟨_, ?_, compactOpen_eq_generateFrom (S := S) hScomp (isBasis_countableBasis _) ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
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})
⊢ ∃ (b : Set (Set C(X, Y))), b.Countable ∧ compactOpen = generateFrom b
have 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
Tactic: refine ⟨_, ?_, compactOpen_eq_generateFrom (S := S) hScomp (isBasis_countableBasis _) ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
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)
⊢ ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K V
have refine_2 : IsOpen[inst_1] V
Tactic: apply hS
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
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
⊢ ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) K V
have refine_2₁ : Membership.mem (γ := Set X) ((⇑f : (a : X) → Y) ⁻¹' V) x
Tactic: apply hS
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
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
⊢ SecondCountableTopology C(X, Y)
have 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
Tactic: apply secondCountableTopology
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (hypothesis)
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
⊢ ∃ (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
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
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)
⊢ ∃ (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
have 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
Tactic: use ⋃ U : countableBasis X, Set.range fun n ↦ K U n
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
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
have 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
Tactic: refine ⟨countable_iUnion fun _ ↦ countable_range _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
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
⊢ 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
have 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
Tactic: refine ⟨countable_iUnion fun _ ↦ countable_range _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
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)
⊢ ∀ (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
have 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
Tactic: simp only [mem_iUnion, mem_range]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
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 ∈ countableBasis X, x ∈ U ∧ U ⊆ (⇑f : (a : X) → Y) ⁻¹' V
have rw : (⇑f : (a : X) → Y) ⁻¹' V ∈ 𝓝 x
Tactic: rw [← (isBasis_countableBasis _).mem_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
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
⊢ ∃ (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
have 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
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
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.SecondCountableSpace (goal)
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
⊢ ∃ (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
have 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
Tactic: lift x to U using hxU
Cleared hypotheses: x, hxV, hxU