awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : P ≤ isFinitelyPresentable C
inst_1 : LocallySmall.{w, v, u} C
X : C
J : Type w
Jc : SmallCategory J
Jf : IsFiltered J
pres : ColimitPresentation.{w, w, v, u} J X
K : (i : J) → Type w
Kc : (i : J) → SmallCategory (K i)
Kf : ∀ (i : J), IsFiltered.{w, w} (K i)
pres' : (i : J) → ColimitPresentation.{w, w, v, u} (K i) (pres.diag.obj i)
hp : ∀ (i : J) (i_1 : K i), P ((pres' i).diag.obj i_1)
this : ∀ (j : J) (i : K j), IsFinitelyPresentable.{w, v, u} ((pres' j).diag.obj i)
⊢ IsFiltered.{w, w} (ShrinkHoms.{w} (ColimitPresentation.Total (I := K) pres'))

Tactic:
have := IsFiltered.of_equivalence (ShrinkHoms.equivalence (ColimitPresentation.Total pres'))
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : P ≤ isFinitelyPresentable C
inst_1 : LocallySmall.{w, v, u} C
X : C
J : Type w
Jc : SmallCategory J
Jf : IsFiltered J
pres : ColimitPresentation.{w, w, v, u} J X
K : (i : J) → Type w
Kc : (i : J) → SmallCategory (K i)
Kf : ∀ (i : J), IsFiltered.{w, w} (K i)
pres' : (i : J) → ColimitPresentation.{w, w, v, u} (K i) (pres.diag.obj i)
hp : ∀ (i : J) (i_1 : K i), P ((pres' i).diag.obj i_1)
this_1 : ∀ (j : J) (i : K j), IsFinitelyPresentable.{w, v, u} ((pres' j).diag.obj i)
this : IsFiltered.{w, w} (ShrinkHoms.{w} (ColimitPresentation.Total (I := K) pres'))
k : ShrinkHoms.{w} (ColimitPresentation.Total (I := K) pres')
⊢ P
    (Functor.obj
      (ColimitPresentation.diag
        ((pres.bind (I := K) pres').reindex
          (Equivalence.inverse (ShrinkHoms.equivalence (ColimitPresentation.Total (I := K) pres')))))
      k)

Tactic:
simp [hp]
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : P ≤ isFinitelyPresentable C
inst_1 : LocallySmall.{w, v, u} C
X : C
J : Type w
Jc : SmallCategory J
Jf : IsFiltered J
pres : ColimitPresentation.{w, w, v, u} J X
K : (i : J) → Type w
Kc : (i : J) → SmallCategory (K i)
Kf : ∀ (i : J), IsFiltered.{w, w} (K i)
pres' : (i : J) → ColimitPresentation.{w, w, v, u} (K i) (pres.diag.obj i)
hp : ∀ (i : J) (i_1 : K i), P ((pres' i).diag.obj i_1)
this_1 : ∀ (j : J) (i : K j), IsFinitelyPresentable.{w, v, u} ((pres' j).diag.obj i)
this : IsFiltered.{w, w} (ShrinkHoms.{w} (ColimitPresentation.Total (I := K) pres'))
⊢ P.ind X

Tactic:
exact ⟨_, inferInstance, inferInstance,
    (pres.bind pres').reindex (ShrinkHoms.equivalence _).inverse, fun k ↦ by simp [hp]⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X : C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
inst_2 : EssentiallySmall.{w, v_1, u_1} J
inst_3 : IsFiltered.{v_1, u_1} J
pres : ColimitPresentation.{v_1, u_1, v, u} J X
h : ∀ (i : J), P (pres.diag.obj i)
⊢ P.ind X

Tactic:
⟨SmallModel J, inferInstance, .of_equivalence (equivSmallModel _),
    pres.reindex (equivSmallModel _).inverse, fun _ ↦ h _⟩

Premises used: inferInstance, CategoryTheory.IsFiltered.of_equivalence, Exists.intro, CategoryTheory.SmallModel, CategoryTheory.Limits.ColimitPresentation.reindex, CategoryTheory.ObjectProperty.ind, CategoryTheory.Functor.obj, CategoryTheory.equivSmallModel, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
H : P ≤ isFinitelyPresentable C
inst_1 : IsFinitelyAccessibleCategory.{w, v, u} C
X : C
⊢ P.ind X ↔
    ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable.{w, v, u} Z], ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W

Tactic:
⟨fun ⟨J, _, _, pres, h⟩ Z g hZ ↦ ?_, fun hfac ↦ ?_⟩

Premises used: Exists, And, Iff.intro, CategoryTheory.CategoryStruct.comp, Eq, _private.0.CategoryTheory.ObjectProperty.ind_iff_exists.match_1
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
H : P ≤ isFinitelyPresentable C
inst_1 : IsFinitelyAccessibleCategory.{w, v, u} C
X : C
refine_1 :
  P.ind X →
    ∀ (Z : C) (g : Z ⟶ X) (hZ : IsFinitelyPresentable.{w, v, u} Z) (J : Type w) (w : SmallCategory J),
      IsFiltered J →
        ∀ (pres : ColimitPresentation.{w, w, v, u} J X) (h : ∀ (i : J), P (pres.diag.obj i)),
          ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W
refine_2 :
  ∀
    (hfac :
      ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable.{w, v, u} Z], ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W),
    P.ind X
⊢ P.ind X ↔
    ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable.{w, v, u} Z], ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W

Tactic:
refine ⟨fun ⟨J, _, _, pres, h⟩ Z g hZ ↦ ?_, fun hfac ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
H : P ≤ isFinitelyPresentable C
inst_1 : IsFinitelyAccessibleCategory.{w, v, u} C
X : C
h_1 : P.ind X
Z : C
g : Z ⟶ X
hZ : IsFinitelyPresentable.{w, v, u} Z
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
pres : ColimitPresentation.{w, w, v, u} J X
h : ∀ (i : J), P (pres.diag.obj i)
⊢ IsFinitelyPresentable.{w, v, u} Z

Tactic:
have : IsFinitelyPresentable Z := hZ
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
H : P ≤ isFinitelyPresentable C
inst_1 : IsFinitelyAccessibleCategory.{w, v, u} C
X : C
h_1 : P.ind X
Z : C
g : Z ⟶ X
hZ : IsFinitelyPresentable.{w, v, u} Z
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
pres : ColimitPresentation.{w, w, v, u} J X
h : ∀ (i : J), P (pres.diag.obj i)
this : IsFinitelyPresentable.{w, v, u} Z
refine_1 :
  ∀ (j : J) (u : Z ⟶ pres.diag.obj j) (hcomp : u ≫ { pt := X, ι := pres.ι : Cocone pres.diag }.ι.app j = g),
    ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W
⊢ ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W

Tactic:
obtain ⟨j, u, hcomp⟩ := IsFinitelyPresentable.exists_hom_of_isColimit pres.isColimit g

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
H : P ≤ isFinitelyPresentable C
inst_1 : IsFinitelyAccessibleCategory.{w, v, u} C
X : C
h_1 : P.ind X
Z : C
g : Z ⟶ X
hZ : IsFinitelyPresentable.{w, v, u} Z
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
pres : ColimitPresentation.{w, w, v, u} J X
h : ∀ (i : J), P (pres.diag.obj i)
this : IsFinitelyPresentable.{w, v, u} Z
j : J
u : Z ⟶ pres.diag.obj j
hcomp : u ≫ { pt := X, ι := pres.ι : Cocone pres.diag }.ι.app j = g
⊢ ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W

Tactic:
⟨_, u, pres.ι.app j, hcomp, h j⟩

Premises used: CategoryTheory.Limits.ColimitPresentation.ι, And.intro, Exists.intro, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
H : P ≤ isFinitelyPresentable C
inst_1 : IsFinitelyAccessibleCategory.{w, v, u} C
X : C
h_1 : P.ind X
Z : C
g : Z ⟶ X
hZ : IsFinitelyPresentable.{w, v, u} Z
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
pres : ColimitPresentation.{w, w, v, u} J X
h : ∀ (i : J), P (pres.diag.obj i)
this : IsFinitelyPresentable.{w, v, u} Z
j : J
u : Z ⟶ pres.diag.obj j
hcomp : u ≫ { pt := X, ι := pres.ι : Cocone pres.diag }.ι.app j = g
⊢ ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W

Tactic:
exact ⟨_, u, pres.ι.app j, hcomp, h j⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
H : P ≤ isFinitelyPresentable C
inst_1 : IsFinitelyAccessibleCategory.{w, v, u} C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable.{w, v, u} Z], ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W
incl : Functor.{v, v, u, u} P.FullSubcategory (FullSubcategory.{v, u} (isFinitelyPresentable C)) :=
  ιOfLE (P := P) (P' := isFinitelyPresentable C) H
d :
  CostructuredArrow.{v, v, u, u} (C := FullSubcategory.{v, u} (isFinitelyPresentable C)) (ι (isFinitelyPresentable C)) X
obtain :
  ∀ (W : C) (u : Functor.obj (ι (isFinitelyPresentable C)) d.left ⟶ W) (v : W ⟶ X) (huv : u ≫ v = d.hom) (hW : P W),
    ∃ (c : CostructuredArrow (incl ⋙ ι (isFinitelyPresentable C)) X),
      Nonempty.{v + 1} (d ⟶ (CostructuredArrow.pre incl (ι (isFinitelyPresentable C)) X).obj c)
⊢ ∃ (c : CostructuredArrow (incl ⋙ ι (isFinitelyPresentable C)) X),
    Nonempty.{v + 1} (d ⟶ (CostructuredArrow.pre incl (ι (isFinitelyPresentable C)) X).obj c)

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

Premises used: CategoryTheory.CostructuredArrow.hom
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
H : P ≤ isFinitelyPresentable C
inst_1 : IsFinitelyAccessibleCategory.{w, v, u} C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable.{w, v, u} Z], ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W
incl : Functor.{v, v, u, u} P.FullSubcategory (FullSubcategory.{v, u} (isFinitelyPresentable C)) :=
  ιOfLE (P := P) (P' := isFinitelyPresentable C) H
d :
  CostructuredArrow.{v, v, u, u} (C := FullSubcategory.{v, u} (isFinitelyPresentable C)) (ι (isFinitelyPresentable C)) X
W : C
u : Functor.obj (ι (isFinitelyPresentable C)) d.left ⟶ W
v : W ⟶ X
huv : u ≫ v = d.hom
hW : P W
⊢ ∃ (c : CostructuredArrow (incl ⋙ ι (isFinitelyPresentable C)) X),
    Nonempty.{v + 1} (d ⟶ (CostructuredArrow.pre incl (ι (isFinitelyPresentable C)) X).obj c)

Tactic:
⟨CostructuredArrow.mk (Y := FullSubcategory.mk _ hW) v,
        ⟨CostructuredArrow.homMk ⟨u⟩ huv⟩⟩

Premises used: CategoryTheory.CostructuredArrow.homMk, Nonempty.intro, Exists.intro, CategoryTheory.InducedCategory.Hom.mk, CategoryTheory.CostructuredArrow.mk
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
H : P ≤ isFinitelyPresentable C
inst_1 : IsFinitelyAccessibleCategory.{w, v, u} C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable.{w, v, u} Z], ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W
incl : Functor.{v, v, u, u} P.FullSubcategory (FullSubcategory.{v, u} (isFinitelyPresentable C)) :=
  ιOfLE (P := P) (P' := isFinitelyPresentable C) H
d :
  CostructuredArrow.{v, v, u, u} (C := FullSubcategory.{v, u} (isFinitelyPresentable C)) (ι (isFinitelyPresentable C)) X
W : C
u : Functor.obj (ι (isFinitelyPresentable C)) d.left ⟶ W
v : W ⟶ X
huv : u ≫ v = d.hom
hW : P W
⊢ ∃ (c : CostructuredArrow (incl ⋙ ι (isFinitelyPresentable C)) X),
    Nonempty.{v + 1} (d ⟶ (CostructuredArrow.pre incl (ι (isFinitelyPresentable C)) X).obj c)

Tactic:
exact ⟨CostructuredArrow.mk (Y := FullSubcategory.mk _ hW) v,
        ⟨CostructuredArrow.homMk ⟨u⟩ huv⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
H : P ≤ isFinitelyPresentable C
inst_1 : IsFinitelyAccessibleCategory.{w, v, u} C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable.{w, v, u} Z], ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W
incl : Functor.{v, v, u, u} P.FullSubcategory (FullSubcategory.{v, u} (isFinitelyPresentable C)) :=
  ιOfLE (P := P) (P' := isFinitelyPresentable C) H
⊢ ∀
    (d :
      CostructuredArrow.{v, v, u, u} (C := FullSubcategory.{v, u} (isFinitelyPresentable C))
        (ι (isFinitelyPresentable C)) X),
    ∃ (c : CostructuredArrow (incl ⋙ ι (isFinitelyPresentable C)) X),
      Nonempty.{v + 1} (d ⟶ (CostructuredArrow.pre incl (ι (isFinitelyPresentable C)) X).obj c)

Tactic:
have H (d : CostructuredArrow (isFinitelyPresentable.{w} C).ι X) : ∃ c,
        Nonempty (d ⟶ (CostructuredArrow.pre incl (isFinitelyPresentable.{w} C).ι X).obj c) := by
      obtain ⟨W, u, v, huv, hW⟩ := hfac d.hom
      exact ⟨CostructuredArrow.mk (Y := FullSubcategory.mk _ hW) v,
        ⟨CostructuredArrow.homMk ⟨u⟩ huv⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
H_1 : P ≤ isFinitelyPresentable C
inst_1 : IsFinitelyAccessibleCategory.{w, v, u} C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable.{w, v, u} Z], ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W
incl : Functor.{v, v, u, u} P.FullSubcategory (FullSubcategory.{v, u} (isFinitelyPresentable C)) :=
  ιOfLE (P := P) (P' := isFinitelyPresentable C) H_1
H :
  ∀
    (d :
      CostructuredArrow.{v, v, u, u} (C := FullSubcategory.{v, u} (isFinitelyPresentable C))
        (ι (isFinitelyPresentable C)) X),
    ∃ (c : CostructuredArrow (incl ⋙ ι (isFinitelyPresentable C)) X),
      Nonempty.{v + 1} (d ⟶ (CostructuredArrow.pre incl (ι (isFinitelyPresentable C)) X).obj c)
⊢ (CostructuredArrow.pre incl (ι (isFinitelyPresentable C)) X).Final

Tactic:
have : (CostructuredArrow.pre incl (isFinitelyPresentable.{w} C).ι X).Final :=
      Functor.final_of_exists_of_isFiltered_of_fullyFaithful (C := CostructuredArrow (incl ⋙ _) X)
        (CostructuredArrow.pre incl (isFinitelyPresentable.{w} C).ι X) H
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
H_1 : P ≤ isFinitelyPresentable C
inst_1 : IsFinitelyAccessibleCategory.{w, v, u} C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable.{w, v, u} Z], ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W
incl : Functor.{v, v, u, u} P.FullSubcategory (FullSubcategory.{v, u} (isFinitelyPresentable C)) :=
  ιOfLE (P := P) (P' := isFinitelyPresentable C) H_1
H :
  ∀
    (d :
      CostructuredArrow.{v, v, u, u} (C := FullSubcategory.{v, u} (isFinitelyPresentable C))
        (ι (isFinitelyPresentable C)) X),
    ∃ (c : CostructuredArrow (incl ⋙ ι (isFinitelyPresentable C)) X),
      Nonempty.{v + 1} (d ⟶ (CostructuredArrow.pre incl (ι (isFinitelyPresentable C)) X).obj c)
this : (CostructuredArrow.pre incl (ι (isFinitelyPresentable C)) X).Final
⊢ IsFiltered (CostructuredArrow P.ι X)

Tactic:
have : IsFiltered (CostructuredArrow P.ι X) :=
      .of_exists_of_isFiltered_of_fullyFaithful (C := CostructuredArrow (incl ⋙ _) X)
        (CostructuredArrow.pre incl (isFinitelyPresentable.{w} C).ι X) H
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
H_1 : P ≤ isFinitelyPresentable C
inst_1 : IsFinitelyAccessibleCategory.{w, v, u} C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable.{w, v, u} Z], ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W
incl : Functor.{v, v, u, u} P.FullSubcategory (FullSubcategory.{v, u} (isFinitelyPresentable C)) :=
  ιOfLE (P := P) (P' := isFinitelyPresentable C) H_1
H :
  ∀
    (d :
      CostructuredArrow.{v, v, u, u} (C := FullSubcategory.{v, u} (isFinitelyPresentable C))
        (ι (isFinitelyPresentable C)) X),
    ∃ (c : CostructuredArrow (incl ⋙ ι (isFinitelyPresentable C)) X),
      Nonempty.{v + 1} (d ⟶ (CostructuredArrow.pre incl (ι (isFinitelyPresentable C)) X).obj c)
this_1 : (CostructuredArrow.pre incl (ι (isFinitelyPresentable C)) X).Final
this : IsFiltered (CostructuredArrow P.ι X)
⊢ P.ι.isDenseAt X

Tactic:
Functor.IsDenseAt.of_final (F := (isFinitelyPresentable.{w} C).ι) incl
        (Functor.IsDense.isDenseAt _ _)

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.comp, CategoryTheory.inducedFunctor, CategoryTheory.InducedCategory, CategoryTheory.Functor.IsDense.isDenseAt, CategoryTheory.Functor.IsDenseAt.of_final, CategoryTheory.ObjectProperty.isFinitelyPresentable
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
H_1 : P ≤ isFinitelyPresentable C
inst_1 : IsFinitelyAccessibleCategory.{w, v, u} C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable.{w, v, u} Z], ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W
incl : Functor.{v, v, u, u} P.FullSubcategory (FullSubcategory.{v, u} (isFinitelyPresentable C)) :=
  ιOfLE (P := P) (P' := isFinitelyPresentable C) H_1
H :
  ∀
    (d :
      CostructuredArrow.{v, v, u, u} (C := FullSubcategory.{v, u} (isFinitelyPresentable C))
        (ι (isFinitelyPresentable C)) X),
    ∃ (c : CostructuredArrow (incl ⋙ ι (isFinitelyPresentable C)) X),
      Nonempty.{v + 1} (d ⟶ (CostructuredArrow.pre incl (ι (isFinitelyPresentable C)) X).obj c)
this_1 : (CostructuredArrow.pre incl (ι (isFinitelyPresentable C)) X).Final
this : IsFiltered (CostructuredArrow P.ι X)
refine_2 : ∀ (hc : P.ι.DenseAt X), P.ind X
⊢ P.ind X

Tactic:
obtain ⟨hc⟩ : P.ι.isDenseAt X :=
      Functor.IsDenseAt.of_final (F := (isFinitelyPresentable.{w} C).ι) incl
        (Functor.IsDense.isDenseAt _ _)

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.isDenseAt
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
H_1 : P ≤ isFinitelyPresentable C
inst_1 : IsFinitelyAccessibleCategory.{w, v, u} C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable.{w, v, u} Z], ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W
incl : Functor.{v, v, u, u} P.FullSubcategory (FullSubcategory.{v, u} (isFinitelyPresentable C)) :=
  ιOfLE (P := P) (P' := isFinitelyPresentable C) H_1
H :
  ∀
    (d :
      CostructuredArrow.{v, v, u, u} (C := FullSubcategory.{v, u} (isFinitelyPresentable C))
        (ι (isFinitelyPresentable C)) X),
    ∃ (c : CostructuredArrow (incl ⋙ ι (isFinitelyPresentable C)) X),
      Nonempty.{v + 1} (d ⟶ (CostructuredArrow.pre incl (ι (isFinitelyPresentable C)) X).obj c)
this_1 : (CostructuredArrow.pre incl (ι (isFinitelyPresentable C)) X).Final
this : IsFiltered (CostructuredArrow P.ι X)
hc : P.ι.DenseAt X
⊢ EssentiallySmall.{w, v, max u v} (CostructuredArrow P.ι X)

Tactic:
have : EssentiallySmall.{w} (CostructuredArrow P.ι X) :=
      essentiallySmall_of_fully_faithful (C := CostructuredArrow (incl ⋙ _) X)
        (CostructuredArrow.pre incl (isFinitelyPresentable.{w} C).ι X)
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
H_1 : P ≤ isFinitelyPresentable C
inst_1 : IsFinitelyAccessibleCategory.{w, v, u} C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable.{w, v, u} Z], ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W
incl : Functor.{v, v, u, u} P.FullSubcategory (FullSubcategory.{v, u} (isFinitelyPresentable C)) :=
  ιOfLE (P := P) (P' := isFinitelyPresentable C) H_1
H :
  ∀
    (d :
      CostructuredArrow.{v, v, u, u} (C := FullSubcategory.{v, u} (isFinitelyPresentable C))
        (ι (isFinitelyPresentable C)) X),
    ∃ (c : CostructuredArrow (incl ⋙ ι (isFinitelyPresentable C)) X),
      Nonempty.{v + 1} (d ⟶ (CostructuredArrow.pre incl (ι (isFinitelyPresentable C)) X).obj c)
this_1 : (CostructuredArrow.pre incl (ι (isFinitelyPresentable C)) X).Final
this_2 : IsFiltered (CostructuredArrow P.ι X)
hc : P.ι.DenseAt X
this : EssentiallySmall.{w, v, max u v} (CostructuredArrow P.ι X)
⊢ P.ind X

Tactic:
of_essentiallySmall_index ⟨_, _, hc⟩ fun Y ↦ Y.left.2

Premises used: CategoryTheory.ObjectProperty.of_essentiallySmall_index, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Limits.ColimitPresentation.mk, CategoryTheory.CostructuredArrow.left
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
H_1 : P ≤ isFinitelyPresentable C
inst_1 : IsFinitelyAccessibleCategory.{w, v, u} C
X : C
hfac : ∀ {Z : C} (g : Z ⟶ X) [IsFinitelyPresentable.{w, v, u} Z], ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W
incl : Functor.{v, v, u, u} P.FullSubcategory (FullSubcategory.{v, u} (isFinitelyPresentable C)) :=
  ιOfLE (P := P) (P' := isFinitelyPresentable C) H_1
H :
  ∀
    (d :
      CostructuredArrow.{v, v, u, u} (C := FullSubcategory.{v, u} (isFinitelyPresentable C))
        (ι (isFinitelyPresentable C)) X),
    ∃ (c : CostructuredArrow (incl ⋙ ι (isFinitelyPresentable C)) X),
      Nonempty.{v + 1} (d ⟶ (CostructuredArrow.pre incl (ι (isFinitelyPresentable C)) X).obj c)
this_1 : (CostructuredArrow.pre incl (ι (isFinitelyPresentable C)) X).Final
this_2 : IsFiltered (CostructuredArrow P.ι X)
hc : P.ι.DenseAt X
this : EssentiallySmall.{w, v, max u v} (CostructuredArrow P.ι X)
⊢ P.ind X

Tactic:
exact of_essentiallySmall_index ⟨_, _, hc⟩ fun Y ↦ Y.left.2

Premises used: CategoryTheory.ObjectProperty.of_essentiallySmall_index, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Limits.ColimitPresentation.mk, CategoryTheory.CostructuredArrow.left
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{u_2, u_1} D
P : ObjectProperty.{u_2, u_1} D
F : Functor.{v, u_2, u, u_1} C D
inst_2 : PreservesFilteredColimitsOfSize.{w, w, v, u_2, u, u_1} F
X : C
this :
  ∀ (J : Type w) (w : SmallCategory J),
    IsFiltered J →
      ∀ (pres : ColimitPresentation.{w, w, v, u} J X) (h : ∀ (i : J), P.inverseImage F (pres.diag.obj i)),
        P.ind.inverseImage F X
⊢ (P.inverseImage F).ind X ≤ P.ind.inverseImage F X

Tactic:
⟨J, _, _, pres, h⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{u_2, u_1} D
P : ObjectProperty.{u_2, u_1} D
F : Functor.{v, u_2, u, u_1} C D
inst_2 : PreservesFilteredColimitsOfSize.{w, w, v, u_2, u, u_1} F
X : C
J : Type w
w_1 : SmallCategory J
w_2 : IsFiltered J
pres : ColimitPresentation.{w, w, v, u} J X
h : ∀ (i : J), P.inverseImage F (pres.diag.obj i)
w : Type w
w₁ : SmallCategory J
w₂ : IsFiltered J
w₃ : ColimitPresentation.{w, w, u_2, u_1} J (F.obj X)
h₁ : ∀ (i : J), P ((pres.map F).diag.obj i)
⊢ P.ind (F.obj X)

Tactic:
use J, inferInstance, inferInstance, pres.map F, h

Premises used: CategoryTheory.Limits.ColimitPresentation.map
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{u_2, u_1} D
P : ObjectProperty.{u_2, u_1} D
F : Functor.{v, u_2, u, u_1} C D
inst_2 : P.IsClosedUnderIsomorphisms
inst_3 : F.IsEquivalence
⊢ (P.inverseImage F).ind = P.ind.inverseImage F

Tactic:
le_antisymm (ind_inverseImage_le _ _) fun X ⟨J, _, _, pres, h⟩ ↦ ?_

Premises used: _private.0.CategoryTheory.ObjectProperty.ind_inverseImage_eq_of_isEquivalence.match_1, le_antisymm, CategoryTheory.ObjectProperty.ind, CategoryTheory.ObjectProperty.inverseImage, CategoryTheory.ObjectProperty.ind_inverseImage_le
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{u_2, u_1} D
P : ObjectProperty.{u_2, u_1} D
F : Functor.{v, u_2, u, u_1} C D
inst_2 : P.IsClosedUnderIsomorphisms
inst_3 : F.IsEquivalence
refine :
  ∀ (X : C),
    P.ind.inverseImage F X →
      ∀ (J : Type w) (w : SmallCategory J),
        IsFiltered J →
          ∀ (pres : ColimitPresentation.{w, w, u_2, u_1} J (F.obj X)) (h : ∀ (i : J), P (pres.diag.obj i)),
            (P.inverseImage F).ind X
⊢ (P.inverseImage F).ind = P.ind.inverseImage F

Tactic:
refine le_antisymm (ind_inverseImage_le _ _) fun X ⟨J, _, _, pres, h⟩ ↦ ?_

Premises used: le_antisymm, CategoryTheory.ObjectProperty.ind_inverseImage_le
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{u_2, u_1} D
P : ObjectProperty.{u_2, u_1} D
F : Functor.{v, u_2, u, u_1} C D
inst_2 : P.IsClosedUnderIsomorphisms
inst_3 : F.IsEquivalence
X : C
h_1 : P.ind.inverseImage F X
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
pres : ColimitPresentation.{w, w, u_2, u_1} J (F.obj X)
h : ∀ (i : J), P (pres.diag.obj i)
⊢ (P.inverseImage F).ind X

Tactic:
⟨J, ‹_›, ‹_›, .ofIso (pres.map F.asEquivalence.inverse) ?_, fun j ↦ ?_⟩

Premises used: Exists.intro, CategoryTheory.ObjectProperty.ind