awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
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)
refine_2 : Functor.obj (Functor.const J) X ⟶ pres.diag ⋙ CategoryTheory.Under.forget X
refine_2₁ : pres.diag ⋙ CategoryTheory.Under.forget X ⟶ Functor.obj (Functor.const J) Y
refine_2₂ :
  IsColimit
    { pt := Y, ι := Functor.whiskerRight pres.ι (CategoryTheory.Under.forget X) :
      Cocone (pres.diag ⋙ CategoryTheory.Under.forget X) }
refine_2₃ :
  ∀ (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)
⊢ P.ind f
have refine_2₄ : ∀ (j : J),
  NatTrans.app { app := fun (j : J) ↦ (pres.diag.obj j).hom, naturality := sorry } j ≫
      (Functor.whiskerRight pres.ι (CategoryTheory.Under.forget X)).app j =
    f
Tactic: refine ⟨J, ‹_›, ‹_›, pres.diag ⋙ CategoryTheory.Under.forget _, ?_, ?_, ?_, fun j ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
X : C
⊢ Eq (α := ObjectProperty (Under.{v, u} X)) P.ind.underObj (ObjectProperty.ind P.underObj)
have h : ∀ (f : Under.{v, u} X), P.ind.underObj f ↔ ObjectProperty.ind P.underObj f
Tactic: ext f
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
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
⊢ P.ind (i ≫ f)
have refine : ∀ (j : J), P ((Functor.map (Functor.const J) i ≫ t).app j)
Tactic: refine ⟨J, ‹_›, ‹_›, D, (Functor.const J).map i ≫ t, s, hs, fun j ↦ ⟨?_, by simp [hst]⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
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)
have refine_1 : IsColimit { pt := Z, ι := s ≫ Functor.map (Functor.const J) i : Cocone D }
Tactic: refine ⟨J, ‹_›, ‹_›, D, t, s ≫ (Functor.const J).map i, ?_, fun j ↦ ⟨(hst j).1, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
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 }
⊢ P.ind (f ≫ i)
have refine_2 : ∀ (j : J), t.app j ≫ (s ≫ Functor.map (Functor.const J) i).app j = f ≫ i
Tactic: refine ⟨J, ‹_›, ‹_›, D, t, s ≫ (Functor.const J).map i, ?_, fun j ↦ ⟨(hst j).1, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
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)
⊢ ObjectProperty.ind P.underObj ((Under.pushout g).obj f)
have h : ∀ (i : J), P.underObj ((pres.map (Under.pushout g)).diag.obj i)
Tactic: use J, inferInstance, inferInstance, pres.map (Under.pushout g)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
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
have 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)
Tactic: refine .mk' fun A B A' f g _ hf ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
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
⊢ P.ind (Y := pushout f g) (pushout.inr f g)
have 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))
Tactic: rw [ind_iff_ind_underMk] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
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
have refine : ∀ (X Y : C) (f : X ⟶ Y) (hf : P.ind.ind f), P.ind f
Tactic: refine le_antisymm (fun X Y f hf ↦ ?_) P.ind.le_ind
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (hypothesis)
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
⊢ P.ind f
have this : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
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)
⊢ 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)
have 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)
Tactic: rw [ind_iff_ind_underMk, ObjectProperty.ind_iff_exists]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
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)
⊢ 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)
have H₁ : LE.le (α := ObjectProperty (Under.{v, u} X)) P.underObj (ObjectProperty.isFinitelyPresentable (Under.{v, u} X))
Tactic: rw [ind_iff_ind_underMk, ObjectProperty.ind_iff_exists]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
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)
have 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)
Tactic: refine ⟨fun H Z p g hp hpg ↦ ?_, fun H Z g hZ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
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)
⊢ (∀ {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)
have 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
Tactic: refine ⟨fun H Z p g hp hpg ↦ ?_, fun H Z g hZ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (hypothesis)
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
⊢ ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ Y), u ≫ v = g ∧ P (p ≫ u)
have this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
Tactic: have : IsFinitelyPresentable (CategoryTheory.Under.mk p) := hp
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
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 : C) (u : Z ⟶ W) (v : W ⟶ Y), u ≫ v = g ∧ P (p ≫ u)
have 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)
Tactic: obtain ⟨W, u, v, huv, hW⟩ := H (CategoryTheory.Under.homMk (U := CategoryTheory.Under.mk p)
        (V := CategoryTheory.Under.mk f) g hpg)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
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
⊢ ∃ (W : C) (u : Z ⟶ W) (v : W ⟶ Y), u ≫ v = g ∧ P (p ≫ u)
have right : P (p ≫ Under.Hom.right u)
Tactic: use W.right, u.right, v.right, congr($(huv).right)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
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
⊢ P (p ≫ Under.Hom.right u)
have right : P W.hom
Tactic: rwa [show p ≫ u.right = W.hom from CategoryTheory.Under.w u]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
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 : Under.{v, u} X) (u : Z ⟶ W) (v : W ⟶ CategoryTheory.Under.mk f), u ≫ v = g ∧ P.underObj W
have 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
Tactic: obtain ⟨W, u, v, huv, hW⟩ := H Z.hom g.right hZ (CategoryTheory.Under.w g)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
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)
⊢ CategoryStruct.comp (Y := CategoryTheory.Under.mk (Z.hom ≫ u)) (CategoryTheory.Under.homMk u ⋯)
      (CategoryTheory.Under.homMk v ⋯) =
    g
have h : Under.Hom.right
    (CategoryStruct.comp (Y := CategoryTheory.Under.mk (Z.hom ≫ u)) (CategoryTheory.Under.homMk u sorry)
      (CategoryTheory.Under.homMk v sorry)) =
  Under.Hom.right g
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : ∀ (X : C), IsFinitelyAccessibleCategory (Under.{v, u} X)
inst_2 : HasPushouts.{v, u} C
inst_3 : P.IsStableUnderComposition
inst_4 : P.IsStableUnderCobaseChange
inst_5 : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.ind f
hg : P.ind g
⊢ P.ind (f ≫ g)
have rw : ∀ {Z_1 : C} (p : X ⟶ Z_1) (g_1 : Z_1 ⟶ Z),
  isFinitelyPresentable C p → p ≫ g_1 = f ≫ g → ∃ (W : C) (u : Z_1 ⟶ W) (v : W ⟶ Z), u ≫ v = g_1 ∧ P (p ≫ u)
Tactic: rw [ind_iff_exists H]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : ∀ (X : C), IsFinitelyAccessibleCategory (Under.{v, u} X)
inst_2 : HasPushouts.{v, u} C
inst_3 : P.IsStableUnderComposition
inst_4 : P.IsStableUnderCobaseChange
inst_5 : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.ind f
hg : P.ind g
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
hpu : p ≫ u = f ≫ g
⊢ ∃ (W : C) (u_1 : T ⟶ W) (v : W ⟶ Z), u_1 ≫ v = u ∧ P (p ≫ u_1)
have obtain : ∀ (J₁ : Type w) (w : SmallCategory J₁),
  IsFiltered J₁ →
    ∀ (D₁ : Functor.{w, v, w, u} J₁ C) (s₁ : Functor.obj (Functor.const J₁) X ⟶ D₁)
      (t₁ : D₁ ⟶ Functor.obj (Functor.const J₁) Y) (ht₁ : IsColimit { pt := Y, ι := t₁ : Cocone D₁ })
      (h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f),
      ∃ (W : C) (u_1 : T ⟶ W) (v : W ⟶ Z), u_1 ≫ v = u ∧ P (p ≫ u_1)
Tactic: obtain ⟨J₁, _, _, D₁, s₁, t₁, ht₁, h₁⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : ∀ (X : C), IsFinitelyAccessibleCategory (Under.{v, u} X)
inst_2 : HasPushouts.{v, u} C
inst_3 : P.IsStableUnderComposition
inst_4 : P.IsStableUnderCobaseChange
inst_5 : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : P.ind g
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
hpu : p ≫ u = f ≫ g
J₁ : Type w
w : SmallCategory J₁
w_1 : IsFiltered J₁
D₁ : Functor.{w, v, w, u} J₁ C
s₁ : Functor.obj (Functor.const J₁) X ⟶ D₁
t₁ : D₁ ⟶ Functor.obj (Functor.const J₁) Y
ht₁ : IsColimit { pt := Y, ι := t₁ : Cocone D₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
⊢ ∃ (W : C) (u_1 : T ⟶ W) (v : W ⟶ Z), u_1 ≫ v = u ∧ P (p ≫ u_1)
have obtain : ∀ (J₂ : Type w) (w : SmallCategory J₂),
  IsFiltered J₂ →
    ∀ (D₂ : Functor.{w, v, w, u} J₂ C) (s₂ : Functor.obj (Functor.const J₂) Y ⟶ D₂)
      (t₂ : D₂ ⟶ Functor.obj (Functor.const J₂) Z) (ht₂ : IsColimit { pt := Z, ι := t₂ : Cocone D₂ })
      (h₂ : ∀ (j : J₂), P (s₂.app j) ∧ s₂.app j ≫ t₂.app j = g),
      ∃ (W : C) (u_1 : T ⟶ W) (v : W ⟶ Z), u_1 ≫ v = u ∧ P (p ≫ u_1)
Tactic: obtain ⟨J₂, _, _, D₂, s₂, t₂, ht₂, h₂⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : ∀ (X : C), IsFinitelyAccessibleCategory (Under.{v, u} X)
inst_2 : HasPushouts.{v, u} C
inst_3 : P.IsStableUnderComposition
inst_4 : P.IsStableUnderCobaseChange
inst_5 : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
hpu : p ≫ u = f ≫ g
J₁ : Type w
w : SmallCategory J₁
w_1 : IsFiltered J₁
D₁ : Functor.{w, v, w, u} J₁ C
s₁ : Functor.obj (Functor.const J₁) X ⟶ D₁
t₁ : D₁ ⟶ Functor.obj (Functor.const J₁) Y
ht₁ : IsColimit { pt := Y, ι := t₁ : Cocone D₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
J₂ : Type w
w_2 : SmallCategory J₂
w_3 : IsFiltered J₂
D₂ : Functor.{w, v, w, u} J₂ C
s₂ : Functor.obj (Functor.const J₂) Y ⟶ D₂
t₂ : D₂ ⟶ Functor.obj (Functor.const J₂) Z
ht₂ : IsColimit { pt := Z, ι := t₂ : Cocone D₂ }
h₂ : ∀ (j : J₂), P (s₂.app j) ∧ s₂.app j ≫ t₂.app j = g
⊢ ∃ (W : C) (u_1 : T ⟶ W) (v : W ⟶ Z), u_1 ≫ v = u ∧ P (p ≫ u_1)
have this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
Tactic: have : IsFinitelyPresentable (CategoryTheory.Under.mk p) := hp
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : ∀ (X : C), IsFinitelyAccessibleCategory (Under.{v, u} X)
inst_2 : HasPushouts.{v, u} C
inst_3 : P.IsStableUnderComposition
inst_4 : P.IsStableUnderCobaseChange
inst_5 : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
hpu : p ≫ u = f ≫ g
J₁ : Type w
w : SmallCategory J₁
w_1 : IsFiltered J₁
D₁ : Functor.{w, v, w, u} J₁ C
s₁ : Functor.obj (Functor.const J₁) X ⟶ D₁
t₁ : D₁ ⟶ Functor.obj (Functor.const J₁) Y
ht₁ : IsColimit { pt := Y, ι := t₁ : Cocone D₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
J₂ : Type w
w_2 : SmallCategory J₂
w_3 : IsFiltered J₂
D₂ : Functor.{w, v, w, u} J₂ C
s₂ : Functor.obj (Functor.const J₂) Y ⟶ D₂
t₂ : D₂ ⟶ Functor.obj (Functor.const J₂) Z
ht₂ : IsColimit { pt := Z, ι := t₂ : Cocone D₂ }
h₂ : ∀ (j : J₂), P (s₂.app j) ∧ s₂.app j ≫ t₂.app j = g
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
⊢ ∃ (W : C) (u_1 : T ⟶ W) (v : W ⟶ Z), u_1 ≫ v = u ∧ P (p ≫ u_1)
have obtain : ∀ (j₂ : J₂) (q : T ⟶ D₂.obj j₂) (hcomp : p ≫ q = (Functor.map (Functor.const J₂) f ≫ s₂).app j₂)
  (hu : q ≫ { pt := Z, ι := t₂ : Cocone D₂ }.ι.app j₂ = u),
  ∃ (W : C) (u_1 : T ⟶ W) (v : W ⟶ Z), u_1 ≫ v = u ∧ P (p ≫ u_1)
Tactic: obtain ⟨j₂, q, hcomp, hu⟩ := IsFinitelyPresentable.exists_hom_of_isColimit_under
        ht₂ p ((Functor.const _).map f ≫ s₂) u <| by simp [h₂, hpu]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : MorphismProperty.{v, u} C
inst_1 : ∀ (X : C), IsFinitelyAccessibleCategory (Under.{v, u} X)
inst_2 : HasPushouts.{v, u} C
inst_3 : P.IsStableUnderComposition
inst_4 : P.IsStableUnderCobaseChange
inst_5 : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
hpu : p ≫ u = f ≫ g
J₁ : Type w
w : SmallCategory J₁
w_1 : IsFiltered J₁
D₁ : Functor.{w, v, w, u} J₁ C
s₁ : Functor.obj (Functor.const J₁) X ⟶ D₁
t₁ : D₁ ⟶ Functor.obj (Functor.const J₁) Y
ht₁ : IsColimit { pt := Y, ι := t₁ : Cocone D₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
J₂ : Type w
w_2 : SmallCategory J₂
w_3 : IsFiltered J₂
D₂ : Functor.{w, v, w, u} J₂ C
s₂ : Functor.obj (Functor.const J₂) Y ⟶ D₂
t₂ : D₂ ⟶ Functor.obj (Functor.const J₂) Z
ht₂ : IsColimit { pt := Z, ι := t₂ : Cocone D₂ }
h₂ : ∀ (j : J₂), P (s₂.app j) ∧ s₂.app j ≫ t₂.app j = g
this : IsFinitelyPresentable (CategoryTheory.Under.mk p)
j₂ : J₂
q : T ⟶ D₂.obj j₂
hcomp : p ≫ q = (Functor.map (Functor.const J₂) f ≫ s₂).app j₂
hu : q ≫ { pt := Z, ι := t₂ : Cocone D₂ }.ι.app j₂ = u
⊢ ∃ (W : C) (u_1 : T ⟶ W) (v : W ⟶ Z), u_1 ≫ v = u ∧ P (p ≫ u_1)
have obtain : ∀ (j₁ : J₁) (W : C) (f' : D₁.obj j₁ ⟶ W) (g' : W ⟶ D₂.obj j₂)
  (h : IsPushout ({ pt := Y, ι := t₁ : Cocone D₁ }.ι.app j₁) f' (s₂.app j₂) g') (hf' : P f'),
  ∃ (W : C) (u_1 : T ⟶ W) (v : W ⟶ Z), u_1 ≫ v = u ∧ P (p ≫ u_1)
Tactic: obtain ⟨j₁, W, f', g', h, hf'⟩ :=
      P.exists_isPushout_of_isFiltered ht₁ (s₂.app j₂) (h₂ j₂).left