no goals
F : Type u_1
G : Type u_4
α : Type ?u.38455
M : Type u_2
N : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MonoidHomClass F M N
inst✝ : MonoidHomClass G N M
f : F
x : M
g : G
hfg : LeftInverse ↑g ↑f
h : IsUnit (↑f x)
⊢ IsUnit x
simpa only [hfg x] using h.map g