mathlib-initiative/mathlib-tactics huggingface dataset:
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'))
⊢ (∀ (c : C) (d c_1 : D), IsIso ((yoneda.map ((pre (adj.unit.app d)).app (R.obj c))).app (Opposite.op c_1))) ↔
    ∀ (d d' : D) (c : C), IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)

Tactic:
rw [forall_comm]

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'))
⊢ (∀ (b : D) (a : C) (c : D), IsIso ((yoneda.map ((pre (adj.unit.app b)).app (R.obj a))).app (Opposite.op c))) ↔
    ∀ (d d' : D) (c : C), IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)
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 : C) (c : D), IsIso ((yoneda.map ((pre (adj.unit.app d)).app (R.obj a))).app (Opposite.op c))) ↔
    ∀ (d' : D) (c : C), IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)

Tactic:
rw [forall_comm]

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
⊢ (∀ (b : D) (a : C), IsIso ((yoneda.map ((pre (adj.unit.app d)).app (R.obj a))).app (Opposite.op b))) ↔
    ∀ (d' : D) (c : C), IsIso ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)
Module: Mathlib.CategoryTheory.Monoidal.Closed.Zero

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasZeroObject C
X Y : C
this : HasInitial C
⊢ Unique (X ⟶ Y)

Tactic:
apply uniqueHomsetOfInitialIsoUnit _ X Y

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasZeroObject C
X Y : C
this : HasInitial C
⊢ ⊥_ C ≅ 𝟙_ C
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'
⊢ 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).unit.app (A ⊗ B) ≫ i.map f ≫ i.map g)))))) =
    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).unit.app (A ⊗ B) ≫ i.map f)))))) ≫
        i.map g

Tactic:
rw [← Category.assoc, ← Category.assoc, curry_natural_right _ (i.map g),
    unitCompPartialBijective_natural, uncurry_natural_right, ← Category.assoc, curry_natural_right,
    unitCompPartialBijective_natural, uncurry_natural_right, Category.assoc]

Goal state after:
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'
⊢ H.map f ≫
      Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
        (fun j ↦ ℌ.π c' j ≫ ((((dayConvolutionInternalHomDiagramFunctor F).map f✝).app c').app (op j)).app j) ⋯ =
    Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
        (fun j ↦ ℌ.π c j ≫ ((((dayConvolutionInternalHomDiagramFunctor F).map f✝).app c).app (op j)).app j) ⋯ ≫
      H'.map f

Tactic:
apply Wedge.IsLimit.hom_ext (ℌ'.isLimitWedge c')

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 ≫ ((((dayConvolutionInternalHomDiagramFunctor F).map f✝).app c').app (op j)).app j) ⋯) ≫
        Multifork.ι (Wedge.mk (H'.obj c') (ℌ'.π c') ⋯) j =
      (Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
            (fun j ↦ ℌ.π c j ≫ ((((dayConvolutionInternalHomDiagramFunctor F).map f✝).app c).app (op j)).app j) ⋯ ≫
          H'.map f) ≫
        Multifork.ι (Wedge.mk (H'.obj c') (ℌ'.π c') ⋯) j
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
inst✝ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C
this :
  ∀ (β : F ⊠ H ⟶ tensor C ⋙ G) (X : C × C),
    (DayConvolution.unit F H).app X ≫
        ((F ⊛ H).descOfIsLeftKanExtension (DayConvolution.unit F H) G β).app ((tensor C).obj X) =
      β.app X
⊢ (DayConvolution.unit F H).app (x, y) ≫ ℌ.ev_app.app (x ⊗ y) = MonoidalClosed.uncurry (ℌ.π y x)

Tactic:
dsimp at this

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
inst✝ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
x y : C
this :
  ∀ (β : F ⊠ H ⟶ tensor C ⋙ G) (X : C × C),
    (DayConvolution.unit F H).app X ≫ ((F ⊛ H).descOfIsLeftKanExtension (DayConvolution.unit F H) G β).app (X.1 ⊗ X.2) =
      β.app X
⊢ (DayConvolution.unit F H).app (x, y) ≫ ℌ.ev_app.app (x ⊗ y) = MonoidalClosed.uncurry (ℌ.π y x)
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided

Goal state before:
pp: case e_a
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
x y z : C
this :
  ((unit F H).app (x, z) ≫ (braiding F H).hom.app (x ⊗ z)) ≫ (H ⊛ F).map (β_ z x).inv =
    ((β_ ((H, F).2.obj (z, x).2) ((H, F).1.obj (z, x).1)).hom ≫
        (unit H F).app (z, x) ≫ (H ⊛ F).map (β_ (z, x).1 (z, x).2).hom) ≫
      (H ⊛ F).map (β_ z x).inv
⊢ ((β_ (F.obj x) (H.obj z)).hom ≫ (unit H F).app (z, x)) ▷ G.obj y ≫
      (unit (H ⊛ F) G).app (z ⊗ x, y) ≫ ((H ⊛ F) ⊛ G).map ((α_ z x y).hom ≫ (β_ z (x ⊗ y)).hom ≫ (α_ x y z).hom) =
    (unit F H).app (x, z) ▷ G.obj y ≫
      (braiding F H).hom.app (x ⊗ z) ▷ G.obj y ≫
        (unit (H ⊛ F) G).app (x ⊗ z, y) ≫ ((H ⊛ F) ⊛ G).map ((α_ x z y).hom ≫ x ◁ (β_ z y).hom)

Tactic:
dsimp at this

Goal state after:
case e_a
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
x y z : C
this :
  ((unit F H).app (x, z) ≫ (braiding F H).hom.app (x ⊗ z)) ≫ (H ⊛ F).map (β_ z x).inv =
    ((β_ (F.obj x) (H.obj z)).hom ≫ (unit H F).app (z, x) ≫ (H ⊛ F).map (β_ z x).hom) ≫ (H ⊛ F).map (β_ z x).inv
⊢ ((β_ (F.obj x) (H.obj z)).hom ≫ (unit H F).app (z, x)) ▷ G.obj y ≫
      (unit (H ⊛ F) G).app (z ⊗ x, y) ≫ ((H ⊛ F) ⊛ G).map ((α_ z x y).hom ≫ (β_ z (x ⊗ y)).hom ≫ (α_ x y z).hom) =
    (unit F H).app (x, z) ▷ G.obj y ≫
      (braiding F H).hom.app (x ⊗ z) ▷ G.obj y ≫
        (unit (H ⊛ F) G).app (x ⊗ z, y) ≫ ((H ⊛ F) ⊛ G).map ((α_ x z y).hom ≫ x ◁ (β_ z y).hom)
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
⊢ (tensorFunc C).map f ≫ (normalizeIsoAux C Y).hom = (normalizeIsoAux C X).hom ≫ (normalize' C).map f

Tactic:
ext ⟨n⟩

Goal state after:
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
n : NormalMonoidalObject C
⊢ ((tensorFunc C).map f ≫ (normalizeIsoAux C Y).hom).app { as := n } =
    ((normalizeIsoAux C X).hom ≫ (normalize' C).map f).app { as := n }
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)
⊢ ((α_ R.X P.X S.X).hom ≫ R.X ◁ P.actRight) ≫ P.actLeft = P.actLeft ▷ S.X ≫ P.actRight

Tactic:
slice_rhs 1 2 => rw [middle_assoc]

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)
⊢ ((α_ R.X P.X S.X).hom ≫ R.X ◁ P.actRight) ≫ P.actLeft = (α_ R.X P.X S.X).hom ≫ R.X ◁ P.actRight ≫ P.actLeft
Module: Mathlib.CategoryTheory.Presentable.Dense

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

Tactic:
exact ⟨(Functor.Final.isColimitWhiskerEquiv (F := p.toCostructuredArrow) _).1
      (IsColimit.ofIsoColimit p.isColimit (Cocone.ext (Iso.refl _)))⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
H : P ≤ isFinitelyPresentable C
inst✝ : IsFinitelyAccessibleCategory C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P W
incl : P.FullSubcategory ⥤ (isFinitelyPresentable C).FullSubcategory := ιOfLE H
d : CostructuredArrow (isFinitelyPresentable C).ι X
⊢ ∃ c, Nonempty (d ⟶ (CostructuredArrow.pre incl (isFinitelyPresentable C).ι X).obj c)

Tactic:
obtain ⟨W, u, v, huv, hW⟩ := hfac d.hom

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
H : P ≤ isFinitelyPresentable C
inst✝ : IsFinitelyAccessibleCategory C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P W
incl : P.FullSubcategory ⥤ (isFinitelyPresentable C).FullSubcategory := ιOfLE H
d : CostructuredArrow (isFinitelyPresentable C).ι X
W : C
u : (isFinitelyPresentable C).ι.obj d.left ⟶ W
v : W ⟶ X
huv : u ≫ v = d.hom
hW : P W
⊢ ∃ c, Nonempty (d ⟶ (CostructuredArrow.pre incl (isFinitelyPresentable C).ι X).obj c)
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
hf : P.localEpi f
Z : C
⊢ P.isoClosure Z → Function.Injective fun g ↦ f ≫ g

Tactic:
⟨T, hT, ⟨e⟩⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : P.localEpi f
Z T : C
hT : P T
e : Z ≅ T
⊢ Function.Injective fun g ↦ f ≫ g
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ IsArtinianObject X ↔ ∀ (F : ℕ ⥤ (MonoOver X)ᵒᵖ), IsFiltered.IsEventuallyConstant F

Tactic:
by
  rw [isArtinianObject_iff_antitone_chain_condition]
  refine ⟨fun h G ↦ ?_, fun h F ↦ ?_⟩
  · obtain ⟨n, hn⟩ := h ⟨_, (G ⋙ (Subobject.equivMonoOver X).inverse.op ⋙
      (orderDualEquivalence _).inverse).monotone⟩
    refine ⟨n, fun m hm ↦ ?_⟩
    rw [← isIso_unop_iff, MonoOver.isIso_iff_subobjectMk_eq]
    exact (hn m (leOfHom hm)).symm
  · obtain ⟨n, hn⟩ := h (F.monotone.functor ⋙ (orderDualEquivalence _).functor ⋙
      Subobject.representative.op)
    refine ⟨n, fun m hm ↦ Eq.symm ?_⟩
    simpa [isIso_op_iff, isIso_iff_of_reflects_iso, PartialOrder.isIso_iff_eq]
      using hn (homOfLE hm)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Comma

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} D
F₁ : C₁ ⥤ D
F₂ : C₂ ⥤ D
P₁ : ObjectProperty C₁
P₂ : ObjectProperty C₂
inst✝² : ObjectProperty.EssentiallySmall.{w, v_1, u_1} P₁
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} P₂
inst✝ : LocallySmall.{w, v_3, u_3} D
Q₁ : ObjectProperty C₁
w✝¹ : ObjectProperty.Small.{w, v_1, u_1} Q₁
h₁ : Q₁ ≤ P₁
h₁' : P₁ ≤ Q₁.isoClosure
Q₂ : ObjectProperty C₂
w✝ : ObjectProperty.Small.{w, v_2, u_2} Q₂
h₂ : Q₂ ≤ P₂
h₂' : P₂ ≤ Q₂.isoClosure
f : Comma F₁ F₂
hf : P₁ f.left ∧ P₂ f.right
X₁ : C₁
hX₁ : Q₁ X₁
e₁ : f.left ≅ X₁
X₂ : C₂
hX₂ : Q₂ X₂
e₂ : f.right ≅ X₂
⊢ comma F₁ F₂ Q₁ Q₂ { left := X₁, right := X₂, hom := F₁.map e₁.inv ≫ f.hom ≫ F₂.map e₂.hom }

Tactic:
by tauto

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
⊢ HasColimitsOfShape J (CardinalDirectedPoset κ)

Tactic:
have := isFiltered_of_isCardinalFiltered J κ
    infer_instance

Goal state after:
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
h :
  (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) x =
    (ConcreteCategory.hom (hc.desc ((forget PartOrdEmb).mapCocone s))) y
⊢ x = y

Tactic:
by
    obtain ⟨j, x', y', rfl, rfl⟩ :=
      Types.FilteredColimit.jointly_surjective_of_isColimit₂ hc x y
    obtain rfl := (s.ι.app j).injective
      (((ConcreteCategory.congr_hom (hc.fac ((forget _).mapCocone s) j) x').symm.trans h).trans
        (ConcreteCategory.congr_hom (hc.fac ((forget _).mapCocone s) j) y'))
    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
F : Mat_ C ⥤ D
inst✝ : F.Additive
M : Mat_ C
i : M.ι
⊢ (additiveObjIsoBiproduct F M).hom ≫ biproduct.π (fun i ↦ F.obj ((embedding C).obj (M.X i))) i =
    F.map (M.isoBiproductEmbedding.hom ≫ biproduct.π (fun i ↦ (embedding C).obj (M.X i)) i)

Tactic:
dsimp [additiveObjIsoBiproduct]
  rw [biproduct.lift_π, Category.assoc]
  erw [biproduct.lift_π, ← F.map_comp]
  simp

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

Goal state before:
pp: J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
prop_id : D.W (𝟙 e)
h₁ : ∀ ⦃j : J⦄, D.P j → ∃ lift, D.W lift
h₂ : ∀ ⦃j : J⦄, D.P j → ∀ (l₁ l₂ : j ⟶ e), D.W l₁ → D.W l₂ → l₁ = l₂
h₃ : ∀ ⦃i j : J⦄ (f : i ⟶ j), D.W f → ∃ li lj, D.W li ∧ D.W lj ∧ f ≫ lj = li
i✝ j✝ : J
x✝ : i✝ ⟶ j✝
hf : D.W x✝
li : i✝ ⟶ e
lj : j✝ ⟶ e
hli : D.W li
hlj : D.W lj
fac : x✝ ≫ lj = li
⊢ x✝ ≫ ⋯.choose = ⋯.choose

Tactic:
h₂ (D.src hf) _ li (h₁ (D.src hf)).choose_spec hli,

Goal state after:
J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
prop_id : D.W (𝟙 e)
h₁ : ∀ ⦃j : J⦄, D.P j → ∃ lift, D.W lift
h₂ : ∀ ⦃j : J⦄, D.P j → ∀ (l₁ l₂ : j ⟶ e), D.W l₁ → D.W l₂ → l₁ = l₂
h₃ : ∀ ⦃i j : J⦄ (f : i ⟶ j), D.W f → ∃ li lj, D.W li ∧ D.W lj ∧ f ≫ lj = li
i✝ j✝ : J
x✝ : i✝ ⟶ j✝
hf : D.W x✝
li : i✝ ⟶ e
lj : j✝ ⟶ e
hli : D.W li
hlj : D.W lj
fac : x✝ ≫ lj = li
⊢ x✝ ≫ ⋯.choose = li
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
D₁ : Diagram J κ
top : J
h₁ : D₁.IsTerminal top
h₁' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
top' : J
h₂ : D₁.IsTerminal top'
h₂' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top'
hW :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' }.W =
    { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' }.W
hP :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' }.P =
    { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' }.P
⊢ { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' } =
    { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' }

Tactic:
obtain rfl : top = top' := h₂' _ h₁

Goal state after:
J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
D₁ : Diagram J κ
top : J
h₁ : D₁.IsTerminal top
h₁' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
h₂ : D₁.IsTerminal top
h₂' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
hW :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' }.W =
    { toDiagram := D₁, top := top, isTerminal := h₂, uniq_terminal := h₂' }.W
hP :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' }.P =
    { toDiagram := D₁, top := top, isTerminal := h₂, uniq_terminal := h₂' }.P
⊢ { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' } =
    { toDiagram := D₁, top := top, isTerminal := h₂, uniq_terminal := h₂' }
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
S : Subtype (J.PropSetWithTop κ')
x✝ : ↑↑S
⊢ ↑x✝ ≤ ⊤

Tactic:
exact le_top

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
K : Type u
α : K → Subtype (J.PropSetWithTop κ')
hK : HasCardinalLT K κ'
hκ' : Cardinal.aleph0 ≤ κ'
⊢ ∃ j, ∀ (k : K), α k ≤ j

Tactic:
refine ⟨⟨(⋃ (k : K), α k) ∪ {⊤},
      hasCardinalLT_union hκ' (hasCardinalLT_iUnion _ hK (fun k ↦ (α k).property.left))
        (hasCardinalLT_of_finite _ _ hκ'), by simp⟩, fun k ↦ ?_⟩

Goal state after:
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
K : Type u
α : K → Subtype (J.PropSetWithTop κ')
hK : HasCardinalLT K κ'
hκ' : Cardinal.aleph0 ≤ κ'
k : K
⊢ α k ≤ ⟨(⋃ k, ↑(α k)) ∪ {⊤}, ⋯⟩
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
inst✝ : PartialOrder X
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
hm : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂) (C : SetCardinalLT κ₁ ↑B) (hC : C ∈ Y B hB), ∀ b ∈ ↑C, ↑b ≤ m B hB C hC
A : Set X
hA : HasCardinalLT (↑A) κ₂
this :
  ∀ ⦃K : Type w⦄ (j : κ₁.ord.ToType) (f : K → ↑(transfiniteIterate (φ Y m) j A)),
    HasCardinalLT K κ₁ → ∃ x, ∀ (k : K), ↑(f k) ≤ ↑x
K : Type w
f : K → ↑(⋃ j, transfiniteIterate (φ Y m) j A)
hK : HasCardinalLT K κ₁
k : K
⊢ ∃ j, ↑(f k) ∈ transfiniteIterate (φ Y m) j A

Tactic:
simpa only [Set.mem_iUnion] using (f k).prop

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

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
⊢ Monotone Subtype.val

Tactic:
by tauto

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

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
x✝ : IsCardinalPresentable X κ
this✝ :
  ∀ (J : Type u) [inst : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J (coyoneda.obj (op X))
A : Set X
hA : HasCardinalLT (↑A) κ
f : (HasCardinalLT.Set.functor X κ ⋙ coyoneda.obj (op X)).obj ⟨A, hA⟩
hf : (hom (((coyoneda.obj (op X)).mapCocone (HasCardinalLT.Set.cocone X κ)).ι.app ⟨A, hA⟩)) f = 𝟙 X
x : X
this :
  (hom ((hom (((coyoneda.obj (op X)).mapCocone (HasCardinalLT.Set.cocone X κ)).ι.app ⟨A, hA⟩)) f)) x = (hom (𝟙 X)) x
⊢ x ∈ A ↔ x ∈ Set.univ

Tactic:
dsimp at this

Goal state after:
X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
x✝ : IsCardinalPresentable X κ
this✝ :
  ∀ (J : Type u) [inst : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J (coyoneda.obj (op X))
A : Set X
hA : HasCardinalLT (↑A) κ
f : (HasCardinalLT.Set.functor X κ ⋙ coyoneda.obj (op X)).obj ⟨A, hA⟩
hf : (hom (((coyoneda.obj (op X)).mapCocone (HasCardinalLT.Set.cocone X κ)).ι.app ⟨A, hA⟩)) f = 𝟙 X
x : X
this : ↑((hom f) x) = x
⊢ x ∈ A ↔ x ∈ Set.univ