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
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      TensorBimod.X
        { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod X X }
        N)
    (X.X ◁ f.hom ≫
      colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one)
    ((((X.X ◁ f.hom ≫ N.actLeft) ≫ Iso.inv (λ_ N.X)) ≫ η ▷ N.X) ≫
      coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))
have h : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
    TensorBimod.X
      { X := X.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry, right_assoc := sorry,
        middle_assoc := sorry : Bimod X X }
      N)
  (X.X ◁ f.hom ≫
    colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one)
  (X.X ◁ f.hom ≫
    ((Iso.inv (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X)) ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ N.actLeft) ≫
        η ▷ N.X) ≫
      coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))
Tactic: slice_rhs 2 3 => rw [leftUnitor_inv_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
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
| tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ N.actLeft ≫ η ▷ N.X
have a : η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X ≫ X.X ◁ N.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
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      TensorBimod.X
        { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod X X }
        N)
    (X.X ◁ f.hom ≫
      colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one)
    (X.X ◁ f.hom ≫
      ((Iso.inv (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X)) ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ N.actLeft) ≫
          η ▷ N.X) ≫
        coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))
have h : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
    TensorBimod.X
      { X := X.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry, right_assoc := sorry,
        middle_assoc := sorry : Bimod X X }
      N)
  (X.X ◁ f.hom ≫
    colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one)
  (X.X ◁ f.hom ≫
    Iso.inv (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X)) ≫
      (η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X ≫ X.X ◁ N.actLeft) ≫
        coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))
Tactic: slice_rhs 3 4 => 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
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
| X.X ◁ N.actLeft
have a : Iso.inv (α_ X.X X.X N.X) ≫ Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft
Tactic: rw [← Iso.inv_hom_id_assoc (α_ X.X X.X N.X) (X.X ◁ N.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
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      TensorBimod.X
        { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod X X }
        N)
    (X.X ◁ f.hom ≫
      colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one)
    (X.X ◁ f.hom ≫
      Iso.inv (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X)) ≫
        (η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X ≫ X.X ◁ N.actLeft) ≫
          coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))
have h : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
    TensorBimod.X
      { X := X.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry, right_assoc := sorry,
        middle_assoc := sorry : Bimod X X }
      N)
  (X.X ◁ f.hom ≫
    colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one)
  (X.X ◁ f.hom ≫
    Iso.inv (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X)) ≫
      η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X ≫
        (Iso.inv (α_ X.X X.X N.X) ≫ Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft) ≫
          coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))
Tactic: slice_rhs 4 4 => rw [← Iso.inv_hom_id_assoc (α_ X.X X.X N.X) (X.X ◁ N.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
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
| Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft ≫ coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)
have a : μ ▷ N.X ≫ coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)
Tactic: rw [← Category.assoc, ← coequalizer.condition]
-- 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
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      TensorBimod.X
        { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod X X }
        N)
    (X.X ◁ f.hom ≫
      colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one)
    (X.X ◁ f.hom ≫
      Iso.inv (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X)) ≫
        η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X ≫
          (Iso.inv (α_ X.X X.X N.X) ≫ Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft) ≫
            coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))
have h : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
    TensorBimod.X
      { X := X.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry, right_assoc := sorry,
        middle_assoc := sorry : Bimod X X }
      N)
  (X.X ◁ f.hom ≫
    colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one)
  (X.X ◁ f.hom ≫
    Iso.inv (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X)) ≫
      η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X ≫
        Iso.inv (α_ X.X X.X N.X) ≫ μ ▷ N.X ≫ coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))
Tactic: slice_rhs 5 7 => rw [← Category.assoc, ← coequalizer.condition]
-- 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
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
| η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X ≫ Iso.inv (α_ X.X X.X N.X)
have a : Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X.X N.X) ≫ η ▷ X.X ▷ N.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
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      TensorBimod.X
        { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod X X }
        N)
    (X.X ◁ f.hom ≫
      colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one)
    (X.X ◁ f.hom ≫
      Iso.inv (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X)) ≫
        η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X ≫
          Iso.inv (α_ X.X X.X N.X) ≫ μ ▷ N.X ≫ coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))
have h : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
    TensorBimod.X
      { X := X.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry, right_assoc := sorry,
        middle_assoc := sorry : Bimod X X }
      N)
  (X.X ◁ f.hom ≫
    colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one)
  (X.X ◁ f.hom ≫
    Iso.inv (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X)) ≫
      ((Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X.X N.X) ≫ η ▷ X.X ▷ N.X) ≫ μ ▷ N.X) ≫
        coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))
Tactic: slice_rhs 3 4 => 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
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
| η ▷ X.X ▷ N.X ≫ μ ▷ N.X
have a : Iso.hom (λ_ X.X) ▷ N.X
Tactic: rw [← comp_whiskerRight, MonObj.one_mul]
-- 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
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      TensorBimod.X
        { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod X X }
        N)
    (X.X ◁ f.hom ≫
      colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one)
    (X.X ◁ f.hom ≫
      Iso.inv (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X)) ≫
        ((Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X.X N.X) ≫ η ▷ X.X ▷ N.X) ≫ μ ▷ N.X) ≫
          coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))
have h : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
    TensorBimod.X
      { X := X.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry, right_assoc := sorry,
        middle_assoc := sorry : Bimod X X }
      N)
  (X.X ◁ f.hom ≫
    colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one)
  (X.X ◁ f.hom ≫
    Iso.inv (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X)) ≫
      Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X.X N.X) ≫
        Iso.hom (λ_ X.X) ▷ N.X ≫ coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))
Tactic: slice_rhs 4 5 => rw [← comp_whiskerRight, MonObj.one_mul]
-- 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
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon.{v₁, u₁} C
M : Bimod W X
N : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
⊢ (M.tensorBimod N).whiskerLeft f =
    Iso.hom (M.associatorBimod N P) ≫ M.whiskerLeft (N.whiskerLeft f) ≫ Iso.inv (M.associatorBimod N P')
have dsimp : { X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := sorry, left_assoc := sorry,
        actRight := TensorBimod.actRight M N, actRight_one := sorry, right_assoc := sorry, middle_assoc := sorry }.whiskerLeft
    f =
  Iso.hom
      (isoOfIso
        { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := sorry, inv_hom_id := sorry :
          TensorBimod.X
              { X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := sorry, left_assoc := sorry,
                actRight := TensorBimod.actRight M N, actRight_one := sorry, right_assoc := sorry, middle_assoc := sorry :
                Bimod W Y }
              P ≅
            TensorBimod.X M
              { X := TensorBimod.X N P, actLeft := TensorBimod.actLeft N P, one_actLeft := sorry, left_assoc := sorry,
                actRight := TensorBimod.actRight N P, actRight_one := sorry, right_assoc := sorry, middle_assoc := sorry :
                Bimod X Z } }
        sorry sorry) ≫
    M.whiskerLeft (N.whiskerLeft f) ≫
      Iso.inv
        (isoOfIso
          { hom := AssociatorBimod.hom M N P', inv := AssociatorBimod.inv M N P', hom_inv_id := sorry, inv_hom_id := sorry :
            TensorBimod.X
                { X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := sorry, left_assoc := sorry,
                  actRight := TensorBimod.actRight M N, actRight_one := sorry, right_assoc := sorry, middle_assoc := sorry :
                  Bimod W Y }
                P' ≅
              TensorBimod.X M
                { X := TensorBimod.X N P', actLeft := TensorBimod.actLeft N P', one_actLeft := sorry, left_assoc := sorry,
                  actRight := TensorBimod.actRight N P', actRight_one := sorry, right_assoc := sorry, middle_assoc := sorry :
                  Bimod X Z } }
          sorry sorry)
Tactic: dsimp [tensorHom, tensorBimod, associatorBimod]
-- 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
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon.{v₁, u₁} C
M : Bimod W X
N : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
| CategoryStruct.comp (Y :=
    coequalizer (TensorBimod.actRight M N ▷ P.X)
      (Iso.hom (α_ (TensorBimod.X M N) Y.X P.X) ≫ TensorBimod.X M N ◁ P.actLeft))
    (coequalizer.π (TensorBimod.actRight M N ▷ P.X)
      (Iso.hom (α_ (TensorBimod.X M N) Y.X P.X) ≫ TensorBimod.X M N ◁ P.actLeft))
    (colimMap
      (parallelPairHom (TensorBimod.actRight M N ▷ P.X)
        (Iso.hom (α_ (TensorBimod.X M N) Y.X P.X) ≫ TensorBimod.X M N ◁ P.actLeft) (TensorBimod.actRight M N ▷ P'.X)
        (Iso.hom (α_ (TensorBimod.X M N) Y.X P'.X) ≫ TensorBimod.X M N ◁ P'.actLeft)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (TensorBimod.X M N) Y.X ◁ f.hom) (TensorBimod.X M N ◁ f.hom) ⋯ ⋯))
have rw : TensorBimod.X M N ◁ f.hom ≫
  colimit.ι
    (parallelPair (TensorBimod.actRight M N ▷ P'.X)
      (Iso.hom (α_ (TensorBimod.X M N) Y.X P'.X) ≫ TensorBimod.X M N ◁ P'.actLeft))
    WalkingParallelPair.one
Tactic: rw [ι_colimMap, parallelPairHom_app_one]
-- 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
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon.{v₁, u₁} C
M : Bimod W X
N : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
| CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) M.X (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
    (M.X ◁ coequalizer.π (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft))
    (M.X ◁
      colimMap
        (parallelPairHom (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (N.actRight ▷ P'.X)
          (Iso.hom (α_ N.X Y.X P'.X) ≫ N.X ◁ P'.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) N.X Y.X ◁ f.hom) (N.X ◁ f.hom)
          ⋯ ⋯))
have a : M.X ◁
  (N.X ◁ f.hom ≫
    colimit.ι (parallelPair (N.actRight ▷ P'.X) (Iso.hom (α_ N.X Y.X P'.X) ≫ N.X ◁ P'.actLeft)) WalkingParallelPair.one)
Tactic: rw [← whiskerLeft_comp, ι_colimMap, parallelPairHom_app_one]
-- 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
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon.{v₁, u₁} C
M : Bimod W X
N : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
| M.X ◁
    (N.X ◁ f.hom ≫
      colimit.ι (parallelPair (N.actRight ▷ P'.X) (Iso.hom (α_ N.X Y.X P'.X) ≫ N.X ◁ P'.actLeft))
        WalkingParallelPair.one)
have a : M.X ◁ N.X ◁ f.hom ≫
  M.X ◁
    colimit.ι (parallelPair (N.actRight ▷ P'.X) (Iso.hom (α_ N.X Y.X P'.X) ≫ N.X ◁ P'.actLeft)) WalkingParallelPair.one
Tactic: rw [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
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon.{v₁, u₁} C
M : Bimod W X
N : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
| (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) M.X
        (coequalizer (N.actRight ▷ P'.X) (Iso.hom (α_ N.X Y.X P'.X) ≫ N.X ◁ P'.actLeft)))
      (M.X ◁
        colimit.ι (parallelPair (N.actRight ▷ P'.X) (Iso.hom (α_ N.X Y.X P'.X) ≫ N.X ◁ P'.actLeft))
          WalkingParallelPair.one)
      (CategoryStruct.comp (Y :=
        coequalizer (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) M.X
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) N.X Y.X) P'.X))
          (M.X ◁ N.actRight ▷ P'.X) (M.X ◁ (Iso.hom (α_ N.X Y.X P'.X) ≫ N.X ◁ P'.actLeft)))
        (Iso.inv
          (PreservesCoequalizer.iso (tensorLeft M.X) (N.actRight ▷ P'.X)
            (Iso.hom (α_ N.X Y.X P'.X) ≫ N.X ◁ P'.actLeft)))
        (coequalizer.desc
          (Iso.inv (α_ M.X N.X P'.X) ≫
            coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X X.X N.X) ≫ M.X ◁ N.actLeft) ▷ P'.X ≫
              coequalizer.π (TensorBimod.actRight M N ▷ P'.X)
                (Iso.hom (α_ (TensorBimod.X M N) Y.X P'.X) ≫ TensorBimod.X M N ◁ P'.actLeft))
          ⋯)) :
    tensorObj.{v₁, u₁} (𝒞 := inst) M.X (tensorObj.{v₁, u₁} (𝒞 := inst) N.X P'.X) ⟶
      colimit
        (parallelPair (TensorBimod.actRight M N ▷ P'.X)
          (Iso.hom (α_ (coequalizer (M.actRight ▷ N.X) (Iso.hom (α_ M.X X.X N.X) ≫ M.X ◁ N.actLeft)) Y.X P'.X) ≫
            coequalizer (M.actRight ▷ N.X) (Iso.hom (α_ M.X X.X N.X) ≫ M.X ◁ N.actLeft) ◁ P'.actLeft)))
have a : Iso.inv (α_ M.X N.X P'.X) ≫
  coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X X.X N.X) ≫ M.X ◁ N.actLeft) ▷ P'.X ≫
    coequalizer.π (TensorBimod.actRight M N ▷ P'.X)
      (Iso.hom (α_ (TensorBimod.X M N) Y.X P'.X) ≫ TensorBimod.X M N ◁ P'.actLeft)
Tactic: rw [id_tensor_π_preserves_coequalizer_inv_desc]
-- 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
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon.{v₁, u₁} C
M : Bimod W X
N : Bimod X Y
P P' : Bimod Y Z
f : P ⟶ P'
| M.X ◁ N.X ◁ f.hom ≫ Iso.inv (α_ M.X N.X P'.X)
have a : Iso.inv (α_ M.X N.X P.X) ≫ tensorObj.{v₁, u₁} (𝒞 := inst) M.X N.X ◁ f.hom
Tactic: rw [associator_inv_naturality_right]