awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G H K : Functor.{v₁, v₂, u₁, u₂} C D
X : C
w w₁ :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1)
        (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1)
          (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (G.obj X)) (H.obj X))
        (K.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X)
        (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj X)
          (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (H.obj X) (K.obj X))))
    (Iso.hom (α_ (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (G.obj X)) (H.obj X) (K.obj X)) ≫
      Iso.hom (α_ (F.obj X) (G.obj X) (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (H.obj X) (K.obj X))))
    (Iso.hom (α_ (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (G.obj X)) (H.obj X) (K.obj X)) ≫
      Iso.hom (α_ (F.obj X) (G.obj X) (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (H.obj X) (K.obj X))))
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1)
        (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1)
          (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (G.obj X)) (H.obj X))
        (K.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X)
        (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj X)
          (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (H.obj X) (K.obj X))))
    (Iso.hom (α_ (F.obj X) (G.obj X) (H.obj X)) ▷ K.obj X ≫
      Iso.hom (α_ (F.obj X) (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj X) (H.obj X)) (K.obj X)) ≫
        F.obj X ◁ Iso.hom (α_ (G.obj X) (H.obj X) (K.obj X)))
    (Iso.hom (α_ (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (G.obj X)) (H.obj X) (K.obj X)) ≫
      Iso.hom (α_ (F.obj X) (G.obj X) (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (H.obj X) (K.obj X))))

Tactic:
rw [pentagon]

Premises used: CategoryTheory.MonoidalCategory.pentagon
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
inst_3 : BraidedCategory.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} C D
w :
  ∀ (X : C),
    Eq (α :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category)
              (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G) H).obj
          X ⟶
        (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G
              (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) H F)).obj
          X)
      (NatTrans.app
        (Iso.hom (α_ F G H) ≫
          Iso.hom
              (NatIso.ofComponents
                (fun (x : C) ↦ β_ (F.obj x) ((MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G H).obj x)) ⋯) ≫
            Iso.hom (α_ G H F))
        X)
      (NatTrans.app
        (Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (F.obj x) (G.obj x)) ⋯) ▷ H ≫
          Iso.hom (α_ G F H) ≫ G ◁ Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (F.obj x) (H.obj x)) ⋯))
        X)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category)
        (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G) H ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G
        (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) H F))
    (Iso.hom (α_ F G H) ≫
      Iso.hom
          (NatIso.ofComponents
            (fun (x : C) ↦ β_ (F.obj x) ((MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G H).obj x)) ⋯) ≫
        Iso.hom (α_ G H F))
    (Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (F.obj x) (G.obj x)) ⋯) ▷ H ≫
      Iso.hom (α_ G F H) ≫ G ◁ Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (F.obj x) (H.obj x)) ⋯))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
inst_3 : BraidedCategory.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category)
            (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G) H).obj
        X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G
            (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) H F)).obj
        X)
    (NatTrans.app
      (Iso.hom (α_ F G H) ≫
        Iso.hom
            (NatIso.ofComponents
              (fun (x : C) ↦ β_ (F.obj x) ((MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G H).obj x)) ⋯) ≫
          Iso.hom (α_ G H F))
      X)
    (NatTrans.app
      (Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (F.obj x) (G.obj x)) ⋯) ▷ H ≫
        Iso.hom (α_ G F H) ≫ G ◁ Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (F.obj x) (H.obj x)) ⋯))
      X)

Tactic:
apply hexagon_forward

Premises used: CategoryTheory.BraidedCategory.hexagon_forward
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
inst_3 : BraidedCategory.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} C D
w :
  ∀ (X : C),
    Eq (α :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F
              (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G H)).obj
          X ⟶
        (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category)
              (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) H F) G).obj
          X)
      (NatTrans.app
        (Iso.inv (α_ F G H) ≫
          Iso.hom
              (NatIso.ofComponents
                (fun (x : C) ↦ β_ ((MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G).obj x) (H.obj x)) ⋯) ≫
            Iso.inv (α_ H F G))
        X)
      (NatTrans.app
        (F ◁ Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (G.obj x) (H.obj x)) ⋯) ≫
          Iso.inv (α_ F H G) ≫ Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (F.obj x) (H.obj x)) ⋯) ▷ G)
        X)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F
        (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G H) ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category)
        (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) H F) G)
    (Iso.inv (α_ F G H) ≫
      Iso.hom
          (NatIso.ofComponents
            (fun (x : C) ↦ β_ ((MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G).obj x) (H.obj x)) ⋯) ≫
        Iso.inv (α_ H F G))
    (F ◁ Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (G.obj x) (H.obj x)) ⋯) ≫
      Iso.inv (α_ F H G) ≫ Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (F.obj x) (H.obj x)) ⋯) ▷ G)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
inst_3 : BraidedCategory.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F
            (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G H)).obj
        X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category)
            (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) H F) G).obj
        X)
    (NatTrans.app
      (Iso.inv (α_ F G H) ≫
        Iso.hom
            (NatIso.ofComponents
              (fun (x : C) ↦ β_ ((MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G).obj x) (H.obj x)) ⋯) ≫
          Iso.inv (α_ H F G))
      X)
    (NatTrans.app
      (F ◁ Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (G.obj x) (H.obj x)) ⋯) ≫
        Iso.inv (α_ F H G) ≫ Iso.hom (NatIso.ofComponents (fun (x : C) ↦ β_ (F.obj x) (H.obj x)) ⋯) ▷ G)
      X)

Tactic:
apply hexagon_reverse

Premises used: CategoryTheory.BraidedCategory.hexagon_reverse
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
inst_3 : SymmetricCategory.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
w :
  ∀ (X : C),
    NatTrans.app (Iso.hom (β_ F G) ≫ Iso.hom (β_ G F)) X =
      NatTrans.app (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G)) X
⊢ Iso.hom (β_ F G) ≫ Iso.hom (β_ G F) = 𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
inst_3 : SymmetricCategory.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ NatTrans.app (Iso.hom (β_ F G) ≫ Iso.hom (β_ G F)) X =
    NatTrans.app (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G)) X

Tactic:
apply symmetry

Premises used: CategoryTheory.SymmetricCategory.symmetry
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
inst_2 : MonoidalCategory.{v₂, u₂} D_1
C : Type u_1
D : Type u_2
E : Type u_3
inst_3 : Category.{v_1, u_1} C
inst_4 : Category.{v_2, u_2} D
inst_5 : Category.{v_3, u_3} E
inst_6 : MonoidalCategory.{v_2, u_2} D
inst_7 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : L.OplaxMonoidal
⊢ ∀ (X : Functor.{v_1, v_2, u_1, u_2} C D),
    Eq (α :=
      obj (obj (Functor.whiskeringRight C D E) L) X ⟶
        tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_3, u_1, u_3} C E)) (𝒞 := category))
          (obj (obj (Functor.whiskeringRight C D E) L) X))
      (Iso.inv (λ_ (obj (obj (Functor.whiskeringRight C D E) L) X)))
      (CategoryStruct.comp (Y :=
        obj (obj (Functor.whiskeringRight C D E) L)
          (tensorObj (𝒞 := category) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} C D)) (𝒞 := category)) X))
        (map (obj (Functor.whiskeringRight C D E) L) (Iso.inv (λ_ X)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := category)
            (obj (obj (Functor.whiskeringRight C D E) L) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} C D)) (𝒞 := category)))
            (obj (obj (Functor.whiskeringRight C D E) L) X))
          {
            app := fun (X_1 : C) ↦
              δ L (obj.{v_1, v_2, u_1, u_2} ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} C D)) (𝒞 := category)) X_1) (X.obj X_1),
            naturality := ⋯ }
          ({ app := fun (X : C) ↦ η L, naturality := ⋯ } ▷ obj (obj (Functor.whiskeringRight C D E) L) X)))

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
inst_2 : MonoidalCategory.{v₂, u₂} D_1
C : Type u_1
D : Type u_2
E : Type u_3
inst_3 : Category.{v_1, u_1} C
inst_4 : Category.{v_2, u_2} D
inst_5 : Category.{v_3, u_3} E
inst_6 : MonoidalCategory.{v_2, u_2} D
inst_7 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_2, v_3, u_2, u_3} D E
inst_8 : L.OplaxMonoidal
⊢ ∀ (X : Functor.{v_1, v_2, u_1, u_2} C D),
    Eq (α :=
      obj (obj (Functor.whiskeringRight C D E) L) X ⟶
        tensorObj (𝒞 := category) (obj (obj (Functor.whiskeringRight C D E) L) X)
          ((𝟙_ (Functor.{v_1, v_3, u_1, u_3} C E)) (𝒞 := category)))
      (Iso.inv (ρ_ (obj (obj (Functor.whiskeringRight C D E) L) X)))
      (CategoryStruct.comp (Y :=
        obj (obj (Functor.whiskeringRight C D E) L)
          (tensorObj (𝒞 := category) X ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} C D)) (𝒞 := category))))
        (map (obj (Functor.whiskeringRight C D E) L) (Iso.inv (ρ_ X)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := category) (obj (obj (Functor.whiskeringRight C D E) L) X)
            (obj (obj (Functor.whiskeringRight C D E) L) ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} C D)) (𝒞 := category))))
          {
            app := fun (X_1 : C) ↦
              δ L (X.obj X_1) (obj.{v_1, v_2, u_1, u_2} ((𝟙_ (Functor.{v_1, v_2, u_1, u_2} C D)) (𝒞 := category)) X_1),
            naturality := ⋯ }
          (obj (obj (Functor.whiskeringRight C D E) L) X ◁ { app := fun (X : C) ↦ η L, naturality := ⋯ })))

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
E : Type u_1
inst_3 : Category.{v_1, u_1} E
inst_4 : MonoidalCategory.{v_1, u_1} E
e : Equivalence.{v₁, v₂, u₁, u₂} C D
X Y : Functor.{v₂, v_1, u₂, u_1} D E
w :
  ∀ (x : C),
    Eq (α :=
      (tensorObj (𝒞 := Functor.category) (Functor.obj (Equivalence.inverse e.congrLeft) X)
              (Functor.obj (Equivalence.inverse e.congrLeft) Y)).obj
          x ⟶
        (Functor.obj (Equivalence.inverse e.congrLeft) (tensorObj (𝒞 := Functor.category) X Y)).obj x)
      (NatTrans.app (Functor.LaxMonoidal.μ (Equivalence.inverse e.congrLeft) X Y) x)
      (NatTrans.app
        (NatTrans.app (Adjunction.unit (Equivalence.toAdjunction e.congrLeft))
            (tensorObj (𝒞 := Functor.category) (Functor.obj (Equivalence.inverse e.congrLeft) X)
              (Functor.obj (Equivalence.inverse e.congrLeft) Y)) ≫
          Functor.map (Equivalence.inverse e.congrLeft)
            (CategoryStruct.comp (Y :=
              tensorObj (𝒞 := Functor.category)
                (Functor.obj (Equivalence.functor e.congrLeft) (Functor.obj (Equivalence.inverse e.congrLeft) X))
                (Functor.obj (Equivalence.functor e.congrLeft) (Functor.obj (Equivalence.inverse e.congrLeft) Y)))
              (Functor.OplaxMonoidal.δ (Equivalence.functor e.congrLeft)
                (Functor.obj (Equivalence.inverse e.congrLeft) X) (Functor.obj (Equivalence.inverse e.congrLeft) Y))
              (NatTrans.app (Adjunction.counit (Equivalence.toAdjunction e.congrLeft)) X ⊗ₘ
                NatTrans.app (Adjunction.counit (Equivalence.toAdjunction e.congrLeft)) Y)))
        x)
⊢ Eq (α :=
    tensorObj (𝒞 := Functor.category) (Functor.obj (Equivalence.inverse e.congrLeft) X)
        (Functor.obj (Equivalence.inverse e.congrLeft) Y) ⟶
      Functor.obj (Equivalence.inverse e.congrLeft) (tensorObj (𝒞 := Functor.category) X Y))
    (Functor.LaxMonoidal.μ (Equivalence.inverse e.congrLeft) X Y)
    (NatTrans.app (Adjunction.unit (Equivalence.toAdjunction e.congrLeft))
        (tensorObj (𝒞 := Functor.category) (Functor.obj (Equivalence.inverse e.congrLeft) X)
          (Functor.obj (Equivalence.inverse e.congrLeft) Y)) ≫
      Functor.map (Equivalence.inverse e.congrLeft)
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := Functor.category)
            (Functor.obj (Equivalence.functor e.congrLeft) (Functor.obj (Equivalence.inverse e.congrLeft) X))
            (Functor.obj (Equivalence.functor e.congrLeft) (Functor.obj (Equivalence.inverse e.congrLeft) Y)))
          (Functor.OplaxMonoidal.δ (Equivalence.functor e.congrLeft) (Functor.obj (Equivalence.inverse e.congrLeft) X)
            (Functor.obj (Equivalence.inverse e.congrLeft) Y))
          (NatTrans.app (Adjunction.counit (Equivalence.toAdjunction e.congrLeft)) X ⊗ₘ
            NatTrans.app (Adjunction.counit (Equivalence.toAdjunction e.congrLeft)) Y)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
E : Type u_1
inst_3 : Category.{v_1, u_1} E
inst_4 : MonoidalCategory.{v_1, u_1} E
e : Equivalence.{v₁, v₂, u₁, u₂} C D
X Y : Functor.{v₂, v_1, u₂, u_1} D E
x : C
⊢ Eq (α :=
    (tensorObj (𝒞 := Functor.category) (Functor.obj (Equivalence.inverse e.congrLeft) X)
            (Functor.obj (Equivalence.inverse e.congrLeft) Y)).obj
        x ⟶
      (Functor.obj (Equivalence.inverse e.congrLeft) (tensorObj (𝒞 := Functor.category) X Y)).obj x)
    (NatTrans.app (Functor.LaxMonoidal.μ (Equivalence.inverse e.congrLeft) X Y) x)
    (NatTrans.app
      (NatTrans.app (Adjunction.unit (Equivalence.toAdjunction e.congrLeft))
          (tensorObj (𝒞 := Functor.category) (Functor.obj (Equivalence.inverse e.congrLeft) X)
            (Functor.obj (Equivalence.inverse e.congrLeft) Y)) ≫
        Functor.map (Equivalence.inverse e.congrLeft)
          (CategoryStruct.comp (Y :=
            tensorObj (𝒞 := Functor.category)
              (Functor.obj (Equivalence.functor e.congrLeft) (Functor.obj (Equivalence.inverse e.congrLeft) X))
              (Functor.obj (Equivalence.functor e.congrLeft) (Functor.obj (Equivalence.inverse e.congrLeft) Y)))
            (Functor.OplaxMonoidal.δ (Equivalence.functor e.congrLeft) (Functor.obj (Equivalence.inverse e.congrLeft) X)
              (Functor.obj (Equivalence.inverse e.congrLeft) Y))
            (NatTrans.app (Adjunction.counit (Equivalence.toAdjunction e.congrLeft)) X ⊗ₘ
              NatTrans.app (Adjunction.counit (Equivalence.toAdjunction e.congrLeft)) Y)))
      x)

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : Grp.{v₁, u₁} C
⊢ (InducedCategory.Hom.hom (𝟙 A)).hom = 𝟙 A.X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
R S T : Grp.{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.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : Grp.{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.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : Grp.{v₁, u₁} C
⊢ InducedCategory.Hom.hom (𝟙 A) = 𝟙 A.toMon

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A₁ A₂ A₃ : Grp.{v₁, u₁} C
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
⊢ (f ≫ g).hom = f.hom ≫ g.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj B
f : A ⟶ B
⊢ f ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (𝟙 B) (@inv _ _ inst_1 _ _)) μ =
    f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η

Tactic:
have := f ≫= right_inv B
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj B
f : A ⟶ B
this :
  f ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (𝟙 B) (@inv _ _ inst_1 _ _)) μ =
    f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ 𝟙 B) (f ≫ @inv _ _ inst_1 _ _)) μ =
        f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (f ≫ @inv _ _ inst_1 _ _)) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
rwa₁ :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (f ≫ @inv _ _ inst_1 _ _)) μ =
        f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (f ≫ @inv _ _ inst_1 _ _)) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (f ≫ @inv _ _ inst_1 _ _)) μ =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (f ≫ @inv _ _ inst_1 _ _)) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift f (f ≫ @inv _ _ inst_1 _ _)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η

Tactic:
rwa [comp_lift_assoc, comp_id, reassoc_of% toUnit_unique (f ≫ toUnit B) (toUnit A)] at this

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique, CategoryTheory.Category.comp_id, CategoryTheory.CartesianMonoidalCategory.comp_lift_assoc, CategoryTheory.CategoryStruct.comp, CategoryTheory.SemiCartesianMonoidalCategory.toUnit
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (𝟙 A) (@inv _ _ inst_1 _ _)) μ ≫ f =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f

Tactic:
have := right_inv A =≫ f
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj B
f : A ⟶ B
⊢ f ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@inv _ _ inst_1 _ _) (𝟙 B)) μ =
    f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η

Tactic:
have := f ≫= left_inv B
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj B
f : A ⟶ B
this :
  f ≫ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (@inv _ _ inst_1 _ _) (𝟙 B)) μ =
    f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η
rwa :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ @inv _ _ inst_1 _ _) (f ≫ 𝟙 B)) μ =
        f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ @inv _ _ inst_1 _ _) f) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
rwa₁ :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ @inv _ _ inst_1 _ _) f) μ =
        f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit B) η),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ @inv _ _ inst_1 _ _) f) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀
    (this :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ @inv _ _ inst_1 _ _) f) μ =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η),
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ @inv _ _ inst_1 _ _) f) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) (lift (f ≫ @inv _ _ inst_1 _ _) f) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η

Tactic:
rwa [comp_lift_assoc, comp_id, reassoc_of% toUnit_unique (f ≫ toUnit B) (toUnit A)] at this

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique, CategoryTheory.Category.comp_id, CategoryTheory.CartesianMonoidalCategory.comp_lift_assoc, CategoryTheory.CategoryStruct.comp, CategoryTheory.SemiCartesianMonoidalCategory.toUnit
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (lift (@inv _ _ inst_1 _ _) (𝟙 A)) μ ≫ f =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit A) η ≫ f

Tactic:
have := left_inv A =≫ f