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 Z : Mon.{v₁, u₁} C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
| CategoryStruct.comp (Y := TensorBimod.X M Q)
    (colimit.ι (parallelPair (M.actRight ▷ Q.X) (Iso.hom (α_ M.X Y.X Q.X) ≫ M.X ◁ Q.actLeft)) WalkingParallelPair.one)
    (colimMap
      (parallelPairHom (M.actRight ▷ Q.X) (Iso.hom (α_ M.X Y.X Q.X) ≫ M.X ◁ Q.actLeft) (N.actRight ▷ Q.X)
        (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft) (f.hom ▷ Y.X ▷ Q.X) (f.hom ▷ Q.X) ⋯ ⋯))
have a : f.hom ▷ Q.X ≫
  colimit.ι (parallelPair (N.actRight ▷ Q.X) (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.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)
X Y Z : Mon.{v₁, u₁} C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) M.X P.X ⟶ TensorBimod.X N Q)
    (CategoryStruct.comp (Y := TensorBimod.X M Q)
      (M.X ◁ g.hom ≫
        colimit.ι (parallelPair (M.actRight ▷ Q.X) (Iso.hom (α_ M.X Y.X Q.X) ≫ M.X ◁ Q.actLeft))
          WalkingParallelPair.one)
      (colimMap
        (parallelPairHom (M.actRight ▷ Q.X) (Iso.hom (α_ M.X Y.X Q.X) ≫ M.X ◁ Q.actLeft) (N.actRight ▷ Q.X)
          (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft) (f.hom ▷ Y.X ▷ Q.X) (f.hom ▷ Q.X) ⋯ ⋯)))
    (CategoryStruct.comp (Y := coequalizer (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
      (coequalizer.π (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
      (CategoryStruct.comp (Y := TensorBimod.X N P)
        (colimMap
          (parallelPairHom (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X)
            (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯))
        (colimMap
          (parallelPairHom (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X)
            (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) N.X Y.X ◁ g.hom) (N.X ◁ g.hom)
            ⋯ ⋯))))
have h : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) M.X P.X ⟶ TensorBimod.X N Q)
  (M.X ◁ g.hom ≫
    f.hom ▷ Q.X ≫
      colimit.ι (parallelPair (N.actRight ▷ Q.X) (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft)) WalkingParallelPair.one)
  (CategoryStruct.comp (Y := coequalizer (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
    (coequalizer.π (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
    (CategoryStruct.comp (Y := TensorBimod.X N P)
      (colimMap
        (parallelPairHom (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X)
          (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) sorry sorry))
      (colimMap
        (parallelPairHom (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X)
          (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) N.X Y.X ◁ g.hom) (N.X ◁ g.hom) sorry
          sorry))))
Tactic: slice_lhs 2 3 => 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)
X Y Z : Mon.{v₁, u₁} 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
have a : f.hom ▷ P.X ≫ N.X ◁ g.hom
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 Z : Mon.{v₁, u₁} C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) M.X P.X ⟶ TensorBimod.X N Q)
    (M.X ◁ g.hom ≫
      f.hom ▷ Q.X ≫
        colimit.ι (parallelPair (N.actRight ▷ Q.X) (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft))
          WalkingParallelPair.one)
    (CategoryStruct.comp (Y := coequalizer (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
      (coequalizer.π (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
      (CategoryStruct.comp (Y := TensorBimod.X N P)
        (colimMap
          (parallelPairHom (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X)
            (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯))
        (colimMap
          (parallelPairHom (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X)
            (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) N.X Y.X ◁ g.hom) (N.X ◁ g.hom)
            ⋯ ⋯))))
have h : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) M.X P.X ⟶ TensorBimod.X N Q)
  ((f.hom ▷ P.X ≫ N.X ◁ g.hom) ≫
    colimit.ι (parallelPair (N.actRight ▷ Q.X) (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft)) WalkingParallelPair.one)
  (CategoryStruct.comp (Y := coequalizer (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
    (coequalizer.π (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
    (CategoryStruct.comp (Y := TensorBimod.X N P)
      (colimMap
        (parallelPairHom (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X)
          (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) sorry sorry))
      (colimMap
        (parallelPairHom (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X)
          (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) N.X Y.X ◁ g.hom) (N.X ◁ g.hom) sorry
          sorry))))
Tactic: slice_lhs 1 2 => 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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
⊢ whiskerRight (Iso.hom (M.associatorBimod N P)) Q ≫
      Iso.hom (M.associatorBimod (N.tensorBimod P) Q) ≫ M.whiskerLeft (Iso.hom (N.associatorBimod P Q)) =
    Iso.hom ((M.tensorBimod N).associatorBimod P Q) ≫ Iso.hom (M.associatorBimod N (P.tensorBimod Q))
have dsimp : whiskerRight
      (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 (M.tensorBimod N) P ≅ TensorBimod.X M (N.tensorBimod P) }
          sorry sorry))
      Q ≫
    Iso.hom
        (isoOfIso
          { hom := AssociatorBimod.hom M (N.tensorBimod P) Q, inv := AssociatorBimod.inv M (N.tensorBimod P) Q,
            hom_inv_id := sorry, inv_hom_id := sorry :
            TensorBimod.X (M.tensorBimod (N.tensorBimod P)) Q ≅ TensorBimod.X M ((N.tensorBimod P).tensorBimod Q) }
          sorry sorry) ≫
      M.whiskerLeft
        (Iso.hom
          (isoOfIso
            { hom := AssociatorBimod.hom N P Q, inv := AssociatorBimod.inv N P Q, hom_inv_id := sorry, inv_hom_id := sorry :
              TensorBimod.X (N.tensorBimod P) Q ≅ TensorBimod.X N (P.tensorBimod Q) }
            sorry sorry)) =
  Iso.hom
      (isoOfIso
        { hom := AssociatorBimod.hom (M.tensorBimod N) P Q, inv := AssociatorBimod.inv (M.tensorBimod N) P Q,
          hom_inv_id := sorry, inv_hom_id := sorry :
          TensorBimod.X ((M.tensorBimod N).tensorBimod P) Q ≅ TensorBimod.X (M.tensorBimod N) (P.tensorBimod Q) }
        sorry sorry) ≫
    Iso.hom
      (isoOfIso
        { hom := AssociatorBimod.hom M N (P.tensorBimod Q), inv := AssociatorBimod.inv M N (P.tensorBimod Q),
          hom_inv_id := sorry, inv_hom_id := sorry }
        sorry sorry)
Tactic: dsimp [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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
| CategoryStruct.comp (Y :=
    coequalizer (TensorBimod.actRight (M.tensorBimod N) P ▷ Q.X)
      (Iso.hom (α_ (TensorBimod.X (M.tensorBimod N) P) Y.X Q.X) ≫ TensorBimod.X (M.tensorBimod N) P ◁ Q.actLeft))
    (coequalizer.π (TensorBimod.actRight (M.tensorBimod N) P ▷ Q.X)
      (Iso.hom (α_ (TensorBimod.X (M.tensorBimod N) P) Y.X Q.X) ≫ TensorBimod.X (M.tensorBimod N) P ◁ Q.actLeft))
    (colimMap
      (parallelPairHom (TensorBimod.actRight (M.tensorBimod N) P ▷ Q.X)
        (Iso.hom (α_ (TensorBimod.X (M.tensorBimod N) P) Y.X Q.X) ≫ TensorBimod.X (M.tensorBimod N) P ◁ Q.actLeft)
        (TensorBimod.actRight M (N.tensorBimod P) ▷ Q.X)
        (Iso.hom (α_ (TensorBimod.X M (N.tensorBimod P)) Y.X Q.X) ≫ TensorBimod.X M (N.tensorBimod P) ◁ Q.actLeft)
        (coequalizer.desc (AssociatorBimod.homAux M N P) ⋯ ▷ Y.X ▷ Q.X)
        (coequalizer.desc (AssociatorBimod.homAux M N P) ⋯ ▷ Q.X) ⋯ ⋯))
have a : coequalizer.desc (AssociatorBimod.homAux M N P) sorry ▷ Q.X ≫
  colimit.ι
    (parallelPair (TensorBimod.actRight M (N.tensorBimod P) ▷ Q.X)
      (Iso.hom (α_ (TensorBimod.X M (N.tensorBimod P)) Y.X Q.X) ≫ TensorBimod.X M (N.tensorBimod P) ◁ Q.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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
| CategoryStruct.comp (Y := TensorBimod.X (M.tensorBimod (N.tensorBimod P)) Q)
    (colimit.ι
      (parallelPair (TensorBimod.actRight M (N.tensorBimod P) ▷ Q.X)
        (Iso.hom (α_ (TensorBimod.X M (N.tensorBimod P)) Y.X Q.X) ≫ TensorBimod.X M (N.tensorBimod P) ◁ Q.actLeft))
      WalkingParallelPair.one)
    (coequalizer.desc (AssociatorBimod.homAux M (N.tensorBimod P) Q) ⋯)
have a : AssociatorBimod.homAux M (N.tensorBimod P) Q
Tactic: rw [coequalizer.π_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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
| CategoryStruct.comp (Y :=
    coequalizer (TensorBimod.actRight (M.tensorBimod N) P ▷ Q.X)
      (Iso.hom (α_ (TensorBimod.X (M.tensorBimod N) P) Y.X Q.X) ≫ TensorBimod.X (M.tensorBimod N) P ◁ Q.actLeft))
    (coequalizer.π (TensorBimod.actRight (M.tensorBimod N) P ▷ Q.X)
      (Iso.hom (α_ (TensorBimod.X (M.tensorBimod N) P) Y.X Q.X) ≫ TensorBimod.X (M.tensorBimod N) P ◁ Q.actLeft))
    (coequalizer.desc (AssociatorBimod.homAux (M.tensorBimod N) P Q) ⋯)
have a : AssociatorBimod.homAux (M.tensorBimod N) P Q
Tactic: rw [coequalizer.π_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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
⊢ coequalizer.desc (AssociatorBimod.homAux M N P) ⋯ ▷ Q.X ≫
      AssociatorBimod.homAux M (N.tensorBimod P) Q ≫
        colimMap
          (parallelPairHom (M.actRight ▷ TensorBimod.X (N.tensorBimod P) Q)
            (Iso.hom (α_ M.X W.X (TensorBimod.X (N.tensorBimod P) Q)) ≫ M.X ◁ TensorBimod.actLeft (N.tensorBimod P) Q)
            (M.actRight ▷ TensorBimod.X N (P.tensorBimod Q))
            (Iso.hom (α_ M.X W.X (TensorBimod.X N (P.tensorBimod Q))) ≫ M.X ◁ TensorBimod.actLeft N (P.tensorBimod Q))
            (tensorObj.{v₁, u₁} (𝒞 := inst) M.X W.X ◁ coequalizer.desc (AssociatorBimod.homAux N P Q) ⋯)
            (M.X ◁ coequalizer.desc (AssociatorBimod.homAux N P Q) ⋯) ⋯ ⋯) =
    CategoryStruct.comp (Y :=
      coequalizer (TensorBimod.actRight (M.tensorBimod N) P ▷ Q.X)
        (Iso.hom (α_ (TensorBimod.X (M.tensorBimod N) P) Y.X Q.X) ≫ TensorBimod.X (M.tensorBimod N) P ◁ Q.actLeft))
      (coequalizer.π (TensorBimod.actRight (M.tensorBimod N) P ▷ Q.X)
        (Iso.hom (α_ (TensorBimod.X (M.tensorBimod N) P) Y.X Q.X) ≫ TensorBimod.X (M.tensorBimod N) P ◁ Q.actLeft))
      (coequalizer.desc (AssociatorBimod.homAux (M.tensorBimod N) P Q) ⋯ ≫
        coequalizer.desc (AssociatorBimod.homAux M N (P.tensorBimod Q)) ⋯)
have h : coequalizer.desc (AssociatorBimod.homAux M N P) sorry ▷ Q.X ≫
    AssociatorBimod.homAux M (N.tensorBimod P) Q ≫
      colimMap
        (parallelPairHom (M.actRight ▷ TensorBimod.X (N.tensorBimod P) Q)
          (Iso.hom (α_ M.X W.X (TensorBimod.X (N.tensorBimod P) Q)) ≫ M.X ◁ TensorBimod.actLeft (N.tensorBimod P) Q)
          (M.actRight ▷ TensorBimod.X N (P.tensorBimod Q))
          (Iso.hom (α_ M.X W.X (TensorBimod.X N (P.tensorBimod Q))) ≫ M.X ◁ TensorBimod.actLeft N (P.tensorBimod Q))
          (tensorObj.{v₁, u₁} (𝒞 := inst) M.X W.X ◁ coequalizer.desc (AssociatorBimod.homAux N P Q) sorry)
          (M.X ◁ coequalizer.desc (AssociatorBimod.homAux N P Q) sorry) sorry sorry) =
  AssociatorBimod.homAux (M.tensorBimod N) P Q ≫ coequalizer.desc (AssociatorBimod.homAux M N (P.tensorBimod Q)) sorry
Tactic: slice_rhs 1 2 => rw [coequalizer.π_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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
| (M.X ◁ coequalizer.π (N.actRight ▷ P.X) (Iso.hom (α_ N.X X.X P.X) ≫ N.X ◁ P.actLeft)) ▷ Q.X ≫
    Iso.hom (α_ M.X (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X X.X P.X) ≫ N.X ◁ P.actLeft)) Q.X)
have a : Iso.hom (α_ M.X (tensorObj.{v₁, u₁} (𝒞 := inst) N.X P.X) Q.X) ≫
  M.X ◁ coequalizer.π (N.actRight ▷ P.X) (Iso.hom (α_ N.X X.X P.X) ≫ N.X ◁ P.actLeft) ▷ Q.X
Tactic: rw [associator_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
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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: slice_lhs 2 3 => rw [associator_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
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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
| coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X W.X N.X) ≫ M.X ◁ N.actLeft) ▷ P.X ▷ Q.X ≫
    Iso.hom (α_ (coequalizer (M.actRight ▷ N.X) (Iso.hom (α_ M.X W.X N.X) ≫ M.X ◁ N.actLeft)) P.X Q.X)
have a : Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N.X) P.X Q.X) ≫
  coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X W.X N.X) ≫ M.X ◁ N.actLeft) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.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
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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
| coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X W.X N.X) ≫ M.X ◁ N.actLeft) ▷
      tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X ≫
    coequalizer (M.actRight ▷ N.X) (Iso.hom (α_ M.X W.X N.X) ≫ M.X ◁ N.actLeft) ◁
      coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft)
have a : tensorObj.{v₁, u₁} (𝒞 := inst) M.X N.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
  coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X W.X N.X) ≫ M.X ◁ N.actLeft) ▷
    coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.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
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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
| tensorObj.{v₁, u₁} (𝒞 := inst) M.X N.X ◁
      coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
    Iso.hom (α_ M.X N.X (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft)))
have a : Iso.hom (α_ M.X N.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ≫
  M.X ◁ N.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.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
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 Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
⊢ Eq (α := (M.tensorBimod (regular Y)).tensorBimod N ⟶ M.tensorBimod N)
    (Iso.hom (M.associatorBimod (regular Y) N) ≫ M.whiskerLeft (Iso.hom N.leftUnitorBimod))
    (whiskerRight (Iso.hom M.rightUnitorBimod) N)
have dsimp : Eq (α := (M.tensorBimod (regular Y)).tensorBimod N ⟶ M.tensorBimod N)
  (Iso.hom
      (isoOfIso
        { hom := AssociatorBimod.hom M (regular Y) N, inv := AssociatorBimod.inv M (regular Y) N, hom_inv_id := sorry,
          inv_hom_id := sorry : TensorBimod.X (M.tensorBimod (regular Y)) N ≅ TensorBimod.X M ((regular Y).tensorBimod N) }
        sorry sorry) ≫
    M.whiskerLeft
      (Iso.hom
        (isoOfIso { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := sorry, inv_hom_id := sorry } sorry
          sorry)))
  (whiskerRight
    (Iso.hom
      (isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := sorry, inv_hom_id := sorry } sorry sorry))
    N)
Tactic: dsimp [associatorBimod, leftUnitorBimod, rightUnitorBimod]
-- 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 Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
⊢ Eq (α := (M.tensorBimod (regular Y)).tensorBimod N ⟶ M.tensorBimod N)
    (Iso.hom
        (isoOfIso
          { hom := AssociatorBimod.hom M (regular Y) N, inv := AssociatorBimod.inv M (regular Y) N, hom_inv_id := ⋯,
            inv_hom_id := ⋯ :
            TensorBimod.X (M.tensorBimod (regular Y)) N ≅ TensorBimod.X M ((regular Y).tensorBimod N) }
          ⋯ ⋯) ≫
      M.whiskerLeft
        (Iso.hom
          (isoOfIso { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯)))
    (whiskerRight
      (Iso.hom
        (isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
          ⋯))
      N)
have h : Eq (α := ((M.tensorBimod (regular Y)).tensorBimod N).X ⟶ (M.tensorBimod N).X)
  (Hom.hom
    (Iso.hom
        (isoOfIso
          { hom := AssociatorBimod.hom M (regular Y) N, inv := AssociatorBimod.inv M (regular Y) N, hom_inv_id := sorry,
            inv_hom_id := sorry :
            TensorBimod.X (M.tensorBimod (regular Y)) N ≅ TensorBimod.X M ((regular Y).tensorBimod N) }
          sorry sorry) ≫
      M.whiskerLeft
        (Iso.hom
          (isoOfIso { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := sorry, inv_hom_id := sorry } sorry
            sorry))))
  (Hom.hom
    (whiskerRight
      (Iso.hom
        (isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := sorry, inv_hom_id := sorry } sorry
          sorry))
      N))
Tactic: ext