awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) R.X (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
      (η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X ≫
          R.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) :
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
          tensorObj.{v₁, u₁} (𝒞 := inst) R.X
            (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
      (actLeft P Q : tensorObj.{v₁, u₁} (𝒞 := inst) R.X (X P Q) ⟶ X P Q) =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
      Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
have slice_lhs : η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X ≫
    Iso.inv (α_ R.X P.X Q.X) ≫
      P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) =
  tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
    Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
Tactic: slice_lhs 2 3 => rw [whiskerLeft_π_actLeft]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X ≫ Iso.inv (α_ R.X P.X Q.X)
have a : Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) P.X Q.X) ≫ η ▷ P.X ▷ Q.X
Tactic: rw [associator_inv_naturality_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X ≫
      Iso.inv (α_ R.X P.X Q.X) ≫
        P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
      Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
have slice_lhs : ((Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) P.X Q.X) ≫ η ▷ P.X ▷ Q.X) ≫ P.actLeft ▷ Q.X) ≫
    coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) =
  tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
    Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
Tactic: slice_lhs 1 2 => rw [associator_inv_naturality_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| η ▷ P.X ▷ Q.X ≫ P.actLeft ▷ Q.X
have a : Iso.hom (λ_ P.X) ▷ Q.X
Tactic: rw [← comp_whiskerRight, one_actLeft]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ ((Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) P.X Q.X) ≫ η ▷ P.X ▷ Q.X) ≫ P.actLeft ▷ Q.X) ≫
      coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
      Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
have slice_lhs : Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) P.X Q.X) ≫
    Iso.hom (λ_ P.X) ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) =
  tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
    Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
Tactic: slice_lhs 2 3 => rw [← comp_whiskerRight, one_actLeft]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
    Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
have rw : Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ≫
  coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)
Tactic: rw [leftUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) P.X Q.X) ≫
      Iso.hom (λ_ P.X) ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
      Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
have slice_rhs : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
    coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
  (Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) P.X Q.X) ≫
    Iso.hom (λ_ P.X) ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
  (Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ≫
    coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
Tactic: slice_rhs 1 2 => rw [leftUnitor_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ μ ▷ X P Q ≫ actLeft P Q = Iso.hom (α_ R.X R.X (X P Q)) ≫ R.X ◁ actLeft P Q ≫ actLeft P Q
have refine : Eq (α :=
  Functor.obj.{v₁, v₁, u₁, u₁} (tensorLeft (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X))
      (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
    X P Q)
  (CategoryTheory.Functor.map (tensorLeft (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X))
      (coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) ≫
    μ ▷ X P Q ≫ actLeft P Q)
  (CategoryTheory.Functor.map (tensorLeft (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X))
      (coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) ≫
    Iso.hom (α_ R.X R.X (X P Q)) ≫ R.X ◁ actLeft P Q ≫ actLeft P Q)
Tactic: refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X ◁
      coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
    μ ▷ coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)
have a : μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X ≫
  R.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)
Tactic: rw [whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X ≫ Iso.inv (α_ R.X P.X Q.X)
have a : Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) P.X Q.X) ≫ μ ▷ P.X ▷ Q.X
Tactic: rw [associator_inv_naturality_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| μ ▷ P.X ▷ Q.X ≫ P.actLeft ▷ Q.X
have a : Iso.hom (α_ R.X R.X P.X) ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.X
Tactic: rw [← comp_whiskerRight, left_assoc, comp_whiskerRight, comp_whiskerRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X ◁
      coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
    Iso.hom (α_ R.X R.X (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
have a : Iso.hom (α_ R.X R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ≫
  R.X ◁ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)
Tactic: rw [associator_naturality_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) R.X
        (tensorObj.{v₁, u₁} (𝒞 := inst) R.X
          (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))))
      (R.X ◁ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) :
        tensorObj.{v₁, u₁} (𝒞 := inst) R.X
            (tensorObj.{v₁, u₁} (𝒞 := inst) R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ⟶
          tensorObj.{v₁, u₁} (𝒞 := inst) R.X
            (tensorObj.{v₁, u₁} (𝒞 := inst) R.X
              (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))))
      (R.X ◁ actLeft P Q :
        tensorObj.{v₁, u₁} (𝒞 := inst) R.X
            (tensorObj.{v₁, u₁} (𝒞 := inst) R.X
              (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))) ⟶
          tensorObj.{v₁, u₁} (𝒞 := inst) R.X
            (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))) :
    tensorObj.{v₁, u₁} (𝒞 := inst) R.X (tensorObj.{v₁, u₁} (𝒞 := inst) R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) R.X (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
have a : R.X ◁ Iso.inv (α_ R.X P.X Q.X) ≫
  R.X ◁ P.actLeft ▷ Q.X ≫ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)
Tactic: rw [← whiskerLeft_comp, whiskerLeft_π_actLeft,
      whiskerLeft_comp, whiskerLeft_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
      coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
    (Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) P.X Q.X) ≫
        (Iso.hom (α_ R.X R.X P.X) ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.X) ≫
          coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
        coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
    (Iso.hom (α_ R.X R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) R.X
            (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
          (R.X ◁ Iso.inv (α_ R.X P.X Q.X) ≫
              R.X ◁ P.actLeft ▷ Q.X ≫
                R.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) :
            tensorObj.{v₁, u₁} (𝒞 := inst) R.X
                (tensorObj.{v₁, u₁} (𝒞 := inst) R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ⟶
              tensorObj.{v₁, u₁} (𝒞 := inst) R.X
                (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
          (actLeft P Q : tensorObj.{v₁, u₁} (𝒞 := inst) R.X (X P Q) ⟶ X P Q) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
        coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
have slice_rhs : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
    coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
  (Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) P.X Q.X) ≫
    (Iso.hom (α_ R.X R.X P.X) ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.X) ≫
      coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
  (Iso.hom (α_ R.X R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ≫
    R.X ◁ Iso.inv (α_ R.X P.X Q.X) ≫
      R.X ◁ P.actLeft ▷ Q.X ≫
        Iso.inv (α_ R.X P.X Q.X) ≫
          P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
Tactic: slice_rhs 4 5 => rw [whiskerLeft_π_actLeft]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
| R.X ◁ P.actLeft ▷ Q.X ≫ Iso.inv (α_ R.X P.X Q.X)
have a : Iso.inv (α_ R.X (tensorObj.{v₁, u₁} (𝒞 := inst) R.X P.X) Q.X) ≫ (R.X ◁ P.actLeft) ▷ Q.X
Tactic: rw [associator_inv_naturality_middle]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
      coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
    (Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) P.X Q.X) ≫
      (Iso.hom (α_ R.X R.X P.X) ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.X) ≫
        coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
    (Iso.hom (α_ R.X R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ≫
      R.X ◁ Iso.inv (α_ R.X P.X Q.X) ≫
        R.X ◁ P.actLeft ▷ Q.X ≫
          Iso.inv (α_ R.X P.X Q.X) ≫
            P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
have slice_rhs : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
    coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
  (Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) P.X Q.X) ≫
    (Iso.hom (α_ R.X R.X P.X) ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.X) ≫
      coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
  (Iso.hom (α_ R.X R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ≫
    R.X ◁ Iso.inv (α_ R.X P.X Q.X) ≫
      ((Iso.inv (α_ R.X (tensorObj.{v₁, u₁} (𝒞 := inst) R.X P.X) Q.X) ≫ (R.X ◁ P.actLeft) ▷ Q.X) ≫ P.actLeft ▷ Q.X) ≫
        coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
Tactic: slice_rhs 3 4 => rw [associator_inv_naturality_middle]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ CategoryTheory.Functor.map (tensorRight T.X) (P.actRight ▷ Q.X) ≫ Iso.hom (α_ P.X Q.X T.X) ≫ P.X ◁ Q.actRight =
    (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
        Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫
          P.X ◁ S.X ◁ Q.actRight ≫ Iso.inv (α_ P.X S.X Q.X)) ≫
      P.actRight ▷ Q.X
have dsimp : P.actRight ▷ Q.X ▷ T.X ≫ Iso.hom (α_ P.X Q.X T.X) ≫ P.X ◁ Q.actRight =
  (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
      Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫
        P.X ◁ S.X ◁ Q.actRight ≫ Iso.inv (α_ P.X S.X Q.X)) ≫
    P.actRight ▷ Q.X
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.actRight ▷ Q.X ▷ T.X ≫ Iso.hom (α_ P.X Q.X T.X)
have a : Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫ P.actRight ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X
Tactic: rw [associator_naturality_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ P.actRight ▷ Q.X ▷ T.X ≫ Iso.hom (α_ P.X Q.X T.X) ≫ P.X ◁ Q.actRight =
    (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
        Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫
          P.X ◁ S.X ◁ Q.actRight ≫ Iso.inv (α_ P.X S.X Q.X)) ≫
      P.actRight ▷ Q.X
have slice_lhs : (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫ P.actRight ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X) ≫
    P.X ◁ Q.actRight =
  (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
      Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫
        P.X ◁ S.X ◁ Q.actRight ≫ Iso.inv (α_ P.X S.X Q.X)) ≫
    P.actRight ▷ Q.X
Tactic: slice_lhs 1 2 => rw [associator_naturality_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.actRight ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X ≫ P.X ◁ Q.actRight
have a : tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X ◁ Q.actRight ≫ P.actRight ▷ Q.X
Tactic: rw [← whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
        P.actRight ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X) ≫
      P.X ◁ Q.actRight =
    (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
        Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫
          P.X ◁ S.X ◁ Q.actRight ≫ Iso.inv (α_ P.X S.X Q.X)) ≫
      P.actRight ▷ Q.X
have slice_lhs : Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
    tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X ◁ Q.actRight ≫ P.actRight ▷ Q.X =
  (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
      Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫
        P.X ◁ S.X ◁ Q.actRight ≫ Iso.inv (α_ P.X S.X Q.X)) ≫
    P.actRight ▷ Q.X
Tactic: slice_lhs 2 3 => rw [← whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ CategoryTheory.Functor.map (tensorRight T.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
      Iso.hom (α_ P.X Q.X T.X) ≫ P.X ◁ Q.actRight =
    (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
        Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫
          P.X ◁ S.X ◁ Q.actRight ≫ Iso.inv (α_ P.X S.X Q.X)) ≫
      Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft
have dsimp : (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ T.X ≫ Iso.hom (α_ P.X Q.X T.X) ≫ P.X ◁ Q.actRight =
  (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
      Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫
        P.X ◁ S.X ◁ Q.actRight ≫ Iso.inv (α_ P.X S.X Q.X)) ≫
    Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
inst_2 : HasCoequalizers.{v₁, u₁} C
R S T : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ T.X ≫ Iso.hom (α_ P.X Q.X T.X) ≫ P.X ◁ Q.actRight =
    (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
        Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫
          P.X ◁ S.X ◁ Q.actRight ≫ Iso.inv (α_ P.X S.X Q.X)) ≫
      Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft
have simp : Iso.hom (α_ P.X S.X Q.X) ▷ T.X ≫
    Iso.hom (α_ P.X (tensorObj.{v₁, u₁} (𝒞 := inst) S.X Q.X) T.X) ≫ P.X ◁ Q.actLeft ▷ T.X ≫ P.X ◁ Q.actRight =
  Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
    Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫ P.X ◁ S.X ◁ Q.actRight ≫ P.X ◁ Q.actLeft
Tactic: simp only [comp_whiskerRight, whisker_assoc, Category.assoc, Iso.inv_hom_id_assoc]