no goals
N : Type u_1
G : Type u_2
H : Type ?u.83486
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
g : G
n : N
⊢ ↑inl (↑(↑φ g)⁻¹ n) = ↑inr g⁻¹ * ↑inl n * ↑inr g
rw [← MonoidHom.map_inv, inl_aut, inv_inv]