awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits (goal)
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
K' : Type u_6
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_2, u_6} K'
inst_2 : Category.{v_3, u_1} J
inst_3 : Category.{v_5, u_3} C
e : Equivalence.{v_1, v_2, u_5, u_6} K K'
⊢ Eq (α := ObjectProperty (Functor.{v_3, v_5, u_1, u_3} J C)) (preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K)
    (preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_2, u_6} K')
have h : ∀ (G : Functor.{v_3, v_5, u_1, u_3} J C),
  preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K G ↔ preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_2, u_6} K' G
Tactic: ext G
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits (goal)
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
⊢ Eq (α := ObjectProperty (Functor.{v_3, v_5, u_1, u_3} J C))
    (preservesColimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K)
    (⨅ (F : Functor.{v_1, v_3, u_5, u_1} K J), preservesColimit F)
have h : ∀ (G : Functor.{v_3, v_5, u_1, u_3} J C),
  preservesColimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K G ↔
    (⨅ (F : Functor.{v_1, v_3, u_5, u_1} K J), preservesColimit F) G
Tactic: ext G
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits (goal)
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
G : Functor.{v_3, v_5, u_1, u_3} J C
⊢ preservesColimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K G ↔
    (⨅ (F : Functor.{v_1, v_3, u_5, u_1} K J), preservesColimit F) G
have h : PreservesColimitsOfShape.{v_1, u_5, v_3, v_5, u_1, u_3} K G ↔
  ∀ (i : Functor.{v_1, v_3, u_5, u_1} K J), PreservesColimit i G
Tactic: simp only [preservesColimitsOfShape_iff, iInf_apply, preservesColimit_iff, iInf_Prop_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits (goal)
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
K' : Type u_6
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_2, u_6} K'
inst_2 : Category.{v_3, u_1} J
inst_3 : Category.{v_5, u_3} C
e : Equivalence.{v_1, v_2, u_5, u_6} K K'
⊢ Eq (α := ObjectProperty (Functor.{v_3, v_5, u_1, u_3} J C))
    (preservesColimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K)
    (preservesColimitsOfShape.{v_3, u_1, v_5, u_3, v_2, u_6} K')
have h : ∀ (G : Functor.{v_3, v_5, u_1, u_3} J C),
  preservesColimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K G ↔
    preservesColimitsOfShape.{v_3, u_1, v_5, u_3, v_2, u_6} K' G
Tactic: ext G
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits (hypothesis)
Goal:
J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_2, u_6} K'
inst_2 : Category.{v_3, u_1} J
inst_3 : Category.{v_4, u_2} J'
inst_4 : Category.{v_5, u_3} C
inst_5 : Category.{v_6, u_4} D
inst_6 : HasColimitsOfShape.{v_2, u_6, v_5, u_3} K' C
inst_7 : PreservesLimitsOfShape (C := Functor.{v_2, v_5, u_6, u_3} K' C) K colim
G : Functor.{v_3, v_5, u_1, u_3} J C
h : ColimitOfShape (preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K) K' G
⊢ preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K G
have this : ∀ (j : K'),
  preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K
    (h.toColimitPresentation (P := preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K).diag.obj j)
Tactic: have := h.prop_diag_obj
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits (hypothesis)
Goal:
J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_2, u_6} K'
inst_2 : Category.{v_3, u_1} J
inst_3 : Category.{v_4, u_2} J'
inst_4 : Category.{v_5, u_3} C
inst_5 : Category.{v_6, u_4} D
inst_6 : HasColimitsOfShape.{v_2, u_6, v_5, u_3} K' C
inst_7 : PreservesLimitsOfShape (C := Functor.{v_2, v_5, u_6, u_3} K' C) K colim
G : Functor.{v_3, v_5, u_1, u_3} J C
h : ColimitOfShape (preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K) K' G
this :
  ∀ (j : K'),
    preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K
      (h.toColimitPresentation (P := preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K).diag.obj j)
⊢ preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K G
have this₁ : PreservesLimitsOfShape K
  h.toColimitPresentation (P := preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K).diag.flip
Tactic: have : PreservesLimitsOfShape K h.diag.flip := ⟨fun {F} ↦ ⟨fun {c} hc ↦
      ⟨evaluationJointlyReflectsLimits _
        (fun k' ↦ isLimitOfPreserves (h.diag.obj k') hc)⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits (hypothesis)
Goal:
J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_2, u_6} K'
inst_2 : Category.{v_3, u_1} J
inst_3 : Category.{v_4, u_2} J'
inst_4 : Category.{v_5, u_3} C
inst_5 : Category.{v_6, u_4} D
inst_6 : HasColimitsOfShape.{v_2, u_6, v_5, u_3} K' C
inst_7 : HasExactColimitsOfShape.{v_5, v_2, u_3, u_6} K' C
G : Functor.{v_3, v_5, u_1, u_3} J C
h : ColimitOfShape preservesFiniteLimits K' G
⊢ preservesFiniteLimits G
have this : ∀ (j : K'), preservesFiniteLimits (h.toColimitPresentation (P := preservesFiniteLimits).diag.obj j)
Tactic: have := h.prop_diag_obj
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
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
⊢ P.ind.ind = P.ind
have refine : ∀ (X : C) (h : P.ind.ind X), P.ind X
Tactic: refine le_antisymm (fun X h ↦ ?_) (le_ind P.ind)
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h_1 : P ≤ isFinitelyPresentable C
inst_1 : LocallySmall.{w, v, u} C
X : C
h : P.ind.ind X
⊢ P.ind X
have choose : ∀ (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)), P.ind X
Tactic: choose J Jc Jf pres K Kc Kf pres' hp using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (hypothesis)
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)
⊢ P.ind X
have this : ∀ (j : J) (i : K j), IsFinitelyPresentable.{w, v, u} ((pres' j).diag.obj i)
Tactic: have (j : J) (i : K j) : IsFinitelyPresentable ((pres' j).diag.obj i) := h _ (hp _ _)
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (hypothesis)
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)
⊢ P.ind X
have this₁ : IsFiltered.{w, w} (ShrinkHoms.{w} (ColimitPresentation.Total (I := K) pres'))
Tactic: have := IsFiltered.of_equivalence (ShrinkHoms.equivalence (ColimitPresentation.Total pres'))
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
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
have 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
Tactic: refine ⟨fun ⟨J, _, _, pres, h⟩ Z g hZ ↦ ?_, fun hfac ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
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
⊢ 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
have 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
Tactic: refine ⟨fun ⟨J, _, _, pres, h⟩ Z g hZ ↦ ?_, fun hfac ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
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
⊢ ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ X), u ≫ v = g ∧ P W
have 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
Tactic: obtain ⟨j, u, hcomp⟩ := IsFinitelyPresentable.exists_hom_of_isColimit pres.isColimit g
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
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)
have 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)
Tactic: obtain ⟨W, u, v, huv, hW⟩ := hfac d.hom
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (hypothesis)
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
⊢ P.ind X
have 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⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (hypothesis)
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)
⊢ P.ind X
have this : (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
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (hypothesis)
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
⊢ P.ind X
have this₁ : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
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.ind X
have refine_2 : ∀ (hc : P.ι.DenseAt X), P.ind X
Tactic: obtain ⟨hc⟩ : P.ι.isDenseAt X :=
      Functor.IsDenseAt.of_final (F := (isFinitelyPresentable.{w} C).ι) incl
        (Functor.IsDense.isDenseAt _ _)
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (hypothesis)
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
⊢ P.ind X
have this₁ : 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)
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
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
⊢ (P.inverseImage F).ind X ≤ P.ind.inverseImage F X
have 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
Tactic: ⟨J, _, _, pres, h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
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
⊢ P.ind (F.obj X)
have w₃ : ColimitPresentation.{w, w, u_2, u_1} J (F.obj X)
Tactic: use J, inferInstance, inferInstance, pres.map F, h
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
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)
⊢ P.ind (F.obj X)
have h₁ : ∀ (i : J), P ((pres.map F).diag.obj i)
Tactic: use J, inferInstance, inferInstance, pres.map F, h
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
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
have 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
Tactic: refine le_antisymm (ind_inverseImage_le _ _) fun X ⟨J, _, _, pres, h⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
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
have refine_1 : F.asEquivalence.inverse.obj (F.obj X) ≅ X
Tactic: refine ⟨J, ‹_›, ‹_›, .ofIso (pres.map F.asEquivalence.inverse) ?_, fun j ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
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)
refine_1 : F.asEquivalence.inverse.obj (F.obj X) ≅ X
⊢ (P.inverseImage F).ind X
have refine_2 : ∀ (j : J), P.inverseImage F (((pres.map F.asEquivalence.inverse).ofIso (F.asEquivalence.unitIso.app X).symm).diag.obj j)
Tactic: refine ⟨J, ‹_›, ‹_›, .ofIso (pres.map F.asEquivalence.inverse) ?_, fun j ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
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
e : Equivalence.{v, u_2, u, u_1} C D
inst_2 : P.IsClosedUnderIsomorphisms
X : D
⊢ (∃ (J : Type w) (x : SmallCategory J) (_ : IsFiltered J) (pres :
      ColimitPresentation.{w, w, v, u} J (e.inverse.obj X)), ∀ (i : J), P.inverseImage e.functor (pres.diag.obj i)) ↔
    ∃ (J : Type w) (x : SmallCategory J) (_ : IsFiltered J) (pres : ColimitPresentation.{w, w, u_2, u_1} J X),
      ∀ (i : J), P (pres.diag.obj i)
have a : ∀ (x : Type w) (x_1 : SmallCategory x),
  IsFiltered x →
    ((∃ (pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X)),
        ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)) ↔
      ∃ (pres : ColimitPresentation.{w, w, u_2, u_1} x X), ∀ (i : x), P (pres.diag.obj i))
Tactic: congr!
-- Lean 4 proof step from Mathlib.CategoryTheory.ObjectProperty.Ind (goal)
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
e : Equivalence.{v, u_2, u, u_1} C D
inst_2 : P.IsClosedUnderIsomorphisms
X : D
x : Type w
x_1 : SmallCategory x
h : IsFiltered x
⊢ (∃ (pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X)),
      ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)) ↔
    ∃ (pres : ColimitPresentation.{w, w, u_2, u_1} x X), ∀ (i : x), P (pres.diag.obj i)
have a : (∃ (pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X)),
    ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)) →
  ∀ (pres : ColimitPresentation.{w, w, v, u} x (e.inverse.obj X))
    (h : ∀ (i : x), P.inverseImage e.functor (pres.diag.obj i)),
    ∃ (pres : ColimitPresentation.{w, w, u_2, u_1} x X), ∀ (i : x), P (pres.diag.obj i)
Tactic: refine ⟨fun ⟨pres, h⟩ ↦ ?_, fun ⟨pres, h⟩ ↦ ?_⟩