no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ (𝟙_ C) X).hom ≫ (ρ_ X).hom = (λ_ X).hom
rw [← tensor_left_iff, id_tensor_comp, braiding_rightUnitor_aux₂]