awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.CommMon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : F'.LaxBraided
inst_11 : G.LaxBraided
M : C
inst_12 : MonObj M
inst_13 : IsCommMonObj.{v₁, u₁} M
⊢ Eq.{v₂ + 1} (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj M) (F.obj M) ⟶ F.obj M)
    (Iso.hom (β_ (F.obj M) (F.obj M)) ≫ μ) μ
have dsimp : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj M) (F.obj M) ⟶ F.obj M)
  (Iso.hom (β_ (F.obj M) (F.obj M)) ≫
    CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M) (F.map μ))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M) (F.map μ))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.CommMon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : F'.LaxBraided
inst_11 : G.LaxBraided
M : C
inst_12 : MonObj M
inst_13 : IsCommMonObj.{v₁, u₁} M
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj M) (F.obj M) ⟶ F.obj M)
    (Iso.hom (β_ (F.obj M) (F.obj M)) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M) (F.map μ))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M) (F.map μ))
have rw : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj M) (F.obj M) ⟶ F.obj M)
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M)
    (F.map (Iso.hom (β_ M M)) ≫ F.map μ))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M) (F.map μ))
Tactic: rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMonObj.mul_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.CommMon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : F'.LaxBraided
inst_11 : G.LaxBraided
M : C
inst_12 : MonObj M
inst_13 : IsCommMonObj.{v₁, u₁} M
rw :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj M) (F.obj M) ⟶ F.obj M)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M)
      (F.map (Iso.hom (β_ M M)) ≫ F.map μ))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M) (F.map μ))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj M) (F.obj M) ⟶ F.obj M)
    (Iso.hom (β_ (F.obj M) (F.obj M)) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M) (F.map μ))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M) (F.map μ))
have rw₁ : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj M) (F.obj M) ⟶ F.obj M)
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M)
    (F.map (Iso.hom (β_ M M) ≫ μ)))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M) (F.map μ))
Tactic: rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMonObj.mul_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.CommMon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : F'.LaxBraided
inst_11 : G.LaxBraided
M : C
inst_12 : MonObj M
inst_13 : IsCommMonObj.{v₁, u₁} M
rw :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj M) (F.obj M) ⟶ F.obj M)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M)
      (F.map (Iso.hom (β_ M M)) ≫ F.map μ))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M) (F.map μ))
rw₁ :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj M) (F.obj M) ⟶ F.obj M)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M)
      (F.map (Iso.hom (β_ M M) ≫ μ)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M) (F.map μ))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj M) (F.obj M) ⟶ F.obj M)
    (Iso.hom (β_ (F.obj M) (F.obj M)) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M) (F.map μ))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M) (F.map μ))
have rw₂ : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj M) (F.obj M) ⟶ F.obj M)
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M) (F.map μ))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) (LaxMonoidal.μ F M M) (F.map μ))
Tactic: rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMonObj.mul_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.CommMon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : F'.LaxBraided
inst_11 : G.LaxBraided
A : CommMon.{v₁, u₁} C
⊢ Eq.{v₂ + 1} (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_3) (Mon.X (obj F.mapMon A.toMon)) (Mon.X (obj F.mapMon A.toMon)) ⟶
      Mon.X (obj F.mapMon A.toMon))
    (Iso.hom (β_ (Mon.X (obj F.mapMon A.toMon)) (Mon.X (obj F.mapMon A.toMon))) ≫ μ) μ
have dsimp : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
  (Iso.hom (β_ (F.obj A.X) (F.obj A.X)) ≫
    CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.CommMon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : F'.LaxBraided
inst_11 : G.LaxBraided
A : CommMon.{v₁, u₁} C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
    (Iso.hom (β_ (F.obj A.X) (F.obj A.X)) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
have rw : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X)
    (F.map (Iso.hom (β_ A.X A.X)) ≫ F.map μ))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
Tactic: rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMonObj.mul_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.CommMon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : F'.LaxBraided
inst_11 : G.LaxBraided
A : CommMon.{v₁, u₁} C
rw :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X)
      (F.map (Iso.hom (β_ A.X A.X)) ≫ F.map μ))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
    (Iso.hom (β_ (F.obj A.X) (F.obj A.X)) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
have rw₁ : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X)
    (F.map (Iso.hom (β_ A.X A.X) ≫ μ)))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
Tactic: rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMonObj.mul_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.CommMon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : F'.LaxBraided
inst_11 : G.LaxBraided
A : CommMon.{v₁, u₁} C
rw :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X)
      (F.map (Iso.hom (β_ A.X A.X)) ≫ F.map μ))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
rw₁ :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X)
      (F.map (Iso.hom (β_ A.X A.X) ≫ μ)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
    (Iso.hom (β_ (F.obj A.X) (F.obj A.X)) ≫
      CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
have rw₂ : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj A.X) (F.obj A.X) ⟶ F.obj A.X)
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ F A.X A.X) (F.map μ))
Tactic: rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMonObj.mul_comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.CommMon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X Y : LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C
f : X ⟶ Y
⊢ Eq (α :=
    obj (𝟭 (LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C)) X ⟶
      obj (laxBraidedToCommMon C ⋙ commMonToLaxBraided C) Y)
    (map (𝟭 (LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C)) f ≫
      Iso.hom
        ((fun (F : LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C) ↦
            (isoOfComponents (fun (x : Discrete PUnit.{u + 1}) ↦ F.mapIso (eqToIso ⋯)) ⋯ ⋯ ⋯ :
              obj (𝟭 (LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C)) F ≅
                obj (laxBraidedToCommMon C ⋙ commMonToLaxBraided C) F))
          Y))
    (Iso.hom
        ((fun (F : LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C) ↦
            (isoOfComponents (fun (x : Discrete PUnit.{u + 1}) ↦ F.mapIso (eqToIso ⋯)) ⋯ ⋯ ⋯ :
              obj (𝟭 (LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C)) F ≅
                obj (laxBraidedToCommMon C ⋙ commMonToLaxBraided C) F))
          X) ≫
      map (laxBraidedToCommMon C ⋙ commMonToLaxBraided C) f)
have h : Eq (α :=
  (obj (𝟭 (LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C)) X).toLaxMonoidalFunctor.obj
      { as := PUnit.unit : Discrete PUnit.{u + 1} } ⟶
    (obj (laxBraidedToCommMon C ⋙ commMonToLaxBraided C) Y).toLaxMonoidalFunctor.obj { as := PUnit.unit })
  (NatTrans.app
    (LaxMonoidalFunctor.Hom.hom
      (InducedCategory.Hom.hom
        (map (𝟭 (LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C)) f ≫
          Iso.hom
            ((fun (F : LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C) ↦
                (isoOfComponents (fun (x : Discrete PUnit.{u + 1}) ↦ F.mapIso (eqToIso sorry)) sorry sorry sorry :
                  obj (𝟭 (LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C)) F ≅
                    obj (laxBraidedToCommMon C ⋙ commMonToLaxBraided C) F))
              Y))))
    { as := PUnit.unit })
  (NatTrans.app
    (LaxMonoidalFunctor.Hom.hom
      (InducedCategory.Hom.hom
        (Iso.hom
            ((fun (F : LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C) ↦
                (isoOfComponents (fun (x : Discrete PUnit.{u + 1}) ↦ F.mapIso (eqToIso sorry)) sorry sorry sorry :
                  obj (𝟭 (LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C)) F ≅
                    obj (laxBraidedToCommMon C ⋙ commMonToLaxBraided C) F))
              X) ≫
          map (laxBraidedToCommMon C ⋙ commMonToLaxBraided C) f)))
    { as := PUnit.unit })
Tactic: ext ⟨⟨⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.CommMon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X Y : LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C
f : X ⟶ Y
⊢ Eq (α :=
    (obj (𝟭 (LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C)) X).toLaxMonoidalFunctor.obj
        { as := PUnit.unit : Discrete PUnit.{u + 1} } ⟶
      (obj (laxBraidedToCommMon C ⋙ commMonToLaxBraided C) Y).toLaxMonoidalFunctor.obj { as := PUnit.unit })
    (NatTrans.app
      (LaxMonoidalFunctor.Hom.hom
        (InducedCategory.Hom.hom
          (map (𝟭 (LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C)) f ≫
            Iso.hom
              ((fun (F : LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C) ↦
                  (isoOfComponents (fun (x : Discrete PUnit.{u + 1}) ↦ F.mapIso (eqToIso ⋯)) ⋯ ⋯ ⋯ :
                    obj (𝟭 (LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C)) F ≅
                      obj (laxBraidedToCommMon C ⋙ commMonToLaxBraided C) F))
                Y))))
      { as := PUnit.unit })
    (NatTrans.app
      (LaxMonoidalFunctor.Hom.hom
        (InducedCategory.Hom.hom
          (Iso.hom
              ((fun (F : LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C) ↦
                  (isoOfComponents (fun (x : Discrete PUnit.{u + 1}) ↦ F.mapIso (eqToIso ⋯)) ⋯ ⋯ ⋯ :
                    obj (𝟭 (LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C)) F ≅
                      obj (laxBraidedToCommMon C ⋙ commMonToLaxBraided C) F))
                X) ≫
            map (laxBraidedToCommMon C ⋙ commMonToLaxBraided C) f)))
      { as := PUnit.unit })
have h : f.hom.hom.app { as := PUnit.unit : Discrete PUnit.{u + 1} } ≫ Y.map (𝟙 { as := PUnit.unit : Discrete PUnit.{u + 1} }) =
  X.map (𝟙 { as := PUnit.unit : Discrete PUnit.{u + 1} }) ≫
    f.hom.hom.app ((𝟙_ (Discrete PUnit.{u + 1})) (𝒞 := discreteCategory PUnit.{u + 1}))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : ComonObj M
Z : C
f : M ⟶ Z
⊢ Eq (α := M ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Z) (Δ ≫ (ε ⊗ₘ f)) (f ≫ Iso.inv (λ_ Z))
have rw : Δ ≫ (ε ⊗ₘ f) = Iso.inv (λ_ M) ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f
Tactic: rw [leftUnitor_inv_naturality, tensorHom_def, counit_comul_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : ComonObj M
Z : C
f : M ⟶ Z
rw : Δ ≫ (ε ⊗ₘ f) = Iso.inv (λ_ M) ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f
⊢ Eq (α := M ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Z) (Δ ≫ (ε ⊗ₘ f)) (f ≫ Iso.inv (λ_ Z))
have rw₁ : Δ ≫ ε ▷ M ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f = Iso.inv (λ_ M) ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f
Tactic: rw [leftUnitor_inv_naturality, tensorHom_def, counit_comul_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : ComonObj M
Z : C
f : M ⟶ Z
rw : Δ ≫ (ε ⊗ₘ f) = Iso.inv (λ_ M) ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f
rw₁ : Δ ≫ ε ▷ M ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f = Iso.inv (λ_ M) ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f
⊢ Eq (α := M ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Z) (Δ ≫ (ε ⊗ₘ f)) (f ≫ Iso.inv (λ_ Z))
have rw₂ : Iso.inv (λ_ M) ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f = Iso.inv (λ_ M) ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ f
Tactic: rw [leftUnitor_inv_naturality, tensorHom_def, counit_comul_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : ComonObj M
Z : C
f : M ⟶ Z
⊢ Eq (α := M ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Δ ≫ (f ⊗ₘ ε)) (f ≫ Iso.inv (ρ_ Z))
have rw : Eq (α := M ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Δ ≫ (f ⊗ₘ ε))
  (Iso.inv (ρ_ M) ≫ f ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
Tactic: rw [rightUnitor_inv_naturality, tensorHom_def', comul_counit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : ComonObj M
Z : C
f : M ⟶ Z
rw :
  Eq (α := M ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Δ ≫ (f ⊗ₘ ε))
    (Iso.inv (ρ_ M) ≫ f ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
⊢ Eq (α := M ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Δ ≫ (f ⊗ₘ ε)) (f ≫ Iso.inv (ρ_ Z))
have rw₁ : Eq (α := M ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  (Δ ≫ M ◁ ε ≫ f ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) (Iso.inv (ρ_ M) ≫ f ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
Tactic: rw [rightUnitor_inv_naturality, tensorHom_def', comul_counit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : ComonObj M
Z : C
f : M ⟶ Z
rw :
  Eq (α := M ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Δ ≫ (f ⊗ₘ ε))
    (Iso.inv (ρ_ M) ≫ f ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
rw₁ :
  Eq (α := M ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Δ ≫ M ◁ ε ≫ f ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) (Iso.inv (ρ_ M) ≫ f ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
⊢ Eq (α := M ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Δ ≫ (f ⊗ₘ ε)) (f ≫ Iso.inv (ρ_ Z))
have rw₂ : Eq (α := M ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  (Iso.inv (ρ_ M) ≫ f ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) (Iso.inv (ρ_ M) ≫ f ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
Tactic: rw [rightUnitor_inv_naturality, tensorHom_def', comul_counit_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Comon.{v₁, u₁} C
f : A ⟶ trivial C
⊢ f = { hom := ε, isComonHom_hom := ⋯ }
have w : f.hom = Hom.hom { hom := ε, isComonHom_hom := sorry }
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Comon.{v₁, u₁} C
f : A ⟶ trivial C
⊢ f.hom = Hom.hom { hom := ε, isComonHom_hom := ⋯ }
have w : f.hom ≫ 𝟙 (X.{v₁, u₁} (trivial C)) = Hom.hom { hom := ε, isComonHom_hom := sorry }
Tactic: rw [← Category.comp_id f.hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Comon.{v₁, u₁} C
f : A ⟶ trivial C
⊢ f.hom ≫ 𝟙 (X.{v₁, u₁} (trivial C)) = Hom.hom { hom := ε, isComonHom_hom := ⋯ }
have w : f.hom ≫ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) = ε
Tactic: dsimp only [trivial_X]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Comon.{v₁, u₁} C
f : A ⟶ trivial C
⊢ f.hom ≫ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) = ε
have w : Eq (α := A.X ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst)) (f.hom ≫ ε) ε
Tactic: rw [← trivial_comon_counit, IsComonHom.hom_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Comon.{v₁, u₁} C
f : A ⟶ trivial C
w : Eq (α := A.X ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst)) (f.hom ≫ ε) ε
⊢ f.hom ≫ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) = ε
have w₁ : Eq.{v₁ + 1} (α := A.X ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε ε
Tactic: rw [← trivial_comon_counit, IsComonHom.hom_counit]