no goals
α : Type u_1
β : Type u_2
M : Type ?u.226815
N : Type ?u.226818
P : Type ?u.226821
G : Type ?u.226824
H : Type ?u.226827
F : Type ?u.226830
inst✝³ : Group G
inst✝² : CommGroup H
inst✝¹ : Group α
inst✝ : DivisionMonoid β
f : α →* β
g h : α
⊢ ↑f (g * h⁻¹) = ↑f g * (↑f h)⁻¹
simp