no goals
F : Type ?u.14417
A : Type u_1
B : Type u_2
C : Type ?u.14426
D : Type ?u.14429
E : Type ?u.14432
inst✝¹⁰ : Monoid A
inst✝⁹ : Monoid B
inst✝⁸ : Monoid C
inst✝⁷ : Monoid D
inst✝⁶ : CommGroup E
inst✝⁵ : TopologicalSpace A
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace C
inst✝² : TopologicalSpace D
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalGroup E
f g : ContinuousMonoidHom A B
h : toContinuousMap f = toContinuousMap g
⊢ ∀ (x : A), ↑f x = ↑g x
convert FunLike.ext_iff.1 h