awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
W X Y Z : C
⊢ Iso.inv (α_ W (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z) ≫
      (Iso.inv (α_ W X Y) ⊗ₘ 𝟙 Z) ≫ hom (α_ (tensorObj.{v_1, u_1} (𝒞 := inst) W X) Y Z) =
    (𝟙 W ⊗ₘ hom (α_ X Y Z)) ≫ Iso.inv (α_ W X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
⊢ hom (λ_ (tensorUnit.{v_1, u_1} C (𝒞 := inst))) = hom (ρ_ (tensorUnit.{v_1, u_1} C (𝒞 := inst)))

Tactic:
monoidal_coherence
-- Module: Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
⊢ Iso.inv (λ_ (tensorUnit.{v_1, u_1} C (𝒞 := inst))) = Iso.inv (ρ_ (tensorUnit.{v_1, u_1} C (𝒞 := inst)))

Tactic:
monoidal_coherence
-- Module: Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
W X Y Z : C
⊢ hom (α_ W X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)) ≫ (𝟙 W ⊗ₘ Iso.inv (α_ X Y Z)) =
    Iso.inv (α_ (tensorObj.{v_1, u_1} (𝒞 := inst) W X) Y Z) ≫
      (hom (α_ W X Y) ⊗ₘ 𝟙 Z) ≫ hom (α_ W (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
W X Y Z : C
⊢ Iso.inv (α_ (tensorObj.{v_1, u_1} (𝒞 := inst) W X) Y Z) ≫ (hom (α_ W X Y) ⊗ₘ 𝟙 Z) =
    hom (α_ W X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)) ≫
      (𝟙 W ⊗ₘ Iso.inv (α_ X Y Z)) ≫ Iso.inv (α_ W (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.CommComon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Δ ≫ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) Δ

Tactic:
simp [← unitors_equal]

Premises used: CategoryTheory.MonoidalCategory.unitors_equal
-- Module: Mathlib.CategoryTheory.Monoidal.CommComon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : CommComon.{v₁, u₁} C
⊢ (InducedCategory.Hom.hom (𝟙 A)).hom = 𝟙 A.X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommComon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
R S T : CommComon.{v₁, u₁} C
f : R ⟶ S
g : S ⟶ T
⊢ (f ≫ g).hom.hom = f.hom.hom ≫ g.hom.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommComon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : CommComon.{v₁, u₁} C
f g : A ⟶ B
h : f.hom.hom = g.hom.hom
⊢ f = g

Tactic:
InducedCategory.hom_ext (Comon.Hom.ext h)

Premises used: CategoryTheory.InducedCategory.hom_ext, CategoryTheory.Comon.Hom.ext
-- Module: Mathlib.CategoryTheory.Monoidal.CommComon_
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
inst_1 : MonoidalCategory.{v₁, u₁} C_1
inst_2 : BraidedCategory.{v₁, u₁} C_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_1, u_1} C
inst_5 : SymmetricCategory.{v_1, u_1} C
A B : C
inst_6 : ComonObj A
inst_7 : ComonObj B
inst_8 : IsCommComonObj.{v_1, u_1} A
inst_9 : IsCommComonObj.{v_1, u_1} B
rw :
  Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_3) A B ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_3) (tensorObj.{v_1, u_1} (𝒞 := inst_3) A B)
        (tensorObj.{v_1, u_1} (𝒞 := inst_3) A B))
    ((Δ ⊗ₘ Δ) ≫ (Iso.hom (β_ A A) ⊗ₘ Iso.hom (β_ B B)) ≫ tensorμ A A B B) ((Δ ⊗ₘ Δ) ≫ tensorμ A A B B)
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_3) A B ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_3) (tensorObj.{v_1, u_1} (𝒞 := inst_3) A B)
        (tensorObj.{v_1, u_1} (𝒞 := inst_3) A B))
    (Δ ≫ Iso.hom (β_ (tensorObj.{v_1, u_1} (𝒞 := inst_3) A B) (tensorObj.{v_1, u_1} (𝒞 := inst_3) A B))) Δ

Tactic:
rw [Comon.tensorObj_comul, Category.assoc, SymmetricCategory.tensorμ_braid_swap]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Comon.tensorObj_comul, CategoryTheory.SymmetricCategory.tensorμ_braid_swap
-- Module: Mathlib.CategoryTheory.Monoidal.CommComon_
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
inst_1 : MonoidalCategory.{v₁, u₁} C_1
inst_2 : BraidedCategory.{v₁, u₁} C_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_1, u_1} C
inst_5 : SymmetricCategory.{v_1, u_1} C
A B : C
inst_6 : ComonObj A
inst_7 : ComonObj B
inst_8 : IsCommComonObj.{v_1, u_1} A
inst_9 : IsCommComonObj.{v_1, u_1} B
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_3) A B ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_3) (tensorObj.{v_1, u_1} (𝒞 := inst_3) A B)
        (tensorObj.{v_1, u_1} (𝒞 := inst_3) A B))
    ((Δ ⊗ₘ Δ) ≫ (Iso.hom (β_ A A) ⊗ₘ Iso.hom (β_ B B)) ≫ tensorμ A A B B) ((Δ ⊗ₘ Δ) ≫ tensorμ A A B B)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : CommGrp.{v₁, u₁} C
⊢ InducedCategory.Hom.hom (𝟙 A) = 𝟙 A.toGrp

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
R S T : CommGrp.{v₁, u₁} C
f : R ⟶ S
g : S ⟶ T
⊢ (f ≫ g).hom = f.hom ≫ g.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : CommGrp.{v₁, u₁} C
f g : A ⟶ B
h : f.hom.hom.hom = g.hom.hom.hom
⊢ f = g

Tactic:
InducedCategory.hom_ext (Grp.hom_ext _ _ h)

Premises used: CategoryTheory.InducedCategory.hom_ext, CategoryTheory.Grp.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ Functor.Full (C := CommGrp.{v₁, u₁} C) (forget₂Grp C)

Tactic:
InducedCategory.full _

Premises used: CategoryTheory.CommGrp.forget₂Grp, CategoryTheory.InducedCategory, CategoryTheory.InducedCategory.full
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ Functor.Faithful (C := CommGrp.{v₁, u₁} C) (forget₂Grp C)

Tactic:
InducedCategory.faithful _

Premises used: CategoryTheory.InducedCategory.faithful, CategoryTheory.CommGrp.forget₂Grp, CategoryTheory.InducedCategory
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : CommGrp.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ (Functor.obj (forget₂Grp C) A).X) η η

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : CommGrp.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj (forget₂Grp C) A).X (Functor.obj (forget₂Grp C) A).X ⟶
      (Functor.obj (forget₂Grp C) A).X)
    μ μ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : CommGrp.{v₁, u₁} C
f : A ⟶ B
⊢ InducedCategory.Hom.hom (Functor.map (forget₂Grp C) f) = f.hom.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ Functor.Full (C := CommGrp.{v₁, u₁} C) (forget₂CommMon C)

Tactic:
(fullyFaithfulForget₂CommMon _).full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CategoryTheory.CommGrp.fullyFaithfulForget₂CommMon
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ Functor.Faithful (C := CommGrp.{v₁, u₁} C) (forget₂CommMon C)

Tactic:
(fullyFaithfulForget₂CommMon _).faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CategoryTheory.CommGrp.fullyFaithfulForget₂CommMon
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : CommGrp.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ (Functor.obj (forget₂CommMon C) A).X) η η

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : CommGrp.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj (forget₂CommMon C) A).X (Functor.obj (forget₂CommMon C) A).X ⟶
      (Functor.obj (forget₂CommMon C) A).X)
    μ μ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : CommGrp.{v₁, u₁} C
f : A ⟶ B
⊢ InducedCategory.Hom.hom (Functor.map (forget₂CommMon C) f) = f.hom.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ Eq (α := CommGrp.{v₁, u₁} C ⥤ C) (forget₂Grp C ⋙ Grp.forget C) (forget C)

Tactic:
rfl

Premises used: CategoryTheory.CommGrp.forget, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ Eq (α := CommGrp.{v₁, u₁} C ⥤ C) (forget₂CommMon C ⋙ CommMon.forget C) (forget C)

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.CommGrp.forget₂CommMon, CategoryTheory.CommGrp.forget₂Grp, CategoryTheory.inducedFunctor, CategoryTheory.CommGrp.forget, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G H : CommGrp.{v₁, u₁} C
f : G ⟶ H
inst_3 : IsIso f
⊢ IsIso f.hom

Tactic:
inferInstanceAs (IsIso ((forget₂Grp C).map f))

Premises used: _private.0.CategoryTheory.CommGrp.instIsIsoGrpHom._proof_1
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G H : CommGrp.{v₁, u₁} C
f : G ⟶ H
inst_3 : IsIso f
⊢ IsIso f.hom.hom

Tactic:
inferInstanceAs (IsIso ((forget₂Grp C ⋙ Grp.forget₂Mon C).map f))

Premises used: _private.0.CategoryTheory.CommGrp.instIsIsoMonHomGrp._proof_1
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G H : CommGrp.{v₁, u₁} C
e : G.X ≅ H.X
one_f : Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ H.X) (η ≫ e.hom) η
mul_f : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) G.X G.X ⟶ H.X) (μ ≫ e.hom) ((e.hom ⊗ₘ e.hom) ≫ μ)
⊢ (mkIso e one_f mul_f).hom.hom.hom.hom = e.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G H : CommGrp.{v₁, u₁} C
e : G.X ≅ H.X
one_f : Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ H.X) (η ≫ e.hom) η
mul_f : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) G.X G.X ⟶ H.X) (μ ≫ e.hom) ((e.hom ⊗ₘ e.hom) ≫ μ)
⊢ (mkIso e one_f mul_f).inv.hom.hom.hom = e.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ HasInitial (CommGrp.{v₁, u₁} C)

Tactic:
hasInitial_of_unique (trivial C)

Premises used: CategoryTheory.Limits.hasInitial_of_unique, CategoryTheory.CommGrp.trivial
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : CartesianMonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : CartesianMonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
inst_9 : F.Braided
inst_10 : F'.Braided
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_11 : G.Braided
A : CommGrp.{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) (Grp.X (obj F.mapGrp A.toGrp)) (Grp.X (obj F.mapGrp A.toGrp)) ⟶
      Grp.X (obj F.mapGrp A.toGrp))
    (Iso.hom (β_ (Grp.X (obj F.mapGrp A.toGrp)) (Grp.X (obj F.mapGrp A.toGrp))) ≫ μ) μ

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : CartesianMonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : CartesianMonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
inst_9 : F.Braided
inst_10 : F'.Braided
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_11 : G.Braided
A : CommGrp.{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.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : CartesianMonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : CartesianMonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
inst_9 : F.Braided
inst_10 : F'.Braided
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_11 : G.Braided
inst_12 : F.Full
inst_13 : F.Faithful
⊢ Full (C := CommGrp.{v₁, u₁} C) (D := CommGrp.{v₂, u₂} D) F.mapCommGrp

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

Premises used: CategoryTheory.Functor.FullyFaithful.full, CategoryTheory.Functor.FullyFaithful.ofFullyFaithful, CategoryTheory.Functor.FullyFaithful.mapCommGrp
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A : CommGrp.{v₁, u₁} C
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ CommGrp.X (obj (mapCommGrp (𝟭 C)) A)) η
    (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ η)

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : CartesianMonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : CartesianMonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_9 : F.Braided
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_10 : G.Braided
A : CommGrp.{v₁, u₁} C
⊢ Eq (α := tensorUnit.{v₃, u₃} E (𝒞 := inst_6) ⟶ CommGrp.X (obj (F ⋙ G).mapCommGrp 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.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : CartesianMonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : CartesianMonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_9 : F.Braided
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_10 : G.Braided
A : CommGrp.{v₁, u₁} C
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_6) (CommGrp.X (obj (F ⋙ G).mapCommGrp A)) (CommGrp.X (obj (F ⋙ G).mapCommGrp A)) ⟶
      CommGrp.X (obj (F ⋙ G).mapCommGrp 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.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : CartesianMonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : CartesianMonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
inst_9 : F.Braided
inst_10 : F'.Braided
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_11 : G.Braided
X : CommGrp.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ (obj (𝟭 (CommGrp.{v₁, u₁} C)) X).X)
    (η ≫ Iso.hom (Iso.refl (CommGrp.X (obj (mapCommGrp (𝟭 C)) X)))) η

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.CommGrp_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : CartesianMonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : CartesianMonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
inst_9 : F.Braided
inst_10 : F'.Braided
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_11 : G.Braided
X : CommGrp.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (CommGrp.X (obj (mapCommGrp (𝟭 C)) X)) (CommGrp.X (obj (mapCommGrp (𝟭 C)) X)) ⟶
      (obj (𝟭 (CommGrp.{v₁, u₁} C)) X).X)
    (μ ≫ Iso.hom (Iso.refl (CommGrp.X (obj (mapCommGrp (𝟭 C)) X))))
    ((Iso.hom (Iso.refl (CommGrp.X (obj (mapCommGrp (𝟭 C)) X))) ⊗ₘ
        Iso.hom (Iso.refl (CommGrp.X (obj (mapCommGrp (𝟭 C)) X)))) ≫
      μ)

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
⊢ (InducedCategory.Hom.hom (𝟙 A)).hom = 𝟙 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
R S T : CommMon.{v₁, u₁} C
f : R ⟶ S
g : S ⟶ T
⊢ (f ≫ g).hom.hom = f.hom.hom ≫ g.hom.hom

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 B : CommMon.{v₁, u₁} C
f g : A ⟶ B
h : f.hom.hom = g.hom.hom
⊢ f = g

Tactic:
InducedCategory.hom_ext (Mon.Hom.ext h)

Premises used: CategoryTheory.Mon.Hom.ext, CategoryTheory.InducedCategory.hom_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
M : CommMon.{v₁, u₁} C
⊢ Functor.Full (C := CommMon.{v₁, u₁} C) (forget₂Mon C)

Tactic:
InducedCategory.full _

Premises used: CategoryTheory.CommMon.forget₂Mon, CategoryTheory.InducedCategory, CategoryTheory.InducedCategory.full
-- 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
⊢ Functor.Faithful (C := CommMon.{v₁, u₁} C) (forget₂Mon C)

Tactic:
InducedCategory.faithful _

Premises used: CategoryTheory.InducedCategory.faithful, CategoryTheory.CommMon.forget₂Mon, CategoryTheory.InducedCategory
-- 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) ⟶ (Functor.obj (forget₂Mon C) 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) (Functor.obj (forget₂Mon C) A).X (Functor.obj (forget₂Mon C) A).X ⟶
      (Functor.obj (forget₂Mon C) 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 B : CommMon.{v₁, u₁} C
f : A ⟶ B
⊢ Mon.Hom.hom (Functor.map (forget₂Mon C) f) = f.hom.hom

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
⊢ Eq (α := CommMon.{v₁, u₁} C ⥤ C) (forget₂Mon C ⋙ Mon.forget C) (forget C)

Tactic:
rfl

Premises used: CategoryTheory.CommMon.forget, rfl