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 : Bimod X Y
N : Bimod Y Z
⊢ 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 := ⋯,
              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 := ⋯ } ⋯
              ⋯))))
    (Hom.hom
      (whiskerRight
        (Iso.hom
          (isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯))
        N))
have h : coequalizer.π ((M.tensorBimod (regular Y)).actRight ▷ N.X)
      (Iso.hom (α_ (M.tensorBimod (regular Y)).X Y.X N.X) ≫ (M.tensorBimod (regular Y)).X ◁ N.actLeft) ≫
    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 :
                TensorBimod.X (regular Y) N ≅ N.X }
              sorry sorry))) =
  coequalizer.π ((M.tensorBimod (regular Y)).actRight ▷ N.X)
      (Iso.hom (α_ (M.tensorBimod (regular Y)).X Y.X N.X) ≫ (M.tensorBimod (regular Y)).X ◁ N.actLeft) ≫
    Hom.hom
      (whiskerRight
        (Iso.hom
          (isoOfIso
            { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := sorry, inv_hom_id := sorry :
              TensorBimod.X M (regular Y) ≅ M.X }
            sorry sorry))
        N)
Tactic: apply 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
| CategoryStruct.comp (Y :=
    coequalizer (TensorBimod.actRight M (regular Y) ▷ N.X)
      (Iso.hom (α_ (TensorBimod.X M (regular Y)) Y.X N.X) ≫ TensorBimod.X M (regular Y) ◁ N.actLeft))
    (coequalizer.π (TensorBimod.actRight M (regular Y) ▷ N.X)
      (Iso.hom (α_ (TensorBimod.X M (regular Y)) Y.X N.X) ≫ TensorBimod.X M (regular Y) ◁ N.actLeft))
    (coequalizer.desc (AssociatorBimod.homAux M (regular Y) N) ⋯)
have a : AssociatorBimod.homAux M (regular Y) N
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 Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
| CategoryStruct.comp (Y :=
    coequalizer (TensorBimod.actRight M (regular Y) ▷ N.X)
      (Iso.hom (α_ (TensorBimod.X M (regular Y)) Y.X N.X) ≫ TensorBimod.X M (regular Y) ◁ N.actLeft))
    (coequalizer.π (TensorBimod.actRight M (regular Y) ▷ N.X)
      (Iso.hom (α_ (TensorBimod.X M (regular Y)) Y.X N.X) ≫ TensorBimod.X M (regular Y) ◁ N.actLeft))
    (colimMap
      (parallelPairHom (TensorBimod.actRight M (regular Y) ▷ N.X)
        (Iso.hom (α_ (TensorBimod.X M (regular Y)) Y.X N.X) ≫ TensorBimod.X M (regular Y) ◁ N.actLeft)
        (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft) (RightUnitorBimod.hom M ▷ Y.X ▷ N.X)
        (RightUnitorBimod.hom M ▷ N.X) ⋯ ⋯))
have rw : RightUnitorBimod.hom M ▷ N.X ≫
  colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.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 Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
| CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) M.X (coequalizer (μ ▷ N.X) (Iso.hom (α_ Y.X Y.X N.X) ≫ Y.X ◁ N.actLeft)))
    (M.X ◁ coequalizer.π (μ ▷ N.X) (Iso.hom (α_ Y.X Y.X N.X) ≫ Y.X ◁ N.actLeft)) (M.X ◁ coequalizer.desc N.actLeft ⋯)
have a : M.X ◁ N.actLeft
Tactic: rw [← whiskerLeft_comp, 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 Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) N.X ⟶ TensorBimod.X M N)
    (Iso.hom (α_ M.X Y.X N.X) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) M.X (coequalizer (μ ▷ N.X) (Iso.hom (α_ Y.X Y.X N.X) ≫ Y.X ◁ N.actLeft)))
        (M.X ◁ coequalizer.π (μ ▷ N.X) (Iso.hom (α_ Y.X Y.X N.X) ≫ Y.X ◁ N.actLeft))
        (M.X ◁ coequalizer.desc N.actLeft ⋯ ≫
          colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))
            WalkingParallelPair.one))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ)) N.X)
      (coequalizer.π (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ) ▷ N.X)
      (coequalizer.desc M.actRight ⋯ ▷ N.X ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))
          WalkingParallelPair.one))
have h : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) N.X ⟶ TensorBimod.X M N)
  (Iso.hom (α_ M.X Y.X N.X) ≫
    M.X ◁ N.actLeft ≫
      colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one)
  (CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ)) N.X)
    (coequalizer.π (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ) ▷ N.X)
    (coequalizer.desc M.actRight sorry ▷ N.X ≫
      colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one))
Tactic: slice_lhs 2 3 => rw [← whiskerLeft_comp, 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 Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
| CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ)) N.X)
    (coequalizer.π (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ) ▷ N.X) (coequalizer.desc M.actRight ⋯ ▷ N.X)
have a : M.actRight ▷ N.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
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 (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) N.X ⟶ TensorBimod.X M N)
    (Iso.hom (α_ M.X Y.X N.X) ≫
      M.X ◁ N.actLeft ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))
          WalkingParallelPair.one)
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ)) N.X)
      (coequalizer.π (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ) ▷ N.X)
      (coequalizer.desc M.actRight ⋯ ▷ N.X ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))
          WalkingParallelPair.one))
have h : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) N.X ⟶ TensorBimod.X M N)
  (Iso.hom (α_ M.X Y.X N.X) ≫
    M.X ◁ N.actLeft ≫
      colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one)
  (M.actRight ▷ N.X ≫
    colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one)
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
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.actRight ▷ N.X ≫
    colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one
have rw : (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft) ≫
  coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)
Tactic: rw [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 Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) N.X ⟶ TensorBimod.X M N)
    (Iso.hom (α_ M.X Y.X N.X) ≫
      M.X ◁ N.actLeft ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))
          WalkingParallelPair.one)
    (M.actRight ▷ N.X ≫
      colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one)
have h : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) N.X ⟶ TensorBimod.X M N)
  (Iso.hom (α_ M.X Y.X N.X) ≫
    M.X ◁ N.actLeft ≫
      colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one)
  ((Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft) ≫
    coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))
Tactic: slice_rhs 1 2 => rw [coequalizer.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Bimon.{v₁, u₁} C
⊢ Eq (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M.X.X)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
      (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X) (Mon.Hom.hom ε ▷ M.X.X))
    (Iso.inv (λ_ M.X.X))
have rw : Eq (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M.X.X)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
    (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X) (ε ▷ M.X.X))
  (Iso.inv (λ_ M.X.X))
Tactic: rw [← BimonObjAux_counit, ← BimonObjAux_comul, ComonObj.counit_comul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Bimon.{v₁, u₁} C
rw :
  Eq (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M.X.X)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
      (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X) (ε ▷ M.X.X))
    (Iso.inv (λ_ M.X.X))
⊢ Eq (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M.X.X)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
      (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X) (Mon.Hom.hom ε ▷ M.X.X))
    (Iso.inv (λ_ M.X.X))
have rw₁ : Eq.{v₁ + 1} (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M.X.X) (Δ ≫ ε ▷ M.X.X)
  (Iso.inv (λ_ M.X.X))
Tactic: rw [← BimonObjAux_counit, ← BimonObjAux_comul, ComonObj.counit_comul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Bimon.{v₁, u₁} C
rw :
  Eq (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M.X.X)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
      (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X) (ε ▷ M.X.X))
    (Iso.inv (λ_ M.X.X))
rw₁ :
  Eq.{v₁ + 1} (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M.X.X) (Δ ≫ ε ▷ M.X.X)
    (Iso.inv (λ_ M.X.X))
⊢ Eq (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M.X.X)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
      (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X) (Mon.Hom.hom ε ▷ M.X.X))
    (Iso.inv (λ_ M.X.X))
have rw₂ : Eq.{v₁ + 1} (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M.X.X) (Iso.inv (λ_ M.X.X))
  (Iso.inv (λ_ M.X.X))
Tactic: rw [← BimonObjAux_counit, ← BimonObjAux_comul, ComonObj.counit_comul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Bimon.{v₁, u₁} C
⊢ Eq (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
      (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X) (M.X.X ◁ Mon.Hom.hom ε))
    (Iso.inv (ρ_ M.X.X))
have rw : Eq (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
    (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X) (M.X.X ◁ ε))
  (Iso.inv (ρ_ M.X.X))
Tactic: rw [← BimonObjAux_counit, ← BimonObjAux_comul, ComonObj.comul_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Bimon.{v₁, u₁} C
rw :
  Eq (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
      (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X) (M.X.X ◁ ε))
    (Iso.inv (ρ_ M.X.X))
⊢ Eq (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
      (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X) (M.X.X ◁ Mon.Hom.hom ε))
    (Iso.inv (ρ_ M.X.X))
have rw₁ : Eq.{v₁ + 1} (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Δ ≫ M.X.X ◁ ε)
  (Iso.inv (ρ_ M.X.X))
Tactic: rw [← BimonObjAux_counit, ← BimonObjAux_comul, ComonObj.comul_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Bimon.{v₁, u₁} C
rw :
  Eq (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
      (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X) (M.X.X ◁ ε))
    (Iso.inv (ρ_ M.X.X))
rw₁ :
  Eq.{v₁ + 1} (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Δ ≫ M.X.X ◁ ε)
    (Iso.inv (ρ_ M.X.X))
⊢ Eq (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
      (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X) (M.X.X ◁ Mon.Hom.hom ε))
    (Iso.inv (ρ_ M.X.X))
have rw₂ : Eq.{v₁ + 1} (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.inv (ρ_ M.X.X))
  (Iso.inv (ρ_ M.X.X))
Tactic: rw [← BimonObjAux_counit, ← BimonObjAux_comul, ComonObj.comul_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Bimon.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
      (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X) (M.X.X ◁ Mon.Hom.hom Δ))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
      (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X) M.X.X)
        (Mon.Hom.hom Δ ▷ M.X.X :
          tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X ⟶
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X) M.X.X)
        (Iso.hom (α_ M.X.X M.X.X M.X.X) :
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X) M.X.X ⟶
            tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X))))
have simp_rw : Eq.{v₁ + 1} (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X))
  (Δ ≫ M.X.X ◁ Δ) (Δ ≫ Δ ▷ M.X.X ≫ Iso.hom (α_ M.X.X M.X.X M.X.X))
Tactic: simp_rw [← BimonObjAux_comul, ComonObj.comul_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
⊢ Iso.hom (β_ (tensorObj.{v, u} (𝒞 := inst) X Y) Z) =
    Iso.hom (α_ X Y Z) ≫ X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y)
have apply : Iso.inv (α_ X Y Z) ≫ Iso.hom (β_ (tensorObj.{v, u} (𝒞 := inst) X Y) Z) =
  Iso.inv (α_ X Y Z) ≫
    Iso.hom (α_ X Y Z) ≫ X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y)
Tactic: apply (cancel_epi (α_ X Y Z).inv).1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
⊢ Iso.inv (α_ X Y Z) ≫ Iso.hom (β_ (tensorObj.{v, u} (𝒞 := inst) X Y) Z) =
    Iso.inv (α_ X Y Z) ≫
      Iso.hom (α_ X Y Z) ≫ X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y)
have apply : (Iso.inv (α_ X Y Z) ≫ Iso.hom (β_ (tensorObj.{v, u} (𝒞 := inst) X Y) Z)) ≫ Iso.inv (α_ Z X Y) =
  (Iso.inv (α_ X Y Z) ≫
      Iso.hom (α_ X Y Z) ≫ X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y)) ≫
    Iso.inv (α_ Z X Y)
Tactic: apply (cancel_mono (α_ Z X Y).inv).1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y Z) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)))
    (Iso.inv (α_ X Y Z) ≫ Iso.hom (β_ X Y) ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (β_ X Z) ≫ Iso.inv (α_ Y Z X))
have apply : Eq.{v + 1} (α :=
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y Z) X)
  (Iso.hom (α_ X Y Z) ≫ Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)))
  (Iso.hom (α_ X Y Z) ≫
    Iso.inv (α_ X Y Z) ≫ Iso.hom (β_ X Y) ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (β_ X Z) ≫ Iso.inv (α_ Y Z X))
Tactic: apply (cancel_epi (α_ X Y Z).hom).1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y Z) X)
    (Iso.hom (α_ X Y Z) ≫ Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)))
    (Iso.hom (α_ X Y Z) ≫
      Iso.inv (α_ X Y Z) ≫ Iso.hom (β_ X Y) ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (β_ X Z) ≫ Iso.inv (α_ Y Z X))
have apply : Eq.{v + 1} (α :=
  tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
    tensorObj.{v, u} (𝒞 := inst) Y (tensorObj.{v, u} (𝒞 := inst) Z X))
  ((Iso.hom (α_ X Y Z) ≫ Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z))) ≫ Iso.hom (α_ Y Z X))
  ((Iso.hom (α_ X Y Z) ≫
      Iso.inv (α_ X Y Z) ≫ Iso.hom (β_ X Y) ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (β_ X Z) ≫ Iso.inv (α_ Y Z X)) ≫
    Iso.hom (α_ Y Z X))
Tactic: apply (cancel_mono (α_ Y Z X).hom).1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X X' ⟶ tensorObj.{v, u} (𝒞 := inst) Y' Y) ((f ⊗ₘ g) ≫ Iso.hom (β_ Y Y'))
    (Iso.hom (β_ X X') ≫ (g ⊗ₘ f))
have rw : Eq (α := tensorObj.{v, u} (𝒞 := inst) X X' ⟶ tensorObj.{v, u} (𝒞 := inst) Y' Y) ((X ◁ g ≫ f ▷ Y') ≫ Iso.hom (β_ Y Y'))
  (Iso.hom (β_ X X') ≫ g ▷ X ≫ Y' ◁ f)
Tactic: rw [tensorHom_def' f g, tensorHom_def g f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X X' ⟶ tensorObj.{v, u} (𝒞 := inst) Y' Y) ((X ◁ g ≫ f ▷ Y') ≫ Iso.hom (β_ Y Y'))
    (Iso.hom (β_ X X') ≫ g ▷ X ≫ Y' ◁ f)
have simp_rw : Eq (α := tensorObj.{v, u} (𝒞 := inst) X X' ⟶ tensorObj.{v, u} (𝒞 := inst) Y' Y) (X ◁ g ≫ f ▷ Y' ≫ Iso.hom (β_ Y Y'))
  (Iso.hom (β_ X X') ≫ g ▷ X ≫ Y' ◁ f)
Tactic: simp_rw [Category.assoc, braiding_naturality_left, braiding_naturality_right_assoc]