awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.CommMon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M_1 M N : CommMon.{v₁, u₁} C
f : M ⟶ N
inst_3 : IsIso f
⊢ IsIso f.hom.hom

Tactic:
inferInstanceAs <| IsIso <| (forget C).map f

Premises used: _private.0.CategoryTheory.CommMon.instIsIsoHomHomMon._proof_1
-- Module: Mathlib.CategoryTheory.Monoidal.CommMon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : CommMon.{v₁, u₁} C
⊢ HasInitial (CommMon.{v₁, u₁} C)

Tactic:
hasInitial_of_unique (trivial C)

Premises used: CategoryTheory.CommMon.trivial, CategoryTheory.Limits.hasInitial_of_unique
-- Module: Mathlib.CategoryTheory.Monoidal.CommMon_
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
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 μ))
⊢ 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)) ≫ μ) μ

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.CommMon_
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 μ))
rw₂ 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 μ))
⊢ 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:
rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMonObj.mul_comm]

Premises used: CategoryTheory.IsCommMonObj.mul_comm, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.LaxBraided.braided_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.CommMon_
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
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 μ))
⊢ 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))) ≫ μ) μ

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.CommMon_
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 μ))
rw₂ 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 μ))
⊢ 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:
rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMonObj.mul_comm]

Premises used: CategoryTheory.IsCommMonObj.mul_comm, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.LaxBraided.braided_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.CommMon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : CommMon.{v₁, u₁} C
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ CommMon.X (obj (mapCommMon (𝟭 C)) A)) η
    (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ η)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommMon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : CommMon.{v₁, u₁} C
⊢ μ = 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X) ≫ μ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommMon_
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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : G.LaxBraided
A : CommMon.{v₁, u₁} C
⊢ Eq (α := tensorUnit.{v₃, u₃} E (𝒞 := inst_6) ⟶ CommMon.X (obj (F ⋙ G).mapCommMon A)) η
    (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (LaxMonoidal.ε (F ⋙ G)) ((F ⋙ G).map η))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommMon_
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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : G.LaxBraided
A : CommMon.{v₁, u₁} C
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_6) (CommMon.X (obj (F ⋙ G).mapCommMon A)) (CommMon.X (obj (F ⋙ G).mapCommMon A)) ⟶
      CommMon.X (obj (F ⋙ G).mapCommMon A))
    μ
    (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A.X A.X)) (LaxMonoidal.μ (F ⋙ G) A.X A.X)
      ((F ⋙ G).map μ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommMon_
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.Braided
inst_10 : F.Full
inst_11 : F.Faithful
⊢ Full (C := CommMon.{v₁, u₁} C) (D := CommMon.{v₂, u₂} D) F.mapCommMon

Tactic:
(FullyFaithful.ofFullyFaithful F).mapCommMon.full

Premises used: CategoryTheory.Functor.FullyFaithful.mapCommMon, CategoryTheory.Functor.FullyFaithful.full, CategoryTheory.Functor.FullyFaithful.ofFullyFaithful
-- Module: Mathlib.CategoryTheory.Monoidal.CommMon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : CommMon.{v₁, u₁} C
⊢ Eq (α :=
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶
      (commMonToLaxBraidedObj A).obj ((𝟙_ (Discrete PUnit.{u_1 + 1})) (𝒞 := discreteCategory PUnit.{u_1 + 1})))
    (ε (commMonToLaxBraidedObj A)) η

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommMon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : CommMon.{v₁, u₁} C
X Y : Discrete PUnit.{u_1 + 1}
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) ((commMonToLaxBraidedObj A).obj X) ((commMonToLaxBraidedObj A).obj Y) ⟶
      (commMonToLaxBraidedObj A).obj (tensorObj (𝒞 := discreteCategory PUnit.{u_1 + 1}) X Y))
    («μ» (commMonToLaxBraidedObj A) X Y) μ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommMon_
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_1 F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
F : LaxBraidedFunctor.{u, v₁, u, u₁} (Discrete PUnit.{u + 1}) C
x : Discrete PUnit.{u + 1}
⊢ x = Mon.X (toMon (trivial (Discrete PUnit.{u + 1})))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.CommMon_
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
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 ⋯)) ⋯ ⋯ ⋯ :
                    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 })
⊢ 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)

Tactic:
ext ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Monoidal.CommMon_
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
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}))
⊢ 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 })

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.CommMon_
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
⊢ 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:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.CommMon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : CommMon.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ (obj (commMonToLaxBraided C ⋙ laxBraidedToCommMon C) A).X) η
    (η ≫ 𝟙 A.X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommMon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : CommMon.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (obj (commMonToLaxBraided C ⋙ laxBraidedToCommMon C) A).X
        (obj (commMonToLaxBraided C ⋙ laxBraidedToCommMon C) A).X ⟶
      (obj (commMonToLaxBraided C ⋙ laxBraidedToCommMon C) A).X)
    μ (μ ≫ 𝟙 A.X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
inst_1 : MonoidalCategory.{v₁, u₁} C_1
C : Type u₁
inst_2 : Category.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₁, u₁} C
⊢ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst_2))) ≫
      𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst_2)) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst_2) =
    Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst_2)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
inst_1 : MonoidalCategory.{v₁, u₁} C_1
C : Type u₁
inst_2 : Category.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₁, u₁} C
⊢ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst_2))) ≫
      tensorUnit.{v₁, u₁} C (𝒞 := inst_2) ◁ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst_2)) =
    Iso.inv (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst_2)))

Tactic:
monoidal_coherence
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
inst_1 : MonoidalCategory.{v₁, u₁} C_1
C : Type u₁
inst_2 : Category.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₁, u₁} C
⊢ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst_2))) ≫
      tensorUnit.{v₁, u₁} C (𝒞 := inst_2) ◁ Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst_2))) =
    Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst_2))) ≫
      Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst_2))) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst_2) ≫
        Iso.hom
          (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst_2)) (tensorUnit.{v₁, u₁} C (𝒞 := inst_2))
            (tensorUnit.{v₁, u₁} C (𝒞 := inst_2)))

Tactic:
monoidal_coherence
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
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
f : M ≅ N
inst_5 : IsComonHom f.hom
⊢ Eq (α := N ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst)) (f.inv ≫ ε) ε

Tactic:
simp [Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
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
f : M ≅ N
inst_5 : IsComonHom f.hom
⊢ Eq (α := N ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M M) (f.inv ≫ Δ) (Δ ≫ (f.inv ⊗ₘ f.inv))

Tactic:
simp [Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
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
rw₂ rw₃ :
  Iso.inv (λ_ 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))

Tactic:
rw [leftUnitor_inv_naturality, tensorHom_def, counit_comul_assoc]

Premises used: CategoryTheory.ComonObj.counit_comul_assoc, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
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))
rw₂ 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))
⊢ Eq (α := M ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) Z (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Δ ≫ (f ⊗ₘ ε)) (f ≫ Iso.inv (ρ_ Z))

Tactic:
rw [rightUnitor_inv_naturality, tensorHom_def', comul_counit_assoc]

Premises used: CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality, CategoryTheory.MonoidalCategory.tensorHom_def', CategoryTheory.ComonObj.comul_counit_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
inst_2 : ComonObj X
⊢ Eq.{v₁ + 1} (α := X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X X) X) (Δ ≫ Δ ▷ X)
    (Δ ≫ X ◁ Δ ≫ Iso.inv (α_ X X X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M_1 N_1 O : C
inst_2 : ComonObj M_1
inst_3 : ComonObj N_1
inst_4 : ComonObj O
M N : Comon.{v₁, u₁} C
f : M ⟶ N
⊢ IsComonHom f.hom

Tactic:
inferInstanceAs (IsComonHom f.hom)

Premises used: _private.0.CategoryTheory.Comon.instIsComonHomHom._proof_1
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Comon.{v₁, u₁} C
f g : X ⟶ Y
w : f.hom = g.hom
⊢ f = g

Tactic:
Hom.ext w

Premises used: CategoryTheory.Comon.Hom.ext