case h.a
α : Type ?u.8737
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
x✝ : Mˣ
⊢ ↑(↑(map (MonoidHom.id M)) x✝) = ↑(↑(MonoidHom.id Mˣ) x✝)
α : Type ?u.8737
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
⊢ map (MonoidHom.id M) = MonoidHom.id Mˣ
ext
no goals
case h.a
α : Type ?u.8737
M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
x✝ : Mˣ
⊢ ↑(↑(map (MonoidHom.id M)) x✝) = ↑(↑(MonoidHom.id Mˣ) x✝)
rfl