Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
P : MorphismProperty C
inst✝⁴ : ∀ (X : C), IsFinitelyAccessibleCategory (Under X)
inst✝³ : HasPushouts C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : 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✝² : IsFiltered J₁
D₁ : J₁ ⥤ C
s₁ : (Functor.const J₁).obj X ⟶ D₁
t₁ : D₁ ⟶ (Functor.const J₁).obj Y
ht₁ : IsColimit { pt := Y, ι := t₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
J₂ : Type w
w✝¹ : SmallCategory J₂
w✝ : IsFiltered J₂
D₂ : J₂ ⥤ C
s₂ : (Functor.const J₂).obj Y ⟶ D₂
t₂ : D₂ ⟶ (Functor.const J₂).obj Z
ht₂ : IsColimit { pt := Z, ι := t₂ }
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.const J₂).map f ≫ s₂).app j₂
hu : q ≫ { pt := Z, ι := t₂ }.ι.app j₂ = u
j₁ : J₁
W : C
f' : D₁.obj j₁ ⟶ W
g' : W ⟶ D₂.obj j₂
h : IsPushout ({ pt := Y, ι := t₁ }.ι.app j₁) f' (s₂.app j₂) g'
hf' : P f'
D' : 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
    h.isoPushout.inv
hc' : IsColimit c' :=
  IsColimit.extendIso h.isoPushout.inv
    (isColimitOfPreserves (Under.pushout f' ⋙ CategoryTheory.Under.forget W) (ht₁.underPost j₁))
s' : (Functor.const (Under j₁)).obj X ⟶ D' :=
  { app := fun k ↦ s₁.app k.right ≫ pushout.inl ((Under.post D₁).obj k).hom f', naturality := ⋯ }
⊢ ∃ W u_1 v, 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]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
P : MorphismProperty C
inst✝⁴ : ∀ (X : C), IsFinitelyAccessibleCategory (Under X)
inst✝³ : HasPushouts C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : 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✝² : IsFiltered J₁
D₁ : J₁ ⥤ C
s₁ : (Functor.const J₁).obj X ⟶ D₁
t₁ : D₁ ⟶ (Functor.const J₁).obj Y
ht₁ : IsColimit { pt := Y, ι := t₁ }
h₁ : ∀ (j : J₁), P (s₁.app j) ∧ s₁.app j ≫ t₁.app j = f
J₂ : Type w
w✝¹ : SmallCategory J₂
w✝ : IsFiltered J₂
D₂ : J₂ ⥤ C
s₂ : (Functor.const J₂).obj Y ⟶ D₂
t₂ : D₂ ⟶ (Functor.const J₂).obj Z
ht₂ : IsColimit { pt := Z, ι := t₂ }
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.const J₂).map f ≫ s₂).app j₂
hu : q ≫ { pt := Z, ι := t₂ }.ι.app j₂ = u
j₁ : J₁
W : C
f' : D₁.obj j₁ ⟶ W
g' : W ⟶ D₂.obj j₂
h : IsPushout ({ pt := Y, ι := t₁ }.ι.app j₁) f' (s₂.app j₂) g'
hf' : P f'
D' : 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
    h.isoPushout.inv
hc' : IsColimit c' :=
  IsColimit.extendIso h.isoPushout.inv
    (isColimitOfPreserves (Under.pushout f' ⋙ CategoryTheory.Under.forget W) (ht₁.underPost j₁))
s' : (Functor.const (Under j₁)).obj X ⟶ D' :=
  { app := fun k ↦ s₁.app k.right ≫ pushout.inl ((Under.post D₁).obj 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 u_1 v, u_1 ≫ v = u ∧ P (p ≫ u_1)