awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u''
inst_1 : Category.{v'', u''} J
inst_2 : HasPushouts.{v, u} C
h :
  ∀ ⦃X Y : Functor.{v'', v, u'', u} J C⦄ (f : X ⟶ Y),
    functorCategory (epimorphisms C) J f ↔ epimorphisms (Functor.{v'', v, u'', u} J C) f
⊢ Eq (α := MorphismProperty (Functor.{v'', v, u'', u} J C)) (functorCategory (epimorphisms C) J)
    (epimorphisms (Functor.{v'', v, u'', u} J C))

Tactic:
ext _ _ f
-- Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u''
inst_1 : Category.{v'', u''} J
inst_2 : HasPushouts.{v, u} C
X Y : Functor.{v'', v, u'', u} J C
f : X ⟶ Y
⊢ functorCategory (epimorphisms C) J f ↔ epimorphisms (Functor.{v'', v, u'', u} J C) f

Tactic:
simp only [functorCategory, epimorphisms.iff, NatTrans.epi_iff_epi_app]

Premises used: CategoryTheory.NatTrans.epi_iff_epi_app, CategoryTheory.MorphismProperty.epimorphisms.iff, CategoryTheory.MorphismProperty.functorCategory
-- Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u''
inst_1 : Category.{v'', u''} J
K : Type u'
inst_2 : LinearOrder K
inst_3 : SuccOrder K
inst_4 : OrderBot K
inst_5 : WellFoundedLT K
inst_6 : IsStableUnderTransfiniteCompositionOfShape.{u', v, u} (monomorphisms C) K
inst_7 : HasPullbacks.{v, u} C
inst_8 : HasIterationOfShape.{u', v, u} K C
rw :
  IsStableUnderTransfiniteCompositionOfShape (C := Functor.{v'', v, u'', u} J C) (functorCategory (monomorphisms C) J) K
⊢ IsStableUnderTransfiniteCompositionOfShape (C := Functor.{v'', v, u'', u} J C)
    (monomorphisms (Functor.{v'', v, u'', u} J C)) K

Tactic:
rw [← functorCategory_monomorphisms]

Premises used: CategoryTheory.MorphismProperty.functorCategory_monomorphisms
-- Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u''
inst_1 : Category.{v'', u''} J
K : Type u'
inst_2 : LinearOrder K
inst_3 : SuccOrder K
inst_4 : OrderBot K
inst_5 : WellFoundedLT K
inst_6 : IsStableUnderTransfiniteCompositionOfShape.{u', v, u} (monomorphisms C) K
inst_7 : HasPullbacks.{v, u} C
inst_8 : HasIterationOfShape.{u', v, u} K C
⊢ IsStableUnderTransfiniteCompositionOfShape (C := Functor.{v'', v, u'', u} J C) (functorCategory (monomorphisms C) J) K

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u''
inst_1 : Category.{v'', u''} J
K' : Type u'
inst_2 : IsStableUnderCoproductsOfShape.{v, u, u'} (monomorphisms C) K'
inst_3 : HasCoproductsOfShape.{u', u, v} K' C
inst_4 : HasPullbacks.{v, u} C
rw : IsStableUnderCoproductsOfShape (C := Functor.{v'', v, u'', u} J C) (functorCategory (monomorphisms C) J) K'
⊢ IsStableUnderCoproductsOfShape (C := Functor.{v'', v, u'', u} J C) (monomorphisms (Functor.{v'', v, u'', u} J C)) K'

Tactic:
rw [← functorCategory_monomorphisms]

Premises used: CategoryTheory.MorphismProperty.functorCategory_monomorphisms
-- Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u''
inst_1 : Category.{v'', u''} J
K' : Type u'
inst_2 : IsStableUnderCoproductsOfShape.{v, u, u'} (monomorphisms C) K'
inst_3 : HasCoproductsOfShape.{u', u, v} K' C
inst_4 : HasPullbacks.{v, u} C
⊢ IsStableUnderCoproductsOfShape (C := Functor.{v'', v, u'', u} J C) (functorCategory (monomorphisms C) J) K'

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
X Y : ι → C
f_1 : (i : ι) → X i ⟶ Y i
κ : Cardinal.{u_3}
h : HasCardinalLT ι κ
f : Arrow.{v_1, u_1} C
hf : f ∈ (ofHoms f_1).toSet
⊢ ∃ (i : ι), Arrow.mk f.hom = Arrow.mk (f_1 i)

Tactic:
rw [MorphismProperty.mem_toSet_iff, MorphismProperty.ofHoms_iff] at hf

Premises used: CategoryTheory.MorphismProperty.ofHoms_iff, CategoryTheory.MorphismProperty.mem_toSet_iff
-- Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
X Y : ι → C
f_1 : (i : ι) → X i ⟶ Y i
κ : Cardinal.{u_3}
h : HasCardinalLT ι κ
f : Arrow.{v_1, u_1} C
hf_1 : f ∈ (ofHoms f_1).toSet
hf : ∃ (i : ι), Arrow.mk f.hom = Arrow.mk (f_1 i)
obtain :
  ∀ (i : ι) (hf : Arrow.mk f.hom = Arrow.mk (f_1 i)),
    ∃ (a : ι),
      (fun (i : ι) ↦
            (Subtype.mk (p := fun (x : Arrow.{v_1, u_1} C) ↦ x ∈ (ofHoms f_1).toSet) (Arrow.mk (f_1 i)) ⋯ :
              { x : Arrow.{v_1, u_1} C // x ∈ (ofHoms f_1).toSet }))
          a =
        Subtype.mk (p := fun (x : Arrow.{v_1, u_1} C) ↦ x ∈ (ofHoms f_1).toSet) f hf_1
⊢ ∃ (a : ι),
    (fun (i : ι) ↦
          (Subtype.mk (p := fun (x : Arrow.{v_1, u_1} C) ↦ x ∈ (ofHoms f_1).toSet) (Arrow.mk (f_1 i)) ⋯ :
            { x : Arrow.{v_1, u_1} C // x ∈ (ofHoms f_1).toSet }))
        a =
      Subtype.mk (p := fun (x : Arrow.{v_1, u_1} C) ↦ x ∈ (ofHoms f_1).toSet) f hf_1

Tactic:
obtain ⟨i, hf⟩ := hf
-- Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
X Y : ι → C
f_1 : (i : ι) → X i ⟶ Y i
κ : Cardinal.{u_3}
h : HasCardinalLT ι κ
f : Arrow.{v_1, u_1} C
hf_1 : f ∈ (ofHoms f_1).toSet
i : ι
hf : Arrow.mk f.hom = Arrow.mk (f_1 i)
⊢ f = Arrow.mk (f_1 i)

Tactic:
hf

Premises used: CategoryTheory.Arrow, CategoryTheory.Arrow.mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
X Y : ι → C
f_1 : (i : ι) → X i ⟶ Y i
κ : Cardinal.{u_3}
h : HasCardinalLT ι κ
f : Arrow.{v_1, u_1} C
hf_1 : f ∈ (ofHoms f_1).toSet
i : ι
hf : Arrow.mk f.hom = Arrow.mk (f_1 i)
obtain :
  ∀ (hf : Arrow.mk (f_1 i) ∈ (ofHoms f_1).toSet),
    ∃ (a : ι),
      (fun (i : ι) ↦
            (Subtype.mk (p := fun (x : Arrow.{v_1, u_1} C) ↦ x ∈ (ofHoms f_1).toSet) (Arrow.mk (f_1 i)) ⋯ :
              { x : Arrow.{v_1, u_1} C // x ∈ (ofHoms f_1).toSet }))
          a =
        Subtype.mk (p := fun (x : Arrow.{v_1, u_1} C) ↦ x ∈ (ofHoms f_1).toSet) (Arrow.mk (f_1 i)) hf
⊢ ∃ (a : ι),
    (fun (i : ι) ↦
          (Subtype.mk (p := fun (x : Arrow.{v_1, u_1} C) ↦ x ∈ (ofHoms f_1).toSet) (Arrow.mk (f_1 i)) ⋯ :
            { x : Arrow.{v_1, u_1} C // x ∈ (ofHoms f_1).toSet }))
        a =
      Subtype.mk (p := fun (x : Arrow.{v_1, u_1} C) ↦ x ∈ (ofHoms f_1).toSet) f hf_1

Tactic:
obtain rfl : f = _ := hf

Premises used: rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
κ : Cardinal.{u_3}
h : HasCardinalLT ι κ
i : ι
hf : Arrow.mk (f i) ∈ (ofHoms f).toSet
⊢ ∃ (a : ι),
    (fun (i : ι) ↦
          (Subtype.mk (p := fun (x : Arrow.{v_1, u_1} C) ↦ x ∈ (ofHoms f).toSet) (Arrow.mk (f i)) ⋯ :
            { x : Arrow.{v_1, u_1} C // x ∈ (ofHoms f).toSet }))
        a =
      Subtype.mk (p := fun (x : Arrow.{v_1, u_1} C) ↦ x ∈ (ofHoms f).toSet) (Arrow.mk (f i)) hf

Tactic:
⟨i, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
ι : Type u_2
X Y : ι → C
f : (i : ι) → X i ⟶ Y i
κ : Cardinal.{u_3}
h : HasCardinalLT ι κ
i : ι
hf : Arrow.mk (f i) ∈ (ofHoms f).toSet
⊢ ∃ (a : ι),
    (fun (i : ι) ↦
          (Subtype.mk (p := fun (x : Arrow.{v_1, u_1} C) ↦ x ∈ (ofHoms f).toSet) (Arrow.mk (f i)) ⋯ :
            { x : Arrow.{v_1, u_1} C // x ∈ (ofHoms f).toSet }))
        a =
      Subtype.mk (p := fun (x : Arrow.{v_1, u_1} C) ↦ x ∈ (ofHoms f).toSet) (Arrow.mk (f i)) hf

Tactic:
exact ⟨i, rfl⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
P : ι → MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
hP : ∀ (i : ι), (P i).HasCardinalLT κ
hι : HasCardinalLT ι κ
rw : HasCardinalLT (↑(⋃ (i : ι), (P i).toSet) : Type (max u v)) κ
⊢ HasCardinalLT (↑(toSet (⨆ (i : ι), P i)) : Type (max u v)) κ

Tactic:
rw [toSet_iSup]

Premises used: CategoryTheory.MorphismProperty.toSet_iSup
-- Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
P : ι → MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
hP : ∀ (i : ι), (P i).HasCardinalLT κ
hι : HasCardinalLT ι κ
⊢ HasCardinalLT (↑(⋃ (i : ι), (P i).toSet) : Type (max u v)) κ

Tactic:
hasCardinalLT_iUnion _ hι hP

Premises used: hasCardinalLT_iUnion
-- Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
P : ι → MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
hP : ∀ (i : ι), (P i).HasCardinalLT κ
hι : HasCardinalLT ι κ
⊢ HasCardinalLT (↑(⋃ (i : ι), (P i).toSet) : Type (max u v)) κ

Tactic:
exact hasCardinalLT_iUnion _ hι hP

Premises used: hasCardinalLT_iUnion
-- Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT
Goal:
C : Type u
inst : Category.{v, u} C
P₁ P₂ : MorphismProperty.{v, u} C
κ : Cardinal.{w}
h₁ : P₁.HasCardinalLT κ
h₂ : P₂.HasCardinalLT κ
hκ : Cardinal.aleph0 ≤ κ
rw : HasCardinalLT (↑(P₁.toSet ∪ P₂.toSet) : Type (max u v)) κ
⊢ HasCardinalLT (↑(P₁ ⊔ P₂).toSet : Type (max u v)) κ

Tactic:
rw [MorphismProperty.toSet_max]

Premises used: CategoryTheory.MorphismProperty.toSet_max
-- Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT
Goal:
C : Type u
inst : Category.{v, u} C
P₁ P₂ : MorphismProperty.{v, u} C
κ : Cardinal.{w}
h₁ : P₁.HasCardinalLT κ
h₂ : P₂.HasCardinalLT κ
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT (↑(P₁.toSet ∪ P₂.toSet) : Type (max u v)) κ

Tactic:
hasCardinalLT_union hκ h₁ h₂

Premises used: hasCardinalLT_union
-- Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT
Goal:
C : Type u
inst : Category.{v, u} C
P₁ P₂ : MorphismProperty.{v, u} C
κ : Cardinal.{w}
h₁ : P₁.HasCardinalLT κ
h₂ : P₂.HasCardinalLT κ
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT (↑(P₁.toSet ∪ P₂.toSet) : Type (max u v)) κ

Tactic:
exact hasCardinalLT_union hκ h₁ h₂

Premises used: hasCardinalLT_union
-- Module: Mathlib.CategoryTheory.MorphismProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
inst_2 : IsFiltered J
D : Functor.{w, v, w, u} J C
c : Cocone D
hc : IsColimit c
X A : C
p : X ⟶ A
hp : isFinitelyPresentable C p
s : Functor.obj (Functor.const J) X ⟶ D
f : A ⟶ c.pt
h : ∀ (j : J), s.app j ≫ c.ι.app j = p ≫ f
⊢ ∃ (j : J) (q : A ⟶ D.obj j), p ≫ q = s.app j ∧ q ≫ c.ι.app j = f

Tactic:
hp.exists_hom_of_isColimit_under hc _ s _ h

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
X Y : C
f : X ⟶ Y
hf : P f
⊢ P.ind f

Tactic:
⟨PUnit, inferInstance, inferInstance, (Functor.const PUnit).obj Y, ?_, 𝟙 _, ?_, ?_⟩

Premises used: CategoryTheory.CategoryStruct.id, inferInstance, CategoryTheory.MorphismProperty.ind, PUnit, Exists.intro, CategoryTheory.Functor.const, CategoryTheory.Functor.obj
-- 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
hf : P f
refine_1 :
  Quiver.Hom (V := Functor.{w, v, w, u} PUnit.{w + 1} C) (Functor.obj (Functor.const PUnit.{w + 1}) X)
    (Functor.obj (Functor.const PUnit.{w + 1}) Y)
refine_2 : IsColimit.{w, v, w, u} { pt := Y, ι := 𝟙 (Functor.obj (Functor.const PUnit.{w + 1}) Y) }
refine_3 :
  ∀ (j : PUnit.{w + 1}),
    P (X := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const PUnit.{w + 1}) X) j) (Y :=
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const PUnit.{w + 1}) Y) j)
        (NatTrans.app { app := fun (x : PUnit.{w + 1}) ↦ f, naturality := ⋯ } j) ∧
      NatTrans.app { app := fun (x : PUnit.{w + 1}) ↦ f, naturality := ⋯ } j ≫
          NatTrans.app (𝟙 (Functor.obj (Functor.const PUnit.{w + 1}) Y)) j =
        f
⊢ P.ind f

Tactic:
refine ⟨PUnit, inferInstance, inferInstance, (Functor.const PUnit).obj Y, ?_, 𝟙 _, ?_, ?_⟩
-- 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
hf : P f
⊢ Quiver.Hom (V := Functor.{w, v, w, u} PUnit.{w + 1} C) (Functor.obj (Functor.const PUnit.{w + 1}) X)
    (Functor.obj (Functor.const PUnit.{w + 1}) Y)

Tactic:
exact { app _ := f }
-- 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
hf : P f
⊢ IsColimit.{w, v, w, u} { pt := Y, ι := 𝟙 (Functor.obj (Functor.const PUnit.{w + 1}) Y) }

Tactic:
exact isColimitConstCocone _ _

Premises used: CategoryTheory.Limits.isColimitConstCocone
-- 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
hf : P f
⊢ ∀ (j : PUnit.{w + 1}),
    P (X := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const PUnit.{w + 1}) X) j) (Y :=
        Functor.obj.{w, v, w, u} (Functor.obj (Functor.const PUnit.{w + 1}) Y) j)
        (NatTrans.app { app := fun (x : PUnit.{w + 1}) ↦ f, naturality := ⋯ } j) ∧
      NatTrans.app { app := fun (x : PUnit.{w + 1}) ↦ f, naturality := ⋯ } j ≫
          NatTrans.app (𝟙 (Functor.obj (Functor.const PUnit.{w + 1}) Y)) j =
        f

Tactic:
simpa
-- 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
⊢ P.ind f ↔ ObjectProperty.ind P.underObj (CategoryTheory.Under.mk f)

Tactic:
⟨fun ⟨J, _, _, D, t, s, hs, hst⟩ ↦ ?_, fun ⟨J, _, _, pres, hpres⟩ ↦ ?_⟩

Premises used: _private.0.CategoryTheory.MorphismProperty.ind_iff_ind_underMk.match_2, _private.0.CategoryTheory.MorphismProperty.ind_iff_ind_underMk.match_1, CategoryTheory.Under.mk, CategoryTheory.MorphismProperty.underObj, CategoryTheory.MorphismProperty.ind, Iff.intro, CategoryTheory.ObjectProperty.ind
-- 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
refine_1 :
  P.ind f →
    ∀ (J : Type w) (w : SmallCategory J),
      IsFiltered J →
        ∀ (D : Functor.{w, v, w, 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),
          ObjectProperty.ind P.underObj (CategoryTheory.Under.mk f)
refine_2 :
  ObjectProperty.ind P.underObj (CategoryTheory.Under.mk f) →
    ∀ (J : Type w) (w : SmallCategory J),
      IsFiltered J →
        ∀ (pres : ColimitPresentation J (CategoryTheory.Under.mk f)) (hpres : ∀ (i : J), P.underObj (pres.diag.obj i)),
          P.ind f
⊢ P.ind f ↔ ObjectProperty.ind P.underObj (CategoryTheory.Under.mk f)

Tactic:
refine ⟨fun ⟨J, _, _, D, t, s, hs, hst⟩ ↦ ?_, fun ⟨J, _, _, pres, hpres⟩ ↦ ?_⟩
-- 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 : P.ind f
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
D : Functor.{w, v, w, 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
⊢ ObjectProperty.ind P.underObj (CategoryTheory.Under.mk f)

Tactic:
⟨J, ‹_›, ‹_›, ⟨Under.lift D t, ?_, ?_⟩, ?_⟩

Premises used: CategoryTheory.Limits.ColimitPresentation.mk, Exists.intro, CategoryTheory.ObjectProperty.ind
-- 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 : P.ind f
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
D : Functor.{w, v, w, 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 : Under.lift D t ⟶ Functor.obj (Functor.const J) (CategoryTheory.Under.mk f)
refine_1₁ :
  IsColimit (J := J) (F := Under.lift D t)
    { pt := CategoryTheory.Under.mk f,
      ι := { app := fun (j : J) ↦ CategoryTheory.Under.homMk (s.app j) ⋯, naturality := ⋯ } }
refine_1₂ :
  ∀ (i : J),
    P.underObj
      ((ColimitPresentation.diag (X := CategoryTheory.Under.mk f)
            { diag := Under.lift D t,
              ι :=
                { app := fun (j : J) ↦ CategoryTheory.Under.homMk (s.app j) ⋯, naturality := ⋯ :
                  NatTrans (Under.lift D t) (Functor.obj (Functor.const J) (CategoryTheory.Under.mk f)) },
              isColimit :=
                have this : Nonempty J := ⋯;
                Under.isColimitLiftCocone D t { pt := Y, ι := s : Cocone D } f ⋯ hs :
              ColimitPresentation J (CategoryTheory.Under.mk f) }).obj
        i)
⊢ ObjectProperty.ind P.underObj (CategoryTheory.Under.mk f)

Tactic:
refine ⟨J, ‹_›, ‹_›, ⟨Under.lift D t, ?_, ?_⟩, ?_⟩
-- 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 : P.ind f
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
D : Functor.{w, v, w, 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
⊢ ((Under.lift D t).obj j).hom ≫ s.app j =
    (Functor.obj (Functor.obj (Functor.const J) (CategoryTheory.Under.mk f)) j).hom

Tactic:
simp [hst]
-- 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 : P.ind f
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
D : Functor.{w, v, w, 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
⊢ Under.lift D t ⟶ Functor.obj (Functor.const J) (CategoryTheory.Under.mk f)

Tactic:
exact { app j := CategoryTheory.Under.homMk (s.app j) (by simp [hst]) }
-- 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 : P.ind f
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
D : Functor.{w, v, w, 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
⊢ Nonempty J

Tactic:
have : Nonempty J := IsFiltered.nonempty
-- 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 : P.ind f
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
D : Functor.{w, v, w, 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
this : Nonempty J
⊢ ∀ (j : J), t.app j ≫ { pt := Y, ι := s : Cocone D }.ι.app j = f

Tactic:
simp [hst]
-- 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 : P.ind f
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
D : Functor.{w, v, w, 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
this : Nonempty J
⊢ IsColimit (J := J) (F := Under.lift D t)
    { pt := CategoryTheory.Under.mk f,
      ι := { app := fun (j : J) ↦ CategoryTheory.Under.homMk (s.app j) ⋯, naturality := ⋯ } }

Tactic:
exact Under.isColimitLiftCocone _ _ _ _ (by simp [hst]) hs

Premises used: CategoryTheory.Under.isColimitLiftCocone
-- 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 : P.ind f
J : Type w
w : SmallCategory J
w_1 : IsFiltered J
D : Functor.{w, v, w, 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
⊢ ∀ (i : J),
    P.underObj
      ((ColimitPresentation.diag (X := CategoryTheory.Under.mk f)
            { diag := Under.lift D t,
              ι :=
                { app := fun (j : J) ↦ CategoryTheory.Under.homMk (s.app j) ⋯, naturality := ⋯ :
                  NatTrans (Under.lift D t) (Functor.obj (Functor.const J) (CategoryTheory.Under.mk f)) },
              isColimit :=
                have this : Nonempty J := ⋯;
                Under.isColimitLiftCocone D t { pt := Y, ι := s : Cocone D } f ⋯ hs :
              ColimitPresentation J (CategoryTheory.Under.mk f) }).obj
        i)

Tactic:
simp [underObj, hst]

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)
⊢ P.ind f

Tactic:
⟨J, ‹_›, ‹_›, pres.diag ⋙ CategoryTheory.Under.forget _, ?_, ?_, ?_, fun j ↦ ⟨?_, ?_⟩⟩

Premises used: CategoryTheory.Functor.comp, CategoryTheory.MorphismProperty.ind, CategoryTheory.Under.forget, And.intro, Exists.intro
-- 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)
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)
refine_2₄ :
  ∀ (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
⊢ P.ind f

Tactic:
refine ⟨J, ‹_›, ‹_›, pres.diag ⋙ CategoryTheory.Under.forget _, ?_, ?_, ?_, fun 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)
⊢ Functor.obj (Functor.const J) X ⟶ pres.diag ⋙ CategoryTheory.Under.forget X

Tactic:
exact { app j := (pres.diag.obj j).hom }
-- 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)
⊢ pres.diag ⋙ CategoryTheory.Under.forget X ⟶ Functor.obj (Functor.const J) Y

Tactic:
exact Functor.whiskerRight pres.ι (CategoryTheory.Under.forget X)

Premises used: CategoryTheory.Limits.ColimitPresentation.ι, CategoryTheory.Under.forget, CategoryTheory.Functor.whiskerRight