case H
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
a x✝ : G
⊢ ↑(Homeomorph.symm (Homeomorph.mulRight a)) x✝ = ↑(Homeomorph.mulRight a⁻¹) x✝
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
a : G
⊢ Homeomorph.symm (Homeomorph.mulRight a) = Homeomorph.mulRight a⁻¹
ext
no goals
case H
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
a x✝ : G
⊢ ↑(Homeomorph.symm (Homeomorph.mulRight a)) x✝ = ↑(Homeomorph.mulRight a⁻¹) x✝
rfl