awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 (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
have 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)
Tactic: have h2 := s₁.naturality a.right
-- 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
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)
⊢ 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
have h2₁ : 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
Cleared hypotheses: h2
-- 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
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 := ⋯ }
⊢ ∃ (W : C) (u_1 : T ⟶ W) (v : W ⟶ Z), u_1 ≫ v = u ∧ P (p ≫ u_1)
have 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)
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]
-- 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
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)
have refine_1 : v ≫ c'.ι.app j₃ ≫ t₂.app j₂ = u
Tactic: refine ⟨D'.obj j₃, v, c'.ι.app j₃ ≫ t₂.app 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
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
refine_1 : v ≫ c'.ι.app j₃ ≫ t₂.app j₂ = u
⊢ ∃ (W : C) (u_1 : T ⟶ W) (v : W ⟶ Z), u_1 ≫ v = u ∧ P (p ≫ u_1)
have refine_2 : P (p ≫ v)
Tactic: refine ⟨D'.obj j₃, v, c'.ι.app j₃ ≫ t₂.app 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
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
⊢ v ≫ c'.ι.app j₃ ≫ t₂.app j₂ = u
have refine_1 : q ≫ t₂.app j₂ = u
Tactic: rwa [reassoc_of% hq]
-- 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
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
⊢ P (p ≫ v)
have refine_2 : P (s'.app j₃)
Tactic: rw [hcomp']
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsSmall (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
ι : Type t
inst_1 : Small.{w, t} ι
A B : ι → C
f : (i : ι) → A i ⟶ B i
φ : (i : ι) → (↑(ofHoms f).toSet : Type (max u v)) :=
  fun (i : ι) ↦ Subtype.mk (p := fun (x : Arrow.{v, u} C) ↦ x ∈ (ofHoms f).toSet) (Arrow.mk (f i)) ⋯
⊢ IsSmall.{w, v, u} (ofHoms f)
have hφ : Function.Surjective φ
Tactic: have hφ : Function.Surjective φ := by
    rintro ⟨⟨_, _, f⟩, ⟨i⟩⟩
    exact ⟨i, rfl⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsSmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
⊢ IsSmall.{w, v, u} W ↔ ∃ (ι : Type w) (A : ι → C) (B : ι → C) (f : (i : ι) → A i ⟶ B i), W = ofHoms f
have mp : IsSmall.{w, v, u} W → ∃ (ι : Type w) (A : ι → C) (B : ι → C) (f : (i : ι) → A i ⟶ B i), W = ofHoms f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsSmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
mp : IsSmall.{w, v, u} W → ∃ (ι : Type w) (A : ι → C) (B : ι → C) (f : (i : ι) → A i ⟶ B i), W = ofHoms f
⊢ IsSmall.{w, v, u} W ↔ ∃ (ι : Type w) (A : ι → C) (B : ι → C) (f : (i : ι) → A i ⟶ B i), W = ofHoms f
have mpr : (∃ (ι : Type w) (A : ι → C) (B : ι → C) (f : (i : ι) → A i ⟶ B i), W = ofHoms f) → IsSmall.{w, v, u} W
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsSmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
h : IsSmall.{w, v, u} W
⊢ ∃ (ι : Type w) (A : ι → C) (B : ι → C) (f : (i : ι) → A i ⟶ B i), W = ofHoms f
have mp : W =
  ofHoms (X := fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
    Arrow.left.{v, u}
      (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
              (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
            i) :
        Arrow C))
    (Y := fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
    Arrow.right.{v, u}
      (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
              (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
            i) :
        Arrow C))
    fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
    Arrow.hom
      (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
              (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
            i) :
        Arrow C)
Tactic: refine ⟨Shrink.{w} W.toSet, _, _, fun i ↦ ((equivShrink _).symm i).1.hom, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsSmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
h : IsSmall.{w, v, u} W
⊢ W =
    ofHoms (X := fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
      Arrow.left.{v, u}
        (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
              i) :
          Arrow C))
      (Y := fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
      Arrow.right.{v, u}
        (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
              i) :
          Arrow C))
      fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
      Arrow.hom
        (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
              i) :
          Arrow C)
have mp : ∀ ⦃A B : C⦄ (f : A ⟶ B),
  W f ↔
    ofHoms (X := fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
      Arrow.left.{v, u}
        (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
              i) :
          Arrow C))
      (Y := fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
      Arrow.right.{v, u}
        (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
              i) :
          Arrow C))
      (fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
        Arrow.hom
          (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                  (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                i) :
            Arrow C))
      f
Tactic: ext A B f
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsSmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
h : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ W f ↔
    ofHoms (X := fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
      Arrow.left.{v, u}
        (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
              i) :
          Arrow C))
      (Y := fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
      Arrow.right.{v, u}
        (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
              i) :
          Arrow C))
      (fun (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) ↦
        Arrow.hom
          (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                  (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                i) :
            Arrow C))
      f
have mp : W f ↔
  ∃ (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))),
    Arrow.mk f =
      Arrow.mk (X :=
        Arrow.left.{v, u}
          (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                  (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                i) :
            Arrow C))
        (Arrow.hom
          (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                  (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                i) :
            Arrow C))
Tactic: rw [ofHoms_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.IsSmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
h : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ W f ↔
    ∃ (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))),
      Arrow.mk f =
        Arrow.mk (X :=
          Arrow.left.{v, u}
            (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                    (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                  i) :
              Arrow C))
          (Arrow.hom
            (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                    (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                  i) :
              Arrow C))
have mp : W f →
  ∃ (i : Shrink.{w, max u v} (↑W.toSet : Type (max u v))),
    Arrow.mk f =
      Arrow.mk (X :=
        Arrow.left.{v, u}
          (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                  (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                i) :
            Arrow C))
        (Arrow.hom
          (↑((Equiv.symm (equivShrink (↑W.toSet : Type (max u v))) :
                  (a : Shrink.{w, max u v} (↑W.toSet : Type (max u v))) → (↑W.toSet : Type (max u v)))
                i) :
            Arrow C))
Tactic: constructor