mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
r : R
a : ↑A
⊢ (let __src := Hom.hom η;
        { toFun := __src.toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
        r *
      a =
    a *
      (let __src := Hom.hom η;
        { toFun := __src.toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
        r

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
⊢ MonoidalCategoryStruct.whiskerRight (↟(Algebra.linearMap R ↑A)) (of R ↑A) ≫ ↟(mul' R ↑A) =
    (MonoidalCategoryStruct.leftUnitor (of R ↑A)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
⊢ MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(Algebra.linearMap R ↑A)) ≫ ↟(mul' R ↑A) =
    (MonoidalCategoryStruct.rightUnitor (of R ↑A)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
⊢ MonoidalCategoryStruct.whiskerRight (↟(mul' R ↑A)) (of R ↑A) ≫ ↟(mul' R ↑A) =
    (MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom ≫
      MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A)) ≫ ↟(mul' R ↑A)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : Mon (ModuleCat R)
⊢ μ ≫ ↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ } =
    MonoidalCategoryStruct.tensorHom (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ })
        (↟{ toFun := _root_.id, map_add' := ⋯, map_smul' := ⋯ }) ≫
      μ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F G : J ⥤ C
j j' : J
f : j ⟶ j'
⊢ ((Functor.const J).obj (limit F ⊗ limit G)).map f ≫ (limit.π F j' ⊗ₘ limit.π G j') =
    (limit.π F j ⊗ₘ limit.π G j) ≫ (F ⊗ G).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
X✝ Y✝ X'✝ Y'✝ : J ⥤ C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
j : J
⊢ ((lim.map f ⊗ₘ lim.map g) ≫
        limit.lift (Y✝ ⊗ Y'✝)
          { pt := limit Y✝ ⊗ limit Y'✝, π := { app := fun j ↦ limit.π Y✝ j ⊗ₘ limit.π Y'✝ j, naturality := ⋯ } }) ≫
      limit.π (Y✝ ⊗ Y'✝) j =
    (limit.lift (X✝ ⊗ X'✝)
          { pt := limit X✝ ⊗ limit X'✝, π := { app := fun j ↦ limit.π X✝ j ⊗ₘ limit.π X'✝ j, naturality := ⋯ } } ≫
        lim.map (f ⊗ₘ g)) ≫
      limit.π (Y✝ ⊗ Y'✝) j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ hom P Q L ≫ inv P Q L = 𝟙 ((P.tensorBimod Q).tensorBimod L).X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
V : Type u₂
inst✝² : Category.{v₂, u₂} V
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalCategory V
F G : C ⥤ V
h h' : DayConvolution F G
⊢ unit F G ≫ (tensor C).whiskerLeft (h.uniqueUpToIso h').hom = unit F G

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F G H : J ⥤ C
j : J
⊢ ((limit.lift (F ⊗ G)
            { pt := limit F ⊗ limit G, π := { app := fun j ↦ limit.π F j ⊗ₘ limit.π G j, naturality := ⋯ } } ⊗ₘ
          𝟙 (lim.obj H)) ≫
        limit.lift ((F ⊗ G) ⊗ H)
            { pt := limit (F ⊗ G) ⊗ limit H,
              π := { app := fun j ↦ limit.π (F ⊗ G) j ⊗ₘ limit.π H j, naturality := ⋯ } } ≫
          lim.map (α_ F G H).hom) ≫
      limit.π (F ⊗ G ⊗ H) j =
    ((α_ (lim.obj F) (lim.obj G) (lim.obj H)).hom ≫
        (𝟙 (lim.obj F) ⊗ₘ
            limit.lift (G ⊗ H)
              { pt := limit G ⊗ limit H, π := { app := fun j ↦ limit.π G j ⊗ₘ limit.π H j, naturality := ⋯ } }) ≫
          limit.lift (F ⊗ G ⊗ H)
            { pt := limit F ⊗ limit (G ⊗ H),
              π := { app := fun j ↦ limit.π F j ⊗ₘ limit.π (G ⊗ H) j, naturality := ⋯ } }) ≫
      limit.π (F ⊗ G ⊗ H) j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
V : Type u₂
inst✝² : Category.{v₂, u₂} V
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalCategory V
F G : C ⥤ V
h h' : DayConvolution F G
⊢ unit F G ≫ (tensor C).whiskerLeft (h.uniqueUpToIso h').inv = unit F G

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
F G : C ⥤ V
inst✝ : DayConvolution F G
x x' y y' : C
f : x ⟶ x'
g : y ⟶ y'
⊢ (F.map f ⊗ₘ G.map g) ≫ (unit F G).app (x', y') = (unit F G).app (x, y) ≫ (F ⊛ G).map (f ⊗ₘ g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
F G : C ⥤ V
inst✝ : DayConvolution F G
x x' y : C
f : x ⟶ x'
⊢ F.map f ▷ G.obj y ≫ (unit F G).app (x', y) = (unit F G).app (x, y) ≫ (F ⊛ G).map (f ▷ y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
F G : C ⥤ V
inst✝ : DayConvolution F G
x y y' : C
g : y ⟶ y'
⊢ F.obj x ◁ G.map g ≫ (unit F G).app (x, y') = (unit F G).app (x, y) ≫ (F ⊛ G).map (x ◁ g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁴ : Category.{v₂, u₂} V
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory V
F G : C ⥤ V
inst✝¹ : DayConvolution F G
F' G' : C ⥤ V
inst✝ : DayConvolution F' G'
f : F ⟶ F'
g : G ⟶ G'
x y : C
⊢ (unit F G).app (x, y) ≫ (map f g).app (x ⊗ y) = (f.app x ⊗ₘ g.app y) ≫ (unit F' G').app (x, y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (λ_ (lim.obj F)).hom ≫ limit.π F j =
    ((limit.lift ((Functor.const J).obj (𝟙_ C))
            { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (((Functor.const J).obj (𝟙_ C)).obj x), naturality := ⋯ } } ⊗ₘ
          𝟙 (lim.obj F)) ≫
        limit.lift (𝟙_ (J ⥤ C) ⊗ F)
            { pt := limit (𝟙_ (J ⥤ C)) ⊗ limit F,
              π := { app := fun j ↦ limit.π (𝟙_ (J ⥤ C)) j ⊗ₘ limit.π F j, naturality := ⋯ } } ≫
          lim.map (λ_ F).hom) ≫
      limit.π F j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
F G : C ⥤ V
inst✝ : DayConvolution F G
⊢ ∀ {Y Y' : C ⥤ V} (g : Y ⟶ Y') (f : F ⊛ G ⟶ Y),
    ((F ⊛ G).homEquivOfIsLeftKanExtension (unit F G) Y') (f ≫ g) =
      (ConcreteCategory.hom
          (((Functor.whiskeringLeft (C × C) C V).obj (tensor C) ⋙ coyoneda.obj (Opposite.op (F ⊠ G))).map g))
        (((F ⊛ G).homEquivOfIsLeftKanExtension (unit F G) Y) f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
F G : C ⥤ V
inst✝ : DayConvolution F G
c : C
v : V
f g : (F ⊛ G).obj c ⟶ v
h : ∀ {x y : C} (u : x ⊗ y ⟶ c), (unit F G).app (x, y) ≫ (F ⊛ G).map u ≫ f = (unit F G).app (x, y) ≫ (F ⊛ G).map u ≫ g
j : CostructuredArrow (tensor C) c
⊢ ((Functor.LeftExtension.mk (F ⊛ G) (unit F G)).coconeAt c).ι.app j ≫ f =
    ((Functor.LeftExtension.mk (F ⊛ G) (unit F G)).coconeAt c).ι.app j ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ (lim.obj F)).hom ≫ limit.π F j =
    ((𝟙 (lim.obj F) ⊗ₘ
          limit.lift ((Functor.const J).obj (𝟙_ C))
            { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (((Functor.const J).obj (𝟙_ C)).obj x), naturality := ⋯ } }) ≫
        limit.lift (F ⊗ 𝟙_ (J ⥤ C))
            { pt := limit F ⊗ limit (𝟙_ (J ⥤ C)),
              π := { app := fun j ↦ limit.π F j ⊗ₘ limit.π (𝟙_ (J ⥤ C)) j, naturality := ⋯ } } ≫
          lim.map (ρ_ F).hom) ≫
      limit.π F j

Tactic:
dsimp
      simp only [id_tensorHom, limit.lift_map, Category.assoc, limit.lift_π]
      dsimp
      simp only [tensorHom_def, ← whisker_exchange, whiskerRight_id, Category.assoc, Iso.inv_hom_id,
        Category.comp_id, ← whiskerLeft_comp_assoc]
      erw [limit.lift_π]
      rw [whiskerLeft_id, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ (lim.obj F)).hom ≫ limit.π F j =
    ((𝟙 (lim.obj F) ⊗ₘ
          limit.lift ((Functor.const J).obj (𝟙_ C))
            { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (((Functor.const J).obj (𝟙_ C)).obj x), naturality := ⋯ } }) ≫
        limit.lift (F ⊗ 𝟙_ (J ⥤ C))
            { pt := limit F ⊗ limit (𝟙_ (J ⥤ C)),
              π := { app := fun j ↦ limit.π F j ⊗ₘ limit.π (𝟙_ (J ⥤ C)) j, naturality := ⋯ } } ≫
          lim.map (ρ_ F).hom) ≫
      limit.π F j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Cokernels

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X₁ Y₁ : C
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
inst✝ : HasBinaryCoproduct (X₁ ⊗ Y₂) (Y₁ ⊗ X₂)
⊢ coprod.desc (f₁ ▷ Y₂) (Y₁ ◁ f₂) ≫ (Cofork.π c₁ ⊗ₘ Cofork.π c₂) = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Cokernels

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : MonoidalPreadditive C
X₁ Y₁ : C
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
inst✝³ : HasBinaryCoproduct (X₁ ⊗ Y₂) (Y₁ ⊗ X₂)
inst✝² : PreservesColimit (parallelPair f₂ 0) (tensorLeft c₁.pt)
inst✝¹ : PreservesColimit (parallelPair f₁ 0) (tensorRight Y₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (tensorRight X₂)
⊢ HasBinaryCoproduct (((curriedTensor C).obj X₁).obj Y₂) (((curriedTensor C).obj Y₁).obj X₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
F G : C ⥤ V
inst✝⁵ : DayConvolution F G
H : C ⥤ V
inst✝⁴ : DayConvolution G H
inst✝³ : DayConvolution F (G ⊛ H)
inst✝² : DayConvolution (F ⊛ G) H
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
⊢ ∀ {Y Y' : C ⥤ V} (g : Y ⟶ Y') (f : F ⊛ G ⊛ H ⟶ Y),
    ((corepresentableBy F (G ⊛ H)).homEquiv.trans
          ((F ⊠ G ⊛ H).homEquivOfIsLeftKanExtension (extensionUnitRight (G ⊛ H) (unit G H) F)
            (((whiskeringLeft (C × C) C V).obj (tensor C)).obj Y')))
        (f ≫ g) =
      (ConcreteCategory.hom
          (((whiskeringLeft (C × C) C V).obj (tensor C) ⋙
                (whiskeringLeft (C × C × C) (C × C) V).obj ((𝟭 C).prod (tensor C)) ⋙
                  coyoneda.obj (Opposite.op (F ⊠ G ⊠ H))).map
            g))
        (((corepresentableBy F (G ⊛ H)).homEquiv.trans
            ((F ⊠ G ⊛ H).homEquivOfIsLeftKanExtension (extensionUnitRight (G ⊛ H) (unit G H) F)
              (((whiskeringLeft (C × C) C V).obj (tensor C)).obj Y)))
          f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Cokernels

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : MonoidalPreadditive C
X₁ Y₁ : C
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
inst✝³ : HasBinaryCoproduct (X₁ ⊗ Y₂) (Y₁ ⊗ X₂)
inst✝² : PreservesColimit (parallelPair f₂ 0) (tensorLeft c₁.pt)
inst✝¹ : PreservesColimit (parallelPair f₁ 0) (tensorRight Y₂)
inst✝ : PreservesColimit (parallelPair f₁ 0) (tensorRight X₂)
this : HasBinaryCoproduct (((curriedTensor C).obj X₁).obj Y₂) (((curriedTensor C).obj Y₁).obj X₂)
⊢ Cofork.π (c₁.mapBifunctor c₂ (curriedTensor C)) ≫ (Iso.refl (c₁.mapBifunctor c₂ (curriedTensor C)).pt).hom =
    Cofork.π (c₁.tensor c₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
F G : C ⥤ V
inst✝⁵ : DayConvolution F G
H : C ⥤ V
inst✝⁴ : DayConvolution G H
inst✝³ : DayConvolution F (G ⊛ H)
inst✝² : DayConvolution (F ⊛ G) H
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
⊢ ∀ {Y Y' : C ⥤ V} (g : Y ⟶ Y') (f : (F ⊛ G) ⊛ H ⟶ Y),
    ((corepresentableBy (F ⊛ G) H).homEquiv.trans
          (((F ⊛ G) ⊠ H).homEquivOfIsLeftKanExtension (extensionUnitLeft (F ⊛ G) (unit F G) H)
            (((whiskeringLeft (C × C) C V).obj (tensor C)).obj Y')))
        (f ≫ g) =
      (ConcreteCategory.hom
          (((whiskeringLeft (C × C) C V).obj (tensor C) ⋙
                (whiskeringLeft ((C × C) × C) (C × C) V).obj ((tensor C).prod (𝟭 C)) ⋙
                  coyoneda.obj (Opposite.op ((F ⊠ G) ⊠ H))).map
            g))
        (((corepresentableBy (F ⊛ G) H).homEquiv.trans
            (((F ⊛ G) ⊠ H).homEquivOfIsLeftKanExtension (extensionUnitLeft (F ⊛ G) (unit F G) H)
              (((whiskeringLeft (C × C) C V).obj (tensor C)).obj Y)))
          f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ inv P Q L ≫ hom P Q L = 𝟙 (P.tensorBimod (Q.tensorBimod L)).X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ (regular R).actRight ▷ P.X ≫ P.actLeft = ((α_ (regular R).X R.X P.X).hom ≫ (regular R).X ◁ P.actLeft) ≫ P.actLeft

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| 𝟙_ C ◁ P.actLeft ≫ η ▷ P.X

pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (λ_ (R.X ⊗ P.X)).inv

Tactic:
whisker_exchange

Goal state after:
case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| η ▷ (R.X ⊗ P.X) ≫ R.X ◁ P.actLeft

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| (λ_ (R.X ⊗ P.X)).inv
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
F G : C ⥤ V
inst✝⁵ : DayConvolution F G
H : C ⥤ V
inst✝⁴ : DayConvolution G H
inst✝³ : DayConvolution F (G ⊛ H)
inst✝² : DayConvolution (F ⊛ G) H
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
x y z : C
⊢ (unit F G).app (x, y) ▷ H.obj z ≫ (unit (F ⊛ G) H).app (x ⊗ y, z) ≫ (associator F G H).hom.app ((x ⊗ y) ⊗ z) =
    (α_ (F.obj x) ((G, H).1.obj (y, z).1) ((G, H).2.obj (y, z).2)).hom ≫
      F.obj x ◁ (unit G H).app (y, z) ≫ (unit F (G ⊛ H)).app (x, y ⊗ z) ≫ (F ⊛ G ⊛ H).map (α_ (x, y ⊗ z).1 y z).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
f g : C
⊢ ∀ {Z : C} (f_1 : g ⟶ Z), f ◁ f_1 ≫ (coprod.braiding f Z).hom = (coprod.braiding f g).hom ≫ f_1 ▷ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
g : C
⊢ f ▷ g ≫ (coprod.braiding Y✝ g).hom = (coprod.braiding X✝ g).hom ≫ g ◁ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X Y Z : C
⊢ (α_ X Y Z).hom ≫ (coprod.braiding X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom =
    (coprod.braiding X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (coprod.braiding X Z).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X Y Z : C
⊢ (α_ X Y Z).inv ≫ (coprod.braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv =
    X ◁ (coprod.braiding Y Z).hom ≫ (α_ X Z Y).inv ≫ (coprod.braiding X Z).hom ▷ Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X Y Z : C
⊢ (α_ X Y Z).inv ≫ (coprod.braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv =
    X ◁ (coprod.braiding Y Z).hom ≫ (α_ X Z Y).inv ≫ (coprod.braiding X Z).hom ▷ Y

Tactic:
by dsimp [monoidalOfHasFiniteCoproducts.associator_inv]; simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
inst✝¹ : HasInitial C
inst✝ : HasBinaryCoproducts C
X Y : C
⊢ (coprod.braiding X Y).hom ≫ (coprod.braiding Y X).hom = 𝟙 (X ⊗ Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ hom P ≫ inv P = 𝟙 (TensorBimod.X (regular R) P)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ inv P ≫ hom P = 𝟙 P.X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
F G : C ⥤ V
inst✝⁵ : DayConvolution F G
H : C ⥤ V
inst✝⁴ : DayConvolution G H
inst✝³ : DayConvolution F (G ⊛ H)
inst✝² : DayConvolution (F ⊛ G) H
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
x y z : C
⊢ F.obj x ◁ (unit G H).app (y, z) ≫ (unit F (G ⊛ H)).app (x, y ⊗ z) ≫ (associator F G H).inv.app (x ⊗ y ⊗ z) =
    (α_ (F.obj x) (G.obj y) (H.obj z)).inv ≫
      (unit F G).app (x, y) ▷ H.obj z ≫ (unit (F ⊛ G) H).app (x ⊗ y, z) ≫ ((F ⊛ G) ⊛ H).map (α_ x y z).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ ((regular R).tensorBimod P).actLeft ≫ hom P = R.X ◁ hom P ≫ P.actLeft

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Opposite.Mon

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
⊢ MonObj.one.mop ▷ { unmop := M } ≫ MonObj.mul.mop = (λ_ { unmop := M }).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Opposite.Mon

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
⊢ { unmop := M } ◁ MonObj.one.mop ≫ MonObj.mul.mop = (ρ_ { unmop := M }).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Opposite.Mon

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
⊢ MonObj.mul.mop ▷ { unmop := M } ≫ MonObj.mul.mop =
    (α_ { unmop := M } { unmop := M } { unmop := M }).hom ≫ { unmop := M } ◁ MonObj.mul.mop ≫ MonObj.mul.mop

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Opposite.Mon

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : MonoidalCategory C
M : C
inst✝² : MonObj M
N : C
inst✝¹ : MonObj N
f : M ⟶ N
inst✝ : IsMonHom f
⊢ MonObj.one ≫ f.mop = MonObj.one

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Opposite.Mon

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : MonoidalCategory C
M : C
inst✝² : MonObj M
N : C
inst✝¹ : MonObj N
f : M ⟶ N
inst✝ : IsMonHom f
⊢ MonObj.mul ≫ f.mop = (f.mop ⊗ₘ f.mop) ≫ MonObj.mul

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Opposite.Mon

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
M : Cᴹᵒᵖ
inst✝ : MonObj M
⊢ MonObj.one.unmop ▷ M.unmop ≫ MonObj.mul.unmop = (λ_ M.unmop).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Opposite.Mon

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
M : Cᴹᵒᵖ
inst✝ : MonObj M
⊢ M.unmop ◁ MonObj.one.unmop ≫ MonObj.mul.unmop = (ρ_ M.unmop).hom

Tactic:
by

Goal state after: