-- Mathlib/CategoryTheory/Monoidal/Bimod.lean
theorem hom_inv_id : hom P ≫ inv P = 𝟙 _

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ coequalizer.desc P.actRight ⋯ ≫
      (ρ_ P.X).inv ≫
        P.X ◁ S.one ≫
          coequalizer.π (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft) =
    𝟙 (coequalizer (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft))

Tactic:
ext

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ coequalizer.π (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft) ≫
      coequalizer.desc P.actRight ⋯ ≫
        (ρ_ P.X).inv ≫
          P.X ◁ S.one ≫
            coequalizer.π (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft) =
    coequalizer.π (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft) ≫
      𝟙 (coequalizer (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft))

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ (((ρ_ (P.X ⊗ S.X)).inv ≫ P.actRight ▷ 𝟙_ C) ≫ P.X ◁ S.one) ≫
      coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))

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

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ (ρ_ (P.X ⊗ S.X)).inv ≫
      ((P.X ⊗ S.X) ◁ S.one ≫ P.actRight ▷ S.X) ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ coequalizer.π (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft) ≫
      coequalizer.desc P.actRight ⋯ ≫
        (ρ_ P.X).inv ≫
          P.X ◁ S.one ≫
            coequalizer.π (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft) =
    coequalizer.π (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft) ≫
      𝟙 (coequalizer (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft))

Tactic:
dsimp

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫
      coequalizer.desc P.actRight ⋯ ≫
        (ρ_ P.X).inv ≫ P.X ◁ S.one ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ ((P.actRight ≫ (ρ_ P.X).inv) ≫ P.X ◁ S.one) ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))

Tactic:
slice_lhs 1 2 => rw [rightUnitor_inv_naturality]

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ (((ρ_ (P.X ⊗ S.X)).inv ≫ P.actRight ▷ 𝟙_ C) ≫ P.X ◁ S.one) ≫
      coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫
      coequalizer.desc P.actRight ⋯ ≫
        (ρ_ P.X).inv ≫ P.X ◁ S.one ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))

Tactic:
slice_lhs 1 2 => rw [coequalizer.π_desc]

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ ((P.actRight ≫ (ρ_ P.X).inv) ≫ P.X ◁ S.one) ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ (ρ_ (P.X ⊗ S.X)).inv ≫
      (α_ P.X S.X (𝟙_ C)).hom ≫
        P.X ◁ (ρ_ S.X).hom ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))

Tactic:
slice_rhs 1 2 => rw [Category.comp_id]

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ (ρ_ (P.X ⊗ S.X)).inv ≫
      (α_ P.X S.X (𝟙_ C)).hom ≫
        P.X ◁ (ρ_ S.X).hom ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul)

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ (ρ_ (P.X ⊗ S.X)).inv ≫
      (((α_ P.X S.X (𝟙_ C)).hom ≫ P.X ◁ S.X ◁ S.one) ≫ P.X ◁ S.mul) ≫
        coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))

Tactic:
slice_lhs 3 4 => rw [← MonoidalCategory.whiskerLeft_comp, Mon_.mul_one]

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ (ρ_ (P.X ⊗ S.X)).inv ≫
      (α_ P.X S.X (𝟙_ C)).hom ≫
        P.X ◁ (ρ_ S.X).hom ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul))

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ hom P ≫ inv P = 𝟙 (TensorBimod.X P (regular S))

Tactic:
dsimp only [hom, inv, TensorBimod.X]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ coequalizer.desc P.actRight ⋯ ≫
      (ρ_ P.X).inv ≫
        P.X ◁ S.one ≫
          coequalizer.π (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft) =
    𝟙 (coequalizer (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft))