awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Polynomial (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
A : Type u_2
inst_3 : StarRing R
inst_4 : ContinuousStar R
inst_5 : Semiring A
inst_6 : StarRing A
inst_7 : Algebra R A
s : Set R
φ ψ : C((↑s : Type u_1), R) →⋆ₐ[R] A
h :
  Eq.{u_2 + 1} (α := A)
    ((φ : (a : C((↑s : Type u_1), R)) → A)
        ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R)) :
      A)
    ((ψ : (a : C((↑s : Type u_1), R)) → A)
        ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R)) :
      A)
⊢ LE.le (α := StarSubalgebra R C((↑s : Type u_1), R)) (Subalgebra.starClosure (polynomialFunctions s))
    (StarAlgHom.equalizer φ ψ)
have rw : LE.le (α := StarSubalgebra R C((↑s : Type u_1), R))
  (adjoin R
    (singleton (α := C((↑s : Type u_1), R))
      ((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))))
  (StarAlgHom.equalizer φ ψ)
Tactic: rw [polynomialFunctions.starClosure_eq_adjoin_X s]
-- 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
⊢ Eq (α := TopologicalSpace C(X, Y)) compactOpen
    (generateFrom
      (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}))
have a : LE.le (α := TopologicalSpace C(X, Y)) compactOpen
  (generateFrom
    (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}))
Tactic: apply le_antisymm
-- 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
a :
  LE.le (α := TopologicalSpace C(X, Y)) compactOpen
    (generateFrom
      (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}))
⊢ Eq (α := TopologicalSpace C(X, Y)) compactOpen
    (generateFrom
      (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}))
have a₁ : LE.le (α := TopologicalSpace C(X, Y))
  (generateFrom
    (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}))
  compactOpen
Tactic: apply le_antisymm
-- 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
⊢ LE.le (α := TopologicalSpace C(X, Y)) compactOpen
    (generateFrom
      (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}))
have a : ∀ x ∈ S,
  ∀ (y : Set (Set Y)),
    Membership.mem (γ := Set (Set (Set Y))) {t : Set (Set Y) | t.Finite ∧ t ⊆ T} y →
      Membership.mem (γ := Set (Set C(X, Y)))
        (image2 (fun (K : Set X) (U : Set Y) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U}) {K : Set X | IsCompact K}
          {U : Set Y | IsOpen[inst_1] U})
        {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) x (⋃₀ y)}
Tactic: apply_rules [generateFrom_anti, image2_subset_iff.mpr]
-- 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
⊢ LE.le (α := TopologicalSpace C(X, Y))
    (generateFrom
      (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}))
    compactOpen
have a : ∀ (f : C(X, Y)), 𝓝 f ≤ 𝓝 f
Tactic: refine le_of_nhds_le_nhds fun f ↦ ?_
-- 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)
⊢ 𝓝 f ≤ 𝓝 f
have a : ∀ (i : Set X) (i_1 : IsCompact i) (i_2 : Set Y) (i_3 : IsOpen[inst_1] i_2) (i_4 : MapsTo (⇑f : (a : X) → Y) i i_2),
  {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) i i_2} ∈ 𝓝 f
Tactic: simp only [nhds_compactOpen, le_iInf_iff, le_principal_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
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
⊢ {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U} ∈ 𝓝 f
have a : 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: simp only [TopologicalSpace.nhds_generateFrom]
-- 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 ⊆ T, t.Finite ∧ (∀ V ∈ t, V ⊆ U) ∧ (⇑f : (a : X) → Y) '' K ⊆ ⋃₀ t
have hfKU₁ : Subset.{u_2} (α := Set Y) ((⇑f : (a : X) → Y) '' K)
  (⋃ (i : Set Y), ⋃ (_ : Membership.mem (γ := Set (Set Y)) {s : Set Y | s ∈ T ∧ s ⊆ U} i), i)
Tactic: rw [hT.open_eq_sUnion' hU, mapsTo_iff_image_subset, sUnion_eq_biUnion] at hfKU
Cleared hypotheses: hfKU
-- 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 :
  Subset.{u_2} (α := Set Y) ((⇑f : (a : X) → Y) '' K)
    (⋃ (i : Set Y), ⋃ (_ : Membership.mem (γ := Set (Set Y)) {s : Set Y | s ∈ T ∧ s ⊆ U} i), i)
⊢ ∃ t ⊆ T, t.Finite ∧ (∀ V ∈ t, V ⊆ U) ∧ (⇑f : (a : X) → Y) '' K ⊆ ⋃₀ t
have obtain : ∀ (t : Set (Set Y)) (ht : t ⊆ {s : Set Y | s ∈ T ∧ s ⊆ U}) (hfin : t.Finite)
  (htK : Subset.{u_2} (α := Set Y) ((⇑f : (a : X) → Y) '' K) (⋃ i ∈ t, i)),
  ∃ t ⊆ T, t.Finite ∧ (∀ V ∈ t, V ⊆ U) ∧ (⇑f : (a : X) → Y) '' K ⊆ ⋃₀ t
Tactic: obtain ⟨t, ht, hfin, htK⟩ :=
        (hK.image (map_continuous f)).elim_finite_subcover_image (fun V hV ↦ hT.isOpen hV.1) hfKU
-- 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 :
  Subset.{u_2} (α := Set Y) ((⇑f : (a : X) → Y) '' K)
    (⋃ (i : Set Y), ⋃ (_ : Membership.mem (γ := Set (Set Y)) {s : Set Y | s ∈ T ∧ s ⊆ U} i), i)
t : Set (Set Y)
ht : t ⊆ {s : Set Y | s ∈ T ∧ s ⊆ U}
hfin : t.Finite
htK : Subset.{u_2} (α := Set Y) ((⇑f : (a : X) → Y) '' K) (⋃ i ∈ t, i)
⊢ ∃ t ⊆ T, t.Finite ∧ (∀ V ∈ t, V ⊆ U) ∧ (⇑f : (a : X) → Y) '' K ⊆ ⋃₀ t
have refine : (⇑f : (a : X) → Y) '' K ⊆ ⋃₀ t
Tactic: refine ⟨t, fun _ h ↦ (ht h).1, hfin, fun _ h ↦ (ht h).2, ?_⟩
-- 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
⊢ 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 : ∀ (t : Set (Set Y)) (htT : t ⊆ T) (htf : t.Finite) (hTU : ∀ V ∈ t, V ⊆ U) (hKT : (⇑f : (a : X) → Y) '' K ⊆ ⋃₀ 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: 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_iff_image_subset, 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]
-- 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 : (⇑f : (a : X) → Y) '' K ⊆ ⋃₀ 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 hKT₁ : K ⊆ (⇑f : (a : X) → Y) ⁻¹' ⋃₀ t
Tactic: rw [image_subset_iff] at hKT
Cleared hypotheses: hKT
-- 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
x : X
hx : x ∈ K
⊢ ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) L (⋃₀ t)
have 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)
Tactic: rcases hKT hx with ⟨V, hVt, 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
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 ∈ S, L ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) L (⋃₀ t)
have 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)
Tactic: rcases hS₂ f x V (htT hVt) hxV with ⟨L, hLS, hLx, hLV⟩
-- 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 ⊆ S, s.Finite ∧ K ⊆ ⋃₀ s ∧ MapsTo (⇑f : (a : X) → Y) (⋃₀ s) (⋃₀ t)
have this : ∀ 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⟩
-- 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
this : ∀ x ∈ K, ∃ L ∈ S, L ∈ 𝓝 x ∧ MapsTo (⇑f : (a : X) → Y) L (⋃₀ t)
⊢ ∃ s ⊆ S, s.Finite ∧ K ⊆ ⋃₀ s ∧ MapsTo (⇑f : (a : X) → Y) (⋃₀ s) (⋃₀ t)
have 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)
Tactic: choose! L hLS hLmem hLt using this
Cleared hypotheses: this
-- 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
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)
have 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)
Tactic: rcases hK.elim_nhds_subcover L hLmem with ⟨s, hsK, 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
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
⊢ K ⊆ ⋃₀ (L '' (↑s : Set X))
have rwa : K ⊆ ⋃ a ∈ (↑s : Set X), L a
Tactic: rwa [sUnion_image]
-- 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
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
⊢ ∃ s ⊆ S, s.Finite ∧ K ⊆ ⋃₀ s ∧ MapsTo (⇑f : (a : X) → Y) (⋃₀ s) (⋃₀ t)
have refine : MapsTo (⇑f : (a : X) → Y) (⋃₀ (L '' (↑s : Set X))) (⋃₀ 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], ?_⟩
-- 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
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
⊢ MapsTo (⇑f : (a : X) → Y) (⋃₀ (L '' (↑s : Set X))) (⋃₀ t)
have rw : ∀ ⦃x : X⦄, x ∈ (↑s : Set X) → MapsTo (⇑f : (a : X) → Y) (L x) (⋃₀ t)
Tactic: rw [mapsTo_sUnion, forall_mem_image]
-- 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
⊢ 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 : ∀ (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}
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
-- 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)
⊢ 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}
have 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}
Tactic: simp only [← setOf_forall, ← mapsTo_iUnion, ← sUnion_eq_biUnion]