C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((λ_ X).inv ≫ (β_ (𝟙_ C) X).hom) ≫ (ρ_ X).hom = (ρ_ X).inv ≫ (ρ_ X).hom
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (λ_ X).inv ≫ (β_ (𝟙_ C) X).hom = (ρ_ X).inv
apply (cancel_mono (ρ_ X).hom).1
no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((λ_ X).inv ≫ (β_ (𝟙_ C) X).hom) ≫ (ρ_ X).hom = (ρ_ X).inv ≫ (ρ_ X).hom
simp only [assoc, braiding_rightUnitor, Iso.inv_hom_id]