no goals
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
N : Type ?u.215701
inst✝¹ : Monoid N
inst✝ : DecidableEq ι
i : ι
x : M i
⊢ ↑(↑lift (Pi.mulSingle i (MonoidHom.id (M i)))) (↑of x) = x
simp only [lift_of, Pi.mulSingle_eq_same, MonoidHom.id_apply]