ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt (FunLike.coe ∘ F) 1
⊢ UniformContinuous (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F))
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt (FunLike.coe ∘ F) 1
⊢ UniformEquicontinuous (FunLike.coe ∘ F)
rw [uniformEquicontinuous_iff_uniformContinuous]
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
⊢ UniformContinuous (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F))
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt (FunLike.coe ∘ F) 1
⊢ UniformContinuous (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F))
rw [equicontinuousAt_iff_continuousAt] at hf
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
φ : G →* ι →ᵤ M :=
  { toOneHom := { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) },
    map_mul' :=
      (_ :
        ∀ (a b : G),
          OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } (a * b) =
            OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } a *
              OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } b) }
⊢ UniformContinuous (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F))
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
⊢ UniformContinuous (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F))
let φ : G →* (ι →ᵤ M) :=
  { toFun := swap ((↑) ∘ F)
    map_one' := by dsimp [UniformFun] ; ext ; exact map_one _
    map_mul' := fun a b => by dsimp [UniformFun] ; ext ; exact map_mul _ _ _ }
no goals
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
φ : G →* ι →ᵤ M :=
  { toOneHom := { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) },
    map_mul' :=
      (_ :
        ∀ (a b : G),
          OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } (a * b) =
            OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } a *
              OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } b) }
⊢ UniformContinuous (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F))
exact uniformContinuous_of_continuousAt_one φ hf
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
⊢ swap (FunLike.coe ∘ F) 1 = 1
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
⊢ swap (FunLike.coe ∘ F) 1 = 1
dsimp [UniformFun]
case h
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
x✝ : ι
⊢ swap (FunLike.coe ∘ F) 1 x✝ = OfNat.ofNat 1 x✝
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
⊢ swap (FunLike.coe ∘ F) 1 = 1
ext
no goals
case h
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
x✝ : ι
⊢ swap (FunLike.coe ∘ F) 1 x✝ = OfNat.ofNat 1 x✝
exact map_one _
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
a b : G
⊢ swap (FunLike.coe ∘ F) (a * b) = swap (FunLike.coe ∘ F) a * swap (FunLike.coe ∘ F) b
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
a b : G
⊢ OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } (a * b) =
    OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } a *
      OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } b
dsimp [UniformFun]
case h
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
a b : G
x✝ : ι
⊢ swap (FunLike.coe ∘ F) (a * b) x✝ = (swap (FunLike.coe ∘ F) a * swap (FunLike.coe ∘ F) b) x✝
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
a b : G
⊢ swap (FunLike.coe ∘ F) (a * b) = swap (FunLike.coe ∘ F) a * swap (FunLike.coe ∘ F) b
ext
no goals
case h
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
a b : G
x✝ : ι
⊢ swap (FunLike.coe ∘ F) (a * b) x✝ = (swap (FunLike.coe ∘ F) a * swap (FunLike.coe ∘ F) b) x✝
exact map_mul _ _ _