no goals
ι : Type u_3
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
N✝ : Type ?u.134151
inst✝¹ : Monoid N✝
N : Type u_1
inst✝ : Monoid N
fi : (i : ι) → M i →* N
i : ι
m : M i
⊢ ↑(↑lift fi) (↑of m) = ↑(fi i) m
conv_rhs => rw [← lift.symm_apply_apply fi, lift_symm_apply, MonoidHom.comp_apply]