awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : Membership.mem (γ := Filter Y) (𝓝 1) V
W : Set Y
hWo : Membership.mem (γ := Filter Y) (𝓝 1) W
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S2 : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe (β := fun (x : X) ↦ Y) '' S3
hS4 : S4 = DFunLike.coe (β := fun (x : X) ↦ Y) '' S1
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
⊢ ∀ (x : X → Y),
    (∃ (x_1 : X →* Y), Set.MapsTo (⇑x_1 : (a : X) → Y) U W ∧ (⇑x_1 : (a : X) → Y) = x) ↔
      Membership.mem (γ := Set (X → Y))
        ((U.pi (α := fun (x : X) ↦ Y) fun (x : X) ↦ W) ∩ Set.range (ι := X →* Y) (DFunLike.coe (β := fun (x : X) ↦ Y)))
        x

Tactic:
fun f ↦ ⟨fun ⟨g, hg, hf⟩ ↦ hf ▸ ⟨hg, g, rfl⟩, fun ⟨hg, g, hf⟩ ↦ ⟨g, hf ▸ hg, hf⟩⟩

Premises used: _private.0.ContinuousMonoidHom.locallyCompactSpace_of_equicontinuousAt.match_2, Membership.mem, Exists, Eq.rec, Inter.inter, And, Set.MapsTo, And.intro, Iff.intro, Exists.intro, Set.pi, Set.range, _private.0.ContinuousMonoidHom.locallyCompactSpace_of_equicontinuousAt.match_3, Eq.symm, Eq, DFunLike.coe, rfl
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : Membership.mem (γ := Filter Y) (𝓝 1) V
W : Set Y
hWo : Membership.mem (γ := Filter Y) (𝓝 1) W
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S2 : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe (β := fun (x : X) ↦ Y) '' S3
hS4 : S4 = DFunLike.coe (β := fun (x : X) ↦ Y) '' S1
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
⊢ ∀ (x : X → Y),
    (∃ (x_1 : X →* Y), Set.MapsTo (⇑x_1 : (a : X) → Y) U W ∧ (⇑x_1 : (a : X) → Y) = x) ↔
      Membership.mem (γ := Set (X → Y))
        ((U.pi (α := fun (x : X) ↦ Y) fun (x : X) ↦ W) ∩ Set.range (ι := X →* Y) (DFunLike.coe (β := fun (x : X) ↦ Y)))
        x

Tactic:
exact fun f ↦ ⟨fun ⟨g, hg, hf⟩ ↦ hf ▸ ⟨hg, g, rfl⟩, fun ⟨hg, g, hf⟩ ↦ ⟨g, hf ▸ hg, hf⟩⟩
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : Membership.mem (γ := Filter Y) (𝓝 1) V
W : Set Y
hWo : Membership.mem (γ := Filter Y) (𝓝 1) W
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S2 : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe (β := fun (x : X) ↦ Y) '' S3
hS4 : S4 = DFunLike.coe (β := fun (x : X) ↦ Y) '' S1
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
⊢ S4 = (U.pi (α := fun (x : X) ↦ Y) fun (x : X) ↦ W) ∩ Set.range (ι := X →* Y) (DFunLike.coe (β := fun (x : X) ↦ Y))

Tactic:
replace hS4 : S4 = Set.pi U (fun _ ↦ W) ∩ Set.range ((↑) : (X →* Y) → (X → Y)) := by
    simp_rw [hS4, Set.ext_iff, Set.mem_image, S1, Set.mem_setOf_eq]
    exact fun f ↦ ⟨fun ⟨g, hg, hf⟩ ↦ hf ▸ ⟨hg, g, rfl⟩, fun ⟨hg, g, hf⟩ ↦ ⟨g, hf ▸ hg, hf⟩⟩
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : Membership.mem (γ := Filter Y) (𝓝 1) V
W : Set Y
hWo : Membership.mem (γ := Filter Y) (𝓝 1) W
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S2 : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe (β := fun (x : X) ↦ Y) '' S3
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
hS4 : S4 = (U.pi (α := fun (x : X) ↦ Y) fun (x : X) ↦ W) ∩ Set.range (ι := X →* Y) (DFunLike.coe (β := fun (x : X) ↦ Y))
⊢ IsClosed[Pi.topologicalSpace] S4

Tactic:
replace hS4 : IsClosed S4 :=
    hS4.symm ▸ (isClosed_set_pi (fun _ _ ↦ hWc.isClosed)).inter (MonoidHom.isClosed_range_coe X Y)
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : Membership.mem (γ := Filter Y) (𝓝 1) V
W : Set Y
hWo : Membership.mem (γ := Filter Y) (𝓝 1) W
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S2 : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe (β := fun (x : X) ↦ Y) '' S3
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
hS4 : IsClosed[Pi.topologicalSpace] S4
T : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U (interior W)}
⊢ T.Nonempty

Tactic:
have h1 : T.Nonempty := ⟨1, fun _ _ ↦ mem_interior_iff_mem_nhds.mpr hWo⟩
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : Membership.mem (γ := Filter Y) (𝓝 1) V
W : Set Y
hWo : Membership.mem (γ := Filter Y) (𝓝 1) W
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S2 : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe (β := fun (x : X) ↦ Y) '' S3
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
hS4 : IsClosed[Pi.topologicalSpace] S4
T : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U (interior W)}
h1 : T.Nonempty
⊢ T ⊆ S2

Tactic:
have h2 : T ⊆ S2 := fun f hf ↦ hf.mono_right interior_subset
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : Membership.mem (γ := Filter Y) (𝓝 1) V
W : Set Y
hWo : Membership.mem (γ := Filter Y) (𝓝 1) W
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S2 : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe (β := fun (x : X) ↦ Y) '' S3
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
hS4 : IsClosed[Pi.topologicalSpace] S4
T : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U (interior W)}
h1 : T.Nonempty
h2 : T ⊆ S2
⊢ IsOpen T

Tactic:
have h3 : IsOpen T := isOpen_induced (ContinuousMap.isOpen_setOf_mapsTo hU isOpen_interior)
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : Membership.mem (γ := Filter Y) (𝓝 1) V
W : Set Y
hWo : Membership.mem (γ := Filter Y) (𝓝 1) W
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S2 : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe (β := fun (x : X) ↦ Y) '' S3
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
hS4 : IsClosed[Pi.topologicalSpace] S4
T : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U (interior W)}
h1 : T.Nonempty
h2 : T ⊆ S2
h3 : IsOpen T
⊢ (interior S2).Nonempty

Tactic:
h1.mono (interior_maximal h2 h3)

Premises used: interior_maximal, Set.Nonempty.mono
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : Membership.mem (γ := Filter Y) (𝓝 1) V
W : Set Y
hWo : Membership.mem (γ := Filter Y) (𝓝 1) W
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S2 : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe (β := fun (x : X) ↦ Y) '' S3
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
hS4 : IsClosed[Pi.topologicalSpace] S4
T : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U (interior W)}
h1 : T.Nonempty
h2 : T ⊆ S2
h3 : IsOpen T
⊢ (interior S2).Nonempty

Tactic:
exact h1.mono (interior_maximal h2 h3)

Premises used: interior_maximal, Set.Nonempty.mono
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : Membership.mem (γ := Filter Y) (𝓝 1) V
W : Set Y
hWo : Membership.mem (γ := Filter Y) (𝓝 1) W
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S2 : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe (β := fun (x : X) ↦ Y) '' S3
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
hS4 : IsClosed[Pi.topologicalSpace] S4
⊢ (interior S2).Nonempty

Tactic:
have hS2 : (interior S2).Nonempty := by
    let T : Set (ContinuousMonoidHom X Y) := {f | Set.MapsTo f U (interior W)}
    have h1 : T.Nonempty := ⟨1, fun _ _ ↦ mem_interior_iff_mem_nhds.mpr hWo⟩
    have h2 : T ⊆ S2 := fun f hf ↦ hf.mono_right interior_subset
    have h3 : IsOpen T := isOpen_induced (ContinuousMap.isOpen_setOf_mapsTo hU isOpen_interior)
    exact h1.mono (interior_maximal h2 h3)
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : Membership.mem (γ := Filter Y) (𝓝 1) V
W : Set Y
hWo : Membership.mem (γ := Filter Y) (𝓝 1) W
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S2 : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe (β := fun (x : X) ↦ Y) '' S3
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
hS4 : IsClosed[Pi.topologicalSpace] S4
hS2 : (interior S2).Nonempty
⊢ LocallyCompactSpace (X →ₜ* Y)

Tactic:
TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group
    ⟨⟨S2, (isInducing_toContinuousMap X Y).isCompact_iff.mpr
      (ArzelaAscoli.isCompact_of_equicontinuous S3 hS4.isCompact h)⟩, hS2⟩

Premises used: Iff.mpr, ArzelaAscoli.isCompact_of_equicontinuous, ContinuousMonoidHom.isInducing_toContinuousMap, TopologicalSpace.Compacts.mk, IsClosed.isCompact, TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group, Topology.IsInducing.isCompact_iff, TopologicalSpace.PositiveCompacts.mk
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : Membership.mem (γ := Filter Y) (𝓝 1) V
W : Set Y
hWo : Membership.mem (γ := Filter Y) (𝓝 1) W
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S2 : Set (X →ₜ* Y) := {f : X →ₜ* Y | Set.MapsTo (⇑f : (a : X) → Y) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe (β := fun (x : X) ↦ Y) '' S3
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)
hS4 : IsClosed[Pi.topologicalSpace] S4
hS2 : (interior S2).Nonempty
⊢ LocallyCompactSpace (X →ₜ* Y)

Tactic:
exact TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group
    ⟨⟨S2, (isInducing_toContinuousMap X Y).isCompact_iff.mpr
      (ArzelaAscoli.isCompact_of_equicontinuous S3 hS4.isCompact h)⟩, hS2⟩

Premises used: Iff.mpr, ArzelaAscoli.isCompact_of_equicontinuous, ContinuousMonoidHom.isInducing_toContinuousMap, TopologicalSpace.Compacts.mk, IsClosed.isCompact, TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group, Topology.IsInducing.isCompact_iff, TopologicalSpace.PositiveCompacts.mk
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
inst_8 : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : Filter.HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) V
obtain :
  ∀ (U0 : Set X) (hU0c : IsCompact U0) (hU0o : Membership.mem (γ := Filter X) (𝓝 1) U0), LocallyCompactSpace (X →ₜ* Y)
⊢ LocallyCompactSpace (X →ₜ* Y)

Tactic:
obtain ⟨U0, hU0c, hU0o⟩ := exists_compact_mem_nhds (1 : X)

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
inst_8 : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : Filter.HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : Membership.mem (γ := Filter X) (𝓝 1) U0
U_aux : ℕ → (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7) :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7))
      (Subtype.mk (p := fun (x : Set X) ↦
        Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x) U0 hU0o)
      (fun (x : ℕ) (S : (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7)) ↦
        let h := ⋯;
        Subtype.mk (p := fun (x : Set X) ↦
          Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x)
          (Classical.choose (p := fun (x : Set X) ↦
            Membership.mem (γ := Filter X) (𝓝 1) x ∧ IsClosed[inst] x ∧ x⁻¹ = x ∧ x * x ⊆ (↑S : Set X)) h)
          ⋯)
      t
U : ℕ → Set X := fun (n : ℕ) ↦ (↑(U_aux n) : Set X)
⊢ ∀ (n : ℕ), Membership.mem (γ := Filter X) (𝓝 1) (U n)

Tactic:
have hU1 : ∀ n, U n ∈ nhds 1 := fun n ↦ (U_aux n).2
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
inst_8 : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : Filter.HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : Membership.mem (γ := Filter X) (𝓝 1) U0
U_aux : ℕ → (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7) :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7))
      (Subtype.mk (p := fun (x : Set X) ↦
        Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x) U0 hU0o)
      (fun (x : ℕ) (S : (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7)) ↦
        let h := ⋯;
        Subtype.mk (p := fun (x : Set X) ↦
          Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x)
          (Classical.choose (p := fun (x : Set X) ↦
            Membership.mem (γ := Filter X) (𝓝 1) x ∧ IsClosed[inst] x ∧ x⁻¹ = x ∧ x * x ⊆ (↑S : Set X)) h)
          ⋯)
      t
U : ℕ → Set X := fun (n : ℕ) ↦ (↑(U_aux n) : Set X)
hU1 : ∀ (n : ℕ), Membership.mem (γ := Filter X) (𝓝 1) (U n)
⊢ ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n

Tactic:
have hU2 : ∀ n, U (n + 1) * U (n + 1) ⊆ U n :=
    fun n ↦ (Classical.choose_spec (exists_closed_nhds_one_inv_eq_mul_subset (U_aux n).2)).2.2.2
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
inst_8 : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : Filter.HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : Membership.mem (γ := Filter X) (𝓝 1) U0
U_aux : ℕ → (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7) :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7))
      (Subtype.mk (p := fun (x : Set X) ↦
        Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x) U0 hU0o)
      (fun (x : ℕ) (S : (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7)) ↦
        let h := ⋯;
        Subtype.mk (p := fun (x : Set X) ↦
          Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x)
          (Classical.choose (p := fun (x : Set X) ↦
            Membership.mem (γ := Filter X) (𝓝 1) x ∧ IsClosed[inst] x ∧ x⁻¹ = x ∧ x * x ⊆ (↑S : Set X)) h)
          ⋯)
      t
U : ℕ → Set X := fun (n : ℕ) ↦ (↑(U_aux n) : Set X)
hU1 : ∀ (n : ℕ), Membership.mem (γ := Filter X) (𝓝 1) (U n)
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
⊢ ∀ (n : ℕ), U (n + 1) ⊆ U n

Tactic:
have hU3 : ∀ n, U (n + 1) ⊆ U n :=
    fun n x hx ↦ hU2 n (mul_one x ▸ Set.mul_mem_mul hx (mem_of_mem_nhds (hU1 (n + 1))))
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
inst_8 : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : Filter.HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : Membership.mem (γ := Filter X) (𝓝 1) U0
U_aux : ℕ → (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7) :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7))
      (Subtype.mk (p := fun (x : Set X) ↦
        Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x) U0 hU0o)
      (fun (x : ℕ) (S : (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7)) ↦
        let h := ⋯;
        Subtype.mk (p := fun (x : Set X) ↦
          Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x)
          (Classical.choose (p := fun (x : Set X) ↦
            Membership.mem (γ := Filter X) (𝓝 1) x ∧ IsClosed[inst] x ∧ x⁻¹ = x ∧ x * x ⊆ (↑S : Set X)) h)
          ⋯)
      t
U : ℕ → Set X := fun (n : ℕ) ↦ (↑(U_aux n) : Set X)
hU1 : ∀ (n : ℕ), Membership.mem (γ := Filter X) (𝓝 1) (U n)
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
f : X →* Y
hf : Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0)
⊢ Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0)

Tactic:
hf
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
inst_8 : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : Filter.HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : Membership.mem (γ := Filter X) (𝓝 1) U0
U_aux : ℕ → (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7) :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7))
      (Subtype.mk (p := fun (x : Set X) ↦
        Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x) U0 hU0o)
      (fun (x : ℕ) (S : (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7)) ↦
        let h := ⋯;
        Subtype.mk (p := fun (x : Set X) ↦
          Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x)
          (Classical.choose (p := fun (x : Set X) ↦
            Membership.mem (γ := Filter X) (𝓝 1) x ∧ IsClosed[inst] x ∧ x⁻¹ = x ∧ x * x ⊆ (↑S : Set X)) h)
          ⋯)
      t
U : ℕ → Set X := fun (n : ℕ) ↦ (↑(U_aux n) : Set X)
hU1 : ∀ (n : ℕ), Membership.mem (γ := Filter X) (𝓝 1) (U n)
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
f : X →* Y
hf : Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0)
⊢ Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0)

Tactic:
exact hf