-- Mathlib/CategoryTheory/Monoidal/Bimod.lean
theorem whisker_exchange_bimod {X Y Z : Mon_ C} {M N : Bimod X Y} {P Q : Bimod Y Z} (f : M ⟶ N)
    (g : P ⟶ Q) : whiskerLeft M g ≫ whiskerRight f Q =
      whiskerRight f P ≫ whiskerLeft N g

Proof state:
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ (M.whiskerLeft g ≫ whiskerRight f Q).hom = (whiskerRight f P ≫ N.whiskerLeft g).hom

Tactic:
apply coequalizer.hom_ext

Result:
case h.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫ (M.whiskerLeft g ≫ whiskerRight f Q).hom =
    coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫ (whiskerRight f P ≫ N.whiskerLeft g).hom

Proof state:
case h.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ (f.hom ▷ P.X ≫ N.X ◁ g.hom) ≫
      colimit.ι (parallelPair (N.actRight ▷ Q.X) ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft)) WalkingParallelPair.one =
    f.hom ▷ P.X ≫
      N.X ◁ g.hom ≫
        colimit.ι (parallelPair (N.actRight ▷ Q.X) ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft)) WalkingParallelPair.one

Tactic:
simp only [Category.assoc]

Result:
no goals

Proof state:
case h.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ (M.X ◁ g.hom ≫
        colimit.ι (parallelPair (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft)) WalkingParallelPair.one) ≫
      colimMap
        (parallelPairHom (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) (N.actRight ▷ Q.X)
          ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) (f.hom ▷ Y.X ▷ Q.X) (f.hom ▷ Q.X) ⋯ ⋯) =
    coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫
      colimMap
          (parallelPairHom (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X)
            ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯) ≫
        colimMap
          (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X)
            ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) ((N.X ⊗ Y.X) ◁ g.hom) (N.X ◁ g.hom) ⋯ ⋯)

Tactic:
slice_lhs 2 3 => rw [ι_colimMap, parallelPairHom_app_one]

Result:
case h.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ M.X ◁ g.hom ≫
      f.hom ▷ Q.X ≫
        colimit.ι (parallelPair (N.actRight ▷ Q.X) ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft)) WalkingParallelPair.one =
    coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫
      colimMap
          (parallelPairHom (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X)
            ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯) ≫
        colimMap
          (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X)
            ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) ((N.X ⊗ Y.X) ◁ g.hom) (N.X ◁ g.hom) ⋯ ⋯)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ M.whiskerLeft g ≫ whiskerRight f Q = whiskerRight f P ≫ N.whiskerLeft g

Tactic:
ext

Result:
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ (M.whiskerLeft g ≫ whiskerRight f Q).hom = (whiskerRight f P ≫ N.whiskerLeft g).hom

Proof state:
case h.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫
      colimMap
          (parallelPairHom (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) (M.actRight ▷ Q.X)
            ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) ((M.X ⊗ Y.X) ◁ g.hom) (M.X ◁ g.hom) ⋯ ⋯) ≫
        colimMap
          (parallelPairHom (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) (N.actRight ▷ Q.X)
            ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) (f.hom ▷ Y.X ▷ Q.X) (f.hom ▷ Q.X) ⋯ ⋯) =
    coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫
      colimMap
          (parallelPairHom (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X)
            ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯) ≫
        colimMap
          (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X)
            ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) ((N.X ⊗ Y.X) ◁ g.hom) (N.X ◁ g.hom) ⋯ ⋯)

Tactic:
slice_lhs 1 2 => rw [ι_colimMap, parallelPairHom_app_one]

Result:
case h.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ (M.X ◁ g.hom ≫
        colimit.ι (parallelPair (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft)) WalkingParallelPair.one) ≫
      colimMap
        (parallelPairHom (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) (N.actRight ▷ Q.X)
          ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) (f.hom ▷ Y.X ▷ Q.X) (f.hom ▷ Q.X) ⋯ ⋯) =
    coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫
      colimMap
          (parallelPairHom (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X)
            ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯) ≫
        colimMap
          (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X)
            ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) ((N.X ⊗ Y.X) ◁ g.hom) (N.X ◁ g.hom) ⋯ ⋯)