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
G' H' : C ⥤ V
ℌ' : DayConvolutionInternalHom F G' H'
inst✝ : DayConvolution F H'
η : G ⟶ G'
⊢ (DayConvolution.corepresentableBy F H).homEquiv (DayConvolution.map (𝟙 F) (ℌ.map η ℌ') ≫ ℌ'.ev_app) =
    (DayConvolution.corepresentableBy F H).homEquiv (ℌ.ev_app ≫ η)

Tactic:
ext ⟨x, y⟩

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
inst✝¹ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
ℌ' : DayConvolutionInternalHom F G' H'
inst✝ : DayConvolution F H'
η : G ⟶ G'
x y : C
⊢ ((DayConvolution.corepresentableBy F H).homEquiv (DayConvolution.map (𝟙 F) (ℌ.map η ℌ') ≫ ℌ'.ev_app)).app (x, y) =
    ((DayConvolution.corepresentableBy F H).homEquiv (ℌ.ev_app ≫ η)).app (x, y)
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 G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' c'' : C
f : c' ⟶ c''
this :
  MonoidalClosed.curry (F.map f ▷ G.obj c ≫ (DayConvolution.unit F G).app (c'', c)) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c) ≫ (F ⊛ G).map (f ▷ c))
⊢ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c)) ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj (F ⊛ G)).obj c).obj (op c')).map f =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (c'', c)) ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj (F ⊛ G)).obj c).map f.op).app c''

Tactic:
simp only [MonoidalClosed.curry_natural_right] at this

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 G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' c'' : C
f : c' ⟶ c''
this :
  MonoidalClosed.curry (F.map f ▷ G.obj c) ≫ (ihom (F.obj c')).map ((DayConvolution.unit F G).app (c'', c)) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c)) ≫ (ihom (F.obj c')).map ((F ⊛ G).map (f ▷ c))
⊢ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c)) ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj (F ⊛ G)).obj c).obj (op c')).map f =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (c'', c)) ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj (F ⊛ G)).obj c).map f.op).app c''
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 G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' : C
f : c ⟶ c'
j : C
this :
  MonoidalClosed.curry (F.obj j ◁ G.map f ≫ (DayConvolution.unit F G).app (j, c')) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c) ≫ (F ⊛ G).map (j ◁ f))
⊢ G.map f ≫ MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c')) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c)) ≫ (ihom (F.obj j)).map ((F ⊛ G).map (j ◁ f))

Tactic:
simp only [MonoidalClosed.curry_natural_right] at this

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 G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' : C
f : c ⟶ c'
j : C
this :
  MonoidalClosed.curry (F.obj j ◁ G.map f) ≫ (ihom (F.obj j)).map ((DayConvolution.unit F G).app (j, c')) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c)) ≫ (ihom (F.obj j)).map ((F ⊛ G).map (j ◁ f))
⊢ G.map f ≫ MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c')) =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c)) ≫ (ihom (F.obj j)).map ((F ⊛ G).map (j ◁ f))
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✝⁴ : SymmetricCategory C
inst✝³ : MonoidalCategory V
inst✝² : SymmetricCategory V
F G : C ⥤ V
inst✝¹ : DayConvolution F G
inst✝ : DayConvolution G F
⊢ unit F G ≫ (tensor C).whiskerLeft ((braiding F G).hom ≫ (braiding G F).hom) =
    unit F G ≫ (tensor C).whiskerLeft (𝟙 (F ⊛ G))

Tactic:
ext ⟨x, y⟩

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁶ : Category.{v₂, u₂} V
inst✝⁵ : MonoidalCategory C
inst✝⁴ : SymmetricCategory C
inst✝³ : MonoidalCategory V
inst✝² : SymmetricCategory V
F G : C ⥤ V
inst✝¹ : DayConvolution F G
inst✝ : DayConvolution G F
x y : C
⊢ (unit F G ≫ (tensor C).whiskerLeft ((braiding F G).hom ≫ (braiding G F).hom)).app (x, y) =
    (unit F G ≫ (tensor C).whiskerLeft (𝟙 (F ⊛ G))).app (x, y)
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor

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
hasDayConvolution : ∀ (F G : C ⥤ V), (tensor C).HasPointwiseLeftKanExtension (F ⊠ G)
hasDayConvolutionUnit : (Functor.fromPUnit (𝟙_ C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (𝟙_ V))
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)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
F G H : C ⊛⥤ V
α β : F ⊗ G ⟶ H
h : ∀ (x y : C), (F.η G).app (x, y) ≫ α.natTrans.app (x ⊗ y) = (F.η G).app (x, y) ≫ β.natTrans.app (x ⊗ y)
⊢ F.η G ≫ (tensor C).whiskerLeft α.natTrans = F.η G ≫ (tensor C).whiskerLeft β.natTrans

Tactic:
ext ⟨x, y⟩

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
hasDayConvolution : ∀ (F G : C ⥤ V), (tensor C).HasPointwiseLeftKanExtension (F ⊠ G)
hasDayConvolutionUnit : (Functor.fromPUnit (𝟙_ C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (𝟙_ V))
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)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
F G H : C ⊛⥤ V
α β : F ⊗ G ⟶ H
h : ∀ (x y : C), (F.η G).app (x, y) ≫ α.natTrans.app (x ⊗ y) = (F.η G).app (x, y) ≫ β.natTrans.app (x ⊗ y)
x y : C
⊢ (F.η G ≫ (tensor C).whiskerLeft α.natTrans).app (x, y) = (F.η G ≫ (tensor C).whiskerLeft β.natTrans).app (x, y)
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
inst✝ : DayConvolution F H
⊢ (DayConvolution.corepresentableBy F G).homEquiv (DayConvolution.map (𝟙 F) ℌ.coev_app ≫ ℌ.ev_app) =
    (DayConvolution.corepresentableBy F G).homEquiv (𝟙 (F ⊛ G))

Tactic:
ext ⟨x, y⟩

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
inst✝ : DayConvolution F H
x y : C
⊢ ((DayConvolution.corepresentableBy F G).homEquiv (DayConvolution.map (𝟙 F) ℌ.coev_app ≫ ℌ.ev_app)).app (x, y) =
    ((DayConvolution.corepresentableBy F G).homEquiv (𝟙 (F ⊛ G))).app (x, y)
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).hom ≫ A ◁ Δ ▷ A) ≫ A ◁ (α_ A A A).hom) ≫ A ◁ A ◁ (𝒮 ⊗ₘ 𝒮)) ≫ A ◁ (α_ A A A).inv) ≫
              A ◁ μ ▷ A) ≫
            A ◁ μ) ≫
          μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
rw [tensorHom_def']

Goal state after:
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).hom ≫ A ◁ Δ ▷ A) ≫ A ◁ (α_ A A A).hom) ≫ A ◁ A ◁ (A ◁ 𝒮 ≫ 𝒮 ▷ A)) ≫ A ◁ (α_ A A A).inv) ≫
              A ◁ μ ▷ A) ≫
            A ◁ μ) ≫
          μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
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
⊢ ((α_ 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)) ≫
      coequalizer.desc
        ((PreservesCoequalizer.iso (tensorLeft P.X) (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)).inv ≫
          coequalizer.desc
            ((α_ P.X Q.X L.X).inv ≫
              coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
                coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
                  ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ L.actLeft))
            ⋯)
        ⋯ =
    coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
          ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft) ≫
        𝟙 (TensorBimod.X (P.tensorBimod Q) L)

Tactic:
slice_lhs 3 4 => rw [coequalizer.π_desc]

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
⊢ (α_ 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) ≫
        (PreservesCoequalizer.iso (tensorLeft P.X) (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)).inv ≫
          coequalizer.desc
            ((α_ P.X Q.X L.X).inv ≫
              coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
                coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
                  ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ L.actLeft))
            ⋯ =
    coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
          ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft) ≫
        𝟙 (TensorBimod.X (P.tensorBimod Q) L)
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:
dsimp only [Cofork.π]

Goal state after:
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₂)
⊢ (c₁.mapBifunctor c₂ (curriedTensor C)).ι.app WalkingParallelPair.one ≫
      (Iso.refl (c₁.mapBifunctor c₂ (curriedTensor C)).pt).hom =
    (c₁.tensor c₂).ι.app WalkingParallelPair.one
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
⊢ ((α_ P.X Q.X L.X).inv ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
          coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
            ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ L.actLeft)) ≫
      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))
            ⋯)
        ⋯ =
    P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
      coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X)
          ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft) ≫
        𝟙 (TensorBimod.X P (Q.tensorBimod L))

Tactic:
slice_lhs 3 4 => rw [coequalizer.π_desc]

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
⊢ (α_ P.X Q.X L.X).inv ≫
      coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ 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))
            ⋯ =
    P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
      coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X)
          ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft) ≫
        𝟙 (TensorBimod.X P (Q.tensorBimod L))
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:
dsimp [hom, homAux, inv, invAux]
  apply coequalizer.hom_ext
  slice_lhs 1 2 => rw [coequalizer.π_desc]
  refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_
  simp only [curriedTensor_obj_map]
  slice_lhs 1 3 => rw [id_tensor_π_preserves_coequalizer_inv_desc]
  slice_lhs 3 4 => rw [coequalizer.π_desc]
  slice_lhs 2 4 => rw [π_tensor_id_preserves_coequalizer_inv_desc]
  slice_lhs 1 3 => rw [Iso.inv_hom_id_assoc]
  dsimp only [TensorBimod.X]
  slice_rhs 2 3 => rw [Category.comp_id]
  rfl

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
⊢ ((λ_ P.X).inv ≫
        η ▷ P.X ≫
          coequalizer.π ((regular R).actRight ▷ P.X) ((α_ (regular R).X R.X P.X).hom ≫ (regular R).X ◁ P.actLeft)) ≫
      coequalizer.desc P.actLeft ⋯ =
    𝟙 P.X

Tactic:
slice_lhs 3 4 => rw [coequalizer.π_desc]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ (λ_ P.X).inv ≫ η ▷ P.X ≫ P.actLeft = 𝟙 P.X
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
⊢ ((ρ_ P.X).inv ≫
        P.X ◁ η ≫
          coequalizer.π (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft)) ≫
      coequalizer.desc P.actRight ⋯ =
    𝟙 P.X

Tactic:
slice_lhs 3 4 => rw [coequalizer.π_desc]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ (ρ_ P.X).inv ≫ P.X ◁ η ≫ P.actRight = 𝟙 P.X
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ 𝟙 Y ⊗≫ (η_ X Y ▷ Y ≫ (β_ (X ⊗ Y) Y).hom) ⊗≫ ((β_ Y (Y ⊗ X)).inv ≫ Y ◁ ε_ X Y) ⊗≫ 𝟙 Y = 𝟙 Y

Tactic:
braiding_naturality_left,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ 𝟙 Y ⊗≫ ((β_ (𝟙_ C) Y).hom ≫ Y ◁ η_ X Y) ⊗≫ ((β_ Y (Y ⊗ X)).inv ≫ Y ◁ ε_ X Y) ⊗≫ 𝟙 Y = 𝟙 Y
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
D : Type u₃
inst✝² : Category.{v₃, u₃} D
inst✝¹ : MonoidalCategoryStruct D
inst✝ : LawfulDayConvolutionMonoidalCategoryStruct C V D
d₁ d₂ d₁' d₂' : D
f : d₁ ⟶ d₂
f' : d₁' ⟶ d₂'
⊢ (DayConvolution.corepresentableBy ((ι C V D).obj d₁) ((ι C V D).obj d₁')).homEquiv ((ι C V D).map (f ⊗ₘ f')) =
    (DayConvolution.corepresentableBy ((ι C V D).obj d₁) ((ι C V D).obj d₁')).homEquiv
      (DayConvolution.map ((ι C V D).map f) ((ι C V D).map f'))

Tactic:
ext ⟨x, y⟩

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
D : Type u₃
inst✝² : Category.{v₃, u₃} D
inst✝¹ : MonoidalCategoryStruct D
inst✝ : LawfulDayConvolutionMonoidalCategoryStruct C V D
d₁ d₂ d₁' d₂' : D
f : d₁ ⟶ d₂
f' : d₁' ⟶ d₂'
x y : C
⊢ ((DayConvolution.corepresentableBy ((ι C V D).obj d₁) ((ι C V D).obj d₁')).homEquiv ((ι C V D).map (f ⊗ₘ f'))).app
      (x, y) =
    ((DayConvolution.corepresentableBy ((ι C V D).obj d₁) ((ι C V D).obj d₁')).homEquiv
          (DayConvolution.map ((ι C V D).map f) ((ι C V D).map f'))).app
      (x, y)
Module: Mathlib.CategoryTheory.ObjectProperty.Ind

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
ι : Type u_1
inst✝³ : Small.{w, u_1} ι
inst✝² : P.IsClosedUnderLimitsOfShape (Discrete ι)
inst✝¹ : HasProductsOfShape ι C
inst✝ : IsIPCOfShape.{w, u_1, v, u} ι C
X : C
x✝ : P.ind.strictLimitsOfShape (Discrete ι) X
Y : Discrete ι ⥤ C
h : ∀ (j : Discrete ι), P.ind (Y.obj j)
e : ι ≃ Shrink.{w, u_1} ι := equivShrink ι
this✝¹ : HasProductsOfShape (Shrink.{w, u_1} ι) C
this✝ : IsIPCOfShape.{w, w, v, u} (Shrink.{w, u_1} ι) C
this : P.IsClosedUnderLimitsOfShape (Discrete (Shrink.{w, u_1} ι))
⊢ P.ind (limit Y)

Tactic:
let iso : limit Y ≅ ∏ᶜ fun i ↦ Y.obj ⟨e.symm i⟩ :=
    (Pi.isoLimit _).symm ≪≫ (Pi.reindex e.symm _).symm

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
ι : Type u_1
inst✝³ : Small.{w, u_1} ι
inst✝² : P.IsClosedUnderLimitsOfShape (Discrete ι)
inst✝¹ : HasProductsOfShape ι C
inst✝ : IsIPCOfShape.{w, u_1, v, u} ι C
X : C
x✝ : P.ind.strictLimitsOfShape (Discrete ι) X
Y : Discrete ι ⥤ C
h : ∀ (j : Discrete ι), P.ind (Y.obj j)
e : ι ≃ Shrink.{w, u_1} ι := equivShrink ι
this✝¹ : HasProductsOfShape (Shrink.{w, u_1} ι) C
this✝ : IsIPCOfShape.{w, w, v, u} (Shrink.{w, u_1} ι) C
this : P.IsClosedUnderLimitsOfShape (Discrete (Shrink.{w, u_1} ι))
iso : limit Y ≅ ∏ᶜ fun i ↦ Y.obj { as := e.symm i } :=
  (Pi.isoLimit Y).symm ≪≫ (Pi.reindex e.symm fun j ↦ Y.obj { as := j }).symm
⊢ P.ind (limit Y)