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
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)
⊢ ∃ (W : Under.{v, u} X) (u : Z ⟶ W) (v : W ⟶ CategoryTheory.Under.mk f), u ≫ v = g ∧ P.underObj W

Tactic:
exact ⟨CategoryTheory.Under.mk (Z.hom ≫ u), CategoryTheory.Under.homMk u,
          CategoryTheory.Under.homMk v, by ext; simpa, hW⟩
-- 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_1 : C
f : X ⟶ Y_1
inst_1 : IsFinitelyAccessibleCategory (Under.{v, u} X)
Y : Under.{v, u} X
hY : P.underObj Y
⊢ ObjectProperty.isFinitelyPresentable (Under.{v, u} X) Y

Tactic:
H _ hY

Premises used: CategoryTheory.MorphismProperty.isFinitelyPresentable, CategoryTheory.Under.mk, CategoryTheory.Under, CategoryTheory.StructuredArrow.mk, CategoryTheory.StructuredArrow
-- 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_1 : C
f : X ⟶ Y_1
inst_1 : IsFinitelyAccessibleCategory (Under.{v, u} X)
Y : Under.{v, u} X
hY : P.underObj Y
⊢ ObjectProperty.isFinitelyPresentable (Under.{v, u} X) Y

Tactic:
exact H _ hY
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
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
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)
⊢ P.ind (f ≫ g)

Tactic:
rw [ind_iff_exists H]

Premises used: CategoryTheory.MorphismProperty.ind_iff_exists
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
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
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)
⊢ ∃ (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
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
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
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)
⊢ ∃ (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
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
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
⊢ 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
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₂), (Functor.map (Functor.const J₂) f ≫ s₂).app j ≫ { pt := Z, ι := t₂ : Cocone D₂ }.ι.app j = p ≫ u

Tactic:
simp [h₂, hpu]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
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)
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)
⊢ ∃ (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]

Premises used: CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit_under, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.const
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
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
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)
⊢ ∃ (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

Premises used: CategoryTheory.MorphismProperty.exists_isPushout_of_isFiltered, And.left, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
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
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'
D' : Functor.{w, v, w, u} (Under j₁) C := (Under.post D₁ ⋙ Under.pushout f') ⋙ CategoryTheory.Under.forget W
c' : Cocone D' :=
  ((Under.pushout f' ⋙ CategoryTheory.Under.forget W).mapCocone ({ pt := Y, ι := t₁ }.underPost j₁)).extend (X :=
    D₂.obj j₂) (Iso.inv h.isoPushout)
hc' : IsColimit c' :=
  IsColimit.extendIso (Iso.inv h.isoPushout)
    (isColimitOfPreserves (Under.pushout f' ⋙ CategoryTheory.Under.forget W) (ht₁.underPost j₁))
k l : Under j₁
a : k ⟶ l
⊢ Functor.map (Functor.obj (Functor.const J₁) X) (Under.Hom.right a) ≫ s₁.app l.right =
    s₁.app k.right ≫ D₁.map (Under.Hom.right a)

Tactic:
have h2 := s₁.naturality a.right
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
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
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'
D' : Functor.{w, v, w, u} (Under j₁) C := (Under.post D₁ ⋙ Under.pushout f') ⋙ CategoryTheory.Under.forget W
c' : Cocone D' :=
  ((Under.pushout f' ⋙ CategoryTheory.Under.forget W).mapCocone ({ pt := Y, ι := t₁ }.underPost j₁)).extend (X :=
    D₂.obj j₂) (Iso.inv h.isoPushout)
hc' : IsColimit c' :=
  IsColimit.extendIso (Iso.inv h.isoPushout)
    (isColimitOfPreserves (Under.pushout f' ⋙ CategoryTheory.Under.forget W) (ht₁.underPost j₁))
k l : Under j₁
a : k ⟶ l
h2 :
  Functor.map (Functor.obj (Functor.const J₁) X) (Under.Hom.right a) ≫ s₁.app l.right =
    s₁.app k.right ≫ D₁.map (Under.Hom.right a)
⊢ s₁.app l.right = s₁.app k.right ≫ D₁.map (Under.Hom.right a)

Tactic:
simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.id_comp] at h2

Premises used: CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.const_obj_map, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
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
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'
D' : Functor.{w, v, w, u} (Under j₁) C := (Under.post D₁ ⋙ Under.pushout f') ⋙ CategoryTheory.Under.forget W
c' : Cocone D' :=
  ((Under.pushout f' ⋙ CategoryTheory.Under.forget W).mapCocone ({ pt := Y, ι := t₁ }.underPost j₁)).extend (X :=
    D₂.obj j₂) (Iso.inv h.isoPushout)
hc' : IsColimit c' :=
  IsColimit.extendIso (Iso.inv h.isoPushout)
    (isColimitOfPreserves (Under.pushout f' ⋙ CategoryTheory.Under.forget W) (ht₁.underPost j₁))
k l : Under j₁
a : k ⟶ l
h2 : s₁.app l.right = s₁.app k.right ≫ D₁.map (Under.Hom.right a)
⊢ Functor.map (Functor.obj (Functor.const (Under j₁)) X) a ≫
      s₁.app l.right ≫ pushout.inl (Functor.obj (Under.post D₁) l).hom f' =
    (s₁.app k.right ≫ pushout.inl (Functor.obj (Under.post D₁) k).hom f') ≫ D'.map a

Tactic:
simp [h2, D']
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
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
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'
D' : Functor.{w, v, w, u} (Under j₁) C := (Under.post D₁ ⋙ Under.pushout f') ⋙ CategoryTheory.Under.forget W
c' : Cocone D' :=
  ((Under.pushout f' ⋙ CategoryTheory.Under.forget W).mapCocone ({ pt := Y, ι := t₁ }.underPost j₁)).extend (X :=
    D₂.obj j₂) (Iso.inv h.isoPushout)
hc' : IsColimit c' :=
  IsColimit.extendIso (Iso.inv h.isoPushout)
    (isColimitOfPreserves (Under.pushout f' ⋙ CategoryTheory.Under.forget W) (ht₁.underPost j₁))
s' : Functor.obj (Functor.const (Under j₁)) X ⟶ D' :=
  { app := fun (k : Under j₁) ↦ s₁.app k.right ≫ pushout.inl (Functor.obj (Under.post D₁) k).hom f', naturality := ⋯ }
k : Under j₁
⊢ s'.app k ≫ c'.ι.app k = p ≫ q

Tactic:
simp [c', s', hcomp, reassoc_of% (h₁ k.right).right]

Premises used: CategoryTheory.Under.right, And.right
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
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
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'
D' : Functor.{w, v, w, u} (Under j₁) C := (Under.post D₁ ⋙ Under.pushout f') ⋙ CategoryTheory.Under.forget W
c' : Cocone D' :=
  ((Under.pushout f' ⋙ CategoryTheory.Under.forget W).mapCocone ({ pt := Y, ι := t₁ }.underPost j₁)).extend (X :=
    D₂.obj j₂) (Iso.inv h.isoPushout)
hc' : IsColimit c' :=
  IsColimit.extendIso (Iso.inv h.isoPushout)
    (isColimitOfPreserves (Under.pushout f' ⋙ CategoryTheory.Under.forget W) (ht₁.underPost j₁))
s' : Functor.obj (Functor.const (Under j₁)) X ⟶ D' :=
  { app := fun (k : Under j₁) ↦ s₁.app k.right ≫ pushout.inl (Functor.obj (Under.post D₁) k).hom f', naturality := ⋯ }
obtain :
  ∀ (j₃ : Under j₁) (v : T ⟶ D'.obj j₃) (hcomp' : p ≫ v = s'.app j₃) (hq : v ≫ c'.ι.app j₃ = q),
    ∃ (W : C) (u_1 : T ⟶ W) (v : W ⟶ Z), u_1 ≫ v = u ∧ P (p ≫ u_1)
⊢ ∃ (W : C) (u_1 : T ⟶ W) (v : W ⟶ Z), u_1 ≫ v = u ∧ P (p ≫ u_1)

Tactic:
obtain ⟨j₃, v, hcomp', hq⟩ := IsFinitelyPresentable.exists_hom_of_isColimit_under
        hc' p s' q <| fun k ↦ by
      simp [c', s', hcomp, reassoc_of% (h₁ k.right).right]

Premises used: CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit_under
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
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
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'
D' : Functor.{w, v, w, u} (Under j₁) C := (Under.post D₁ ⋙ Under.pushout f') ⋙ CategoryTheory.Under.forget W
c' : Cocone D' :=
  ((Under.pushout f' ⋙ CategoryTheory.Under.forget W).mapCocone ({ pt := Y, ι := t₁ }.underPost j₁)).extend (X :=
    D₂.obj j₂) (Iso.inv h.isoPushout)
hc' : IsColimit c' :=
  IsColimit.extendIso (Iso.inv h.isoPushout)
    (isColimitOfPreserves (Under.pushout f' ⋙ CategoryTheory.Under.forget W) (ht₁.underPost j₁))
s' : Functor.obj (Functor.const (Under j₁)) X ⟶ D' :=
  { app := fun (k : Under j₁) ↦ s₁.app k.right ≫ pushout.inl (Functor.obj (Under.post D₁) k).hom f', naturality := ⋯ }
j₃ : Under j₁
v : T ⟶ D'.obj j₃
hcomp' : p ≫ v = s'.app j₃
hq : v ≫ c'.ι.app j₃ = q
⊢ ∃ (W : C) (u_1 : T ⟶ W) (v : W ⟶ Z), u_1 ≫ v = u ∧ P (p ≫ u_1)

Tactic:
⟨D'.obj j₃, v, c'.ι.app j₃ ≫ t₂.app j₂, ?_, ?_⟩

Premises used: CategoryTheory.Limits.Cocone.ι, And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app