awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
h : ObjectProperty.ind P.underObj (CategoryTheory.Under.mk f)
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
⊢ IsColimit
    { pt := Y, ι := Functor.whiskerRight pres.ι (CategoryTheory.Under.forget X) :
      Cocone (pres.diag ⋙ CategoryTheory.Under.forget X) }

Tactic:
exact isColimitOfPreserves (CategoryTheory.Under.forget _) pres.isColimit

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.Under.forget, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
h : ObjectProperty.ind P.underObj (CategoryTheory.Under.mk f)
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
j : J
⊢ P (X := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) X) j) (Y :=
    (pres.diag ⋙ CategoryTheory.Under.forget X).obj j)
    (NatTrans.app { app := fun (j : J) ↦ (pres.diag.obj j).hom, naturality := ⋯ } j)

Tactic:
hpres j

Premises used: CategoryTheory.MorphismProperty.underObj
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
h : ObjectProperty.ind P.underObj (CategoryTheory.Under.mk f)
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
j : J
⊢ P (X := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) X) j) (Y :=
    (pres.diag ⋙ CategoryTheory.Under.forget X).obj j)
    (NatTrans.app { app := fun (j : J) ↦ (pres.diag.obj j).hom, naturality := ⋯ } j)

Tactic:
exact hpres j
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
f : X ⟶ Y
h : ObjectProperty.ind P.underObj (CategoryTheory.Under.mk f)
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
j : J
⊢ NatTrans.app { app := fun (j : J) ↦ (pres.diag.obj j).hom, naturality := ⋯ } j ≫
      (Functor.whiskerRight pres.ι (CategoryTheory.Under.forget X)).app j =
    f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X : C
h : ∀ (f : Under.{v, u} X), P.ind.underObj f ↔ ObjectProperty.ind P.underObj f
⊢ Eq (α := ObjectProperty (Under.{v, u} X)) P.ind.underObj (ObjectProperty.ind P.underObj)

Tactic:
ext f
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X : C
f : Under.{v, u} X
⊢ P.ind.underObj f ↔ ObjectProperty.ind P.underObj f

Tactic:
simp [underObj, show f = CategoryTheory.Under.mk f.hom from rfl, ind_iff_ind_underMk]

Premises used: CategoryTheory.MorphismProperty.ind_iff_ind_underMk, CategoryTheory.MorphismProperty.underObj, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : P.RespectsLeft Q
X Y Z : C
i : X ⟶ Y
hi : Q i
f : Y ⟶ Z
h : P.ind f
J : Type u_1
w : SmallCategory J
w_1 : IsFiltered J
D : Functor.{u_1, v, u_1, u} J C
t : Functor.obj (Functor.const J) Y ⟶ D
s : D ⟶ Functor.obj (Functor.const J) Z
hs : IsColimit { pt := Z, ι := s : Cocone D }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
j : J
⊢ (Functor.map (Functor.const J) i ≫ t).app j ≫ s.app j = i ≫ f

Tactic:
simp [hst]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : P.RespectsLeft Q
X Y Z : C
i : X ⟶ Y
hi : Q i
f : Y ⟶ Z
h : P.ind f
J : Type u_1
w : SmallCategory J
w_1 : IsFiltered J
D : Functor.{u_1, v, u_1, u} J C
t : Functor.obj (Functor.const J) Y ⟶ D
s : D ⟶ Functor.obj (Functor.const J) Z
hs : IsColimit { pt := Z, ι := s : Cocone D }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
refine : ∀ (j : J), P ((Functor.map (Functor.const J) i ≫ t).app j)
⊢ P.ind (i ≫ f)

Tactic:
refine ⟨J, ‹_›, ‹_›, D, (Functor.const J).map i ≫ t, s, hs, fun j ↦ ⟨?_, by simp [hst]⟩⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : P.RespectsLeft Q
X Y Z : C
i : X ⟶ Y
hi : Q i
f : Y ⟶ Z
h : P.ind f
J : Type u_1
w : SmallCategory J
w_1 : IsFiltered J
D : Functor.{u_1, v, u_1, u} J C
t : Functor.obj (Functor.const J) Y ⟶ D
s : D ⟶ Functor.obj (Functor.const J) Z
hs : IsColimit { pt := Z, ι := s : Cocone D }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
j : J
⊢ P ((Functor.map (Functor.const J) i ≫ t).app j)

Tactic:
RespectsLeft.precomp _ hi _ (hst j).1

Premises used: CategoryTheory.MorphismProperty.RespectsLeft.precomp, And.left
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : P.RespectsLeft Q
X Y Z : C
i : X ⟶ Y
hi : Q i
f : Y ⟶ Z
h : P.ind f
J : Type u_1
w : SmallCategory J
w_1 : IsFiltered J
D : Functor.{u_1, v, u_1, u} J C
t : Functor.obj (Functor.const J) Y ⟶ D
s : D ⟶ Functor.obj (Functor.const J) Z
hs : IsColimit { pt := Z, ι := s : Cocone D }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
j : J
⊢ P ((Functor.map (Functor.const J) i ≫ t).app j)

Tactic:
exact RespectsLeft.precomp _ hi _ (hst j).1

Premises used: CategoryTheory.MorphismProperty.RespectsLeft.precomp, And.left
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
X Y Z : C
i : Y ⟶ Z
hi : IsIso i
f : X ⟶ Y
h : P.ind f
J : Type u_1
w : SmallCategory J
w_1 : IsFiltered J
D : Functor.{u_1, v, u_1, u} J C
t : Functor.obj (Functor.const J) X ⟶ D
s : D ⟶ Functor.obj (Functor.const J) Y
hs : IsColimit { pt := Y, ι := s : Cocone D }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
⊢ P.ind (f ≫ i)

Tactic:
⟨J, ‹_›, ‹_›, D, t, s ≫ (Functor.const J).map i, ?_, fun j ↦ ⟨(hst j).1, ?_⟩⟩

Premises used: CategoryTheory.MorphismProperty.ind, And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
X Y Z : C
i : Y ⟶ Z
hi : IsIso i
f : X ⟶ Y
h : P.ind f
J : Type u_1
w : SmallCategory J
w_1 : IsFiltered J
D : Functor.{u_1, v, u_1, u} J C
t : Functor.obj (Functor.const J) X ⟶ D
s : D ⟶ Functor.obj (Functor.const J) Y
hs : IsColimit { pt := Y, ι := s : Cocone D }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
refine_1 : IsColimit { pt := Z, ι := s ≫ Functor.map (Functor.const J) i : Cocone D }
refine_2 : ∀ (j : J), t.app j ≫ (s ≫ Functor.map (Functor.const J) i).app j = f ≫ i
⊢ P.ind (f ≫ i)

Tactic:
refine ⟨J, ‹_›, ‹_›, D, t, s ≫ (Functor.const J).map i, ?_, fun j ↦ ⟨(hst j).1, ?_⟩⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
X Y Z : C
i : Y ⟶ Z
hi : IsIso i
f : X ⟶ Y
h : P.ind f
J : Type u_1
w : SmallCategory J
w_1 : IsFiltered J
D : Functor.{u_1, v, u_1, u} J C
t : Functor.obj (Functor.const J) X ⟶ D
s : D ⟶ Functor.obj (Functor.const J) Y
hs : IsColimit { pt := Y, ι := s : Cocone D }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
⊢ IsColimit { pt := Z, ι := s ≫ Functor.map (Functor.const J) i : Cocone D }

Tactic:
exact (IsColimit.equivIsoColimit (Cocone.ext (asIso i))) hs

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Limits.IsColimit.equivIsoColimit, DFunLike.coe, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : P.RespectsIso
X Y Z : C
i : Y ⟶ Z
hi : IsIso i
f : X ⟶ Y
h : P.ind f
J : Type u_1
w : SmallCategory J
w_1 : IsFiltered J
D : Functor.{u_1, v, u_1, u} J C
t : Functor.obj (Functor.const J) X ⟶ D
s : D ⟶ Functor.obj (Functor.const J) Y
hs : IsColimit { pt := Y, ι := s : Cocone D }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
j : J
⊢ t.app j ≫ (s ≫ Functor.map (Functor.const J) i).app j = f ≫ i

Tactic:
simp [reassoc_of% (hst j).2]

Premises used: And.right
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
g : X ⟶ Y
inst_1 : HasPushouts.{v, u} C
inst_2 : P.IsStableUnderCobaseChange
f : Under.{v, u} X
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
pres : ColimitPresentation J f
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
h : ∀ (i : J), P.underObj ((pres.map (Under.pushout g)).diag.obj i)
⊢ ObjectProperty.ind P.underObj ((Under.pushout g).obj f)

Tactic:
use J, inferInstance, inferInstance, pres.map (Under.pushout g)

Premises used: CategoryTheory.Under.pushout, CategoryTheory.Limits.ColimitPresentation.map
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
g : X ⟶ Y
inst_1 : HasPushouts.{v, u} C
inst_2 : P.IsStableUnderCobaseChange
f : Under.{v, u} X
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
pres : ColimitPresentation J f
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
i : J
⊢ P.underObj ((pres.map (Under.pushout g)).diag.obj i)

Tactic:
P.pushout_inr _ _ (hpres i)

Premises used: CategoryTheory.MorphismProperty.underObj, CategoryTheory.MorphismProperty.pushout_inr, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X Y : C
g : X ⟶ Y
inst_1 : HasPushouts.{v, u} C
inst_2 : P.IsStableUnderCobaseChange
f : Under.{v, u} X
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
pres : ColimitPresentation J f
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
i : J
⊢ P.underObj ((pres.map (Under.pushout g)).diag.obj i)

Tactic:
exact P.pushout_inr _ _ (hpres i)

Premises used: CategoryTheory.MorphismProperty.pushout_inr
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : HasPushouts.{v, u} C
⊢ P.ind.IsStableUnderCobaseChange

Tactic:
.mk' fun A B A' f g _ hf ↦ ?_

Premises used: CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.mk'
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : HasPushouts.{v, u} C
refine :
  ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) (x : HasPushout f g) (hf : P.ind f),
    P.ind (Y := pushout f g) (pushout.inr f g)
⊢ P.ind.IsStableUnderCobaseChange

Tactic:
refine .mk' fun A B A' f g _ hf ↦ ?_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : HasPushouts.{v, u} C
A B A' : C
f : A ⟶ A'
g : A ⟶ B
h : HasPushout f g
hf : P.ind f
rw :
  ∀ (hf : ObjectProperty.ind P.underObj (CategoryTheory.Under.mk f)),
    ObjectProperty.ind P.underObj (CategoryTheory.Under.mk (Y := pushout f g) (pushout.inr f g))
⊢ P.ind (Y := pushout f g) (pushout.inr f g)

Tactic:
rw [ind_iff_ind_underMk] at hf ⊢

Premises used: CategoryTheory.MorphismProperty.ind_iff_ind_underMk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : HasPushouts.{v, u} C
A B A' : C
f : A ⟶ A'
g : A ⟶ B
h : HasPushout f g
hf : ObjectProperty.ind P.underObj (CategoryTheory.Under.mk f)
⊢ ObjectProperty.ind P.underObj (CategoryTheory.Under.mk (Y := pushout f g) (pushout.inr f g))

Tactic:
ind_underObj_pushout g hf

Premises used: CategoryTheory.Under.mk, CategoryTheory.MorphismProperty.ind_underObj_pushout, CategoryTheory.StructuredArrow.mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P Q : MorphismProperty.{v, u} C
inst_1 : P.IsStableUnderCobaseChange
inst_2 : HasPushouts.{v, u} C
A B A' : C
f : A ⟶ A'
g : A ⟶ B
h : HasPushout f g
hf : ObjectProperty.ind P.underObj (CategoryTheory.Under.mk f)
⊢ ObjectProperty.ind P.underObj (CategoryTheory.Under.mk (Y := pushout f g) (pushout.inr f g))

Tactic:
exact ind_underObj_pushout g hf

Premises used: CategoryTheory.MorphismProperty.ind_underObj_pushout
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
hp : P ≤ isFinitelyPresentable C
inst_1 : LocallySmall.{w, v, u} C
⊢ P.ind.ind = P.ind

Tactic:
le_antisymm (fun X Y f hf ↦ ?_) P.ind.le_ind

Premises used: CategoryTheory.MorphismProperty.le_ind, CategoryTheory.MorphismProperty.ind, le_antisymm
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
hp : P ≤ isFinitelyPresentable C
inst_1 : LocallySmall.{w, v, u} C
refine : ∀ (X Y : C) (f : X ⟶ Y) (hf : P.ind.ind f), P.ind f
⊢ P.ind.ind = P.ind

Tactic:
refine le_antisymm (fun X Y f hf ↦ ?_) P.ind.le_ind

Premises used: CategoryTheory.MorphismProperty.le_ind, CategoryTheory.MorphismProperty.ind, le_antisymm
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
hp : P ≤ isFinitelyPresentable C
inst_1 : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
hf : P.ind.ind f
⊢ LE.le (α := ObjectProperty (Under.{v, u} X)) P.underObj (ObjectProperty.isFinitelyPresentable (Under.{v, u} X))

Tactic:
have : P.underObj ≤ ObjectProperty.isFinitelyPresentable.{w} (Under X) := fun f hf ↦ hp _ hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
hp : P ≤ isFinitelyPresentable C
inst_1 : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
hf : P.ind.ind f
this : LE.le (α := ObjectProperty (Under.{v, u} X)) P.underObj (ObjectProperty.isFinitelyPresentable (Under.{v, u} X))
⊢ P.ind f

Tactic:
simpa [ind_iff_ind_underMk, underObj_ind_eq_ind_underObj,
    ObjectProperty.ind_ind.{w} this] using hf

Premises used: CategoryTheory.MorphismProperty.ind_iff_ind_underMk, CategoryTheory.MorphismProperty.underObj_ind_eq_ind_underObj
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
H : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst_1 : IsFinitelyAccessibleCategory (Under.{v, u} X)
rw :
  (∀ {Z : Under.{v, u} X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z],
      ∃ (W : Under.{v, u} X) (u : Z ⟶ W) (v : W ⟶ CategoryTheory.Under.mk f), u ≫ v = g ∧ P.underObj W) ↔
    ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y),
      isFinitelyPresentable C p → p ≫ g = f → ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ Y), u ≫ v = g ∧ P (p ≫ u)
H₁ : LE.le (α := ObjectProperty (Under.{v, u} X)) P.underObj (ObjectProperty.isFinitelyPresentable (Under.{v, u} X))
⊢ P.ind f ↔
    ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y),
      isFinitelyPresentable C p → p ≫ g = f → ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ Y), u ≫ v = g ∧ P (p ≫ u)

Tactic:
rw [ind_iff_ind_underMk, ObjectProperty.ind_iff_exists]

Premises used: CategoryTheory.MorphismProperty.ind_iff_ind_underMk, CategoryTheory.ObjectProperty.ind_iff_exists
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
H : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst_1 : IsFinitelyAccessibleCategory (Under.{v, u} X)
⊢ (∀ {Z : Under.{v, u} X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z],
      ∃ (W : Under.{v, u} X) (u : Z ⟶ W) (v : W ⟶ CategoryTheory.Under.mk f), u ≫ v = g ∧ P.underObj W) ↔
    ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y),
      isFinitelyPresentable C p → p ≫ g = f → ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ Y), u ≫ v = g ∧ P (p ≫ u)

Tactic:
⟨fun H Z p g hp hpg ↦ ?_, fun H Z g hZ ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
H : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst_1 : IsFinitelyAccessibleCategory (Under.{v, u} X)
refine_1 :
  ∀
    (H :
      ∀ {Z : Under.{v, u} X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z],
        ∃ (W : Under.{v, u} X) (u : Z ⟶ W) (v : W ⟶ CategoryTheory.Under.mk f), u ≫ v = g ∧ P.underObj W)
    (Z : C) (p : X ⟶ Z) (g : Z ⟶ Y) (hp : isFinitelyPresentable C p) (hpg : p ≫ g = f),
    ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ Y), u ≫ v = g ∧ P (p ≫ u)
refine_2 :
  ∀
    (H :
      ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y),
        isFinitelyPresentable C p → p ≫ g = f → ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ Y), u ≫ v = g ∧ P (p ≫ u))
    (Z : Under.{v, u} X) (g : Z ⟶ CategoryTheory.Under.mk f) (hZ : IsFinitelyPresentable Z),
    ∃ (W : Under.{v, u} X) (u : Z ⟶ W) (v : W ⟶ CategoryTheory.Under.mk f), u ≫ v = g ∧ P.underObj W
⊢ (∀ {Z : Under.{v, u} X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z],
      ∃ (W : Under.{v, u} X) (u : Z ⟶ W) (v : W ⟶ CategoryTheory.Under.mk f), u ≫ v = g ∧ P.underObj W) ↔
    ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y),
      isFinitelyPresentable C p → p ≫ g = f → ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ Y), u ≫ v = g ∧ P (p ≫ u)

Tactic:
refine ⟨fun H Z p g hp hpg ↦ ?_, fun H Z g hZ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
H_1 : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst_1 : IsFinitelyAccessibleCategory (Under.{v, u} X)
H :
  ∀ {Z : Under.{v, u} X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z],
    ∃ (W : Under.{v, u} X) (u : Z ⟶ W) (v : W ⟶ CategoryTheory.Under.mk f), u ≫ v = g ∧ P.underObj W
Z : C
p : X ⟶ Z
g : Z ⟶ Y
hp : isFinitelyPresentable C p
hpg : p ≫ g = f
⊢ IsFinitelyPresentable (CategoryTheory.Under.mk p)

Tactic:
have : IsFinitelyPresentable (CategoryTheory.Under.mk p) := hp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
H_1 : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst_1 : IsFinitelyAccessibleCategory (Under.{v, u} X)
H :
  ∀ {Z : Under.{v, u} X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z],
    ∃ (W : Under.{v, u} X) (u : Z ⟶ W) (v : W ⟶ CategoryTheory.Under.mk f), u ≫ v = g ∧ P.underObj W
Z : C
p : X ⟶ Z
g : Z ⟶ Y
hp : isFinitelyPresentable C p
hpg : p ≫ g = f
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
refine_1 :
  ∀ (W : Under.{v, u} X) (u : CategoryTheory.Under.mk p ⟶ W) (v : W ⟶ CategoryTheory.Under.mk f)
    (huv : u ≫ v = CategoryTheory.Under.homMk g hpg) (hW : P.underObj W),
    ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ Y), u ≫ v = g ∧ P (p ≫ u)
⊢ ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ Y), u ≫ v = g ∧ P (p ≫ u)

Tactic:
obtain ⟨W, u, v, huv, hW⟩ := H (CategoryTheory.Under.homMk (U := CategoryTheory.Under.mk p)
        (V := CategoryTheory.Under.mk f) g hpg)

Premises used: CategoryTheory.Under.homMk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
H_1 : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst_1 : IsFinitelyAccessibleCategory (Under.{v, u} X)
H :
  ∀ {Z : Under.{v, u} X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z],
    ∃ (W : Under.{v, u} X) (u : Z ⟶ W) (v : W ⟶ CategoryTheory.Under.mk f), u ≫ v = g ∧ P.underObj W
Z : C
p : X ⟶ Z
g : Z ⟶ Y
hp : isFinitelyPresentable C p
hpg : p ≫ g = f
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
W : Under.{v, u} X
u : CategoryTheory.Under.mk p ⟶ W
v : W ⟶ CategoryTheory.Under.mk f
huv : u ≫ v = CategoryTheory.Under.homMk g hpg
hW : P.underObj W
right : P (p ≫ Under.Hom.right u)
⊢ ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ Y), u ≫ v = g ∧ P (p ≫ u)

Tactic:
use W.right, u.right, v.right, congr($(huv).right)

Premises used: CategoryTheory.Under.right, CategoryTheory.Under.Hom.right
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
H_1 : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst_1 : IsFinitelyAccessibleCategory (Under.{v, u} X)
H :
  ∀ {Z : Under.{v, u} X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z],
    ∃ (W : Under.{v, u} X) (u : Z ⟶ W) (v : W ⟶ CategoryTheory.Under.mk f), u ≫ v = g ∧ P.underObj W
Z : C
p : X ⟶ Z
g : Z ⟶ Y
hp : isFinitelyPresentable C p
hpg : p ≫ g = f
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
W : Under.{v, u} X
u : CategoryTheory.Under.mk p ⟶ W
v : W ⟶ CategoryTheory.Under.mk f
huv : u ≫ v = CategoryTheory.Under.homMk g hpg
hW : P.underObj W
right right₁ right₂ right₃ : P W.hom
⊢ P (p ≫ Under.Hom.right u)

Tactic:
rwa [show p ≫ u.right = W.hom from CategoryTheory.Under.w u]

Premises used: CategoryTheory.Under.w
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
H_1 : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst_1 : IsFinitelyAccessibleCategory (Under.{v, u} X)
H :
  ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y),
    isFinitelyPresentable C p → p ≫ g = f → ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ Y), u ≫ v = g ∧ P (p ≫ u)
Z : Under.{v, u} X
g : Z ⟶ CategoryTheory.Under.mk f
hZ : IsFinitelyPresentable Z
refine_2 :
  ∀ (W : C) (u : Z.right ⟶ W) (v : W ⟶ Y) (huv : u ≫ v = Under.Hom.right g) (hW : P (Z.hom ≫ u)),
    ∃ (W : Under.{v, u} X) (u : Z ⟶ W) (v : W ⟶ CategoryTheory.Under.mk f), u ≫ v = g ∧ P.underObj W
⊢ ∃ (W : Under.{v, u} X) (u : Z ⟶ W) (v : W ⟶ CategoryTheory.Under.mk f), u ≫ v = g ∧ P.underObj W

Tactic:
obtain ⟨W, u, v, huv, hW⟩ := H Z.hom g.right hZ (CategoryTheory.Under.w g)

Premises used: CategoryTheory.Under.hom, CategoryTheory.Under.Hom.right, CategoryTheory.Under.w
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
H_1 : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst_1 : IsFinitelyAccessibleCategory (Under.{v, u} X)
H :
  ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y),
    isFinitelyPresentable C p → p ≫ g = f → ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ Y), u ≫ v = g ∧ P (p ≫ u)
Z : Under.{v, u} X
g : Z ⟶ CategoryTheory.Under.mk f
hZ : IsFinitelyPresentable Z
W : C
u : Z.right ⟶ W
v : W ⟶ Y
huv : u ≫ v = Under.Hom.right g
hW : P (Z.hom ≫ u)
h :
  Under.Hom.right
      (CategoryStruct.comp (Y := CategoryTheory.Under.mk (Z.hom ≫ u)) (CategoryTheory.Under.homMk u ⋯)
        (CategoryTheory.Under.homMk v ⋯)) =
    Under.Hom.right g
⊢ CategoryStruct.comp (Y := CategoryTheory.Under.mk (Z.hom ≫ u)) (CategoryTheory.Under.homMk u ⋯)
      (CategoryTheory.Under.homMk v ⋯) =
    g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
H_1 : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst_1 : IsFinitelyAccessibleCategory (Under.{v, u} X)
H :
  ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y),
    isFinitelyPresentable C p → p ≫ g = f → ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ Y), u ≫ v = g ∧ P (p ≫ u)
Z : Under.{v, u} X
g : Z ⟶ CategoryTheory.Under.mk f
hZ : IsFinitelyPresentable Z
W : C
u : Z.right ⟶ W
v : W ⟶ Y
huv : u ≫ v = Under.Hom.right g
hW : P (Z.hom ≫ u)
⊢ Under.Hom.right
      (CategoryStruct.comp (Y := CategoryTheory.Under.mk (Z.hom ≫ u)) (CategoryTheory.Under.homMk u ⋯)
        (CategoryTheory.Under.homMk v ⋯)) =
    Under.Hom.right g

Tactic:
simpa