-- Mathlib/CategoryTheory/Monoidal/Bimod.lean
theorem id_whiskerLeft_bimod {X Y : Mon_ C} {M N : Bimod X Y} (f : M ⟶ N) :
    whiskerLeft (regular X) f = (leftUnitorBimod M).hom ≫ f ≫ (leftUnitorBimod N).inv

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 : Mon_ C
M N : Bimod X Y
f : M ⟶ N
⊢ (regular X).whiskerLeft f = M.leftUnitorBimod.hom ≫ f ≫ N.leftUnitorBimod.inv

Tactic:
dsimp [tensorHom, regular, leftUnitorBimod]

Result:
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 : Mon_ C
M N : Bimod X Y
f : M ⟶ N
⊢ { X := X.X, actLeft := X.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := X.mul, actRight_one := ⋯,
          right_assoc := ⋯, middle_assoc := ⋯ }.whiskerLeft
      f =
    (isoOfIso { hom := LeftUnitorBimod.hom M, inv := LeftUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
          ⋯).hom ≫
      f ≫
        (isoOfIso { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯).inv

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 : Mon_ C
M N : Bimod X Y
f : M ⟶ N
⊢ (λ_ (X.X ⊗ N.X)).inv ≫ (α_ (𝟙_ C) X.X N.X).inv ≫ (λ_ X.X).hom ▷ N.X = 𝟙 (X.X ⊗ N.X)

Tactic:
monoidal

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 : Mon_ C
M N : Bimod X Y
f : M ⟶ N
⊢ X.X ◁ f.hom ≫
      colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    X.X ◁ f.hom ≫
      (λ_ (X.X ⊗ N.X)).inv ≫
        X.one ▷ (X.X ⊗ N.X) ≫
          (α_ X.X X.X N.X).inv ≫ X.mul ▷ N.X ≫ coequalizer.π (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)

Tactic:
slice_rhs 3 4 => rw [associator_inv_naturality_left]

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 : Mon_ C
M N : Bimod X Y
f : M ⟶ N
⊢ X.X ◁ f.hom ≫
      colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    X.X ◁ f.hom ≫
      (λ_ (X.X ⊗ N.X)).inv ≫
        (((α_ (𝟙_ C) X.X N.X).inv ≫ X.one ▷ X.X ▷ N.X) ≫ X.mul ▷ N.X) ≫
          coequalizer.π (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)

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 : Mon_ C
M N : Bimod X Y
f : M ⟶ N
⊢ X.X ◁ f.hom ≫
      colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    (M.actLeft ≫ f.hom) ≫ LeftUnitorBimod.inv N

Tactic:
dsimp [LeftUnitorBimod.inv]

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 : Mon_ C
M N : Bimod X Y
f : M ⟶ N
⊢ X.X ◁ f.hom ≫
      colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    (M.actLeft ≫ f.hom) ≫
      (λ_ N.X).inv ≫ X.one ▷ N.X ≫ coequalizer.π (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)

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 : Mon_ C
M N : Bimod X Y
f : M ⟶ N
this : (λ_ (X.X ⊗ N.X)).inv ≫ (α_ (𝟙_ C) X.X N.X).inv ≫ (λ_ X.X).hom ▷ N.X = 𝟙 (X.X ⊗ N.X)
⊢ X.X ◁ f.hom ≫
      colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    X.X ◁ f.hom ≫ 𝟙 (X.X ⊗ N.X) ≫ coequalizer.π (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)

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

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 : Mon_ C
M N : Bimod X Y
f : M ⟶ N
⊢ X.X ◁ f.hom ≫
      colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    X.X ◁ f.hom ≫
      (((λ_ (X.X ⊗ N.X)).inv ≫ 𝟙_ C ◁ N.actLeft) ≫ X.one ▷ N.X) ≫
        coequalizer.π (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)

Tactic:
slice_rhs 3 4 => rw [whisker_exchange]

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 : Mon_ C
M N : Bimod X Y
f : M ⟶ N
⊢ X.X ◁ f.hom ≫
      colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    X.X ◁ f.hom ≫
      (λ_ (X.X ⊗ N.X)).inv ≫
        (X.one ▷ (X.X ⊗ N.X) ≫ X.X ◁ N.actLeft) ≫ coequalizer.π (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)

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 : Mon_ C
M N : Bimod X Y
f : M ⟶ N
⊢ X.X ◁ f.hom ≫
      colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    X.X ◁ f.hom ≫
      (λ_ (X.X ⊗ N.X)).inv ≫
        (α_ (𝟙_ C) X.X N.X).inv ≫
          (λ_ X.X).hom ▷ N.X ≫ coequalizer.π (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)

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

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 : Mon_ C
M N : Bimod X Y
f : M ⟶ N
this : (λ_ (X.X ⊗ N.X)).inv ≫ (α_ (𝟙_ C) X.X N.X).inv ≫ (λ_ X.X).hom ▷ N.X = 𝟙 (X.X ⊗ N.X)
⊢ X.X ◁ f.hom ≫
      colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    X.X ◁ f.hom ≫
      (λ_ (X.X ⊗ N.X)).inv ≫
        (α_ (𝟙_ C) X.X N.X).inv ≫
          (λ_ X.X).hom ▷ N.X ≫ coequalizer.π (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)