no goals
α : Type u_3
β : Type ?u.36837
γ : Type ?u.36840
M : Type u_1
inst✝¹ : Monoid M
N : Type u_2
inst✝ : Monoid N
g : M →* N
f : α → M
⊢ ∀ (x : α), ↑(MonoidHom.comp g (↑lift f)) (of x) = ↑(↑lift (↑g ∘ f)) (of x)
simp