mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
A'' : Type u₇
B'' : Type u₈
C'' : Type u₉
inst✝⁹ : Category.{v₁, u₁} A
inst✝⁸ : Category.{v₂, u₂} B
inst✝⁷ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
inst✝⁶ : Category.{v₄, u₄} A'
inst✝⁵ : Category.{v₅, u₅} B'
inst✝⁴ : Category.{v₆, u₆} C'
F' : A' ⥤ B'
G' : C' ⥤ B'
inst✝³ : Category.{v₇, u₇} A''
inst✝² : Category.{v₈, u₈} B''
inst✝¹ : Category.{v₉, u₉} C''
F'' : A'' ⥤ B''
G'' : C'' ⥤ B''
ψ ψ' : CatCospanTransform F G F' G'
η : ψ ⟶ ψ'
inst✝ : IsIso η
φ : CatCospanTransform F' G' F'' G''
⊢ inv (η ▷ φ) = inv η ▷ φ

Tactic:
apply IsIso.inv_eq_of_hom_inv_id
  simp [← comp_whiskerRight]

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

Goal state before:
pp: C : Type u
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    Quotient.map₂ Hom.tensor ⋯ f₁ f₂ ≫ Quotient.map₂ Hom.tensor ⋯ g₁ g₂ = Quotient.map₂ Hom.tensor ⋯ (f₁ ≫ g₁) (f₂ ≫ g₂)

Tactic:
rintro ⟨f₁⟩ ⟨f₂⟩ ⟨g₁⟩ ⟨g₂⟩

Goal state after:
case mk.mk.mk.mk
C : Type u
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f₁✝ : X₁ ⟶ Y₁
f₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f₂✝ : X₂ ⟶ Y₂
f₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g₁✝ : Y₁ ⟶ Z₁
g₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g₂✝ : Y₂ ⟶ Z₂
g₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Quotient.map₂ Hom.tensor ⋯ (Quot.mk (⇑(X₁.setoidHom Y₁)) f₁) (Quot.mk (⇑(X₂.setoidHom Y₂)) f₂) ≫
      Quotient.map₂ Hom.tensor ⋯ (Quot.mk (⇑(Y₁.setoidHom Z₁)) g₁) (Quot.mk (⇑(Y₂.setoidHom Z₂)) g₂) =
    Quotient.map₂ Hom.tensor ⋯ (Quot.mk (⇑(X₁.setoidHom Y₁)) f₁ ≫ Quot.mk (⇑(Y₁.setoidHom Z₁)) g₁)
      (Quot.mk (⇑(X₂.setoidHom Y₂)) f₂ ≫ Quot.mk (⇑(Y₂.setoidHom Z₂)) g₂)
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: C : Type u
X₁ X₂ X₃ Y₁ Y₂ Y₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ∀ (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    Quotient.map₂ Hom.tensor ⋯ (Quotient.map₂ Hom.tensor ⋯ f₁ f₂) f₃ ≫
        { hom := ⟦Hom.α_hom Y₁ Y₂ Y₃⟧, inv := ⟦Hom.α_inv Y₁ Y₂ Y₃⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom =
      { hom := ⟦Hom.α_hom X₁ X₂ X₃⟧, inv := ⟦Hom.α_inv X₁ X₂ X₃⟧, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        Quotient.map₂ Hom.tensor ⋯ f₁ (Quotient.map₂ Hom.tensor ⋯ f₂ f₃)

Tactic:
by
    rintro ⟨f₁⟩ ⟨f₂⟩ ⟨f₃⟩
    exact Quotient.sound (associator_naturality _ _ _)

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

Goal state before:
pp: case h.l_hom
C : Type u
motive : {X Y : F C} → (X ⟶ Y) → Prop
X✝ Y : F C
id : ∀ (X : F C), motive (𝟙 X)
α_hom : ∀ (X Y Z : F C), motive (α_ X Y Z).hom
α_inv : ∀ (X Y Z : F C), motive (α_ X Y Z).inv
l_hom : ∀ (X : F C), motive (λ_ X).hom
l_inv : ∀ (X : F C), motive (λ_ X).inv
ρ_hom : ∀ (X : F C), motive (ρ_ X).hom
ρ_inv : ∀ (X : F C), motive (ρ_ X).inv
comp : ∀ {X Y Z : F C} (f : X ⟶ Y) (g : Y ⟶ Z), motive f → motive g → motive (f ≫ g)
whiskerLeft : ∀ (X : F C) {Y Z : F C} (f : Y ⟶ Z), motive f → motive (X ◁ f)
whiskerRight : ∀ {X Y : F C} (f : X ⟶ Y) (Z : F C), motive f → motive (f ▷ Z)
X : F C
⊢ motive ⟦Hom.l_hom X⟧

Tactic:
| l_hom X =>

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

Goal state before:
pp: case ρ_naturality
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝¹ f✝ ▷ 𝟙_ D ≫ (ρ_ (projectObj f✝¹ Y✝)).hom = (ρ_ (projectObj f✝¹ X✝)).hom ≫ projectMapAux f✝¹ f✝

Tactic:
rw [MonoidalCategory.rightUnitor_naturality]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
⊢ F.CoreMonoidal

Tactic:
letI e := Lifting.iso L W G F

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ F.CoreMonoidal
Module: Mathlib.CategoryTheory.MarkovCategory.Positive

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
inst✝¹ : PositiveCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (f ≫ Δ ≫ (inv f ⊗ₘ 𝟙 Y)) ≫ (f ⊗ₘ 𝟙 Y) = (Δ ≫ (𝟙 X ⊗ₘ f)) ≫ (f ⊗ₘ 𝟙 Y)

Tactic:
rw [copy_comp_natural (h := by rw [IsIso.hom_inv_id]; infer_instance)]
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝ : Type u
⊢ (ofTypeFunctor m).map ({ app := fun X ↦ ↾pure, naturality := ⋯ }.app x✝) ≫
      { app := fun X ↦ ↾joinM, naturality := ⋯ }.app x✝ =
    𝟙 ((ofTypeFunctor m).obj ((𝟭 (Type u)).obj x✝))

Tactic:
by ext; exact joinM_map_pure _

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalLeftAction C D
x y : C
f : x ⟶ y
inst✝ : IsIso f
z : D
⊢ inv f ⊵ₗ z ≫ f ⊵ₗ z = 𝟙 (y ⊙ₗ z)

Tactic:
rw [← comp_actionHomLeft, IsIso.inv_hom_id, id_actionHomLeft]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalRightAction C D
x y : D
f : x ⟶ y
inst✝ : IsIso f
z : C
⊢ inv f ⊵ᵣ z ≫ f ⊵ᵣ z = 𝟙 (y ⊙ᵣ z)

Tactic:
rw [← comp_actionHomLeft, IsIso.inv_hom_id, id_actionHomLeft]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y : Arrow C
f : X ⟶ Y
⊢ f ▷ 𝟙_ (Arrow C) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f

Tactic:
refine Arrow.hom_ext _ _ (pushout.hom_ext ?_ (by simp)) (by simp)
  apply (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).hom_ext

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

Goal state before:
pp: case refine_2.refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
hnormal : ∀ (X : C), (monoidHom φ X).range.Normal
h' : (X : C) → (X ⟶ G) → (X ⟶ H) → (X ⟶ H)
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
⊢ yoneda.obj (G ⊗ H) ⟶ yoneda.obj H

Tactic:
refine ⟨fun X ↦ ↾fun x ↦ h' _ (x ≫ fst _ _) (x ≫ snd _ _), fun X Y f ↦ ?_⟩

Goal state after:
case refine_2.refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : CartesianMonoidalCategory C
G H : C
inst✝³ : GrpObj G
inst✝² : GrpObj H
φ : H ⟶ G
inst✝¹ : IsMonHom φ
inst✝ : Mono φ
hnormal : ∀ (X : C), (monoidHom φ X).range.Normal
h' : (X : C) → (X ⟶ G) → (X ⟶ H) → (X ⟶ H)
hh' : ∀ (X : C) (g : X ⟶ G) (h : X ⟶ H), h' X g h ≫ φ = g * h ≫ φ * g⁻¹
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ((yoneda.obj (G ⊗ H)).map f ≫ ↾fun x ↦ h' (Opposite.unop Y) (x ≫ fst G H) (x ≫ snd G H)) =
    (↾fun x ↦ h' (Opposite.unop X) (x ≫ fst G H) (x ≫ snd G H)) ≫ (yoneda.obj H).map f
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
d : D
⊢ ∀ (a : D) (b : C),
    IsIso ((yoneda.map ((pre (adj.unit.app d)).app (R.obj b))).app (Opposite.op a)) ↔
      IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ a)).op).app b)

Tactic:
intro d' c

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
d d' : D
c : C
⊢ IsIso ((yoneda.map ((pre (adj.unit.app d)).app (R.obj c))).app (Opposite.op d')) ↔
    IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (α_ P.X Q.X (T.X ⊗ T.X)).hom ≫
      (P.X ◁ (α_ Q.X T.X T.X).inv ≫ P.X ◁ Q.actRight ▷ T.X ≫ P.X ◁ Q.actRight) ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) =
    (((α_ (P.X ⊗ Q.X) T.X T.X).inv ≫
          coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ T.X ▷ T.X) ≫
        actRight P Q ▷ T.X) ≫
      actRight P Q

Tactic:
slice_rhs 2 3 => rw [← comp_whiskerRight, π_tensor_id_actRight, comp_whiskerRight,
    comp_whiskerRight]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (α_ P.X Q.X (T.X ⊗ T.X)).hom ≫
      (P.X ◁ (α_ Q.X T.X T.X).inv ≫ P.X ◁ Q.actRight ▷ T.X ≫ P.X ◁ Q.actRight) ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) =
    (α_ (P.X ⊗ Q.X) T.X T.X).inv ≫
      ((α_ P.X Q.X T.X).hom ▷ T.X ≫
          (P.X ◁ Q.actRight) ▷ T.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ T.X) ≫
        actRight P Q
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
⊢ (fun f ↦ { app := fun j ↦ end_.lift (fun k ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯, naturality := ⋯ })
      ((fun g ↦
          {
            app := fun j ↦
              uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
            naturality := ⋯ })
        g) =
    g

Tactic:
ext j
    dsimp
    ext k
    -- this following list was obtained by
    -- `simp? [enrichedOrdinaryCategorySelf_eHomWhiskerLeft, Under.map, Comma.mapLeft]`
    simp only [diagram_obj_obj, Functor.comp_obj, Under.forget_obj, enrichedCategorySelf_hom,
      curry_uncurry, NatTrans.naturality_assoc, functorEnrichedHom_obj, functorEnrichedHom_map,
      Under.map, Comma.mapLeft, Functor.const_obj_obj, Functor.id_obj, Discrete.natTrans_app,
      StructuredArrow.left_eq_id, end_.lift_π, Under.mk_right, Under.mk_hom, Iso.refl_inv,
      NatTrans.id_app, enrichedOrdinaryCategorySelf_eHomWhiskerRight, pre_id, Iso.refl_hom,
      enrichedOrdinaryCategorySelf_eHomWhiskerLeft, Functor.map_id, Category.comp_id]
    congr
    simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
⊢ (α_ M.X N₁.X Z.X).hom ≫
      M.X ◁ N₁.actRight ≫
        M.X ◁ f.hom ≫
          colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft))
            WalkingParallelPair.one =
    coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ▷ Z.X ≫
      colimMap
            (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
              ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ▷
          Z.X ≫
        TensorBimod.actRight M N₂

Tactic:
slice_lhs 2 3 => rw [← whiskerLeft_comp, Hom.right_act_hom]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M✝ : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
⊢ (α_ M.X N₁.X Z.X).hom ≫
      M.X ◁ (f.hom ▷ Z.X ≫ N₂.actRight) ≫
        colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft))
          WalkingParallelPair.one =
    coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ▷ Z.X ≫
      colimMap
            (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
              ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ▷
          Z.X ≫
        TensorBimod.actRight M N₂
Module: Mathlib.CategoryTheory.Monoidal.CommComon_

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
⊢ Δ ≫ (β_ (𝟙_ C) (𝟙_ C)).hom = Δ

Tactic:
simp [← unitors_equal]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
⊢ (α_ X.X M₁.X N.X).inv ≫
      M₁.actLeft ▷ N.X ≫
        f.hom ▷ N.X ≫
          colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft))
            WalkingParallelPair.one =
    X.X ◁ coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) ≫
      X.X ◁
          colimMap
            (parallelPairHom (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) (M₂.actRight ▷ N.X)
              ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ≫
        TensorBimod.actLeft M₂ N

Tactic:
slice_lhs 2 3 => rw [← comp_whiskerRight, Hom.left_act_hom]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M₁ M₂ : Bimod X Y
f : M₁ ⟶ M₂
N : Bimod Y Z
⊢ (α_ X.X M₁.X N.X).inv ≫
      (X.X ◁ f.hom ≫ M₂.actLeft) ▷ N.X ≫
        colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft))
          WalkingParallelPair.one =
    X.X ◁ coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) ≫
      X.X ◁
          colimMap
            (parallelPairHom (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) (M₂.actRight ▷ N.X)
              ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ≫
        TensorBimod.actLeft M₂ N
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case comm1
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : Reflective i
inst✝² : MonoidalClosed C
inst✝¹ : CartesianMonoidalCategory D
inst✝ : ExponentialIdeal i
l : i.EssImageSubcategory ⥤ D
φ : l ⋙ i ≅ i.essImage.ι
B : D
⊢ tensorLeft B ⋙ i ≅ i ⋙ tensorLeft (i.obj B)

Tactic:
refine NatIso.ofComponents (fun X => ?_) (fun f => ?_)

Goal state after:
case comm1.refine_1
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : Reflective i
inst✝² : MonoidalClosed C
inst✝¹ : CartesianMonoidalCategory D
inst✝ : ExponentialIdeal i
l : i.EssImageSubcategory ⥤ D
φ : l ⋙ i ≅ i.essImage.ι
B X : D
⊢ (tensorLeft B ⋙ i).obj X ≅ (i ⋙ tensorLeft (i.obj B)).obj X

case comm1.refine_2
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : Reflective i
inst✝² : MonoidalClosed C
inst✝¹ : CartesianMonoidalCategory D
inst✝ : ExponentialIdeal i
l : i.EssImageSubcategory ⥤ D
φ : l ⋙ i ≅ i.essImage.ι
B X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ (tensorLeft B ⋙ i).map f ≫ Iso.hom ?comm1.refine_1 = Iso.hom ?comm1.refine_1 ≫ (i ⋙ tensorLeft (i.obj B)).map 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✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ 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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H (F ⊛ G)
inst✝⁵ : DayConvolution H F
inst✝⁴ : DayConvolution (H ⊛ F) G
inst✝³ : DayConvolution H G
inst✝² : DayConvolution F (H ⊛ G)
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution (F ⊛ H) G
⊢ (associator F G H).inv ≫ (braiding (F ⊛ G) H).hom ≫ (associator H F G).inv =
    map (𝟙 F) (braiding G H).hom ≫ (associator F H G).inv ≫ map (braiding F H).hom (𝟙 G)

Tactic:
by
  apply Functor.hom_ext_of_isLeftKanExtension (F ⊛ G ⊛ H) (unit _ _)
  apply Functor.hom_ext_of_isLeftKanExtension (F ⊠ (G ⊛ H))
    (ExternalProduct.extensionUnitRight (G ⊛ H) (unit G H) F)
  ext ⟨x, y, z⟩
  dsimp
  simp only [whiskerRight_tensor, id_whiskerRight, Category.id_comp,
    Iso.inv_hom_id, associator_inv_unit_unit_assoc,
    externalProductBifunctor_obj_obj, tensor_obj, NatTrans.naturality_assoc,
    NatTrans.naturality, unit_app_braiding_hom_app_assoc,
    BraidedCategory.braiding_tensor_right_hom, Functor.map_comp, Category.assoc,
    Iso.map_inv_hom_id, Category.comp_id,
    BraidedCategory.braiding_naturality_left_assoc,
    BraidedCategory.braiding_tensor_left_hom, Iso.map_hom_inv_id_assoc,
    Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc, unit_app_map_app_assoc,
    NatTrans.id_app, id_tensorHom]
  simp only [← comp_whiskerRight_assoc, ← whiskerLeft_comp_assoc,
    unit_app_braiding_hom_app]
  simp only [comp_whiskerRight, ← Functor.map_comp, Category.assoc, Functor.comp_obj, tensor_obj,
    whiskerLeft_comp, whiskerLeft_comp_unit_app_assoc, NatTrans.naturality_assoc,
    NatTrans.naturality, associator_inv_unit_unit_assoc, externalProductBifunctor_obj_obj,
    unit_app_map_app_assoc, NatTrans.id_app, tensorHom_id]
  congr 2
  rw [← BraidedCategory.hexagon_forward, ← comp_whiskerRight_assoc]
  have := unit_app_braiding_hom_app F H x z =≫ (H ⊛ F).map (β_ z x).inv
  dsimp at this
  simp only [Category.assoc, Iso.map_hom_inv_id, Category.comp_id] at this
  rw [← this, comp_whiskerRight_assoc]
  simp [← Functor.map_comp]

Goal state after:
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 : J ⥤ C
j : J
⊢ (ρ_ (limit F)).hom ≫ limit.π F j =
    limit F ◁
        limit.lift ((Functor.const J).obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (𝟙_ C), naturality := ⋯ } } ≫
      (limit.π F j ⊗ₘ limit.π (𝟙_ (J ⥤ C)) j) ≫ (ρ_ (F.obj j)).hom

Tactic:
simp only [tensorHom_def, ← whisker_exchange, whiskerRight_id, Category.assoc, Iso.inv_hom_id,
        Category.comp_id, ← whiskerLeft_comp_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 : J ⥤ C
j : J
⊢ (ρ_ (limit F)).hom ≫ limit.π F j =
    limit F ◁
        (limit.lift ((Functor.const J).obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (𝟙_ C), naturality := ⋯ } } ≫
          limit.π (𝟙_ (J ⥤ C)) j) ≫
      (ρ_ (limit F)).hom ≫ limit.π F j
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
⊢ (regular R).actRight ▷ P.X ≫ P.actLeft = ((α_ (regular R).X R.X P.X).hom ≫ (regular R).X ◁ P.actLeft) ≫ P.actLeft

Tactic:
by dsimp; rw [Category.assoc, left_assoc]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : LeftRigidCategory C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (ᘁf ≫ g).op.mop = (ᘁf).op.mop ≫ (ᘁg).op.mop

Tactic:
simp [comp_leftAdjointMate]

Goal state after: