C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (ρ_ (X ⊗ 𝟙_ C)).hom ≫ (β_ (𝟙_ C) X).inv = (𝟙 X ⊗ (ρ_ (𝟙_ C)).hom) ≫ (β_ (𝟙_ C) X).inv
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ ((β_ (𝟙_ C) X).inv ⊗ 𝟙 (𝟙_ C)) ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ (𝟙 (𝟙_ C) ⊗ (ρ_ X).hom) =
    (𝟙 X ⊗ (ρ_ (𝟙_ C)).hom) ≫ (β_ (𝟙_ C) X).inv
rw [← rightUnitor_tensor, rightUnitor_naturality]
no goals
C : Type u₁
inst✝² : Category C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (ρ_ (X ⊗ 𝟙_ C)).hom ≫ (β_ (𝟙_ C) X).inv = (𝟙 X ⊗ (ρ_ (𝟙_ C)).hom) ≫ (β_ (𝟙_ C) X).inv
simp