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

Goal state before:
pp: case h_snd
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h :
  lift (fst R (R ⊗ R)) (lift (snd R (R ⊗ R) ≫ fst R R) (snd R (R ⊗ R) ≫ snd R R) ≫ σ) ≫ μ =
    lift (lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ fst R R) ≫ μ) (lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ snd R R) ≫ μ) ≫ σ
⊢ lift (R ◁ fst R R ≫ μ) (R ◁ snd R R ≫ μ) ≫ snd R R =
    lift (lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ fst R R) ≫ μ) (lift (fst R (R ⊗ R)) (snd R (R ⊗ R) ≫ snd R R) ≫ μ) ≫
      snd R R

Tactic:
· simp only [lift_snd]
        congr 1
        cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor

Goal state before:
pp: case e'_3.e'_7.e'_8
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
e_1✝ :
  (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ ihom (F.obj A)).obj (A ⊗ B)) =
    (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ ihom (F.obj A)).obj (((curriedTensor C).obj A).obj B))
e_4✝ :
  (tensorLeft (F.obj A) ⋙ ihom (F.obj A)).obj (F.obj B) =
    ((curriedTensor D).obj (F.obj A) ⋙ ihom (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_5✝ : (ihom (F.obj A)).obj (F.obj (A ⊗ B)) = (ihom (F.obj A)).obj (((curriedTensor C).obj A ⋙ F).obj ((𝟭 C).obj B))
e_6✝ : (tensorLeft (F.obj A)).obj (F.obj B) = ((curriedTensor D).obj (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_7✝ : F.obj (A ⊗ B) = ((curriedTensor C).obj A ⋙ F).obj ((𝟭 C).obj B)
⊢ prodComparison F A B ≫ (prodComparisonNatIso F A).inv.app ((𝟭 C).obj B) = 𝟙 (F.obj (A ⊗ B))

Tactic:
simp

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

Goal state before:
pp: case h_snd
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
R : C
inst✝¹ : MonObj R
inst✝ : AddMonObj R
h :
  lift (lift (fst (R ⊗ R) R ≫ fst R R) (fst (R ⊗ R) R ≫ snd R R) ≫ σ) (snd (R ⊗ R) R) ≫ μ =
    lift (lift (fst (R ⊗ R) R ≫ fst R R) (snd (R ⊗ R) R) ≫ μ) (lift (fst (R ⊗ R) R ≫ snd R R) (snd (R ⊗ R) R) ≫ μ) ≫ σ
⊢ lift (fst R R ▷ R ≫ μ) (snd R R ▷ R ≫ μ) ≫ snd R R =
    lift (lift (fst (R ⊗ R) R ≫ fst R R) (snd (R ⊗ R) R) ≫ μ) (lift (fst (R ⊗ R) R ≫ snd R R) (snd (R ⊗ R) R) ≫ μ) ≫
      snd R R

Tactic:
· simp only [lift_snd]
        congr 1
        cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor

Goal state before:
pp: case e_6
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A A' : C
f : A' ⟶ A
vcomp1 :
  (mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')))
      (TwoSquare.whiskerRight (prodComparisonNatIso F A).inv ((curriedTensor D).map (F.map f))) =
    ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A))) (prodComparisonNatIso F A).inv).whiskerBottom
      ((conjugateEquiv (ihom.adjunction (F.obj A)) (ihom.adjunction (F.obj A'))) ((curriedTensor D).map (F.map f)))
vcomp2 :
  (mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A')))
      (TwoSquare.whiskerLeft (prodComparisonNatIso F A').inv ((curriedTensor C).map f)) =
    ((mateEquiv (ihom.adjunction A') (ihom.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv).whiskerTop
      ((conjugateEquiv (ihom.adjunction A) (ihom.adjunction A')) ((curriedTensor C).map f))
B : C
⊢ prodComparison F A' B ≫ inv (prodComparison F A' B) ≫ F.map (f ▷ B) = F.map (f ▷ B)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Ring

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
R : C
inst✝ : RingObj R
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ f.unop ≫ 1 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Ring

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
R : C
inst✝ : RingObj R
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ f.unop ≫ 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Ring

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X✝ Y✝ : RingObjCat C
f : X✝ ⟶ Y✝
X : Cᵒᵖ
⊢ 1 ≫ f.hom = 1

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Ring

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X✝ Y✝ : RingObjCat C
f : X✝ ⟶ Y✝
X : Cᵒᵖ
⊢ 0 ≫ f.hom = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Ring

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X✝ Y✝ : CommRingObjCat C
f : X✝ ⟶ Y✝
X : Cᵒᵖ
⊢ 1 ≫ f.hom = 1

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Ring

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X✝ Y✝ : CommRingObjCat C
f : X✝ ⟶ Y✝
X : Cᵒᵖ
⊢ 0 ≫ f.hom = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid

Goal state before:
pp: D : Type u
C : Type u_1
inst✝³ : Groupoid D
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ (ihom.coev (F.obj Y)).app (G.obj X) ≫ (ihom (F.obj Y)).map (F.obj Y ◁ G.map f) =
    (ihom.coev (F.obj Y)).app (G.obj X) ≫
      (ihom (F.obj Y)).map (CategoryTheory.inv (F.map f) ▷ G.obj X ≫ F.map f ▷ G.obj X ≫ F.obj Y ◁ G.map f)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid

Goal state before:
pp: D : Type u
C : Type u_1
inst✝³ : Groupoid D
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ (F.map f ▷ (ihom (F.obj X)).obj (G.obj X) ≫
        F.obj Y ◁ ((ihom (F.obj X)).map (G.map f) ≫ (pre (CategoryTheory.inv (F.map f))).app (G.obj Y))) ≫
      (ihom.ev (F.obj Y)).app (G.obj Y) =
    (ihom.ev (F.obj X)).app (G.obj X) ≫ G.map f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid

Goal state before:
pp: D : Type u
C : Type u_1
inst✝³ : Groupoid D
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
⊢ ∀ ⦃X Y : D⦄ (f : X ⟶ Y),
    ((F.closedIhom ⋙ tensorLeft F).obj G).map f ≫ (ihom.ev (F.obj Y)).app (G.obj Y) =
      (ihom.ev (F.obj X)).app (G.obj X) ≫ ((𝟭 (D ⥤ C)).obj G).map f

Tactic:
intro X Y f
      dsimp
      simp only [closedIhom_obj_map, pre_comm_ihom_map]
      rw [tensorHom_def]
      simp

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 T : Mon C
P : Bimod R S
Q : Bimod S T
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.X P.X Q.X).inv ▷ T.X ≫
      (((α_ (R.X ⊗ P.X) Q.X T.X).hom ≫ P.actLeft ▷ (Q.X ⊗ T.X)) ≫ P.X ◁ Q.actRight) ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) =
    (α_ R.X (P.X ⊗ Q.X) T.X).hom ≫
      R.X ◁ (α_ P.X Q.X T.X).hom ≫
        (α_ R.X P.X (Q.X ⊗ T.X)).inv ≫
          (P.actLeft ▷ (Q.X ⊗ T.X) ≫ P.X ◁ Q.actRight) ≫
            coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

Tactic:
simp

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
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
⊢ M.X ◁ (Y.X ◁ f.hom ≫ N₂.actLeft) = M.X ◁ Y.X ◁ f.hom ≫ M.X ◁ N₂.actLeft

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
L : D ⥤ C
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
conjeq :
  ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)))
        ((mateEquiv h h)
          (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A))))).natTrans =
    (conjugateEquiv (h.comp (ihom.adjunction A)) ((ihom.adjunction (F.obj A)).comp h))
      (prodComparisonNatTrans L (F.obj A) ≫ L.whiskerLeft ((curriedTensor C).map (h.counit.app A)))
B : C
⊢ h.unit.app (F.obj A ⊗ F.obj B) ≫
      lift ((L ⋙ F).map (fst (F.obj A) (F.obj B))) ((L ⋙ F).map (snd (F.obj A) (F.obj B))) ≫
        F.map (h.counit.app A) ▷ F.obj (L.obj (F.obj B)) ≫ F.obj A ◁ F.map (h.counit.app B) =
    𝟙 (F.obj A ⊗ F.obj B)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: case e_a.e_12
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j : J
k : Under j
⊢ k.hom ≫ 𝟙 k.right = k.hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : IsSubterminal A
inst✝ : HasBinaryProduct A A
⊢ diag A ≫ prod.fst = 𝟙 A

Tactic:
simp

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
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
⊢ (α_ X.X M.X N₁.X).inv ≫
      M.actLeft ▷ N₁.X ≫
        M.X ◁ f.hom ≫
          colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft))
            WalkingParallelPair.one =
    (α_ X.X M.X N₁.X).inv ≫
      (M.actLeft ▷ N₁.X ≫ M.X ◁ f.hom) ≫ coequalizer.π (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
x y z : C
inst✝² : Closed x
inst✝¹ : Closed y
inst✝ : Closed (x ⊗ y)
⊢ (α_ x y ((ihom y).obj ((ihom x).obj z))).inv ≫
      (α_ x y ((ihom y).obj ((ihom x).obj z))).hom ≫ x ◁ (ihom.ev y).app ((ihom x).obj z) ≫ (ihom.ev x).app z =
    uncurry ((ihom.ev y).app ((ihom x).obj z))

Tactic:
simp

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
x y z : C
inst✝² : Closed x
inst✝¹ : Closed y
inst✝ : Closed (x ⊗ y)
⊢ x ◁ (ihom.ev y).app ((ihom x).obj z) ≫ (ihom.ev x).app z = uncurry ((ihom.ev y).app ((ihom x).obj z))
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
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
⊢ (α_ M.X N₁.X Z.X).hom ≫
      M.X ◁ (f.hom ▷ Z.X ≫ N₂.actRight) ≫
        colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft))
          WalkingParallelPair.one =
    ((M.X ◁ f.hom) ▷ Z.X ≫
        colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft))
            WalkingParallelPair.one ▷
          Z.X) ≫
      TensorBimod.actRight M N₂

Tactic:
slice_rhs 2 3 => rw [TensorBimod.π_tensor_id_actRight]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
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)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
⊢ (α_ M.X N₁.X Z.X).hom ≫
      M.X ◁ (f.hom ▷ Z.X ≫ N₂.actRight) ≫
        colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft))
          WalkingParallelPair.one =
    (M.X ◁ f.hom) ▷ Z.X ≫
      (α_ M.X N₂.X Z.X).hom ≫
        M.X ◁ N₂.actRight ≫ coequalizer.π (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)
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
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
⊢ (α_ M.X N₁.X Z.X).hom ≫
      M.X ◁ (f.hom ▷ Z.X ≫ N₂.actRight) ≫
        colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft))
          WalkingParallelPair.one =
    (M.X ◁ f.hom) ▷ Z.X ≫
      (α_ M.X N₂.X Z.X).hom ≫
        M.X ◁ N₂.actRight ≫ coequalizer.π (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)

Tactic:
simp

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
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
⊢ (α_ M₁.X Y.X N.X).hom ≫ f.hom ▷ (Y.X ⊗ N.X) ≫ M₂.X ◁ N.actLeft =
    f.hom ▷ Y.X ▷ N.X ≫ (α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft

Tactic:
simp

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

Goal state before:
pp: C✝ : Type u₁
inst✝⁹ : Category.{v₁, u₁} C✝
inst✝⁸ : MonoidalCategory C✝
inst✝⁷ : BraidedCategory C✝
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : MonoidalCategory C
inst✝⁴ : SymmetricCategory C
A B : C
inst✝³ : ComonObj A
inst✝² : ComonObj B
inst✝¹ : IsCommComonObj A
inst✝ : IsCommComonObj B
⊢ (Δ ⊗ₘ Δ) ≫ ((β_ A A).hom ⊗ₘ (β_ B B).hom) ≫ tensorμ A A B B = (Δ ⊗ₘ Δ) ≫ tensorμ A A B B

Tactic:
simp

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
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
⊢ (α_ X.X M₁.X N.X).inv ≫
      (X.X ◁ f.hom ≫ M₂.actLeft) ▷ N.X ≫
        colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft))
          WalkingParallelPair.one =
    (((α_ X.X M₁.X N.X).inv ≫ (X.X ◁ f.hom) ▷ N.X) ≫ M₂.actLeft ▷ N.X) ≫
      coequalizer.π (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
M N : C
inst✝¹ : ComonObj M
inst✝ : MonObj N
f g h : Conv M N
⊢ Δ ≫ Δ ▷ M ≫ f ▷ M ▷ M ≫ (α_ N M M).hom ≫ N ◁ g ▷ M ≫ (α_ N N M).inv ≫ ((N ⊗ N) ◁ h ≫ μ ▷ N) ≫ μ =
    Δ ≫ ((((M ◁ Δ ≫ f ▷ (M ⊗ M)) ≫ N ◁ g ▷ M) ≫ N ◁ N ◁ h) ≫ N ◁ μ) ≫ μ

Tactic:
simp

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
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
⊢ (α_ M₁.X N.X Z.X).hom ≫
      (f.hom ▷ (N.X ⊗ Z.X) ≫ M₂.X ◁ N.actRight) ≫
        colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft))
          WalkingParallelPair.one =
    (f.hom ▷ N.X ▷ Z.X ≫
        colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft))
            WalkingParallelPair.one ▷
          Z.X) ≫
      TensorBimod.actRight M₂ N

Tactic:
slice_rhs 2 3 => rw [TensorBimod.π_tensor_id_actRight]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
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)
X Y Z : Mon C
M₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
⊢ (α_ M₁.X N.X Z.X).hom ≫
      (f.hom ▷ (N.X ⊗ Z.X) ≫ M₂.X ◁ N.actRight) ≫
        colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft))
          WalkingParallelPair.one =
    f.hom ▷ N.X ▷ Z.X ≫
      (α_ M₂.X N.X Z.X).hom ≫
        M₂.X ◁ N.actRight ≫ coequalizer.π (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft)
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
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
⊢ (α_ M₁.X N.X Z.X).hom ≫
      (f.hom ▷ (N.X ⊗ Z.X) ≫ M₂.X ◁ N.actRight) ≫
        colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft))
          WalkingParallelPair.one =
    f.hom ▷ N.X ▷ Z.X ≫
      (α_ M₂.X N.X Z.X).hom ≫
        M₂.X ◁ N.actRight ≫ coequalizer.π (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
inst✝⁵ : MonoidalCategory V
inst✝⁴ : BraidedCategory V
F G H : C ⥤ V
η : F ⟶ G
inst✝³ : DayConvolution F H
inst✝² : DayConvolution H F
inst✝¹ : DayConvolution G H
inst✝ : DayConvolution H G
fst✝ snd✝ : C
⊢ (unit H F ≫ (tensor C).whiskerLeft (map (𝟙 H) η ≫ (braiding H G).hom)).app (fst✝, snd✝) =
    (unit H F ≫ (tensor C).whiskerLeft ((braiding H F).hom ≫ map η (𝟙 H))).app (fst✝, snd✝)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
inst✝⁵ : MonoidalCategory V
inst✝⁴ : BraidedCategory V
F G : C ⥤ V
η : F ⟶ G
H : C ⥤ V
inst✝³ : DayConvolution F H
inst✝² : DayConvolution H F
inst✝¹ : DayConvolution G H
inst✝ : DayConvolution H G
fst✝ snd✝ : C
⊢ (unit F H ≫ (tensor C).whiskerLeft (map η (𝟙 H) ≫ (braiding G H).hom)).app (fst✝, snd✝) =
    (unit F H ≫ (tensor C).whiskerLeft ((braiding F H).hom ≫ map (𝟙 H) η)).app (fst✝, snd✝)

Tactic:
simp

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
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
⊢ (α_ (P.X ⊗ S.X) Q.X L.X).hom ≫
      (α_ P.X S.X (Q.X ⊗ L.X)).hom ≫
        (P.X ◁ (α_ S.X Q.X L.X).inv ≫
            P.X ◁ (Q.actLeft ▷ L.X ≫ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))) ≫
          coequalizer.π (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))
            ((α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))).hom ≫
              P.X ◁ TensorBimod.actLeft Q L) =
    ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      (α_ P.X Q.X L.X).hom ≫
        P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
          coequalizer.π (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))
            ((α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))).hom ≫
              P.X ◁ TensorBimod.actLeft Q L)

Tactic:
simp

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

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
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j j' : C
φ : j ⟶ j'
this :
  (MonoidalClosed.pre (F.map φ)).app (G.obj (j' ⊗ c)) ≫ (ihom (F.obj j)).map (f.app (j' ⊗ c)) =
    (ihom (F.obj j')).map (f.app (j' ⊗ c)) ≫ (MonoidalClosed.pre (F.map φ)).app (G'.obj (j' ⊗ c))
⊢ ℌ.π c j' ≫ (MonoidalClosed.pre (F.map φ)).app (G.obj (j' ⊗ c)) ≫ (ihom (F.obj j)).map (f.app (j' ⊗ c)) =
    (ℌ.π c j' ≫ (ihom (F.obj j')).map (f.app (j' ⊗ c))) ≫ (MonoidalClosed.pre (F.map φ)).app (G'.obj (j' ⊗ c))

Tactic:
simp

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

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
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f✝ : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
⊢ ∀ (j : (multicospanShapeEnd C).L),
    (H.map f ≫
          Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
            (fun j ↦ ℌ.π c' j ≫ ((((dayConvolutionInternalHomDiagramFunctor F).map f✝).app c').app (op j)).app j) ⋯) ≫
        Multifork.ι (Wedge.mk (H'.obj c') (ℌ'.π c') ⋯) j =
      (Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
            (fun j ↦ ℌ.π c j ≫ ((((dayConvolutionInternalHomDiagramFunctor F).map f✝).app c).app (op j)).app j) ⋯ ≫
          H'.map f) ≫
        Multifork.ι (Wedge.mk (H'.obj c') (ℌ'.π c') ⋯) j

Tactic:
intro j

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f✝ : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
j : (multicospanShapeEnd C).L
⊢ (H.map f ≫
        Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
          (fun j ↦ ℌ.π c' j ≫ ((((dayConvolutionInternalHomDiagramFunctor F).map f✝).app c').app (op j)).app j) ⋯) ≫
      Multifork.ι (Wedge.mk (H'.obj c') (ℌ'.π c') ⋯) j =
    (Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
          (fun j ↦ ℌ.π c j ≫ ((((dayConvolutionInternalHomDiagramFunctor F).map f✝).app c).app (op j)).app j) ⋯ ≫
        H'.map f) ≫
      Multifork.ι (Wedge.mk (H'.obj c') (ℌ'.π c') ⋯) j