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

Goal state before:
pp: case mk.α_hom
C : Type u
X Y X✝ Y✝ Z✝ : F C
⊢ (fun n ↦ ((X✝.tensor Y✝).tensor Z✝).normalizeObj n) = (X✝.tensor (Y✝.tensor Z✝)).normalizeObj

Tactic:
funext; rfl

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

Goal state before:
pp: case mk.α_inv
C : Type u
X Y X✝ Y✝ Z✝ : F C
⊢ (fun n ↦ (X✝.tensor (Y✝.tensor Z✝)).normalizeObj n) = ((X✝.tensor Y✝).tensor Z✝).normalizeObj

Tactic:
funext; rfl

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

Goal state before:
pp: case mk.l_hom
C : Type u
X Y X✝ : F C
⊢ (fun n ↦ (unit.tensor X✝).normalizeObj n) = X✝.normalizeObj

Tactic:
funext; rfl

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

Goal state before:
pp: case mk.l_inv
C : Type u
X Y X✝ : F C
⊢ (fun n ↦ X✝.normalizeObj n) = (unit.tensor X✝).normalizeObj

Tactic:
funext; rfl

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

Goal state before:
pp: case mk.ρ_hom
C : Type u
X Y X✝ : F C
⊢ (fun n ↦ (X✝.tensor unit).normalizeObj n) = X✝.normalizeObj

Tactic:
funext; rfl

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

Goal state before:
pp: case mk.ρ_inv
C : Type u
X Y X✝ : F C
⊢ (fun n ↦ X✝.normalizeObj n) = (X✝.tensor unit).normalizeObj

Tactic:
funext; rfl

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
A B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
⊢ f ≫ 𝒮 = 𝒮 ≫ f

Tactic:
apply left_inv_eq_right_inv
    (M := Conv A B)
    (a := f)
  · rw [Conv.mul_eq, Conv.one_eq]
    simp only [comp_whiskerRight, Category.assoc]
    slice_lhs 3 4 =>
      rw [← whisker_exchange]
    slice_lhs 2 3 =>
      rw [← tensorHom_def]
    slice_lhs 1 2 =>
      rw [← IsComonHom.hom_comul f]
    slice_lhs 2 4 =>
      rw [antipode_left]
    slice_lhs 1 2 =>
      rw [IsComonHom.hom_counit]
  · rw [Conv.mul_eq, Conv.one_eq]
    simp only [whiskerLeft_comp, Category.assoc]
    slice_lhs 2 3 =>
      rw [← whisker_exchange]
    slice_lhs 3 4 =>
      rw [← tensorHom_def]
    slice_lhs 3 4 =>
      rw [← IsMonHom.mul_hom]
    slice_lhs 1 3 =>
      rw [antipode_right]
    slice_lhs 2 3 =>
      rw [IsMonHom.one_hom]

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
⊢ coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
        ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ 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))
              ⋯)
          ⋯ ≫
        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.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 1 2 => 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
⊢ ((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))
          ⋯) ≫
      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.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.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
⊢ coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X)
        ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft) ≫
      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.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))
              ⋯)
          ⋯ =
    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 1 2 => 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
⊢ ((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.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))
            ⋯)
        ⋯ =
    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.Limits.Cokernels

Goal state before:
pp: case h₂
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.inr ≫ coprod.desc (f₁ ▷ Y₂) (Y₁ ◁ f₂) ≫ (Cofork.π c₁ ⊗ₘ Cofork.π c₂) = coprod.inr ≫ 0

Tactic:
simp [tensorHom_def', ← whiskerLeft_comp_assoc, coprod.inr_desc]

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

Goal state before:
pp: case a.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) ≫ coequalizer.desc P.actLeft ⋯

pp: case a.a.a
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

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
| η ▷ P.X

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
| coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)

Tactic:
rw [coequalizer.π_desc]

Goal state after:
case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| P.actLeft

case a.a.a
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

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
| η ▷ P.X

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

Tactic:
slice_lhs 1 2 => 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.actLeft ≫ (λ_ P.X).inv) ≫ η ▷ P.X) ≫ coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) =
    coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫
      𝟙 (coequalizer (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft))
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
⊢ (λ_ (R.X ⊗ P.X)).inv ≫
      (α_ (𝟙_ C) R.X P.X).inv ≫ (λ_ R.X).hom ▷ P.X ≫ coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) =
    coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫
      𝟙 (coequalizer (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft))

Tactic:
slice_rhs 1 2 => rw [Category.comp_id]

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

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
| η ▷ P.X

Tactic:
rw [coequalizer.π_desc]

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
| 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
| (λ_ P.X).inv

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
| η ▷ P.X
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.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.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫ coequalizer.desc P.actRight ⋯

pp: case a.a.a
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

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
| P.X ◁ η

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
| coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)

Tactic:
rw [coequalizer.π_desc]

Goal state after:
case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
| P.actRight

case a.a.a
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

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
| P.X ◁ η

case 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.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ 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
⊢ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫
      coequalizer.desc P.actRight ⋯ ≫
        (ρ_ P.X).inv ≫ P.X ◁ η ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ))

Tactic:
slice_lhs 1 2 => 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.actRight ≫ (ρ_ P.X).inv) ≫ P.X ◁ η) ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ 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 ⊗ S.X)).inv ≫
      (α_ P.X S.X (𝟙_ C)).hom ≫ P.X ◁ (ρ_ S.X).hom ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ))

Tactic:
slice_rhs 1 2 => rw [Category.comp_id]

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 ⊗ S.X)).inv ≫
      (α_ P.X S.X (𝟙_ C)).hom ≫ P.X ◁ (ρ_ S.X).hom ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)
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
| coequalizer.π (P.actRight ▷ (regular S).X) ((α_ P.X S.X (regular S).X).hom ≫ P.X ◁ (regular S).actLeft) ≫
    coequalizer.desc P.actRight ⋯

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
| (ρ_ P.X).inv

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
| P.X ◁ η

Tactic:
rw [coequalizer.π_desc]

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
| P.actRight

case a
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

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
| 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:
rw [braiding_naturality_left, ← braiding_inv_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) ⊗≫ (ε_ X Y ▷ Y ≫ (β_ Y (𝟙_ C)).inv) ⊗≫ 𝟙 Y = 𝟙 Y
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
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 : Mon C
M N : Bimod X Y
f : M ⟶ N
| coequalizer.π (μ ▷ M.X) ((α_ X.X X.X M.X).hom ≫ X.X ◁ M.actLeft) ≫ coequalizer.desc M.actLeft ⋯

pp: case a.a
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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| f.hom

pp: case a
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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| LeftUnitorBimod.inv N

Tactic:
rw [coequalizer.π_desc]

Goal state after:
case a.a
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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| M.actLeft

case a.a
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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| f.hom

case a
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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| LeftUnitorBimod.inv N
Module: Mathlib.CategoryTheory.Presentable.Dense

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalAccessibleCategory C κ
X : C
⊢ IsCardinalFiltered (CostructuredArrow (isCardinalPresentable C κ).ι X) κ

Tactic:
obtain ⟨J, _, _, ⟨p⟩⟩ :=
    (isCardinalFilteredGenerator_isCardinalPresentable C κ).exists_colimitsOfShape X
  exact IsCardinalFiltered.of_final p.toCostructuredArrow κ

Goal state after: