mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C × C
f : x ⟶ y
this :
  F.obj x.1 ◁ ℌ.π x.2 x.1 ≫ F.obj x.1 ◁ (ihom (F.obj x.1)).map (G.map (f.1 ▷ x.2)) =
    F.obj x.1 ◁ ℌ.π x.2 y.1 ≫ F.obj x.1 ◁ (MonoidalClosed.pre (F.map f.1)).app (G.obj (y.1 ⊗ x.2))
⊢ F.obj x.1 ◁ ℌ.π x.2 y.1 ≫
      F.map f.1 ▷ (ihom (F.obj y.1)).obj (G.obj (y.1 ⊗ x.2)) ≫
        (ihom.ev (F.obj y.1)).app (G.obj (y.1 ⊗ x.2)) ≫ G.map (y.1 ◁ f.2) =
    F.obj x.1 ◁ ℌ.π x.2 y.1 ≫
      F.obj x.1 ◁ (MonoidalClosed.pre (F.map f.1)).app (G.obj (y.1 ⊗ x.2)) ≫
        (ihom.ev (F.obj x.1)).app (G.obj (y.1 ⊗ x.2)) ≫ G.map (y.1 ◁ f.2)

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 Q.X T.X).hom ▷ L.X ≫
      (α_ P.X (Q.X ⊗ T.X) L.X).hom ≫
        ((P.X ◁ (α_ Q.X T.X L.X).hom ≫ P.X ◁ Q.X ◁ L.actLeft) ≫
            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) =
    (α_ (P.X ⊗ Q.X) T.X L.X).hom ≫
      (P.X ⊗ Q.X) ◁ L.actLeft ≫
        (α_ 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 H G : C ⥤ V
inst✝¹ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
G' H' : C ⥤ V
inst✝ : DayConvolution F G'
η : G ⟶ G'
ℌ' : DayConvolutionInternalHom F (F ⊛ G') H'
c : C
⊢ ∀ (j : (multicospanShapeEnd C).L),
    (η.app c ≫ ℌ'.coev_app.app c) ≫ Multifork.ι (Wedge.mk (H'.obj c) (ℌ'.π c) ⋯) j =
      (ℌ.coev_app.app c ≫ (ℌ.map (DayConvolution.map (𝟙 F) η) ℌ').app c) ≫
        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 H G : C ⥤ V
inst✝¹ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
G' H' : C ⥤ V
inst✝ : DayConvolution F G'
η : G ⟶ G'
ℌ' : DayConvolutionInternalHom F (F ⊛ G') H'
c : C
j : (multicospanShapeEnd C).L
⊢ (η.app c ≫ ℌ'.coev_app.app c) ≫ Multifork.ι (Wedge.mk (H'.obj c) (ℌ'.π c) ⋯) j =
    (ℌ.coev_app.app c ≫ (ℌ.map (DayConvolution.map (𝟙 F) η) ℌ').app c) ≫ Multifork.ι (Wedge.mk (H'.obj c) (ℌ'.π c) ⋯) j
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 H G : C ⥤ V
inst✝ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
H' : C ⥤ V
ℌ' : DayConvolutionInternalHom F (F ⊛ H) H'
c : C
⊢ ∀ (j : (multicospanShapeEnd C).L),
    (ℌ'.coev_app ≫ ℌ'.map ℌ.ev_app ℌ).app c ≫ Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j =
      (𝟙 H).app c ≫ 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 H G : C ⥤ V
inst✝ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
H' : C ⥤ V
ℌ' : DayConvolutionInternalHom F (F ⊛ H) H'
c : C
j : (multicospanShapeEnd C).L
⊢ (ℌ'.coev_app ≫ ℌ'.map ℌ.ev_app ℌ).app c ≫ Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j =
    (𝟙 H).app c ≫ Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case mk.mk
C : Type u
Z : F C
as✝ : NormalMonoidalObject C
⊢ ((tensorFunc C).obj Z).map { down := { down := ⋯ } } = inclusion.map { down := { down := ⋯ } } ▷ Z

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X Y : F C
n : (Discrete ∘ NormalMonoidalObject) C
⊢ (α_ (inclusion.obj { as := n.as }) X Y).symm ≪≫
      normalizeIsoApp' C X n.as ▷ᵢ Y ≪≫ normalizeIsoApp' C Y { as := X.normalizeObj n.as }.as =
    (α_ (inclusionObj n.as) X Y).symm ≪≫ normalizeIsoApp' C X n.as ▷ᵢ Y ≪≫ normalizeIsoApp' C Y (X.normalizeObj n.as)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X : NormalMonoidalObject C
⊢ (Discrete.functor fun n ↦ inclusionObj n ⊗ X✝).map (𝟙 { as := X }) ≫ (normalizeIsoApp C X✝ { as := X }).hom =
    (normalizeIsoApp C X✝ { as := X }).hom ≫ 𝟙 (inclusionObj (X✝.normalizeObj X))

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
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
⊢ (α_ R.X (P.tensorBimod Q).X L.X).inv ≫
      (P.tensorBimod Q).actLeft ▷ L.X ≫
        (PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫
          coequalizer.desc
            ((α_ 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 ▷ TensorBimod.X Q L)
                  ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L))
            ⋯ =
    R.X ◁
        coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
          ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft) ≫
      R.X ◁
          coequalizer.desc
            ((PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X)
                  ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫
              coequalizer.desc
                ((α_ 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 ▷ TensorBimod.X Q L)
                      ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L))
                ⋯)
            ⋯ ≫
        TensorBimod.actLeft P (Q.tensorBimod L)

Tactic:
slice_rhs 1 2 => rw [← whiskerLeft_comp, coequalizer.π_desc, whiskerLeft_comp]

Goal state after:
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
⊢ (α_ R.X (P.tensorBimod Q).X L.X).inv ≫
      (P.tensorBimod Q).actLeft ▷ L.X ≫
        (PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫
          coequalizer.desc
            ((α_ 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 ▷ TensorBimod.X Q L)
                  ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L))
            ⋯ =
    (R.X ◁
          (PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫
        R.X ◁
          coequalizer.desc
            ((α_ 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 ▷ TensorBimod.X Q L)
                  ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L))
            ⋯) ≫
      TensorBimod.actLeft P (Q.tensorBimod L)
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X✝ Y✝ X' X Y : F C
f : X ⟶ Y
ih :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom = (normalizeIsoApp' C X n).hom ≫ inclusion.map (eqToHom ⋯)
n : NormalMonoidalObject C
⊢ (α_ (inclusionObj n) X' X).inv ≫
      (normalizeIsoApp' C X' n).hom ▷ X ≫ (normalizeIsoApp' C X (X'.normalizeObj n)).hom ≫ inclusion.map (eqToHom ⋯) =
    ((α_ (inclusionObj n) X' X).inv ≫
        (normalizeIsoApp' C X' n).hom ▷ X ≫ (normalizeIsoApp' C X (X'.normalizeObj n)).hom) ≫
      inclusion.map (eqToHom ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case id
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ 𝟙 X✝ ≫ (normalizeIsoApp' C X✝ n).hom = (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case α_hom
C : Type u
X Y X✝ Y✝ Z✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (α_ X✝ Y✝ Z✝).hom ≫ (normalizeIsoApp' C (X✝ ⊗ Y✝ ⊗ Z✝) n).hom =
      (normalizeIsoApp' C ((X✝ ⊗ Y✝) ⊗ Z✝) n).hom ≫ inclusion.map (eqToHom ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case α_inv
C : Type u
X Y X✝ Y✝ Z✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (α_ X✝ Y✝ Z✝).inv ≫ (normalizeIsoApp' C ((X✝ ⊗ Y✝) ⊗ Z✝) n).hom =
      (normalizeIsoApp' C (X✝ ⊗ Y✝ ⊗ Z✝) n).hom ≫ inclusion.map (eqToHom ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case l_hom
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (λ_ X✝).hom ≫ (normalizeIsoApp' C X✝ n).hom =
      (normalizeIsoApp' C (𝟙_ (F C) ⊗ X✝) n).hom ≫ inclusion.map (eqToHom ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case l_inv
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (λ_ X✝).inv ≫ (normalizeIsoApp' C (𝟙_ (F C) ⊗ X✝) n).hom =
      (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case ρ_hom
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (ρ_ X✝).hom ≫ (normalizeIsoApp' C X✝ n).hom =
      (normalizeIsoApp' C (X✝ ⊗ 𝟙_ (F C)) n).hom ≫ inclusion.map (eqToHom ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case ρ_inv
C : Type u
X Y X✝ : F C
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (ρ_ X✝).inv ≫ (normalizeIsoApp' C (X✝ ⊗ 𝟙_ (F C)) n).hom =
      (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case e'_2
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
n : NormalMonoidalObject C
e_1✝ :
  (((tensorFunc C).obj X).obj { as := n } ⟶ ((normalize' C).obj Y).obj { as := n }) =
    (inclusionObj n ⊗ X ⟶ inclusionObj (Y.normalizeObj n))
⊢ inclusionObj n ◁ f ≫ (normalizeIsoApp C Y { as := n }).hom = inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom

Tactic:
normalizeIsoApp_eq

Goal state after:
case e'_2
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
n : NormalMonoidalObject C
e_1✝ :
  (((tensorFunc C).obj X).obj { as := n } ⟶ ((normalize' C).obj Y).obj { as := n }) =
    (inclusionObj n ⊗ X ⟶ inclusionObj (Y.normalizeObj n))
⊢ inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y { as := n }.as).hom = inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y n).hom
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: case e'_3
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
n : NormalMonoidalObject C
e_1✝ :
  (((tensorFunc C).obj X).obj { as := n } ⟶ ((normalize' C).obj Y).obj { as := n }) =
    (inclusionObj n ⊗ X ⟶ inclusionObj (Y.normalizeObj n))
⊢ (normalizeIsoApp C X { as := n }).hom ≫ eqToHom ⋯ = (normalizeIsoApp' C X n).hom ≫ eqToHom ⋯

Tactic:
normalizeIsoApp_eq

Goal state after:
case e'_3
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
n : NormalMonoidalObject C
e_1✝ :
  (((tensorFunc C).obj X).obj { as := n } ⟶ ((normalize' C).obj Y).obj { as := n }) =
    (inclusionObj n ⊗ X ⟶ inclusionObj (Y.normalizeObj n))
⊢ (normalizeIsoApp' C X { as := n }.as).hom ≫ eqToHom ⋯ = (normalizeIsoApp' C X n).hom ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ⊗ₘ Δ) ≫
      (α_ A A (A ⊗ A)).hom ≫
        A ◁ (α_ A A A).inv ≫
          A ◁ (β_ A A).hom ▷ A ≫
            (α_ A (A ⊗ A) A).inv ≫ (α_ A A A).inv ▷ A ≫ (α_ (A ⊗ A) A A).hom ≫ ((μ ⊗ₘ μ) ≫ 𝒮 ▷ A) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

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

Tactic:
simp

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

Goal state before:
pp: case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ Δ ≫ 𝒮 ▷ A ≫ μ ≫ 𝒮 = ε ≫ η

Tactic:
simp

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

Goal state before:
pp: case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ Δ ≫ 𝒮 ▷ A ≫ A ◁ 𝟙 A ≫ μ = ε ≫ η

Tactic:
simp

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

Goal state before:
pp: case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
comm : (β_ A A).hom ≫ μ = μ
⊢ 𝒮 * 𝟙 A = 1

Tactic:
· rw [Conv.mul_eq, Conv.one_eq]
    simp

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:
simp [uniqueUpToIso]

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:
simp [uniqueUpToIso]

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:
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
f : X✝ ⟶ Y✝
g : C
⊢ f ▷ g ≫ (coprod.braiding Y✝ g).hom = (coprod.braiding X✝ g).hom ≫ g ◁ f

Tactic:
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 Z : C
⊢ coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr) ≫
      (coprod.braiding X (Y ⨿ Z)).hom ≫
        coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr) =
    coprod.map (coprod.braiding X Y).hom (𝟙 Z) ≫
      coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr) ≫
        coprod.map (𝟙 Y) (coprod.braiding X Z).hom

Tactic:
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 Z : C
⊢ coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) ≫
      (coprod.braiding (X ⨿ Y) Z).hom ≫
        coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) =
    coprod.map (𝟙 X) (coprod.braiding Y Z).hom ≫
      coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) ≫
        coprod.map (coprod.braiding X Z).hom (𝟙 Y)

Tactic:
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:
simp

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
this :
  F.obj x ◁ (unit G H).app (y, z) ≫
      (unit F (G ⊛ H)).app (x, y ⊗ z) ≫
        ((F ⊛ G ⊛ H).descOfIsLeftKanExtension (unit F (G ⊛ H)) ((F ⊛ G) ⊛ H)
              ((F ⊠ G ⊛ H).descOfIsLeftKanExtension (extensionUnitRight (G ⊛ H) (unit G H) F) (tensor C ⋙ (F ⊛ G) ⊛ H)
                ((NatIso.ofComponents (fun x ↦ (α_ (F.obj x.1) (G.obj x.2.1) (H.obj x.2.2)).symm) ⋯).hom ≫
                  (ConcreteCategory.hom
                        (𝟙
                          (prod.inverseAssociator C C C ⋙ (F ⊠ G) ⊠ H ⟶
                            prod.inverseAssociator C C C ⋙ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ (F ⊛ G) ⊛ H)))
                      ((prod.associativity C C C).congrLeft.fullyFaithfulFunctor.homEquiv
                        ((((F ⊛ G) ⊠ H).homEquivOfIsLeftKanExtension (extensionUnitLeft (F ⊛ G) (unit F G) H)
                            (tensor C ⋙ (F ⊛ G) ⊛ H))
                          ((corepresentableBy (F ⊛ G) H).homEquiv (𝟙 ((F ⊛ G) ⊛ H))))) ≫
                    ((whiskeringLeft (C × C × C) C V).map (NatIso.ofComponents (fun x ↦ α_ x.1 x.2.1 x.2.2) ⋯).hom).app
                      ((F ⊛ G) ⊛ H)))).app
          (x ⊗ y ⊗ z) =
    (α_ (F.obj x) (G.obj y) (H.obj z)).inv ≫
      ((ConcreteCategory.hom
                (𝟙
                  (prod.inverseAssociator C C C ⋙ (F ⊠ G) ⊠ H ⟶
                    prod.inverseAssociator C C C ⋙ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ (F ⊛ G) ⊛ H)))
              ((prod.associativity C C C).congrLeft.fullyFaithfulFunctor.homEquiv
                ((((F ⊛ G) ⊠ H).homEquivOfIsLeftKanExtension (extensionUnitLeft (F ⊛ G) (unit F G) H)
                    (tensor C ⋙ (F ⊛ G) ⊛ H))
                  ((corepresentableBy (F ⊛ G) H).homEquiv (𝟙 ((F ⊛ G) ⊛ H)))))).app
          (x, y, z) ≫
        ((F ⊛ G) ⊛ H).map (α_ x y z).hom
⊢ (α_ (F.obj x) (G.obj y) (H.obj z)).inv ≫
      ((prod.inverseAssociator C C C).whiskerLeft
              ((((F ⊛ G) ⊠ H).homEquivOfIsLeftKanExtension (extensionUnitLeft (F ⊛ G) (unit F G) H)
                  (tensor C ⋙ (F ⊛ G) ⊛ H))
                ((corepresentableBy (F ⊛ G) H).homEquiv (𝟙 ((F ⊛ G) ⊛ H))))).app
          (x, y, z) ≫
        ((F ⊛ G) ⊛ H).map (α_ x y z).hom =
    (α_ (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:
simp

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
⊢ (mopEquiv C).inverse.map (MonObj.one.mop ▷ { unmop := M } ≫ MonObj.mul.mop) =
    (mopEquiv C).inverse.map (λ_ { unmop := M }).hom

Tactic:
simp

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
⊢ (mopEquiv C).inverse.map ({ unmop := M } ◁ MonObj.one.mop ≫ MonObj.mul.mop) =
    (mopEquiv C).inverse.map (ρ_ { unmop := M }).hom

Tactic:
simp

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
⊢ (mopEquiv C).inverse.map (MonObj.mul.mop ▷ { unmop := M } ≫ MonObj.mul.mop) =
    (mopEquiv C).inverse.map
      ((α_ { unmop := M } { unmop := M } { unmop := M }).hom ≫ { unmop := M } ◁ MonObj.mul.mop ≫ MonObj.mul.mop)

Tactic:
simp

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
⊢ (mopEquiv C).functor.map (MonObj.one.unmop ▷ M.unmop ≫ MonObj.mul.unmop) = (mopEquiv C).functor.map (λ_ M.unmop).hom

Tactic:
simp

Goal state after: