awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst_2 : Category.{v_3, u_3} J
X Y Z_1 : Arrow (Functor.{v_3, v_1, u_3, u_1} J C)
f : X ⟶ Y
g : Y ⟶ Z_1
j : J
⊢ Eq.{v_1 + 1} (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj.{v_3, v_1, u_3, u_1}
        { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (X.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
          map := fun {X_1 Y : J} (φ : X_1 ⟶ Y) ↦
            data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (X.left.map φ) (X.right.map φ) ⋯),
          map_id := ⋯, map_comp := ⋯ }
        j)
      (Functor.obj.{v_3, v_1, u_3, u_1}
        { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Z_1.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
          map := fun {X Y : J} (φ : X ⟶ Y) ↦
            data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (Z_1.left.map φ) (Z_1.right.map φ) ⋯),
          map_id := ⋯, map_comp := ⋯ }
        j))
    (NatTrans.app
      {
        app := fun (j : J) ↦
          data.mapZ (W₁ := W₁) (W₂ := W₂)
            (Arrow.homMk ((Arrow.Hom.left (f ≫ g)).app j) ((Arrow.Hom.right (f ≫ g)).app j) ⋯),
        naturality := ⋯ }
      j)
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        { obj := fun (j : J) ↦ (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Y.hom.app j)).Z (W₁ := W₁) (W₂ := W₂),
          map := fun {X Y_1 : J} (φ : X ⟶ Y_1) ↦
            data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk (Y.left.map φ) (Y.right.map φ) ⋯),
          map_id := ⋯, map_comp := ⋯ })
        {
          app := fun (j : J) ↦
            data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left f).app j) ((Arrow.Hom.right f).app j) ⋯),
          naturality := ⋯ }
        {
          app := fun (j : J) ↦
            data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left g).app j) ((Arrow.Hom.right g).app j) ⋯),
          naturality := ⋯ })
      j)
have w : Eq (α :=
  (data.factorizationData (W₁ := W₁) (W₂ := W₂) (X.hom.app j)).Z (W₁ := W₁) (W₂ := W₂) ⟶
    (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Z_1.hom.app j)).Z (W₁ := W₁) (W₂ := W₂))
  (data.mapZ (W₁ := W₁) (W₂ := W₂)
    (Arrow.homMk ((Arrow.Hom.left f).app j ≫ (Arrow.Hom.left g).app j)
      ((Arrow.Hom.right f).app j ≫ (Arrow.Hom.right g).app j) sorry))
  (CategoryStruct.comp (Y := (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Y.hom.app j)).Z (W₁ := W₁) (W₂ := W₂))
    (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left f).app j) ((Arrow.Hom.right f).app j) sorry))
    (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left g).app j) ((Arrow.Hom.right g).app j) sorry)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst_2 : Category.{v_3, u_3} J
X Y Z_1 : Arrow (Functor.{v_3, v_1, u_3, u_1} J C)
f : X ⟶ Y
g : Y ⟶ Z_1
j : J
⊢ Eq (α :=
    (data.factorizationData (W₁ := W₁) (W₂ := W₂) (X.hom.app j)).Z (W₁ := W₁) (W₂ := W₂) ⟶
      (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Z_1.hom.app j)).Z (W₁ := W₁) (W₂ := W₂))
    (data.mapZ (W₁ := W₁) (W₂ := W₂)
      (Arrow.homMk ((Arrow.Hom.left f).app j ≫ (Arrow.Hom.left g).app j)
        ((Arrow.Hom.right f).app j ≫ (Arrow.Hom.right g).app j) ⋯))
    (CategoryStruct.comp (Y := (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Y.hom.app j)).Z (W₁ := W₁) (W₂ := W₂))
      (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left f).app j) ((Arrow.Hom.right f).app j) ⋯))
      (data.mapZ (W₁ := W₁) (W₂ := W₂) (Arrow.homMk ((Arrow.Hom.left g).app j) ((Arrow.Hom.right g).app j) ⋯)))
have w : Eq (α :=
  (data.factorizationData (W₁ := W₁) (W₂ := W₂) (X.hom.app j)).Z (W₁ := W₁) (W₂ := W₂) ⟶
    (data.factorizationData (W₁ := W₁) (W₂ := W₂) (Z_1.hom.app j)).Z (W₁ := W₁) (W₂ := W₂))
  (data.mapZ (W₁ := W₁) (W₂ := W₂)
    (Arrow.homMk ((Arrow.Hom.left f).app j ≫ (Arrow.Hom.left g).app j)
      ((Arrow.Hom.right f).app j ≫ (Arrow.Hom.right g).app j) sorry))
  (data.mapZ (W₁ := W₁) (W₂ := W₂)
    (CategoryStruct.comp (Y := Arrow.mk (Y.hom.app j))
      (Arrow.homMk ((Arrow.Hom.left f).app j) ((Arrow.Hom.right f).app j) sorry)
      (Arrow.homMk ((Arrow.Hom.left g).app j) ((Arrow.Hom.right g).app j) sorry)))
Tactic: rw [← data.mapZ_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_2 : F.IsEquivalence
inst_3 : W₁.RespectsIso
inst_4 : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
⊢ W₁.inverseImage F (Y := F.objPreimage (h.Z (W₁ := W₁) (W₂ := W₂)))
    (F.preimage (h.i (W₁ := W₁) (W₂ := W₂) ≫ Iso.inv (F.objObjPreimageIso (h.Z (W₁ := W₁) (W₂ := W₂)))))
have refine : Arrow.mk (h.i (W₁ := W₁) (W₂ := W₂)) ≅
  Arrow.mk (Y := F.obj (F.objPreimage (h.Z (W₁ := W₁) (W₂ := W₂))))
    (F.map (F.preimage (h.i (W₁ := W₁) (W₂ := W₂) ≫ Iso.inv (F.objObjPreimageIso (h.Z (W₁ := W₁) (W₂ := W₂))))))
Tactic: refine (W₁.arrow_mk_iso_iff ?_).1 h.hi
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Factorization (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_2 : F.IsEquivalence
inst_3 : W₁.RespectsIso
inst_4 : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
⊢ W₂.inverseImage F (X := F.objPreimage (h.Z (W₁ := W₁) (W₂ := W₂)))
    (F.preimage (Iso.hom (F.objObjPreimageIso (h.Z (W₁ := W₁) (W₂ := W₂))) ≫ h.p (W₁ := W₁) (W₂ := W₂)))
have refine : Arrow.mk (h.p (W₁ := W₁) (W₂ := W₂)) ≅
  Arrow.mk (X := F.obj (F.objPreimage (h.Z (W₁ := W₁) (W₂ := W₂))))
    (F.map (F.preimage (Iso.hom (F.objObjPreimageIso (h.Z (W₁ := W₁) (W₂ := W₂))) ≫ h.p (W₁ := W₁) (W₂ := W₂))))
Tactic: refine (W₂.arrow_mk_iso_iff ?_).1 h.hp
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.FunctorCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
K : Type u'
inst_1 : LinearOrder K
inst_2 : SuccOrder K
inst_3 : OrderBot K
inst_4 : WellFoundedLT K
inst_5 : W.IsStableUnderTransfiniteCompositionOfShape K
J : Type u''
inst_6 : Category.{v'', u''} J
inst_7 : HasIterationOfShape.{u', v, u} K C
X Y : Functor.{v'', v, u'', u} J C
f : X ⟶ Y
hf : TransfiniteCompositionOfShape (W.functorCategory J) K f
j : J
⊢ W (f.app j)
have have : ∀
  (this :
    LE.le (α := MorphismProperty (Functor.{v'', v, u'', u} J C)) (W.functorCategory J)
      (W.inverseImage (Functor.obj (evaluation J C) j))),
  W (f.app j)
Tactic: have : W.functorCategory J ≤ W.inverseImage ((evaluation _ _).obj j) := fun _ _ _ h ↦ h _
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.FunctorCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u''
inst_1 : Category.{v'', u''} J
⊢ Eq (α := MorphismProperty (Functor.{v'', v, u'', u} J C)) (functorCategory (isomorphisms C) J)
    (isomorphisms (Functor.{v'', v, u'', u} J C))
have h : ∀ ⦃X Y : Functor.{v'', v, u'', u} J C⦄ (f : X ⟶ Y),
  functorCategory (isomorphisms C) J f ↔ isomorphisms (Functor.{v'', v, u'', u} J C) f
Tactic: ext _ _ f
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.FunctorCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u''
inst_1 : Category.{v'', u''} J
inst_2 : HasPullbacks.{v, u} C
⊢ Eq (α := MorphismProperty (Functor.{v'', v, u'', u} J C)) (functorCategory (monomorphisms C) J)
    (monomorphisms (Functor.{v'', v, u'', u} J C))
have h : ∀ ⦃X Y : Functor.{v'', v, u'', u} J C⦄ (f : X ⟶ Y),
  functorCategory (monomorphisms C) J f ↔ monomorphisms (Functor.{v'', v, u'', u} J C) f
Tactic: ext _ _ f
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.FunctorCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u''
inst_1 : Category.{v'', u''} J
inst_2 : HasPushouts.{v, u} C
⊢ Eq (α := MorphismProperty (Functor.{v'', v, u'', u} J C)) (functorCategory (epimorphisms C) J)
    (epimorphisms (Functor.{v'', v, u'', u} J C))
have 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
Tactic: ext _ _ f
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.FunctorCategory (goal)
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)
    (monomorphisms (Functor.{v'', v, u'', u} J C)) K
have rw : IsStableUnderTransfiniteCompositionOfShape (C := Functor.{v'', v, u'', u} J C) (functorCategory (monomorphisms C) J) K
Tactic: rw [← functorCategory_monomorphisms]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.FunctorCategory (goal)
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) (monomorphisms (Functor.{v'', v, u'', u} J C)) K'
have rw : IsStableUnderCoproductsOfShape (C := Functor.{v'', v, u'', u} J C) (functorCategory (monomorphisms C) J) K'
Tactic: rw [← functorCategory_monomorphisms]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT (hypothesis)
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
⊢ ∃ (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
have hf₁ : ∃ (i : ι), Arrow.mk f.hom = Arrow.mk (f_1 i)
Tactic: rw [MorphismProperty.mem_toSet_iff, MorphismProperty.ofHoms_iff] at hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT (goal)
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)
⊢ ∃ (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
have 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)) sorry :
            { 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
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT (goal)
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)
⊢ ∃ (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
have 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)) sorry :
            { 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
Tactic: obtain rfl : f = _ := hf
Cleared hypotheses: f, hf_1, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT (goal)
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 (↑(toSet (⨆ (i : ι), P i)) : Type (max u v)) κ
have rw : HasCardinalLT (↑(⋃ (i : ι), (P i).toSet) : Type (max u v)) κ
Tactic: rw [toSet_iSup]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT (goal)
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₁ ⊔ P₂).toSet : Type (max u v)) κ
have rw : HasCardinalLT (↑(P₁.toSet ∪ P₂.toSet) : Type (max u v)) κ
Tactic: rw [MorphismProperty.toSet_max]
-- 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
hf : P f
⊢ P.ind f
have 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)
Tactic: refine ⟨PUnit, inferInstance, inferInstance, (Functor.const PUnit).obj Y, ?_, 𝟙 _, ?_, ?_⟩
-- 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
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)
⊢ P.ind f
have refine_2 : IsColimit.{w, v, w, u} { pt := Y, ι := 𝟙 (Functor.obj (Functor.const PUnit.{w + 1}) Y) }
Tactic: refine ⟨PUnit, inferInstance, inferInstance, (Functor.const PUnit).obj Y, ?_, 𝟙 _, ?_, ?_⟩
-- 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
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) }
⊢ P.ind f
have 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 := sorry } j) ∧
    NatTrans.app { app := fun (x : PUnit.{w + 1}) ↦ f, naturality := sorry } j ≫
        NatTrans.app (𝟙 (Functor.obj (Functor.const PUnit.{w + 1}) Y)) j =
      f
Tactic: refine ⟨PUnit, inferInstance, inferInstance, (Functor.const PUnit).obj Y, ?_, 𝟙 _, ?_, ?_⟩
-- 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
⊢ P.ind f ↔ ObjectProperty.ind P.underObj (CategoryTheory.Under.mk f)
have 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)
Tactic: refine ⟨fun ⟨J, _, _, D, t, s, hs, hst⟩ ↦ ?_, fun ⟨J, _, _, pres, hpres⟩ ↦ ?_⟩
-- 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
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)
⊢ P.ind f ↔ ObjectProperty.ind P.underObj (CategoryTheory.Under.mk f)
have 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
Tactic: refine ⟨fun ⟨J, _, _, D, t, s, hs, hst⟩ ↦ ?_, fun ⟨J, _, _, pres, hpres⟩ ↦ ?_⟩
-- 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 : 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)
have refine_1 : Under.lift D t ⟶ Functor.obj (Functor.const J) (CategoryTheory.Under.mk f)
Tactic: refine ⟨J, ‹_›, ‹_›, ⟨Under.lift D t, ?_, ?_⟩, ?_⟩
-- 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 : 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)
⊢ ObjectProperty.ind P.underObj (CategoryTheory.Under.mk f)
have 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) sorry, naturality := sorry } }
Tactic: refine ⟨J, ‹_›, ‹_›, ⟨Under.lift D t, ?_, ?_⟩, ?_⟩
-- 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 : 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 := ⋯ } }
⊢ ObjectProperty.ind P.underObj (CategoryTheory.Under.mk f)
have 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) sorry, naturality := sorry :
                NatTrans (Under.lift D t) (Functor.obj (Functor.const J) (CategoryTheory.Under.mk f)) },
            isColimit :=
              have this : Nonempty J := sorry;
              Under.isColimitLiftCocone D t { pt := Y, ι := s : Cocone D } f sorry hs :
            ColimitPresentation J (CategoryTheory.Under.mk f) }).obj
      i)
Tactic: refine ⟨J, ‹_›, ‹_›, ⟨Under.lift D t, ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Ind (hypothesis)
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
⊢ IsColimit (J := J) (F := Under.lift D t)
    { pt := CategoryTheory.Under.mk f,
      ι := { app := fun (j : J) ↦ CategoryTheory.Under.homMk (s.app j) ⋯, naturality := ⋯ } }
have this : Nonempty J
Tactic: have : Nonempty J := IsFiltered.nonempty
-- 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)
⊢ P.ind f
have refine_2 : Functor.obj (Functor.const J) X ⟶ pres.diag ⋙ CategoryTheory.Under.forget X
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 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
⊢ P.ind f
have refine_2₁ : pres.diag ⋙ CategoryTheory.Under.forget X ⟶ Functor.obj (Functor.const J) Y
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 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
⊢ P.ind f
have refine_2₂ : IsColimit
  { pt := Y, ι := Functor.whiskerRight pres.ι (CategoryTheory.Under.forget X) :
    Cocone (pres.diag ⋙ CategoryTheory.Under.forget X) }
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 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) }
⊢ P.ind f
have 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 := sorry } j)
Tactic: refine ⟨J, ‹_›, ‹_›, pres.diag ⋙ CategoryTheory.Under.forget _, ?_, ?_, ?_, fun j ↦ ⟨?_, ?_⟩⟩