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 : Mon.{v₁, u₁} C
P : Bimod R S
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)
| P.X ◁ μ ≫ P.actRight
have a : Iso.inv (α_ P.X S.X S.X) ≫ P.actRight ▷ S.X ≫ P.actRight
Tactic: rw [right_assoc]
-- 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 : Mon.{v₁, u₁} C
P : Bimod R S
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)
⊢ (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫ P.actRight =
    CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ)) S.X)
      (coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ▷ S.X)
      (coequalizer.desc P.actRight ⋯ ▷ S.X ≫ P.actRight)
have slice_lhs : Iso.hom (α_ P.X S.X S.X) ≫ Iso.inv (α_ P.X S.X S.X) ≫ P.actRight ▷ S.X ≫ P.actRight =
  CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ)) S.X)
    (coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ▷ S.X)
    (coequalizer.desc P.actRight sorry ▷ S.X ≫ P.actRight)
Tactic: slice_lhs 2 3 => rw [right_assoc]
-- 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 : Mon.{v₁, u₁} C
P : Bimod R S
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)
| CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ)) S.X)
    (coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ▷ S.X) (coequalizer.desc P.actRight ⋯ ▷ S.X)
have a : P.actRight ▷ S.X
Tactic: rw [← comp_whiskerRight, 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
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)
⊢ Iso.hom (α_ P.X S.X S.X) ≫ Iso.inv (α_ P.X S.X S.X) ≫ P.actRight ▷ S.X ≫ P.actRight =
    CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ)) S.X)
      (coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ▷ S.X)
      (coequalizer.desc P.actRight ⋯ ▷ S.X ≫ P.actRight)
have slice_rhs : Iso.hom (α_ P.X S.X S.X) ≫ Iso.inv (α_ P.X S.X S.X) ≫ P.actRight ▷ S.X ≫ P.actRight = P.actRight ▷ S.X ≫ P.actRight
Tactic: slice_rhs 1 2 => rw [← comp_whiskerRight, 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
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)
⊢ Iso.hom (α_ P.X S.X S.X) ≫ Iso.inv (α_ P.X S.X S.X) ≫ P.actRight ▷ S.X ≫ P.actRight = P.actRight ▷ S.X ≫ P.actRight
have rw : P.actRight ▷ S.X ≫ P.actRight = P.actRight ▷ S.X ≫ P.actRight
Tactic: rw [Iso.hom_inv_id_assoc]
-- 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
⊢ M.whiskerLeft (𝟙 N) = 𝟙 (M.tensorBimod N)
have h : Hom.hom (M.whiskerLeft (𝟙 N)) = Hom.hom (𝟙 (M.tensorBimod N))
Tactic: ext
-- 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
⊢ Hom.hom (M.whiskerLeft (𝟙 N)) = Hom.hom (𝟙 (M.tensorBimod N))
have h : coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft) ≫ Hom.hom (M.whiskerLeft (𝟙 N)) =
  coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft) ≫ Hom.hom (𝟙 (M.tensorBimod N))
Tactic: apply Limits.coequalizer.hom_ext
-- 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
⊢ whiskerRight (𝟙 M) N = 𝟙 (M.tensorBimod N)
have h : Hom.hom (whiskerRight (𝟙 M) N) = Hom.hom (𝟙 (M.tensorBimod N))
Tactic: ext
-- 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
⊢ Hom.hom (whiskerRight (𝟙 M) N) = Hom.hom (𝟙 (M.tensorBimod N))
have h : coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft) ≫ Hom.hom (whiskerRight (𝟙 M) N) =
  coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft) ≫ Hom.hom (𝟙 (M.tensorBimod N))
Tactic: apply Limits.coequalizer.hom_ext
-- 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 P Q : Bimod Y Z
f : N ⟶ P
g : P ⟶ Q
⊢ Eq (α := M.tensorBimod N ⟶ M.tensorBimod Q) (M.whiskerLeft (f ≫ g)) (M.whiskerLeft f ≫ M.whiskerLeft g)
have h : Eq (α := (M.tensorBimod N).X ⟶ (M.tensorBimod Q).X) (Hom.hom (M.whiskerLeft (f ≫ g)))
  (Hom.hom (M.whiskerLeft f ≫ M.whiskerLeft g))
Tactic: ext
-- 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 P Q : Bimod Y Z
f : N ⟶ P
g : P ⟶ Q
⊢ Eq (α := (M.tensorBimod N).X ⟶ (M.tensorBimod Q).X) (Hom.hom (M.whiskerLeft (f ≫ g)))
    (Hom.hom (M.whiskerLeft f ≫ M.whiskerLeft g))
have h : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) M.X N.X ⟶ (M.tensorBimod Q).X)
  (coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft) ≫ Hom.hom (M.whiskerLeft (f ≫ g)))
  (coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft) ≫
    Hom.hom (M.whiskerLeft f ≫ M.whiskerLeft g))
Tactic: apply Limits.coequalizer.hom_ext
-- 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 (α := (regular X).tensorBimod M ⟶ (regular X).tensorBimod N) ((regular X).whiskerLeft f)
    (Iso.hom M.leftUnitorBimod ≫ f ≫ Iso.inv N.leftUnitorBimod)
have dsimp : Eq (α :=
  { X := X.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry, right_assoc := sorry,
          middle_assoc := sorry : Bimod X X }.tensorBimod
      M ⟶
    { X := X.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry, right_assoc := sorry,
          middle_assoc := sorry : Bimod X X }.tensorBimod
      N)
  ({ X := X.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry, right_assoc := sorry,
        middle_assoc := sorry }.whiskerLeft
    f)
  (Iso.hom
      (isoOfIso { hom := LeftUnitorBimod.hom M, inv := LeftUnitorBimod.inv M, hom_inv_id := sorry, inv_hom_id := sorry } sorry sorry) ≫
    f ≫
      Iso.inv
        (isoOfIso
          { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := sorry, inv_hom_id := sorry :
            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 ≅
              N.X }
          sorry sorry))
Tactic: dsimp [tensorHom, regular, leftUnitorBimod]
-- 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 (α :=
    { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
            middle_assoc := ⋯ : Bimod X X }.tensorBimod
        M ⟶
      { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
            middle_assoc := ⋯ : Bimod X X }.tensorBimod
        N)
    ({ X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ }.whiskerLeft
      f)
    (Iso.hom
        (isoOfIso { hom := LeftUnitorBimod.hom M, inv := LeftUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
          ⋯) ≫
      f ≫
        Iso.inv
          (isoOfIso
            { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ :
              TensorBimod.X
                  { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ : Bimod X X }
                  N ≅
                N.X }
            ⋯ ⋯))
have h : Eq (α :=
  ({ X := X.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry, right_assoc := sorry,
            middle_assoc := sorry : Bimod X X }.tensorBimod
        M).X ⟶
    ({ X := X.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry, right_assoc := sorry,
            middle_assoc := sorry : Bimod X X }.tensorBimod
        N).X)
  (Hom.hom
    ({ X := X.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry, right_assoc := sorry,
          middle_assoc := sorry }.whiskerLeft
      f))
  (Hom.hom
    (Iso.hom
        (isoOfIso { hom := LeftUnitorBimod.hom M, inv := LeftUnitorBimod.inv M, hom_inv_id := sorry, inv_hom_id := sorry } sorry
          sorry) ≫
      f ≫
        Iso.inv
          (isoOfIso
            { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := sorry, inv_hom_id := sorry :
              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 ≅
                N.X }
            sorry sorry)))
Tactic: ext
-- 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
| CategoryStruct.comp (Y := coequalizer (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft))
    (coequalizer.π (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft))
    (colimMap
      (parallelPairHom (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft) (μ ▷ N.X)
        (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) X.X X.X ◁ f.hom) (X.X ◁ f.hom) ⋯
        ⋯))
have rw : X.X ◁ f.hom ≫ colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.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 : 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 :
      (parallelPair (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft)).obj WalkingParallelPair.one ⟶
        colimit (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)))
    (CategoryStruct.comp (Y := coequalizer (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft))
        (coequalizer.π (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft) :
          tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶ coequalizer (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft))
        (LeftUnitorBimod.hom M ≫ f.hom ≫ LeftUnitorBimod.inv N :
          TensorBimod.X
              { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ : Bimod X X }
              M ⟶
            TensorBimod.X
              { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ : Bimod X X }
              N) :
      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)
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 :
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      colimit (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)))
  (CategoryStruct.comp (Y := coequalizer (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft))
      (coequalizer.π (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft))
      (coequalizer.desc M.actLeft sorry ≫ f.hom ≫ LeftUnitorBimod.inv N) :
    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)
Tactic: dsimp [LeftUnitorBimod.hom]
-- 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
| CategoryStruct.comp (Y := coequalizer (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft))
    (coequalizer.π (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft)) (coequalizer.desc M.actLeft ⋯)
have a : M.actLeft
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)
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 :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
        colimit (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)))
    (CategoryStruct.comp (Y := coequalizer (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft))
        (coequalizer.π (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft))
        (coequalizer.desc M.actLeft ⋯ ≫ f.hom ≫ LeftUnitorBimod.inv N) :
      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)
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 :
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      colimit (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)))
  ((M.actLeft ≫ f.hom) ≫ LeftUnitorBimod.inv N :
    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)
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)
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 :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
        colimit (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)))
    ((M.actLeft ≫ f.hom) ≫ LeftUnitorBimod.inv N :
      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)
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)
  ((M.actLeft ≫ f.hom) ≫
    Iso.inv (λ_ N.X) ≫ η ▷ N.X ≫ coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))
Tactic: dsimp [LeftUnitorBimod.inv]
-- 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
| M.actLeft ≫ f.hom
have a : X.X ◁ f.hom ≫ N.actLeft
Tactic: rw [Hom.left_act_hom]
-- 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)
    ((M.actLeft ≫ f.hom) ≫
      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 ≫ N.actLeft) ≫ Iso.inv (λ_ N.X)) ≫ η ▷ N.X) ≫
    coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))
Tactic: slice_rhs 1 2 => rw [Hom.left_act_hom]
-- 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
| N.actLeft ≫ Iso.inv (λ_ N.X)
have a : Iso.inv (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X)) ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ N.actLeft
Tactic: rw [leftUnitor_inv_naturality]