-- Mathlib/CategoryTheory/Monoidal/Bimod.lean
theorem hom_left_act_hom' :
    ((regular R).tensorBimod P).actLeft ≫ hom P = (R.X ◁ hom P) ≫ P.actLeft

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (α_ R.X R.X P.X).inv ≫ (α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft ≫ P.actLeft = R.X ◁ P.actLeft ≫ P.actLeft

Tactic:
rw [Iso.inv_hom_id_assoc]

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (α_ R.X R.X P.X).inv ≫ (α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft ≫ P.actLeft =
    R.X ◁ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫
      R.X ◁ coequalizer.desc P.actLeft ⋯ ≫ P.actLeft

Tactic:
slice_rhs 1 2 => rw [← MonoidalCategory.whiskerLeft_comp, coequalizer.π_desc]

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (α_ R.X R.X P.X).inv ≫ (α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft ≫ P.actLeft = R.X ◁ P.actLeft ≫ P.actLeft

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ R.X ◁ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫
      ((PreservesCoequalizer.iso (tensorLeft R.X) (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)).inv ≫
          colimMap
            (parallelPairHom (R.X ◁ R.mul ▷ P.X) (R.X ◁ ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)) (R.mul ▷ P.X)
              ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)
              ((α_ R.X (R.X ⊗ R.X) P.X).inv ≫ (α_ R.X R.X R.X).inv ▷ P.X ≫ R.mul ▷ R.X ▷ P.X)
              ((α_ R.X R.X P.X).inv ≫ R.mul ▷ P.X) ⋯ ⋯)) ≫
        coequalizer.desc P.actLeft ⋯ =
    R.X ◁ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫
      R.X ◁ coequalizer.desc P.actLeft ⋯ ≫ P.actLeft

Tactic:
slice_lhs 1 4 => rw [id_tensor_π_preserves_coequalizer_inv_colimMap_desc]

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ ((α_ R.X R.X P.X).inv ≫ R.mul ▷ P.X) ≫ P.actLeft =
    R.X ◁ coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫
      R.X ◁ coequalizer.desc P.actLeft ⋯ ≫ P.actLeft

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ ((PreservesCoequalizer.iso (tensorLeft R.X) (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)).inv ≫
        colimMap
          (parallelPairHom (R.X ◁ R.mul ▷ P.X) (R.X ◁ ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)) (R.mul ▷ P.X)
            ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)
            ((α_ R.X (R.X ⊗ R.X) P.X).inv ≫ (α_ R.X R.X R.X).inv ▷ P.X ≫ R.mul ▷ R.X ▷ P.X)
            ((α_ R.X R.X P.X).inv ≫ R.mul ▷ P.X) ⋯ ⋯)) ≫
      coequalizer.desc P.actLeft ⋯ =
    R.X ◁ coequalizer.desc P.actLeft ⋯ ≫ P.actLeft

Tactic:
refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (tensorLeft R.X).map
        (coequalizer.π
          ({ X := R.X, actLeft := R.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := R.mul, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ }.actRight ▷
            P.X)
          ((α_
                { X := R.X, actLeft := R.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := R.mul, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ }.X
                R.X P.X).hom ≫
            { X := R.X, actLeft := R.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := R.mul, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ }.X ◁
              P.actLeft)) ≫
      ((PreservesCoequalizer.iso (tensorLeft R.X) (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)).inv ≫
          colimMap
            (parallelPairHom (R.X ◁ R.mul ▷ P.X) (R.X ◁ ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)) (R.mul ▷ P.X)
              ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)
              ((α_ R.X (R.X ⊗ R.X) P.X).inv ≫ (α_ R.X R.X R.X).inv ▷ P.X ≫ R.mul ▷ R.X ▷ P.X)
              ((α_ R.X R.X P.X).inv ≫ R.mul ▷ P.X) ⋯ ⋯)) ≫
        coequalizer.desc P.actLeft ⋯ =
    (tensorLeft R.X).map
        (coequalizer.π
          ({ X := R.X, actLeft := R.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := R.mul, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ }.actRight ▷
            P.X)
          ((α_
                { X := R.X, actLeft := R.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := R.mul, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ }.X
                R.X P.X).hom ≫
            { X := R.X, actLeft := R.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := R.mul, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ }.X ◁
              P.actLeft)) ≫
      R.X ◁ coequalizer.desc P.actLeft ⋯ ≫ P.actLeft

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ ((regular R).tensorBimod P).actLeft ≫ hom P = R.X ◁ hom P ≫ P.actLeft

Tactic:
dsimp

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ TensorBimod.actLeft (regular R) P ≫ hom P = R.X ◁ hom P ≫ P.actLeft