awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
inst_4 : ContinuousMul B
inst_5 : T2Space B
refine :
  ∀ (x y : A),
    IsClosed (X := C(A, B))
      {x_1 : C(A, B) |
        (x_1 : (a : A) → B) (x * y) =
          HMul.hMul (α := B) (β := B) ((x_1 : (a : A) → B) x : B) ((x_1 : (a : A) → B) y : B)}
⊢ IsClosed (X := C(A, B))
    ({a : C(A, B) | Eq.{u_3 + 1} (α := B) ((a : (a : A) → B) 1 : B) (1 : B)} ∩
      ⋂ (i : A),
        ⋂ (i_1 : A),
          {x : C(A, B) |
            (x : (a : A) → B) (i * i_1) =
              HMul.hMul (α := B) (β := B) ((x : (a : A) → B) i : B) ((x : (a : A) → B) i_1 : B)})

Tactic:
refine .inter (isClosed_singleton.preimage (continuous_eval_const 1)) <|
      isClosed_iInter fun x ↦ isClosed_iInter fun y ↦ ?_

Premises used: isClosed_iInter
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
inst_4 : ContinuousMul B
inst_5 : T2Space B
x y : A
⊢ IsClosed (X := C(A, B))
    {x_1 : C(A, B) |
      (x_1 : (a : A) → B) (x * y) = HMul.hMul (α := B) (β := B) ((x_1 : (a : A) → B) x : B) ((x_1 : (a : A) → B) y : B)}

Tactic:
isClosed_eq (continuous_eval_const (x * y)) <|
      .mul (continuous_eval_const x) (continuous_eval_const y)

Premises used: HMul.hMul, Continuous.mul, isClosed_eq, ContinuousEvalConst.continuous_eval_const
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
inst_4 : ContinuousMul B
inst_5 : T2Space B
x y : A
⊢ IsClosed (X := C(A, B))
    {x_1 : C(A, B) |
      (x_1 : (a : A) → B) (x * y) = HMul.hMul (α := B) (β := B) ((x_1 : (a : A) → B) x : B) ((x_1 : (a : A) → B) y : B)}

Tactic:
exact isClosed_eq (continuous_eval_const (x * y)) <|
      .mul (continuous_eval_const x) (continuous_eval_const y)

Premises used: HMul.hMul, isClosed_eq, ContinuousEvalConst.continuous_eval_const
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : Monoid D
inst_4 : CommGroup E
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace D
inst_9 : TopologicalSpace E
inst_10 : IsTopologicalGroup E
inst_11 : T2Space B
⊢ T2Space (A →ₜ* B)

Tactic:
(isEmbedding_toContinuousMap A B).t2Space

Premises used: ContinuousMonoidHom.isEmbedding_toContinuousMap, Topology.IsEmbedding.t2Space
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : Monoid D
inst_4 : CommGroup E
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace D
inst_9 : TopologicalSpace E
inst_10 : IsTopologicalGroup E
⊢ IsTopologicalGroup (A →ₜ* E)

Tactic:
let hi := isInducing_toContinuousMap A E
  let hc := hi.continuous
  { continuous_mul := hi.continuous_iff.mpr (continuous_mul.comp (Continuous.prodMap hc hc))
    continuous_inv := hi.continuous_iff.mpr (continuous_inv.comp hc) }

Premises used: ContinuousMonoidHom.isInducing_toContinuousMap, IsTopologicalGroup.mk, Topology.IsInducing.continuous
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
B : Type u_3
C : Type u_4
inst : Monoid B
inst_1 : Monoid C
inst_2 : TopologicalSpace B
inst_3 : TopologicalSpace C
A : Type u_7
inst_4 : TopologicalSpace A
f : A → B →ₜ* C
h : Continuous[instTopologicalSpaceProd, inst_3] (uncurry fun (x : A) (y : B) ↦ (f x : (a : B) → C) y)
⊢ Continuous[inst_4, _] f

Tactic:
(isInducing_toContinuousMap _ _).continuous_iff.mpr
    (ContinuousMap.continuous_of_continuous_uncurry _ h)

Premises used: Iff.mpr, ContinuousMonoidHom.isInducing_toContinuousMap, Topology.IsInducing.continuous_iff, ContinuousMap.continuous_of_continuous_uncurry
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
A : Type u_2
B : Type u_3
C : Type u_4
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
inst_6 : LocallyCompactSpace B
⊢ Continuous (Y := A →ₜ* C) fun (f : (A →ₜ* B) × (B →ₜ* C)) ↦ f.2.comp f.1

Tactic:
(isInducing_toContinuousMap A C).continuous_iff.2 <|
    ContinuousMap.continuous_comp'.comp
      ((isInducing_toContinuousMap A B).prodMap (isInducing_toContinuousMap B C)).continuous

Premises used: Iff.mpr, ContinuousMonoidHom.isInducing_toContinuousMap, Topology.IsInducing.continuous_iff, Continuous.comp, Topology.IsInducing.prodMap, ContinuousMap.continuous_comp', Topology.IsInducing.continuous
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
A : Type u_2
B : Type u_3
C : Type u_4
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
f : A →ₜ* B
⊢ Continuous (Y := A →ₜ* C) fun (g : B →ₜ* C) ↦ g.comp f

Tactic:
(isInducing_toContinuousMap A C).continuous_iff.2 <|
    f.toContinuousMap.continuous_precomp.comp (isInducing_toContinuousMap B C).continuous

Premises used: Iff.mpr, ContinuousMonoidHom.isInducing_toContinuousMap, Topology.IsInducing.continuous_iff, Continuous.comp, ContinuousMonoidHom.toContinuousMap, ContinuousMap.continuous_precomp, Topology.IsInducing.continuous
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
A : Type u_2
B : Type u_3
C : Type u_4
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
f : B →ₜ* C
⊢ Continuous (Y := A →ₜ* C) fun (g : A →ₜ* B) ↦ f.comp g

Tactic:
(isInducing_toContinuousMap A C).continuous_iff.2 <|
    f.toContinuousMap.continuous_postcomp.comp (isInducing_toContinuousMap A B).continuous

Premises used: Iff.mpr, ContinuousMonoidHom.isInducing_toContinuousMap, ContinuousMap.continuous_postcomp, Topology.IsInducing.continuous_iff, Continuous.comp, ContinuousMonoidHom.toContinuousMap, Topology.IsInducing.continuous
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
A : Type u_2
B : Type u_3
inst : Monoid A
inst_1 : Monoid B
inst_2 : TopologicalSpace A
inst_3 : TopologicalSpace B
inst_4 : DiscreteTopology A
inst_5 : ContinuousMul B
inst_6 : T2Space B
⊢ IsClosedEmbedding (X := A →ₜ* B) (Y := (a : A) → B) (DFunLike.coe (β := fun (x : A) ↦ B))

Tactic:
ContinuousMap.isHomeomorph_coe.isClosedEmbedding.comp <| isClosedEmbedding_toContinuousMap ..

Premises used: Topology.IsClosedEmbedding.comp, IsHomeomorph.isClosedEmbedding, ContinuousMap.isHomeomorph_coe, ContinuousMonoidHom.isClosedEmbedding_toContinuousMap
-- Module: Mathlib.Topology.Algebra.Group.CompactOpen
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
E : Type u_6
inst : Monoid A
inst_1 : Monoid B
inst_2 : Monoid C
inst_3 : Monoid D
inst_4 : CommGroup E
inst_5 : TopologicalSpace A
inst_6 : TopologicalSpace B
inst_7 : TopologicalSpace C
inst_8 : TopologicalSpace D
inst_9 : TopologicalSpace E
inst_10 : IsTopologicalGroup E
inst_11 : DiscreteTopology A
inst_12 : ContinuousMul B
inst_13 : T2Space B
inst_14 : CompactSpace B
⊢ CompactSpace (A →ₜ* B)

Tactic:
ContinuousMonoidHom.isClosedEmbedding_coe.compactSpace

Premises used: Topology.IsClosedEmbedding.compactSpace, ContinuousMonoidHom.isClosedEmbedding_coe
-- 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
h :
  EquicontinuousAt (X := X) (α := Y)
    (fun (f : (↑{f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U V} : Type (max u_7 u_8))) ↦
      (⇑(↑f : X →* Y) : (a : X) → Y))
    1
⊢ Equicontinuous (ι := (↑{f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U V} : Type (max u_7 u_8))) (X := X) (α := Y)
    (DFunLike.coe (β := fun (x : X) ↦ Y) ∘
      Subtype.val (p := fun (x : X →* Y) ↦
        Membership.mem (γ := Set (X →* Y)) {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U V} x))

Tactic:
replace h := equicontinuous_of_equicontinuousAt_one _ h
-- 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
h :
  Equicontinuous (ι := (↑{f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U V} : Type (max u_7 u_8))) (X := X) (α := Y)
    (DFunLike.coe (β := fun (x : X) ↦ Y) ∘
      Subtype.val (p := fun (x : X →* Y) ↦
        Membership.mem (γ := Set (X →* Y)) {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U V} x))
obtain :
  ∀ (W : Set Y) (hWo : Membership.mem (γ := Filter Y) (𝓝 1) W) (hWV : W ⊆ V) (hWc : IsCompact W),
    LocallyCompactSpace (X →ₜ* Y)
⊢ LocallyCompactSpace (X →ₜ* Y)

Tactic:
obtain ⟨W, hWo, hWV, hWc⟩ := local_compact_nhds hV

Premises used: local_compact_nhds
-- 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
h :
  Equicontinuous (ι := (↑{f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U V} : Type (max u_7 u_8))) (X := X) (α := Y)
    (DFunLike.coe (β := fun (x : X) ↦ Y) ∘
      Subtype.val (p := fun (x : X →* Y) ↦
        Membership.mem (γ := Set (X →* Y)) {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) U V} x))
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
⊢ Equicontinuous (X := X) (α := Y) fun (x : (↑S1 : Type (max u_7 u_8))) ↦ (⇑(↑x : X →* Y) : (a : X) → Y)

Tactic:
replace h : Equicontinuous ((↑) : S1 → X → Y) :=
    h.comp (Subtype.map _root_.id fun f hf ↦ hf.mono_right hWV)
-- 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 : (↑S1 : Type (max u_7 u_8))) ↦ (⇑(↑x : X →* Y) : (a : X) → Y)
h₁ : ∀ (x : X → Y), x ∈ S4 ↔ Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) x
⊢ S4 = DFunLike.coe (β := fun (x : X) ↦ Y) '' S1

Tactic:
ext
-- 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 : (↑S1 : Type (max u_7 u_8))) ↦ (⇑(↑x : X →* Y) : (a : X) → Y)
x : X → Y
h₁ : x ∈ S4 → Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) x
h₂ : Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) x → x ∈ S4
⊢ x ∈ S4 ↔ Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) x

Tactic:
constructor
-- 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 : (↑S1 : Type (max u_7 u_8))) ↦ (⇑(↑x : X →* Y) : (a : X) → Y)
f : X →ₜ* Y
hf : f ∈ S2
⊢ Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) (⇑(↑f : C(X, Y)) : (a : X) → Y)

Tactic:
⟨f, hf, rfl⟩

Premises used: Set.Mem, setOf, MonoidHomClass.toMonoidHom, And.intro, Exists.intro, Set.image, 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
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S1 : Type (max u_7 u_8))) ↦ (⇑(↑x : X →* Y) : (a : X) → Y)
f : X →ₜ* Y
hf : f ∈ S2
⊢ Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) (⇑(↑f : C(X, Y)) : (a : X) → Y)

Tactic:
exact ⟨f, hf, 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
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S1 : Type (max u_7 u_8))) ↦ (⇑(↑x : X →* Y) : (a : X) → Y)
f : X →* Y
hf : f ∈ S1
⊢ (⇑f : (a : X) → Y) ∈ S4

Tactic:
⟨⟨f, h.continuous ⟨f, hf⟩⟩, ⟨⟨f, h.continuous ⟨f, hf⟩⟩, hf, rfl⟩, rfl⟩

Premises used: Equicontinuous.continuous, ContinuousMonoidHom.mk, Set.Mem, ContinuousMap.mk, setOf, Subtype.mk, And.intro, Exists.intro, Set.image, 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
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S1 : Type (max u_7 u_8))) ↦ (⇑(↑x : X →* Y) : (a : X) → Y)
f : X →* Y
hf : f ∈ S1
⊢ (⇑f : (a : X) → Y) ∈ S4

Tactic:
exact ⟨⟨f, h.continuous ⟨f, hf⟩⟩, ⟨⟨f, h.continuous ⟨f, hf⟩⟩, hf, rfl⟩, 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
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S1 : Type (max u_7 u_8))) ↦ (⇑(↑x : X →* Y) : (a : X) → Y)
⊢ S4 = DFunLike.coe (β := fun (x : X) ↦ Y) '' S1

Tactic:
have hS4 : S4 = (↑) '' S1 := by
    ext
    constructor
    · rintro ⟨-, ⟨f, hf, rfl⟩, rfl⟩
      exact ⟨f, hf, rfl⟩
    · rintro ⟨f, hf, rfl⟩
      exact ⟨⟨f, h.continuous ⟨f, hf⟩⟩, ⟨⟨f, h.continuous ⟨f, hf⟩⟩, hf, rfl⟩, 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
h : Equicontinuous (X := X) (α := Y) fun (x : (↑S1 : Type (max u_7 u_8))) ↦ (⇑(↑x : X →* Y) : (a : X) → Y)
hS4 : S4 = DFunLike.coe (β := fun (x : X) ↦ Y) '' S1
rw :
  ∀
    (h :
      Equicontinuous (ι :=
        { x : X → Y // Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) x })
        (Subtype.val (p := fun (x : X → Y) ↦
          Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) x)))
    (hS4 : S4 = DFunLike.coe (β := fun (x : X) ↦ Y) '' S1),
    Equicontinuous (ι :=
      { x : X → Y // Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S3) x })
      (Subtype.val (p := fun (x : X → Y) ↦
        Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S3) x))
⊢ Equicontinuous (X := X) (α := Y) fun (x : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)

Tactic:
rw [equicontinuous_iff_range, ← Set.image_eq_range] at h ⊢

Premises used: equicontinuous_iff_range, Set.image_eq_range
-- 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 // Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) x })
    (Subtype.val (p := fun (x : X → Y) ↦
      Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S1) x))
hS4 : S4 = DFunLike.coe (β := fun (x : X) ↦ Y) '' S1
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h : Equicontinuous (ι := { x : X → Y // x ∈ S4 }) (Subtype.val (p := fun (x : X → Y) ↦ x ∈ S4)))
    (hS4 : S4 = DFunLike.coe (β := fun (x : X) ↦ Y) '' S1),
    Equicontinuous (ι :=
      { x : X → Y // Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S3) x })
      (Subtype.val (p := fun (x : X → Y) ↦
        Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S3) x))
⊢ Equicontinuous (ι := { x : X → Y // Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S3) x })
    (Subtype.val (p := fun (x : X → Y) ↦
      Membership.mem (γ := Set (X → Y)) (DFunLike.coe (β := fun (x : X) ↦ Y) '' S3) x))

Tactic:
rwa [← hS4] at h
-- 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 : (↑S1 : Type (max u_7 u_8))) ↦ (⇑(↑x : X →* Y) : (a : X) → Y)
hS4 : S4 = DFunLike.coe (β := fun (x : X) ↦ Y) '' S1
⊢ Equicontinuous (X := X) (α := Y) fun (x : (↑S3 : Type (max u_7 u_8))) ↦ (⇑(↑x : C(X, Y)) : (a : X) → Y)

Tactic:
replace h : Equicontinuous ((↑) : S3 → X → Y) := by
    rw [equicontinuous_iff_range, ← Set.image_eq_range] at h ⊢
    rwa [← hS4] at h
-- 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)
simp_rw :
  ∀ (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
⊢ S4 = (U.pi (α := fun (x : X) ↦ Y) fun (x : X) ↦ W) ∩ Set.range (ι := X →* Y) (DFunLike.coe (β := fun (x : X) ↦ Y))

Tactic:
simp_rw [hS4, Set.ext_iff, Set.mem_image, S1, Set.mem_setOf_eq]

Premises used: Set.mem_image, Set.mem_setOf_eq, Set.ext_iff