no goals
C✝ : Type u
𝒞 : Category C✝
inst✝² : MonoidalCategory C✝
C : Type u
inst✝¹ : Category C
inst✝ : MonoidalCategory C
U V W X✝ Y✝ Z✝ X Y Z Z' : C
h : Z ⟶ Z'
⊢ (𝟙 (X ⊗ Y) ⊗ h) ≫ (α_ X Y Z').hom = (α_ X Y Z).hom ≫ (𝟙 X ⊗ 𝟙 Y ⊗ h)
rw [← tensor_id, associator_naturality]