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

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| ((α_ A A (𝟙_ C)).inv ≫ (ρ_ (A ⊗ A)).hom) ≫ μ

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ ▷ A

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (A ◁ 𝒮) ▷ A

pp: case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).hom

pp: case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ A ◁ ε

Tactic:
Category.assoc,

Goal state after:
case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A (𝟙_ C)).inv ≫ (ρ_ (A ⊗ A)).hom ≫ μ

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ ▷ A

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (A ◁ 𝒮) ▷ A

case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).hom

case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ A ◁ ε
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

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

Tactic:
Category.assoc,

Goal state after:
J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F G H : J ⥤ C
j : J
| limit.lift (F ⊗ G) { pt := limit F ⊗ limit G, π := { app := fun j ↦ limit.π F j ⊗ₘ limit.π G j, naturality := ⋯ } } ▷
      limit H ≫
    limit.π (F ⊗ G) j ▷ limit H ≫ (F.obj j ⊗ G.obj j) ◁ limit.π H j ≫ (α_ (F.obj j) (G.obj j) (H.obj j)).hom
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

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

Tactic:
Category.assoc,

Goal state after:
J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F G H : J ⥤ C
j : J
| { pt := limit F ⊗ limit G, π := { app := fun j ↦ limit.π F j ⊗ₘ limit.π G j, naturality := ⋯ } }.π.app j ▷ limit H ≫
    (α_ (F.obj j) (G.obj j) (limit H)).hom ≫
      (F.obj j ◁ G.obj j ◁ limit.π H j ≫ (α_ (F.obj j) (G.obj j) (H.obj j)).inv) ≫
        (α_ (F.obj j) (G.obj j) (H.obj j)).hom
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

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

Tactic:
Category.assoc,

Goal state after:
J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F G H : J ⥤ C
j : J
| { pt := limit F ⊗ limit G, π := { app := fun j ↦ limit.π F j ⊗ₘ limit.π G j, naturality := ⋯ } }.π.app j ▷ limit H ≫
    (α_ (F.obj j) (G.obj j) (limit H)).hom ≫
      F.obj j ◁ G.obj j ◁ limit.π H j ≫ (α_ (F.obj j) (G.obj j) (H.obj j)).inv ≫ (α_ (F.obj j) (G.obj j) (H.obj j)).hom
Module: Mathlib.CategoryTheory.Monoidal.Bimod

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

Tactic:
Category.assoc,

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
R S : Mon C
P : Bimod R S
⊢ μ ▷ P.X ≫ P.actLeft = (α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft ≫ P.actLeft
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

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

Tactic:
rw [← assoc]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫
      (β_ X X).hom ▷ Y ≫
        (α_ X X Y).hom ≫
          X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Bimod

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

Tactic:
Category.assoc,

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
R S : Mon C
P : Bimod R S
⊢ P.actRight ▷ S.X ≫ P.actRight = (α_ P.X S.X S.X).hom ≫ P.X ◁ μ ≫ P.actRight
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

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

Tactic:
rw [← assoc]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫
      (α_ X X Y).hom ≫
        X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

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

Tactic:
rw [← assoc]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫
      X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

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

Tactic:
rw [← assoc]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
      (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

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

Tactic:
rw [← assoc]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
        (α_ X Y X).inv) ≫
      (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

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

Tactic:
rw [← assoc]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
          (α_ X Y X).inv) ≫
        (β_ Y X).inv ▷ X) ≫
      (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

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

Tactic:
rw [← assoc]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
            (α_ X Y X).inv) ≫
          (β_ Y X).inv ▷ X) ≫
        (α_ Y X X).hom) ≫
      Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

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

Tactic:
rw [← assoc]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
              (α_ X Y X).inv) ≫
            (β_ Y X).inv ▷ X) ≫
          (α_ Y X X).hom) ≫
        Y ◁ (β_ X X).inv) ≫
      (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

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

Tactic:
rw [← assoc]

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
              (α_ X Y X).inv) ≫
            (β_ Y X).inv ▷ X) ≫
          (α_ Y X X).hom) ≫
        Y ◁ (β_ X X).inv) ≫
      (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
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).hom =
    inv (α_ Y X Y).hom ≫
      inv ((β_ Y X).inv ▷ Y) ≫
        (α_ X Y Y).hom ≫
          X ◁ (β_ Y Y).hom ≫
            (α_ X Y Y).inv ≫
              (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
rw [← assoc]

Goal state after:
case e_g.e_a
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).hom =
    (inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫
      (α_ X Y Y).hom ≫
        X ◁ (β_ Y Y).hom ≫
          (α_ X Y Y).inv ≫
            (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
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).hom =
    (inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫
      (α_ X Y Y).hom ≫
        X ◁ (β_ Y Y).hom ≫
          (α_ X Y Y).inv ≫
            (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
rw [← assoc]

Goal state after:
case e_g.e_a
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).hom =
    ((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫
      X ◁ (β_ Y Y).hom ≫
        (α_ X Y Y).inv ≫
          (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
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).hom =
    ((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫
      X ◁ (β_ Y Y).hom ≫
        (α_ X Y Y).inv ≫
          (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
rw [← assoc]

Goal state after:
case e_g.e_a
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).hom =
    (((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫
      (α_ X Y Y).inv ≫
        (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
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).hom =
    (((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫
      (α_ X Y Y).inv ≫
        (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
rw [← assoc]

Goal state after:
case e_g.e_a
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).hom =
    ((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
      (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
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).hom =
    ((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
      (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
rw [← assoc]

Goal state after:
case e_g.e_a
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).hom =
    (((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
        (β_ X Y).hom ▷ Y) ≫
      (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
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).hom =
    (((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
        (β_ X Y).hom ▷ Y) ≫
      (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
rw [← assoc]

Goal state after:
case e_g.e_a
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).hom =
    ((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
          (β_ X Y).hom ▷ Y) ≫
        (α_ Y X Y).hom) ≫
      Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
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).hom =
    ((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
          (β_ X Y).hom ▷ Y) ≫
        (α_ Y X Y).hom) ≫
      Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
rw [← assoc]

Goal state after:
case e_g.e_a
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).hom =
    (((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
            (β_ X Y).hom ▷ Y) ≫
          (α_ Y X Y).hom) ≫
        Y ◁ (β_ Y X).inv) ≫
      (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
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).hom =
    (((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
            (β_ X Y).hom ▷ Y) ≫
          (α_ Y X Y).hom) ≫
        Y ◁ (β_ Y X).inv) ≫
      (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
rw [← assoc]

Goal state after:
case e_g.e_a
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).hom =
    ((((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
              (β_ X Y).hom ▷ Y) ≫
            (α_ Y X Y).hom) ≫
          Y ◁ (β_ Y X).inv) ≫
        (α_ Y Y X).inv) ≫
      (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
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).hom =
    ((((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
              (β_ X Y).hom ▷ Y) ≫
            (α_ Y X Y).hom) ≫
          Y ◁ (β_ Y X).inv) ≫
        (α_ Y Y X).inv) ≫
      (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
rw [← assoc]

Goal state after:
case e_g.e_a
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).hom =
    (((((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
                (β_ X Y).hom ▷ Y) ≫
              (α_ Y X Y).hom) ≫
            Y ◁ (β_ Y X).inv) ≫
          (α_ Y Y X).inv) ≫
        (β_ Y Y).inv ▷ X) ≫
      (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
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).hom =
    (((((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
                (β_ X Y).hom ▷ Y) ≫
              (α_ Y X Y).hom) ≫
            Y ◁ (β_ Y X).inv) ≫
          (α_ Y Y X).inv) ≫
        (β_ Y Y).inv ▷ X) ≫
      (α_ Y Y X).hom

Tactic:
rw [← assoc]

Goal state after:
case e_g.e_a
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).hom =
    (((((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
                (β_ X Y).hom ▷ Y) ≫
              (α_ Y X Y).hom) ≫
            Y ◁ (β_ Y X).inv) ≫
          (α_ Y Y X).inv) ≫
        (β_ Y Y).inv ▷ X) ≫
      (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P₁ P₂ : MorphismProperty C
κ : Cardinal.{w}
h₁ : P₁.HasCardinalLT κ
h₂ : P₂.HasCardinalLT κ
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT (↑(P₁ ⊔ P₂).toSet) κ

Tactic:
MorphismProperty.toSet_max

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P₁ P₂ : MorphismProperty C
κ : Cardinal.{w}
h₁ : P₁.HasCardinalLT κ
h₂ : P₂.HasCardinalLT κ
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT (↑(P₁.toSet ∪ P₂.toSet)) κ