mathlib-initiative/mathlib-tactics huggingface dataset:
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.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))
            ⋯)
        ⋯ =
    𝟙 (TensorBimod.X P (Q.tensorBimod L))

Tactic:
apply coequalizer.hom_ext

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
⊢ 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))
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.π F j ▷ limit G ≫ F.obj j ◁ limit.π G j) ▷ limit H ≫
    (F.obj j ⊗ G.obj j) ◁ limit.π H j ≫ (α_ (F.obj j) (G.obj j) (H.obj j)).hom

Tactic:
← tensorHom_def,

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.π F j ⊗ₘ limit.π 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.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 ⊗≫ ((β_ Y X).inv ▷ Y ⊗≫ Y ◁ (β_ X Y).hom) ≫ Y ◁ ε_ X Y ⊗≫ 𝟙 Y =
    𝟙 Y ⊗≫
      η_ X Y ▷ Y ⊗≫
        (𝟙 ((X ⊗ Y) ⊗ Y) ⊗≫
            X ◁ (β_ Y Y).hom ⊗≫ (β_ X Y).hom ▷ Y ⊗≫ Y ◁ (β_ Y X).inv ⊗≫ (β_ Y Y).inv ▷ X ⊗≫ 𝟙 (Y ⊗ Y ⊗ X)) ⊗≫
          Y ◁ ε_ X Y ⊗≫ 𝟙 Y

Tactic:
by
      congr 3
      on_goal 2 => simp [monoidalComp]
      simp only [monoidalComp, MonoidalCoherence.assoc_iso, MonoidalCoherence.whiskerRight_iso,
        MonoidalCoherence.refl_iso, whiskerRightIso_refl, Iso.trans_refl,
        MonoidalCoherence.assoc'_iso, Iso.refl_trans, Iso.symm_hom, comp_id, id_comp]
      iterate 2 rw [← IsIso.eq_inv_comp]
      repeat rw [← assoc]
      iterate 4 rw [← IsIso.comp_inv_eq]
      simpa using (yang_baxter Y X Y).symm

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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
⊢ ({ X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
            middle_assoc := ⋯ }.whiskerLeft
        f).hom =
    ((isoOfIso { hom := LeftUnitorBimod.hom M, inv := LeftUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯).hom ≫
        f ≫
          (isoOfIso { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
              ⋯).inv).hom

Tactic:
apply coequalizer.hom_ext

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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
⊢ coequalizer.π
        ({ X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
              right_assoc := ⋯, middle_assoc := ⋯ }.actRight ▷
          M.X)
        ((α_
              { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ }.X
              X.X M.X).hom ≫
          { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ }.X ◁
            M.actLeft) ≫
      ({ X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
              middle_assoc := ⋯ }.whiskerLeft
          f).hom =
    coequalizer.π
        ({ X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
              right_assoc := ⋯, middle_assoc := ⋯ }.actRight ▷
          M.X)
        ((α_
              { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ }.X
              X.X M.X).hom ≫
          { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ }.X ◁
            M.actLeft) ≫
      ((isoOfIso { hom := LeftUnitorBimod.hom M, inv := LeftUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
              ⋯).hom ≫
          f ≫
            (isoOfIso { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
                ⋯).inv).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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
⊢ X.X ◁ f.hom ≫ colimit.ι (parallelPair (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    (M.actLeft ≫ f.hom) ≫ LeftUnitorBimod.inv N

Tactic:
dsimp [LeftUnitorBimod.inv]

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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
⊢ X.X ◁ f.hom ≫ colimit.ι (parallelPair (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    (M.actLeft ≫ f.hom) ≫ (λ_ N.X).inv ≫ η ▷ N.X ≫ coequalizer.π (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)
Module: Mathlib.CategoryTheory.Presentable.Dense

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsFinitelyAccessibleCategory C
⊢ (ObjectProperty.isFinitelyPresentable C).ι.IsDense

Tactic:
by
  rw [ObjectProperty.isFinitelyPresentable_eq_isCardinalPresentable]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Dense

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsFinitelyAccessibleCategory C
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (ObjectProperty.isFinitelyPresentable C)

Tactic:
by
  rw [ObjectProperty.isFinitelyPresentable_eq_isCardinalPresentable]
  infer_instance

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
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₂'
⊢ (ι C V D).map (f ⊗ₘ f') = DayConvolution.map ((ι C V D).map f) ((ι C V D).map f')

Tactic:
apply DayConvolution.corepresentableBy
    (ι C V D |>.obj d₁) (ι C V D |>.obj d₁') |>.homEquiv.injective
  dsimp
  ext ⟨x, y⟩
  simp only [externalProductBifunctor_obj_obj, Functor.comp_obj, tensor_obj,
    DayConvolution.corepresentableBy_homEquiv_apply_app,
    DayConvolution.unit_app_map_app]
  exact convolutionExtensionUnit_comp_ι_map_tensorHom_app C V _ _ _ _

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H✝ : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
H : ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y), isFinitelyPresentable C p → p ≫ g = f → ∃ W u v, u ≫ v = g ∧ P (p ≫ u)
Z : Under X
g : Z ⟶ CategoryTheory.Under.mk f
hZ : IsFinitelyPresentable Z
W : C
u : Z.right ⟶ W
v : W ⟶ Y
huv : u ≫ v = Under.Hom.right g
hW : P (Z.hom ≫ u)
⊢ CategoryTheory.Under.homMk u ⋯ ≫ CategoryTheory.Under.homMk v ⋯ = g

Tactic:
by ext; simpa

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
hX : IsZero X
⊢ IsArtinianObject X

Tactic:
rw [isArtinianObject_iff_antitone_chain_condition]
  have := Subobject.subsingleton_of_isZero hX
  intro f
  exact ⟨0, fun m hm ↦ Subsingleton.elim _ _⟩

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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
⊢ (whiskerRight f
        { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ }).hom =
    ((isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯).hom ≫
        f ≫
          (isoOfIso { hom := RightUnitorBimod.hom N, inv := RightUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
              ⋯).inv).hom

Tactic:
apply coequalizer.hom_ext

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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
⊢ coequalizer.π
        (M.actRight ▷
          { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
              right_assoc := ⋯, middle_assoc := ⋯ }.X)
        ((α_ M.X Y.X
              { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ }.X).hom ≫
          M.X ◁
            { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ }.actLeft) ≫
      (whiskerRight f
          { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
            right_assoc := ⋯, middle_assoc := ⋯ }).hom =
    coequalizer.π
        (M.actRight ▷
          { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
              right_assoc := ⋯, middle_assoc := ⋯ }.X)
        ((α_ M.X Y.X
              { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ }.X).hom ≫
          M.X ◁
            { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ }.actLeft) ≫
      ((isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
              ⋯).hom ≫
          f ≫
            (isoOfIso { hom := RightUnitorBimod.hom N, inv := RightUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ }
                ⋯ ⋯).inv).hom
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u v : Arrow V
f g : u ⟶ v
inst✝ : HasZeroObject V
⊢ (functor V).Additive

Tactic:
dsimp [functor]; infer_instance

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)
W X Y Z : Mon C
M : Bimod W X
N N' : Bimod X Y
f : N ⟶ N'
P : Bimod Y Z
⊢ (whiskerRight (M.whiskerLeft f) P).hom =
    ((isoOfIso { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ }
            ⋯ ⋯).hom ≫
        M.whiskerLeft (whiskerRight f P) ≫
          (isoOfIso
              { hom := AssociatorBimod.hom M N' P, inv := AssociatorBimod.inv M N' P, hom_inv_id := ⋯, inv_hom_id := ⋯ }
              ⋯ ⋯).inv).hom

Tactic:
apply coequalizer.hom_ext

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)
W X Y Z : Mon C
M : Bimod W X
N N' : Bimod X Y
f : N ⟶ N'
P : Bimod Y Z
⊢ coequalizer.π
        ({ X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯,
              actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actRight ▷
          P.X)
        ((α_
              { X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯,
                  actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X
              Y.X P.X).hom ≫
          { X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯,
                actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X ◁
            P.actLeft) ≫
      (whiskerRight (M.whiskerLeft f) P).hom =
    coequalizer.π
        ({ X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯,
              actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actRight ▷
          P.X)
        ((α_
              { X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯,
                  actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X
              Y.X P.X).hom ≫
          { X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯,
                actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X ◁
            P.actLeft) ≫
      ((isoOfIso
              { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
              ⋯).hom ≫
          M.whiskerLeft (whiskerRight f P) ≫
            (isoOfIso
                { hom := AssociatorBimod.hom M N' P, inv := AssociatorBimod.inv M N' P, hom_inv_id := ⋯,
                  inv_hom_id := ⋯ }
                ⋯ ⋯).inv).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)
X Y Z : Mon C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ (M.whiskerLeft g ≫ whiskerRight f Q).hom = (whiskerRight f P ≫ N.whiskerLeft g).hom

Tactic:
apply coequalizer.hom_ext

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)
X Y Z : Mon C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫ (M.whiskerLeft g ≫ whiskerRight f Q).hom =
    coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫ (whiskerRight f P ≫ N.whiskerLeft g).hom
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
⊢ ((fun x y ↦ if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0) ≫ fun x y ↦
      if h : x.fst = j' then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0) =
    if h : j = j' then eqToHom ⋯ else 0

Tactic:
ext x y

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ ((fun x y ↦ if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0) ≫ fun x y ↦
        if h : x.fst = j' then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0)
      x y =
    (if h : j = j' then eqToHom ⋯ else 0) x y
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
x y : CoconePt hc
j : J
x₁ y₁ : ↑(F.obj j)
hx₁ : (ConcreteCategory.hom (c.ι.app j)) x₁ = x
hy₁ : (ConcreteCategory.hom (c.ι.app j)) y₁ = y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : ↑(F.obj k)
hy₂ : (ConcreteCategory.hom (c.ι.app k)) y₂ = y
hx₂ : (ConcreteCategory.hom (c.ι.app k)) x₂ = x
h₂ : y₂ ≤ x₂
l₁ : J
a : j ⟶ l₁
b : k ⟶ l₁
h₃ :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a)) x₁ = (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map b)) x₂
l₂ : J
a' : j ⟶ l₂
b' : k ⟶ l₂
h₄ :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a')) y₁ =
    (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map b')) y₂
l : J
d : l₁ ⟶ l
d' : l₂ ⟶ l
h₅ : a ≫ d = a' ≫ d'
h₆ : b ≫ d = b' ≫ d'
⊢ (ConcreteCategory.hom (F.map (a' ≫ d'))) y₁ = (ConcreteCategory.hom (F.map (b ≫ d))) y₂

Tactic:
by simpa [h₆]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
⊢ ((biproduct.desc fun i x k ↦ if h : i = k then eqToHom ⋯ else 0) ≫
      biproduct.lift fun i j x ↦ if h : j = i then eqToHom ⋯ else 0) =
    𝟙 (⨁ fun i ↦ (embedding C).obj (M.X i))

Tactic:
by
    apply biproduct.hom_ext
    intro i
    apply biproduct.hom_ext'
    intro j
    simp only [Category.id_comp, Category.assoc, biproduct.lift_π, biproduct.ι_desc_assoc,
      biproduct.ι_π]
    ext ⟨⟩ ⟨⟩
    simp only [embedding, comp_apply, comp_dite, dite_comp, comp_zero, zero_comp,
      Finset.sum_dite_eq', Finset.mem_univ, ite_true, eqToHom_refl, Category.comp_id]
    split_ifs with h
    · subst h
      simp
    · rfl

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case refine_1
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
⊢ ∃ lift, __Diagram✝.W lift

Tactic:
exact ⟨𝟙 _, ⟨⟨⟩⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
ι : Type u_1
D : ι → Diagram J κ
hι : HasCardinalLT ι κ
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
hf : ∃ i, (D i).W f✝
⊢ ∃ i, (D i).P i✝

Tactic:
obtain ⟨i, hi⟩ := hf

Goal state after:
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
ι : Type u_1
D : ι → Diagram J κ
hι : HasCardinalLT ι κ
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
i : ι
hi : (D i).W f✝
⊢ ∃ i, (D i).P i✝
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
ι : Type u_1
D : ι → Diagram J κ
hι : HasCardinalLT ι κ
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
hf : ∃ i, (D i).W f✝
⊢ ∃ i, (D i).P j✝

Tactic:
obtain ⟨i, hi⟩ := hf

Goal state after:
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
ι : Type u_1
D : ι → Diagram J κ
hι : HasCardinalLT ι κ
i✝ j✝ : J
f✝ : i✝ ⟶ j✝
i : ι
hi : (D i).W f✝
⊢ ∃ i, (D i).P j✝
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
Z : C
x✝ : W.isLocal.colimitsOfShape J Z
X Y : C
f : X ⟶ Y
hf : W f
p : W.isLocal.ColimitOfShape J Z
⊢ Function.Bijective fun g ↦ f ≫ g

Tactic:
by
    obtain ⟨_, _⟩ := hW f hf
    refine ⟨fun g₁ g₂ h ↦ ?_, fun g ↦ ?_⟩
    · obtain ⟨j₁, g₁, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit g₁
      obtain ⟨j₂, g₂, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit g₂
      dsimp at h ⊢
      obtain ⟨j₃, u, v, huv⟩ :=
        IsCardinalPresentable.exists_eq_of_isColimit κ p.isColimit (f ≫ g₁) (f ≫ g₂)
          (by simpa)
      simp only [Category.assoc] at huv
      rw [← p.w u, ← p.w v, reassoc_of% ((p.prop_diag_obj j₃ _ hf).1 huv)]
    · obtain ⟨j, g, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit g
      obtain ⟨g, rfl⟩ := (p.prop_diag_obj j _ hf).2 g
      exact ⟨g ≫ p.ι.app j, by simp⟩

Goal state after: