no goals
α : Type ?u.47943
β : Type ?u.47946
M : Type ?u.47949
N : Type ?u.47952
P : Type ?u.47955
G : Type u_1
H : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
a b : G
⊢ ↑f (a * b⁻¹) = ↑f a * (↑f b)⁻¹
rw [map_mul, map_inv]