F : Type ?u.44210
G : Type ?u.44213
α : Type ?u.44216
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (↑f x)
x x✝ : M
⊢ ↑(IsUnit.unit (_ : IsUnit (↑f x✝))) = ↑f x✝
F : Type ?u.44210
G : Type ?u.44213
α : Type ?u.44216
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (↑f x)
x : M
⊢ ∀ (x : M), ↑(IsUnit.unit (_ : IsUnit (↑f x))) = ↑f x
intro
no goals
F : Type ?u.44210
G : Type ?u.44213
α : Type ?u.44216
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (↑f x)
x x✝ : M
⊢ ↑(IsUnit.unit (_ : IsUnit (↑f x✝))) = ↑f x✝
rfl