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

Goal state before:
pp: 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
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ i.fullyFaithfulOfReflective.preimage
      (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
        uncurry
            ((unitCompPartialBijective B ⋯)
              (curry
                ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                  uncurry
                      ((unitCompPartialBijective A ⋯)
                        (curry ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X') (f ≫ g) ≫ 𝟙 (i.obj X')))) ≫
                    𝟙 (i.obj X')))) ≫
          𝟙 (i.obj X')) =
    i.fullyFaithfulOfReflective.preimage
        (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
          uncurry
              ((unitCompPartialBijective B ⋯)
                (curry
                  ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                    uncurry
                        ((unitCompPartialBijective A ⋯)
                          (curry ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X) f ≫ 𝟙 (i.obj X)))) ≫
                      𝟙 (i.obj X)))) ≫
            𝟙 (i.obj X)) ≫
      g

Tactic:
apply i.map_injective

Goal state after:
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
inst✝ : BraidedCategory C
A B : C
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ i.map
      (i.fullyFaithfulOfReflective.preimage
        (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
          uncurry
              ((unitCompPartialBijective B ⋯)
                (curry
                  ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                    uncurry
                        ((unitCompPartialBijective A ⋯)
                          (curry
                            ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X') (f ≫ g) ≫ 𝟙 (i.obj X')))) ≫
                      𝟙 (i.obj X')))) ≫
            𝟙 (i.obj X'))) =
    i.map
      (i.fullyFaithfulOfReflective.preimage
          (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
            uncurry
                ((unitCompPartialBijective B ⋯)
                  (curry
                    ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                      uncurry
                          ((unitCompPartialBijective A ⋯)
                            (curry ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X) f ≫ 𝟙 (i.obj X)))) ≫
                        𝟙 (i.obj X)))) ≫
              𝟙 (i.obj X)) ≫
        g)
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f✝ : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
j : (multicospanShapeEnd C).L
⊢ (H.map f ≫ Wedge.IsLimit.lift (ℌ'.isLimitWedge c') (fun j ↦ ℌ.π c' j ≫ (ihom (F.obj j)).map (f✝.app (j ⊗ c'))) ⋯) ≫
      ℌ'.π c' j =
    (Wedge.IsLimit.lift (ℌ'.isLimitWedge c) (fun j ↦ ℌ.π c j ≫ (ihom (F.obj j)).map (f✝.app (j ⊗ c))) ⋯ ≫ H'.map f) ≫
      ℌ'.π c' j

Tactic:
simp only [Category.assoc, map_comp_π]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f✝ : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
j : (multicospanShapeEnd C).L
⊢ H.map f ≫
      Wedge.IsLimit.lift (ℌ'.isLimitWedge c') (fun j ↦ ℌ.π c' j ≫ (ihom (F.obj j)).map (f✝.app (j ⊗ c'))) ⋯ ≫
        ℌ'.π c' j =
    Wedge.IsLimit.lift (ℌ'.isLimitWedge c) (fun j ↦ ℌ.π c j ≫ (ihom (F.obj j)).map (f✝.app (j ⊗ c))) ⋯ ≫
      ℌ'.π c j ≫ (ihom (F.obj j)).map (G'.map (j ◁ f))
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:
rw [Category.assoc, left_assoc]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ ((PreservesCoequalizer.iso (tensorRight S.X) (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)).inv ≫
        colimMap
          (parallelPairHom (μ ▷ P.X ▷ S.X) (((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ▷ S.X) (μ ▷ P.X)
            ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)
            ((α_ (R.X ⊗ R.X) P.X S.X).hom ≫
              (α_ R.X R.X (P.X ⊗ S.X)).hom ≫ R.X ◁ R.X ◁ P.actRight ≫ (α_ R.X R.X P.X).inv)
            ((α_ R.X P.X S.X).hom ≫ R.X ◁ P.actRight) ⋯ ⋯)) ≫
      coequalizer.desc P.actLeft ⋯ =
    coequalizer.desc P.actLeft ⋯ ▷ S.X ≫ P.actRight

Tactic:
refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_

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
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (tensorRight S.X).map
        (coequalizer.π
          ({ X := R.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ }.actRight ▷
            P.X)
          ((α_
                { X := R.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ }.X
                R.X P.X).hom ≫
            { X := R.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ }.X ◁
              P.actLeft)) ≫
      ((PreservesCoequalizer.iso (tensorRight S.X) (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)).inv ≫
          colimMap
            (parallelPairHom (μ ▷ P.X ▷ S.X) (((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ▷ S.X) (μ ▷ P.X)
              ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)
              ((α_ (R.X ⊗ R.X) P.X S.X).hom ≫
                (α_ R.X R.X (P.X ⊗ S.X)).hom ≫ R.X ◁ R.X ◁ P.actRight ≫ (α_ R.X R.X P.X).inv)
              ((α_ R.X P.X S.X).hom ≫ R.X ◁ P.actRight) ⋯ ⋯)) ≫
        coequalizer.desc P.actLeft ⋯ =
    (tensorRight S.X).map
        (coequalizer.π
          ({ X := R.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ }.actRight ▷
            P.X)
          ((α_
                { X := R.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ }.X
                R.X P.X).hom ≫
            { X := R.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ }.X ◁
              P.actLeft)) ≫
      coequalizer.desc P.actLeft ⋯ ▷ S.X ≫ P.actRight
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
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ ((PreservesCoequalizer.iso (tensorRight S.X) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)).inv ≫
        colimMap
          (parallelPairHom (P.actRight ▷ S.X ▷ S.X) (((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ▷ S.X) (P.actRight ▷ S.X)
            ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)
            ((α_ (P.X ⊗ S.X) S.X S.X).hom ≫ (α_ P.X S.X (S.X ⊗ S.X)).hom ≫ P.X ◁ S.X ◁ μ ≫ (α_ P.X S.X S.X).inv)
            ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ⋯ ⋯)) ≫
      coequalizer.desc P.actRight ⋯ =
    coequalizer.desc P.actRight ⋯ ▷ S.X ≫ P.actRight

Tactic:
refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_

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
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (tensorRight S.X).map
        (coequalizer.π
          (P.actRight ▷
            { X := S.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ }.X)
          ((α_ P.X S.X
                { X := S.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ }.X).hom ≫
            P.X ◁
              { X := S.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ }.actLeft)) ≫
      ((PreservesCoequalizer.iso (tensorRight S.X) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)).inv ≫
          colimMap
            (parallelPairHom (P.actRight ▷ S.X ▷ S.X) (((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ▷ S.X) (P.actRight ▷ S.X)
              ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)
              ((α_ (P.X ⊗ S.X) S.X S.X).hom ≫ (α_ P.X S.X (S.X ⊗ S.X)).hom ≫ P.X ◁ S.X ◁ μ ≫ (α_ P.X S.X S.X).inv)
              ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ⋯ ⋯)) ≫
        coequalizer.desc P.actRight ⋯ =
    (tensorRight S.X).map
        (coequalizer.π
          (P.actRight ▷
            { X := S.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ }.X)
          ((α_ P.X S.X
                { X := S.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ }.X).hom ≫
            P.X ◁
              { X := S.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ }.actLeft)) ≫
      coequalizer.desc P.actRight ⋯ ▷ S.X ≫ P.actRight
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
U : C ⥤ V
inst✝³ : DayConvolutionUnit U
F : C ⥤ V
inst✝² : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ : DayConvolution U F
G : C ⥤ V
inst✝ : DayConvolution U G
f : F ⟶ G
⊢ DayConvolution.map (𝟙 U) f ≫ (leftUnitor U G).hom = (leftUnitor U F).hom ≫ f

Tactic:
by
  apply Functor.hom_ext_of_isLeftKanExtension _ (DayConvolution.unit _ _) _
  apply Functor.hom_ext_of_isLeftKanExtension _ (extensionUnitLeft U (φ U) F) _
  ext
  simp [← whisker_exchange_assoc]

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
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
x : C
snd✝ : Discrete PUnit.{1}
⊢ (𝟙 (((ι C V D).obj d).obj x) ▷ 𝟙_ V ≫ ((ι C V D).obj d).obj x ◁ can) ≫
      (DayConvolution.unit ((ι C V D).obj d) ((ι C V D).obj (𝟙_ D))).app (x, 𝟙_ C) ≫
        ((ι C V D).map (ρ_ d).hom).app (x ⊗ 𝟙_ C) =
    (𝟙 (((ι C V D).obj d).obj x) ▷ 𝟙_ V ≫ ((ι C V D).obj d).obj x ◁ can) ≫
      (DayConvolution.unit ((ι C V D).obj d) ((ι C V D).obj (𝟙_ D))).app (x, 𝟙_ C) ≫
        (DayConvolutionUnit.rightUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj d)).hom.app (x ⊗ 𝟙_ C)

Tactic:
simp only [id_whiskerRight, Category.id_comp,
    DayConvolutionUnit.rightUnitor_hom_unit_app]

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁶ : Category.{v₂, u₂} V
inst✝⁵ : MonoidalCategory C
inst✝⁴ : MonoidalCategory V
D : Type u₃
inst✝³ : Category.{v₃, u₃} D
inst✝² : MonoidalCategoryStruct D
inst✝¹ : LawfulDayConvolutionMonoidalCategoryStruct C V D
d : D
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
x : C
snd✝ : Discrete PUnit.{1}
⊢ ((ι C V D).obj d).obj x ◁ can ≫
      (DayConvolution.unit ((ι C V D).obj d) ((ι C V D).obj (𝟙_ D))).app (x, 𝟙_ C) ≫
        ((ι C V D).map (ρ_ d).hom).app (x ⊗ 𝟙_ C) =
    (ρ_ (((ι C V D).obj d).obj x)).hom ≫ ((ι C V D).obj d).map (ρ_ x).inv
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
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
⊢ (ι C V D).map (ρ_ d).hom = (DayConvolutionUnit.rightUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj d)).hom

Tactic:
by
  apply corepresentableByRight
    (ι C V D |>.obj <| 𝟙_ D) (ι C V D |>.obj d) |>.homEquiv.injective
  dsimp
  ext ⟨x, _⟩
  dsimp [corepresentableByRight]
  simp only [id_whiskerRight, Category.id_comp,
    DayConvolutionUnit.rightUnitor_hom_unit_app]
  exact rightUnitor_hom_unit_app V d x

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

Goal state before:
pp: case refine_1.refine_2
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.ind f
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
D : J ⥤ C
t : (Functor.const J).obj X ⟶ D
s : D ⟶ (Functor.const J).obj Y
hs : IsColimit { pt := Y, ι := s }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
⊢ IsColimit
    { pt := CategoryTheory.Under.mk f, ι := { app := fun j ↦ CategoryTheory.Under.homMk (s.app j) ⋯, naturality := ⋯ } }

Tactic:
have : Nonempty J := IsFiltered.nonempty
      exact Under.isColimitLiftCocone _ _ _ _ (by simp [hst]) hs

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
Z : C
hZ : P Z
u v : Y ⟶ Z
huv : (fun g ↦ f ≫ g) u = (fun g ↦ f ≫ g) v
⊢ u = v

Tactic:
rwa [← cancel_epi f]

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 M' : Bimod W X
f : M ⟶ M'
N : Bimod X Y
P : Bimod Y Z
⊢ M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫
      f.hom ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫
        colimit.ι
          (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))
            ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫
              M'.X ◁ TensorBimod.actLeft N P))
          WalkingParallelPair.one =
    (α_ M.X N.X P.X).inv ≫
      (f.hom ▷ N.X ≫
            colimit.ι (parallelPair (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft))
              WalkingParallelPair.one) ▷
          P.X ≫
        AssociatorBimod.homAux M' N P

Tactic:
dsimp [AssociatorBimod.homAux]

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 M' : Bimod W X
f : M ⟶ M'
N : Bimod X Y
P : Bimod Y Z
⊢ M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫
      f.hom ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫
        colimit.ι
          (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))
            ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫
              M'.X ◁ TensorBimod.actLeft N P))
          WalkingParallelPair.one =
    (α_ M.X N.X P.X).inv ≫
      (f.hom ▷ N.X ≫
            colimit.ι (parallelPair (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft))
              WalkingParallelPair.one) ▷
          P.X ≫
        (PreservesCoequalizer.iso (tensorRight P.X) (M'.actRight ▷ N.X)
              ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft)).inv ≫
          coequalizer.desc
            ((α_ M'.X N.X P.X).hom ≫
              M'.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫
                coequalizer.π (M'.actRight ▷ TensorBimod.X N P)
                  ((α_ M'.X X.X (TensorBimod.X N P)).hom ≫ M'.X ◁ TensorBimod.actLeft N P))
            ⋯
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X : Type u
hX : Cardinal.mk X = κ
α : Type u := (S : Set X) × (x : PartialOrder ↑S) × ULift.{u, 0} (PLift (IsCardinalFiltered (↑S) κ))
this✝ : (a : α) → PartialOrder ↑a.fst := fun a ↦ a.snd.fst
ι : α → CardinalDirectedPoset κ := fun a ↦ { obj := { carrier := ↑a.fst, str := this✝ a }, property := ⋯ }
J : CardinalDirectedPoset κ
x✝ : hasCardinalLTWithTerminal κ J
hJ : HasCardinalLT (↑J.obj) κ
right✝ : HasTerminal ↑J.obj
f : ↑J.obj ↪ X
e : ↑J.obj ≃ ↑(Set.range ⇑f) := Equiv.ofInjective ⇑f ⋯
this : PartialOrder ↑(Set.range ⇑f) := PartialOrder.lift ⇑e.symm ⋯
⊢ ∀ {a b : ↑(Set.range ⇑f)}, e.symm a ≤ e.symm b ↔ a ≤ b

Tactic:
by rfl

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : Mat_ C ⥤ D
inst✝ : F.Additive
M N : Mat_ C
f : M ⟶ N
⊢ F.map f ≫ (additiveObjIsoBiproduct F N).hom =
    (additiveObjIsoBiproduct F M).hom ≫ biproduct.matrix fun i j ↦ F.map ((embedding C).map (f i j))

Tactic:
additiveObjIsoBiproduct_naturality

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : Mat_ C ⥤ D
inst✝ : F.Additive
M N : Mat_ C
f : M ⟶ N
⊢ ((additiveObjIsoBiproduct F M).hom ≫ biproduct.matrix fun i j ↦ F.map ((embedding C).map (f i j))) =
    (additiveObjIsoBiproduct F M).hom ≫ biproduct.matrix fun i j ↦ F.map ((embedding C).map (f i j))
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
s : Cocone F
x y : CoconePt hc
⊢ { toFun := ⇑(ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))), inj' := ⋯ } x ≤
      { toFun := ⇑(ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))), inj' := ⋯ } y ↔
    x ≤ y

Tactic:
obtain ⟨j, x', y', rfl, rfl⟩ :=
      Types.FilteredColimit.jointly_surjective_of_isColimit₂ hc x y
    have hx := ConcreteCategory.congr_hom (hc.fac ((forget _).mapCocone s) j) x'
    have hy := ConcreteCategory.congr_hom (hc.fac ((forget _).mapCocone s) j) y'
    simp only [Functor.mapCocone_pt, Functor.comp_obj, Functor.const_obj_obj,
      CategoryTheory.comp_apply, Functor.mapCocone_ι_app, ConcreteCategory.hom_ofHom,
      TypeCat.Fun.coe_mk, Function.Embedding.coeFn_mk] at hx hy ⊢
    rw [hx, hy, OrderEmbedding.le_iff_le]
    refine ⟨fun h ↦ ⟨j, _, _, rfl, rfl, h⟩, fun ⟨k, x, y, hx', hy', h⟩ ↦ ?_⟩
    obtain ⟨l, f, g, hl⟩ := (Types.FilteredColimit.isColimit_eq_iff _ hc).1 hx'
    obtain ⟨l', f', g', hl'⟩ := (Types.FilteredColimit.isColimit_eq_iff _ hc).1 hy'
    obtain ⟨m, a, b, h₁, h₂⟩ := bowtie f f' g g'
    dsimp at hl hl'
    rw [← (F.map (f ≫ a)).le_iff_le] at h
    rw [← (F.map (g ≫ a)).le_iff_le]
    exact le_of_eq_of_le (by simp [hl]) (le_of_le_of_eq h (by simp [h₁, h₂, hl']))

Goal state after:
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: α : PartOrdEmb
P : Set ↑α → Prop
X✝ Y✝ : Subtype P
f : X✝ ⟶ Y✝
⊢ ∀ {a b : ↑↑X✝}, { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ } a ≤ { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ } b ↔ a ≤ b

Tactic:
by rfl

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

Goal state before:
pp: J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
x✝ : DiagramWithUniqueTerminal J κ
⊢ x✝.W ≤ x✝.W

Tactic:
by rfl

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

Goal state before:
pp: J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
x✝ : DiagramWithUniqueTerminal J κ
⊢ x✝.P ≤ x✝.P

Tactic:
by rfl

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h : κ₁ ≤ κ₂
inst✝ : IsCardinalAccessibleCategory (CardinalDirectedPoset κ₁) κ₂
X : Type w
hX : HasCardinalLT X κ₂
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ₂
p : (isCardinalPresentable (CardinalDirectedPoset κ₁) κ₂).ColimitOfShape J (setCardinalLT κ₁ X)
this : IsCardinalFiltered J κ₁
hp : ∀ (j : J), HasCardinalLT (↑(p.diag.obj j).obj) κ₂
j : X → J
y : (x : X) → ToType (p.diag.obj (j x))
hy : ∀ (x : X), (ConcreteCategory.hom (p.ι.app (j x))) (y x) = SetCardinalLT.singleton κ₁ x
j' : J := IsCardinalFiltered.max j hX
y' : X → ↑(p.diag.obj j').obj := fun x ↦ (ConcreteCategory.hom (p.diag.map (IsCardinalFiltered.toMax j hX x))) (y x)
hy' : ∀ (x : X), (ConcreteCategory.hom (p.ι.app j')) (y' x) = SetCardinalLT.singleton κ₁ x
x✝ : SetCardinalLT κ₁ X
B : Set X
hB : HasCardinalLT (↑B) κ₁
j'' : ↑(p.diag.obj j').obj := IsCardinalFiltered.max (fun b ↦ y' ↑b) hB
⊢ ∃ y ∈ Set.range ⇑(ConcreteCategory.hom (p.ι.app j')), ⟨B, hB⟩ ≤ y

Tactic:
refine ⟨_, ⟨j'', rfl⟩, fun b hb ↦ ?_⟩

Goal state after:
κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h : κ₁ ≤ κ₂
inst✝ : IsCardinalAccessibleCategory (CardinalDirectedPoset κ₁) κ₂
X : Type w
hX : HasCardinalLT X κ₂
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ₂
p : (isCardinalPresentable (CardinalDirectedPoset κ₁) κ₂).ColimitOfShape J (setCardinalLT κ₁ X)
this : IsCardinalFiltered J κ₁
hp : ∀ (j : J), HasCardinalLT (↑(p.diag.obj j).obj) κ₂
j : X → J
y : (x : X) → ToType (p.diag.obj (j x))
hy : ∀ (x : X), (ConcreteCategory.hom (p.ι.app (j x))) (y x) = SetCardinalLT.singleton κ₁ x
j' : J := IsCardinalFiltered.max j hX
y' : X → ↑(p.diag.obj j').obj := fun x ↦ (ConcreteCategory.hom (p.diag.map (IsCardinalFiltered.toMax j hX x))) (y x)
hy' : ∀ (x : X), (ConcreteCategory.hom (p.ι.app j')) (y' x) = SetCardinalLT.singleton κ₁ x
x✝ : SetCardinalLT κ₁ X
B : Set X
hB : HasCardinalLT (↑B) κ₁
j'' : ↑(p.diag.obj j').obj := IsCardinalFiltered.max (fun b ↦ y' ↑b) hB
b : X
hb : b ∈ ↑⟨B, hB⟩
⊢ b ∈ ↑((ConcreteCategory.hom (p.ι.app j')) j'')