awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Module
Goal:
R : Type u
inst : CommRing R
A : Mon (ModuleCat R)
⊢ Eq (α :=
    (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u) →ₗ[R]
      (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u) →ₗ[R]
        (↑(Functor.obj (𝟭 (Mon (ModuleCat R))) A).X : Type u))
    (compr₂ₛₗ (R₄ := R) (M := (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u)) (N :=
        (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u)) (P :=
        (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u) ⊗[R]
          (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u))
        (Q := (↑(Functor.obj (𝟭 (Mon (ModuleCat R))) A).X : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R) (σ₃₄ :=
        RingHom.id R)
        (TensorProduct.mk R (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u)
          (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u))
        (Hom.hom (μ ≫ ↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ })) :
      (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u) →ₗ[R]
        (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u) →ₗ[R]
          (↑(Functor.obj (𝟭 (Mon (ModuleCat R))) A).X : Type u))
    (compr₂ₛₗ (R₄ := R) (M := (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u)) (N :=
        (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u)) (P :=
        (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u) ⊗[R]
          (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u))
        (Q := (↑(Functor.obj (𝟭 (Mon (ModuleCat R))) A).X : Type u)) (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R) (σ₃₄ :=
        RingHom.id R)
        (TensorProduct.mk R (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u)
          (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u))
        (Hom.hom
          (MonoidalCategoryStruct.tensorHom (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ })
              (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }) ≫
            μ)) :
      (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u) →ₗ[R]
        (↑(Functor.obj (functor ⋙ MonModuleEquivalenceAlgebra.inverse) A).X : Type u) →ₗ[R]
          (↑(Functor.obj (𝟭 (Mon (ModuleCat R))) A).X : Type u))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
Goal:
A : Type u
inst : MonObj A
x y z : A
⊢ Eq (α := A)
    ((hom (FC := TypeCat.Fun) (MonoidalCategoryStruct.whiskerRight μ A ≫ μ) :
          (a : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj A A) A) → A)
        ((x, y), z) :
      A)
    ((hom (FC := TypeCat.Fun)
            (Iso.hom (MonoidalCategoryStruct.associator A A A) ≫ MonoidalCategoryStruct.whiskerLeft A μ ≫ μ) :
          (a : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj A A) A) → A)
        ((x, y), z) :
      A)

Tactic:
congr_hom (CC := fun X ↦ X) (mul_assoc A) ((x, y), z)

Premises used: CategoryTheory.MonObj.mul_assoc, Prod.mk, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
Goal:
A : Type u
inst : MonObj A
x y z : A
⊢ x * y * z = x * (y * z)

Tactic:
convert! congr_hom (CC := fun X ↦ X) (mul_assoc A) ((x, y), z)

Premises used: CategoryTheory.MonObj.mul_assoc, Prod.mk, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
Goal:
A : Type u
inst : MonObj A
x : A
⊢ Eq (α := A)
    ((hom (FC := TypeCat.Fun) (MonoidalCategoryStruct.whiskerRight η A ≫ μ) :
          (a : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (Type u)) A) → A)
        (PUnit.unit, x) :
      A)
    ((hom (FC := TypeCat.Fun) (Iso.hom (MonoidalCategoryStruct.leftUnitor A)) :
          (a : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit (Type u)) A) → A)
        (PUnit.unit, x) :
      A)

Tactic:
congr_hom (CC := fun X ↦ X) (one_mul A) (PUnit.unit, x)

Premises used: Prod.mk, PUnit.unit, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.MonObj.one_mul
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
Goal:
A : Type u
inst : MonObj A
x : A
⊢ 1 * x = x

Tactic:
convert! congr_hom (CC := fun X ↦ X) (one_mul A) (PUnit.unit, x)

Premises used: Prod.mk, PUnit.unit, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.MonObj.one_mul
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
Goal:
A : Type u
inst : MonObj A
x : A
⊢ Eq (α := A)
    ((hom (FC := TypeCat.Fun) (MonoidalCategoryStruct.whiskerLeft A η ≫ μ) :
          (a : MonoidalCategoryStruct.tensorObj A (MonoidalCategoryStruct.tensorUnit (Type u))) → A)
        (x, PUnit.unit) :
      A)
    ((hom (FC := TypeCat.Fun) (Iso.hom (MonoidalCategoryStruct.rightUnitor A)) :
          (a : MonoidalCategoryStruct.tensorObj A (MonoidalCategoryStruct.tensorUnit (Type u))) → A)
        (x, PUnit.unit) :
      A)

Tactic:
congr_hom (CC := fun X ↦ X) (mul_one A) (x, PUnit.unit)

Premises used: Prod.mk, CategoryTheory.MonObj.mul_one, PUnit.unit, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
Goal:
A : Type u
inst : MonObj A
x : A
⊢ x * 1 = x

Tactic:
convert! congr_hom (CC := fun X ↦ X) (mul_one A) (x, PUnit.unit)

Premises used: Prod.mk, CategoryTheory.MonObj.mul_one, PUnit.unit, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
Goal:
A : MonCat
h :
  ∀ (z x y : (↑A : Type u)),
    Eq (α := (↑A : Type u))
      (TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑A : Type u) (↑A : Type u))
            (MonoidalCategoryStruct.whiskerRight
              (↾fun (p : MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑A : Type u) (↑A : Type u)) ↦ p.1 * p.2)
              (↑A : Type u))
            (↾fun (p : MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑A : Type u) (↑A : Type u)) ↦ p.1 * p.2)))
        ((x, y), z))
      (TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          (Iso.hom (MonoidalCategoryStruct.associator (↑A : Type u) (↑A : Type u) (↑A : Type u)) ≫
            CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑A : Type u) (↑A : Type u))
              (MonoidalCategoryStruct.whiskerLeft (↑A : Type u)
                (↾fun (p : MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑A : Type u) (↑A : Type u)) ↦ p.1 * p.2))
              (↾fun (p : MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑A : Type u) (↑A : Type u)) ↦ p.1 * p.2)))
        ((x, y), z))
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := types)
        (MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑A : Type u) (↑A : Type u)) (↑A : Type u) ⟶
      (↑A : Type u))
    (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑A : Type u) (↑A : Type u))
      (MonoidalCategoryStruct.whiskerRight
        (↾fun (p : MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑A : Type u) (↑A : Type u)) ↦ p.1 * p.2)
        (↑A : Type u))
      (↾fun (p : MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑A : Type u) (↑A : Type u)) ↦ p.1 * p.2))
    (Iso.hom (MonoidalCategoryStruct.associator (↑A : Type u) (↑A : Type u) (↑A : Type u)) ≫
      CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑A : Type u) (↑A : Type u))
        (MonoidalCategoryStruct.whiskerLeft (↑A : Type u)
          (↾fun (p : MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑A : Type u) (↑A : Type u)) ↦ p.1 * p.2))
        (↾fun (p : MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑A : Type u) (↑A : Type u)) ↦ p.1 * p.2))

Tactic:
ext ⟨⟨x, y⟩, z⟩
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
Goal:
A : MonCat
z x y : (↑A : Type u)
⊢ Eq (α := (↑A : Type u))
    (TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑A : Type u) (↑A : Type u))
          (MonoidalCategoryStruct.whiskerRight
            (↾fun (p : MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑A : Type u) (↑A : Type u)) ↦ p.1 * p.2)
            (↑A : Type u))
          (↾fun (p : MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑A : Type u) (↑A : Type u)) ↦ p.1 * p.2)))
      ((x, y), z))
    (TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (Iso.hom (MonoidalCategoryStruct.associator (↑A : Type u) (↑A : Type u) (↑A : Type u)) ≫
          CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑A : Type u) (↑A : Type u))
            (MonoidalCategoryStruct.whiskerLeft (↑A : Type u)
              (↾fun (p : MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑A : Type u) (↑A : Type u)) ↦ p.1 * p.2))
            (↾fun (p : MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑A : Type u) (↑A : Type u)) ↦ p.1 * p.2)))
      ((x, y), z))

Tactic:
simp [_root_.mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
Goal:
X Y : MonCat
f : X ⟶ Y
simp :
  Eq (α := MonoidalCategoryStruct.tensorUnit (Type u) (𝒞 := types) ⟶ (↑Y : Type u))
    (CategoryStruct.comp (Y := (↑X : Type u)) (↾fun (x : MonoidalCategoryStruct.tensorUnit (Type u) (𝒞 := types)) ↦ 1)
      (↾(⇑(hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := MonCat.carrier) f) :
          (a : (↑X : Type u)) → (↑Y : Type u))))
    (↾fun (x : MonoidalCategoryStruct.tensorUnit (Type u) (𝒞 := types)) ↦ 1)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorUnit (Type u) (𝒞 := types) ⟶
      Mon.X
        { X := (↑Y : Type u),
          mon :=
            { one := ↾fun (x : MonoidalCategoryStruct.tensorUnit (Type u)) ↦ 1,
              mul := ↾fun (p : MonoidalCategoryStruct.tensorObj (↑Y : Type u) (↑Y : Type u)) ↦ p.1 * p.2, one_mul := ⋯,
              mul_one := ⋯, mul_assoc := ⋯ } })
    (CategoryStruct.comp (Y :=
      Mon.X
        { X := (↑X : Type u),
          mon :=
            { one := ↾fun (x : MonoidalCategoryStruct.tensorUnit (Type u)) ↦ 1,
              mul := ↾fun (p : MonoidalCategoryStruct.tensorObj (↑X : Type u) (↑X : Type u)) ↦ p.1 * p.2, one_mul := ⋯,
              mul_one := ⋯, mul_assoc := ⋯ } })
      η
      (↾(⇑(hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := MonCat.carrier) f) :
          (a : (↑X : Type u)) → (↑Y : Type u))))
    η

Tactic:
simp +instances only
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
Goal:
X Y : MonCat
f : X ⟶ Y
simp :
  Eq (α := MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑X : Type u) (↑X : Type u) ⟶ (↑Y : Type u))
    (CategoryStruct.comp (Y := (↑X : Type u))
      (↾fun (p : MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑X : Type u) (↑X : Type u)) ↦ p.1 * p.2)
      (↾(⇑(hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := MonCat.carrier) f) :
          (a : (↑X : Type u)) → (↑Y : Type u))))
    (CategoryStruct.comp (Y := MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑Y : Type u) (↑Y : Type u))
      (MonoidalCategoryStruct.tensorHom
        (↾(⇑(hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := MonCat.carrier) f) :
            (a : (↑X : Type u)) → (↑Y : Type u)))
        (↾(⇑(hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := MonCat.carrier) f) :
            (a : (↑X : Type u)) → (↑Y : Type u))))
      (↾fun (p : MonoidalCategoryStruct.tensorObj (𝒞 := types) (↑Y : Type u) (↑Y : Type u)) ↦ p.1 * p.2))
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := types)
        (Mon.X
          { X := (↑X : Type u),
            mon :=
              { one := ↾fun (x : MonoidalCategoryStruct.tensorUnit (Type u)) ↦ 1,
                mul := ↾fun (p : MonoidalCategoryStruct.tensorObj (↑X : Type u) (↑X : Type u)) ↦ p.1 * p.2,
                one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ } :
            Mon (Type u) })
        (Mon.X
          { X := (↑X : Type u),
            mon :=
              { one := ↾fun (x : MonoidalCategoryStruct.tensorUnit (Type u)) ↦ 1,
                mul := ↾fun (p : MonoidalCategoryStruct.tensorObj (↑X : Type u) (↑X : Type u)) ↦ p.1 * p.2,
                one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ } :
            Mon (Type u) }) ⟶
      Mon.X
        { X := (↑Y : Type u),
          mon :=
            { one := ↾fun (x : MonoidalCategoryStruct.tensorUnit (Type u)) ↦ 1,
              mul := ↾fun (p : MonoidalCategoryStruct.tensorObj (↑Y : Type u) (↑Y : Type u)) ↦ p.1 * p.2, one_mul := ⋯,
              mul_one := ⋯, mul_assoc := ⋯ } })
    (μ ≫
      ↾(⇑(hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := MonCat.carrier) f) :
          (a : (↑X : Type u)) → (↑Y : Type u)))
    (MonoidalCategoryStruct.tensorHom
        (↾(⇑(hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := MonCat.carrier) f) :
            (a : (↑X : Type u)) → (↑Y : Type u)))
        (↾(⇑(hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := MonCat.carrier) f) :
            (a : (↑X : Type u)) → (↑Y : Type u))) ≫
      μ)

Tactic:
simp +instances only
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
Goal:
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ {X Y : MonCat.{u}} (f : X ⟶ Y),
    Eq (α := (inverse ⋙ functor).obj X ⟶ Functor.obj (𝟭 MonCat) Y)
      ((inverse ⋙ functor).map f ≫
        Iso.hom
          ((fun (A : MonCat.{u}) ↦
              (MulEquiv.toMonCatIso
                  (let __src : (inverse.obj A).X ≃ (inverse.obj A).X := Equiv.refl (inverse.obj A).X;
                  { toEquiv := __src, map_mul' := ⋯ }) :
                MonCat.of (inverse.obj A).X ≅ MonCat.of (↑A : Type u)))
            Y))
      (Iso.hom
          ((fun (A : MonCat.{u}) ↦
              (MulEquiv.toMonCatIso
                  (let __src : (inverse.obj A).X ≃ (inverse.obj A).X := Equiv.refl (inverse.obj A).X;
                  { toEquiv := __src, map_mul' := ⋯ }) :
                MonCat.of (inverse.obj A).X ≅ MonCat.of (↑A : Type u)))
            X) ≫
        CategoryTheory.Functor.map (𝟭 MonCat) f)
⊢ ∀ {X Y : MonCat.{u}} (f : X ⟶ Y),
    Eq (α := (inverse ⋙ functor).obj X ⟶ Functor.obj (𝟭 MonCat) Y)
      ((inverse ⋙ functor).map f ≫
        Iso.hom
          ((fun (A : MonCat.{u}) ↦
              (MulEquiv.toMonCatIso
                  (let __src : (inverse.obj A).X ≃ (inverse.obj A).X := Equiv.refl (inverse.obj A).X;
                  { toEquiv := __src, map_mul' := ⋯ }) :
                MonCat.of (inverse.obj A).X ≅ MonCat.of (↑A : Type u)))
            Y))
      (Iso.hom
          ((fun (A : MonCat.{u}) ↦
              (MulEquiv.toMonCatIso
                  (let __src : (inverse.obj A).X ≃ (inverse.obj A).X := Equiv.refl (inverse.obj A).X;
                  { toEquiv := __src, map_mul' := ⋯ }) :
                MonCat.of (inverse.obj A).X ≅ MonCat.of (↑A : Type u)))
            X) ≫
        CategoryTheory.Functor.map (𝟭 MonCat) f)

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
Goal:
A : Type u
inst : MonObj A
inst_1 : IsCommMonObj A
x y : A
⊢ Eq (α := A)
    ((hom (FC := TypeCat.Fun) (Iso.hom (β_ A A) ≫ μ) : (a : MonoidalCategoryStruct.tensorObj A A) → A) (y, x) : A)
    ((hom (FC := TypeCat.Fun) μ : (a : MonoidalCategoryStruct.tensorObj A A) → A) (y, x) : A)

Tactic:
congr_hom (CC := fun X ↦ X) (IsCommMonObj.mul_comm A) (y, x)

Premises used: Prod.mk, CategoryTheory.IsCommMonObj.mul_comm, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
Goal:
A : Type u
inst : MonObj A
inst_1 : IsCommMonObj A
x y : A
⊢ x * y = y * x

Tactic:
convert! congr_hom (CC := fun X ↦ X) (IsCommMonObj.mul_comm A) (y, x)

Premises used: Prod.mk, CategoryTheory.IsCommMonObj.mul_comm, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
Goal:
A : CommMonCat
h :
  ∀ (x y : (↑A : Type u)),
    (hom (FC := TypeCat.Fun)
            (Iso.hom
                (β_
                  (MonTypeEquivalenceMon.inverse.obj
                      (Functor.obj
                        (forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                          (CC := CommMonCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{u}) ↦
                          (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))
                        A)).X
                  (MonTypeEquivalenceMon.inverse.obj
                      (Functor.obj
                        (forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                          (CC := CommMonCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{u}) ↦
                          (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))
                        A)).X) ≫
              μ)).toFun
        (x, y) =
      TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) μ) (x, y)
⊢ Iso.hom
        (β_
          (MonTypeEquivalenceMon.inverse.obj
              (Functor.obj
                (forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                  CommMonCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                  MonCat.carrier))
                A)).X
          (MonTypeEquivalenceMon.inverse.obj
              (Functor.obj
                (forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                  CommMonCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                  MonCat.carrier))
                A)).X) ≫
      μ =
    μ

Tactic:
ext ⟨x : A, y : A⟩
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
Goal:
A : CommMonCat
x y : (↑A : Type u)
⊢ (hom (FC := TypeCat.Fun)
          (Iso.hom
              (β_
                (MonTypeEquivalenceMon.inverse.obj
                    (Functor.obj
                      (forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        CommMonCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                        (CD := MonCat.carrier))
                      A)).X
                (MonTypeEquivalenceMon.inverse.obj
                    (Functor.obj
                      (forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        CommMonCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                        (CD := MonCat.carrier))
                      A)).X) ≫
            μ)).toFun
      (x, y) =
    TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) μ) (x, y)

Tactic:
CommMonoid.mul_comm y x

Premises used: CommMonoid.mul_comm
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
Goal:
A : CommMonCat
x y : (↑A : Type u)
⊢ (hom (FC := TypeCat.Fun)
          (Iso.hom
              (β_
                (MonTypeEquivalenceMon.inverse.obj
                    (Functor.obj
                      (forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        CommMonCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                        (CD := MonCat.carrier))
                      A)).X
                (MonTypeEquivalenceMon.inverse.obj
                    (Functor.obj
                      (forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        CommMonCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                        (CD := MonCat.carrier))
                      A)).X) ≫
            μ)).toFun
      (x, y) =
    TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) μ) (x, y)

Tactic:
exact CommMonoid.mul_comm y x

Premises used: CommMonoid.mul_comm
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
Goal:
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ {X Y : CommMonCat.{u}} (f : X ⟶ Y),
    Eq (α :=
      (CommMonTypeEquivalenceCommMon.inverse ⋙ CommMonTypeEquivalenceCommMon.functor).obj X ⟶
        Functor.obj (𝟭 CommMonCat) Y)
      ((CommMonTypeEquivalenceCommMon.inverse ⋙ CommMonTypeEquivalenceCommMon.functor).map f ≫
        Iso.hom
          ((fun (A : CommMonCat.{u}) ↦
              (MulEquiv.toCommMonCatIso
                  (let __src :
                    (CommMonTypeEquivalenceCommMon.inverse.obj A).X ≃ (CommMonTypeEquivalenceCommMon.inverse.obj A).X :=
                    Equiv.refl (CommMonTypeEquivalenceCommMon.inverse.obj A).X;
                  { toEquiv := __src, map_mul' := ⋯ }) :
                CommMonCat.of (CommMonTypeEquivalenceCommMon.inverse.obj A).X ≅ CommMonCat.of (↑A : Type u)))
            Y))
      (Iso.hom
          ((fun (A : CommMonCat.{u}) ↦
              (MulEquiv.toCommMonCatIso
                  (let __src :
                    (CommMonTypeEquivalenceCommMon.inverse.obj A).X ≃ (CommMonTypeEquivalenceCommMon.inverse.obj A).X :=
                    Equiv.refl (CommMonTypeEquivalenceCommMon.inverse.obj A).X;
                  { toEquiv := __src, map_mul' := ⋯ }) :
                CommMonCat.of (CommMonTypeEquivalenceCommMon.inverse.obj A).X ≅ CommMonCat.of (↑A : Type u)))
            X) ≫
        CategoryTheory.Functor.map (𝟭 CommMonCat) f)
⊢ ∀ {X Y : CommMonCat.{u}} (f : X ⟶ Y),
    Eq (α :=
      (CommMonTypeEquivalenceCommMon.inverse ⋙ CommMonTypeEquivalenceCommMon.functor).obj X ⟶
        Functor.obj (𝟭 CommMonCat) Y)
      ((CommMonTypeEquivalenceCommMon.inverse ⋙ CommMonTypeEquivalenceCommMon.functor).map f ≫
        Iso.hom
          ((fun (A : CommMonCat.{u}) ↦
              (MulEquiv.toCommMonCatIso
                  (let __src :
                    (CommMonTypeEquivalenceCommMon.inverse.obj A).X ≃ (CommMonTypeEquivalenceCommMon.inverse.obj A).X :=
                    Equiv.refl (CommMonTypeEquivalenceCommMon.inverse.obj A).X;
                  { toEquiv := __src, map_mul' := ⋯ }) :
                CommMonCat.of (CommMonTypeEquivalenceCommMon.inverse.obj A).X ≅ CommMonCat.of (↑A : Type u)))
            Y))
      (Iso.hom
          ((fun (A : CommMonCat.{u}) ↦
              (MulEquiv.toCommMonCatIso
                  (let __src :
                    (CommMonTypeEquivalenceCommMon.inverse.obj A).X ≃ (CommMonTypeEquivalenceCommMon.inverse.obj A).X :=
                    Equiv.refl (CommMonTypeEquivalenceCommMon.inverse.obj A).X;
                  { toEquiv := __src, map_mul' := ⋯ }) :
                CommMonCat.of (CommMonTypeEquivalenceCommMon.inverse.obj A).X ≅ CommMonCat.of (↑A : Type u)))
            X) ≫
        CategoryTheory.Functor.map (𝟭 CommMonCat) f)

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_
Goal:
A : Type u
inst : GrpObj A
inst_1 : IsCommMonObj A
x y : A
⊢ Eq (α := A)
    ((hom (FC := TypeCat.Fun) (Iso.hom (β_ A A) ≫ μ) : (a : MonoidalCategoryStruct.tensorObj A A) → A) (y, x) : A)
    ((hom (FC := TypeCat.Fun) μ : (a : MonoidalCategoryStruct.tensorObj A A) → A) (y, x) : A)

Tactic:
congr_hom (CC := fun X ↦ X) (IsCommMonObj.mul_comm A) (y, x)

Premises used: Prod.mk, CategoryTheory.IsCommMonObj.mul_comm, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_
Goal:
A : Type u
inst : GrpObj A
inst_1 : IsCommMonObj A
x y : A
⊢ x * y = y * x

Tactic:
convert! congr_hom (CC := fun X ↦ X) (IsCommMonObj.mul_comm A) (y, x)

Premises used: Prod.mk, CategoryTheory.IsCommMonObj.mul_comm, CategoryTheory.ConcreteCategory.congr_hom