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