no goals
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
x : WithOne α
⊢ ↑(map g) (↑(map f) x) = ↑(map (MulHom.comp g f)) x
induction x using WithOne.cases_on <;> rfl