awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
A : Type u_2
inst_3 : Semiring A
inst_4 : 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)
rw :
  LE.le (α := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    (AlgHom.equalizer φ ψ)
⊢ LE.le (α := Subalgebra R C((↑s : Type u_1), R)) (polynomialFunctions s) (AlgHom.equalizer φ ψ)

Tactic:
rw [polynomialFunctions.eq_adjoin_X s]

Premises used: polynomialFunctions.eq_adjoin_X
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
A : Type u_2
inst_3 : Semiring A
inst_4 : 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 (α := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    (AlgHom.equalizer φ ψ)

Tactic:
φ.adjoin_le_equalizer ψ fun x hx => (Set.mem_singleton_iff.1 hx).symm ▸ h

Premises used: Eq.rec, Set.mem_singleton_iff, AlgHom.adjoin_le_equalizer, Iff.mp, Eq.symm
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
A : Type u_2
inst_3 : Semiring A
inst_4 : 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 (α := Subalgebra R C((↑s : Type u_1), R))
    R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))]
    (AlgHom.equalizer φ ψ)

Tactic:
exact φ.adjoin_le_equalizer ψ fun x hx => (Set.mem_singleton_iff.1 hx).symm ▸ h

Premises used: Eq.rec, Set.mem_singleton_iff, AlgHom.adjoin_le_equalizer, Iff.mp, Eq.symm
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
inst_3 : StarRing R
inst_4 : ContinuousStar R
s : Set R
rw :
  Eq (α := StarSubalgebra R C((↑s : Type u_1), R))
    (Subalgebra.starClosure
      R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : 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))))
rw₁ rw₂ :
  Eq (α := StarSubalgebra R C((↑s : Type u_1), R))
    (Subalgebra.starClosure
      R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))])
    (Subalgebra.starClosure
      R[((toContinuousMapOnAlgHom s : (a : R[X]) → C((↑s : Type u_1), R)) X : C((↑s : Type u_1), R))])
⊢ Eq (α := StarSubalgebra R C((↑s : Type u_1), R)) (Subalgebra.starClosure (polynomialFunctions s))
    (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))))

Tactic:
rw [polynomialFunctions.eq_adjoin_X s, adjoin_eq_starClosure_adjoin]

Premises used: polynomialFunctions.eq_adjoin_X, StarAlgebra.adjoin_eq_starClosure_adjoin
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
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)
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 φ ψ)
⊢ LE.le (α := StarSubalgebra R C((↑s : Type u_1), R)) (Subalgebra.starClosure (polynomialFunctions s))
    (StarAlgHom.equalizer φ ψ)

Tactic:
rw [polynomialFunctions.starClosure_eq_adjoin_X s]

Premises used: polynomialFunctions.starClosure_eq_adjoin_X
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
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))
    (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:
StarAlgHom.adjoin_le_equalizer φ ψ fun x hx => (Set.mem_singleton_iff.1 hx).symm ▸ h

Premises used: Eq.rec, StarAlgHom.adjoin_le_equalizer, Set.mem_singleton_iff, Iff.mp, Eq.symm
-- Module: Mathlib.Topology.ContinuousMap.Polynomial
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))
    (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:
exact StarAlgHom.adjoin_le_equalizer φ ψ fun x hx => (Set.mem_singleton_iff.1 hx).symm ▸ h

Premises used: StarAlgHom.adjoin_le_equalizer
-- 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
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}))
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
⊢ 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}))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
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)}
⊢ 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_rules [generateFrom_anti, image2_subset_iff.mpr]

Premises used: Iff.mpr, TopologicalSpace.generateFrom_anti, Set.image2_subset_iff
-- 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
K : Set X
hK : K ∈ S
t : Set (Set Y)
ht : Membership.mem (γ := Set (Set (Set Y))) {t : Set (Set Y) | t.Finite ∧ t ⊆ T} t
⊢ 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) K (⋃₀ t)}

Tactic:
mem_image2_of_mem (hS₁ K hK) (isOpen_sUnion fun _ h ↦ hT.isOpen <| ht.2 h)

Premises used: Set.Mem, TopologicalSpace.IsTopologicalBasis.isOpen, setOf, And.right, Set.mem_image2_of_mem, isOpen_sUnion
-- 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
K : Set X
hK : K ∈ S
t : Set (Set Y)
ht : Membership.mem (γ := Set (Set (Set Y))) {t : Set (Set Y) | t.Finite ∧ t ⊆ T} t
⊢ 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) K (⋃₀ t)}

Tactic:
exact mem_image2_of_mem (hS₁ K hK) (isOpen_sUnion fun _ h ↦ hT.isOpen <| ht.2 h)

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, And.right, Set.mem_image2_of_mem, isOpen_sUnion
-- 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
⊢ 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:
le_of_nhds_le_nhds fun f ↦ ?_

Premises used: le_of_nhds_le_nhds
-- 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
a : ∀ (f : C(X, Y)), 𝓝 f ≤ 𝓝 f
⊢ 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:
refine le_of_nhds_le_nhds fun f ↦ ?_

Premises used: le_of_nhds_le_nhds
-- 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)
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
⊢ 𝓝 f ≤ 𝓝 f

Tactic:
simp only [nhds_compactOpen, le_iInf_iff, le_principal_iff]

Premises used: Filter.le_principal_iff, le_iInf_iff, ContinuousMap.nhds_compactOpen
-- 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
a :
  ∀ (hK : IsCompact K) (i : Set Y) (i_1 : IsOpen[inst_1] i) (i_2 : MapsTo (⇑f : (a : X) → Y) K i),
    {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K i} ∈ 𝓝 f
⊢ ∀ (i : IsCompact K) (i : Set Y) (i_1 : IsOpen[inst_1] i) (i_2 : MapsTo (⇑f : (a : X) → Y) K i),
    {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K i} ∈ 𝓝 f

Tactic:
(hK : IsCompact K)
-- 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
a : ∀ (hU : IsOpen[inst_1] U) (i : MapsTo (⇑f : (a : X) → Y) K U), {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U} ∈ 𝓝 f
⊢ ∀ (i : IsOpen[inst_1] U) (i : MapsTo (⇑f : (a : X) → Y) K U), {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U} ∈ 𝓝 f

Tactic:
(hU : IsOpen U)
-- 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
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}
⊢ {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) K U} ∈ 𝓝 f

Tactic:
simp only [TopologicalSpace.nhds_generateFrom]

Premises used: TopologicalSpace.nhds_generateFrom
-- 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
⊢ 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

Premises used: Set.mapsTo_iff_image_subset, Set.sUnion_eq_biUnion, TopologicalSpace.IsTopologicalBasis.open_eq_sUnion'
-- 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 :
  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)
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
⊢ ∃ 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

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, IsCompact.elim_finite_subcover_image, ContinuousMapClass.map_continuous, IsCompact.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 :
  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

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

Premises used: And.right, And.left, And.intro, Exists.intro
-- 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 :
  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)
refine : (⇑f : (a : X) → Y) '' K ⊆ ⋃₀ t
⊢ ∃ t ⊆ T, t.Finite ∧ (∀ V ∈ t, V ⊆ U) ∧ (⇑f : (a : X) → Y) '' K ⊆ ⋃₀ t

Tactic:
refine ⟨t, fun _ h ↦ (ht h).1, hfin, fun _ h ↦ (ht h).2, ?_⟩
-- 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 :
  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)
rwa rwa₁ rwa₂ rwa₃ : Subset.{u_2} (α := Set Y) ((⇑f : (a : X) → Y) '' K) (⋃ i ∈ t, i)
⊢ (⇑f : (a : X) → Y) '' K ⊆ ⋃₀ t

Tactic:
rwa [sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- 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
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}
⊢ 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]
-- 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 : (⇑f : (a : X) → Y) '' K ⊆ ⋃₀ t
⊢ K ⊆ (⇑f : (a : X) → Y) ⁻¹' ⋃₀ t

Tactic:
rw [image_subset_iff] at hKT

Premises used: Set.image_subset_iff