-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem braiding_rightUnitor_aux₂ (X : C) :
    (𝟙_ C ◁ (β_ (𝟙_ C) X).hom) ≫ (𝟙_ C ◁ (ρ_ X).hom) = 𝟙_ C ◁ (λ_ X).hom :=
  calc
    (𝟙_ C ◁ (β_ (𝟙_ C) X).hom) ≫ (𝟙_ C ◁ (ρ_ X).hom) =
      (𝟙_ C ◁ (β_ (𝟙_ C) X).hom) ≫ (α_ _ _ _).inv ≫ (α_ _ _ _).hom ≫ (𝟙_ C ◁ (ρ_ X).hom)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X = 𝟙_ C ◁ (λ_ X).hom

Tactic:
rw [triangle_assoc_comp_right]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ 𝟙_ C ◁ (β_ (𝟙_ C) X).hom ≫
      (α_ (𝟙_ C) X (𝟙_ C)).inv ≫
        (β_ (𝟙_ C) X).hom ▷ 𝟙_ C ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫
      (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫
        (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom

Tactic:
(slice_lhs 1 3 => rw [← hexagon_reverse])

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((((α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ (α_ X (𝟙_ C) (𝟙_ C)).inv) ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C) ≫
        (α_ (𝟙_ C) X (𝟙_ C)).hom) ≫
      𝟙_ C ◁ (ρ_ X).hom =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫
      (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫
        (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) (𝟙_ C) X).inv ≫
      (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫
        (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ X ◁ (ρ_ (𝟙_ C)).hom ≫ (β_ (𝟙_ C) X).inv

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ X ◁ (ρ_ (𝟙_ C)).hom ≫ (β_ (𝟙_ C) X).inv =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom ≫ (β_ (𝟙_ C) X).inv

Tactic:
(slice_lhs 2 3 => rw [← braiding_naturality_left])

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ ((ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom) ≫ (β_ (𝟙_ C) X).inv =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom ≫ (β_ (𝟙_ C) X).inv

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ 𝟙_ C ◁ (β_ (𝟙_ C) X).hom ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom =
    𝟙_ C ◁ (β_ (𝟙_ C) X).hom ≫
      (α_ (𝟙_ C) X (𝟙_ C)).inv ≫
        (β_ (𝟙_ C) X).hom ▷ 𝟙_ C ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ 𝟙_ C ◁ (β_ (𝟙_ C) X).hom ≫ 𝟙_ C ◁ (ρ_ X).hom =
    𝟙_ C ◁ (β_ (𝟙_ C) X).hom ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom

Tactic:
monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ 𝟙_ C ◁ (β_ (𝟙_ C) X).hom ≫
      (α_ (𝟙_ C) X (𝟙_ C)).inv ≫
        (β_ (𝟙_ C) X).hom ▷ 𝟙_ C ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫
      (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫
        (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom

Tactic:
slice_lhs 1 3 => rw [← hexagon_reverse]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((((α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ (α_ X (𝟙_ C) (𝟙_ C)).inv) ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C) ≫
        (α_ (𝟙_ C) X (𝟙_ C)).hom) ≫
      𝟙_ C ◁ (ρ_ X).hom =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫
      (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫
        (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom ≫ (β_ (𝟙_ C) X).inv =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X

Tactic:
rw [Iso.hom_inv_id, comp_id]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ X ◁ (ρ_ (𝟙_ C)).hom ≫ (β_ (𝟙_ C) X).inv =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom ≫ (β_ (𝟙_ C) X).inv

Tactic:
slice_lhs 2 3 => rw [← braiding_naturality_left]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ ((ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom) ≫ (β_ (𝟙_ C) X).inv =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom ≫ (β_ (𝟙_ C) X).inv

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((((α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ (α_ X (𝟙_ C) (𝟙_ C)).inv) ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C) ≫
        (α_ (𝟙_ C) X (𝟙_ C)).hom) ≫
      𝟙_ C ◁ (ρ_ X).hom =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫
      (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫
        (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom

Tactic:
simp only [assoc]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ ((ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom) ≫ (β_ (𝟙_ C) X).inv =
    (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom ≫ (β_ (𝟙_ C) X).inv

Tactic:
simp only [assoc]

Result:
no goals