case intro
F : Type u_1
G : Type ?u.37609
α : Type ?u.37612
M : Type u_2
N : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MonoidHomClass F M N
f : F
y : Mˣ
⊢ IsUnit (↑f ↑y)
F : Type u_1
G : Type ?u.37609
α : Type ?u.37612
M : Type u_2
N : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MonoidHomClass F M N
f : F
x : M
h : IsUnit x
⊢ IsUnit (↑f x)
rcases h with ⟨y, rfl⟩
no goals
case intro
F : Type u_1
G : Type ?u.37609
α : Type ?u.37612
M : Type u_2
N : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MonoidHomClass F M N
f : F
y : Mˣ
⊢ IsUnit (↑f ↑y)
exact (Units.map (f : M →* N) y).isUnit