-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem tensor_right_unitality (X₁ X₂ : C) :
    (ρ_ (X₁ ⊗ X₂)).hom =
      ((X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).inv) ≫
        tensorμ X₁ X₂ (𝟙_ C) (𝟙_ C) ≫ ((ρ_ X₁).hom ⊗ (ρ_ X₂).hom)

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

Tactic:
simp [tensorHom_id, id_tensorHom, tensorHom_def]

Result:
no goals

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

Tactic:
dsimp only [tensorμ]

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

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

Tactic:
clear this

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

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

Tactic:
monoidal

Result:
no goals

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

Tactic:
slice_rhs 1 3 => rw [this]

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

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

Tactic:
have :
  ((X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).inv) ≫
      (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv) =
    (α_ X₁ X₂ (𝟙_ C)).hom ≫ (X₁ ◁ (ρ_ X₂).inv ▷ 𝟙_ C) := by
  monoidal

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

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

Tactic:
slice_rhs 2 3 => rw [← MonoidalCategory.whiskerLeft_comp, ← comp_whiskerRight,
  rightUnitor_inv_braiding]

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