no goals
C : Type u₁
inst✝¹ : Category C
inst✝ : MonoidalCategory C
M : Mon_ C
Z : C
f : Z ⟶ M.X
⊢ (M.one ⊗ f) ≫ M.mul = (λ_ Z).hom ≫ f
rw [← id_tensor_comp_tensor_id, Category.assoc, M.one_mul, leftUnitor_naturality]