awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Filtered (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
inst_2 : HasColimit F
i j : J
xi : F.obj i
xj : F.obj j
rw :
  Eq (α := F.ColimitType)
      ((Equiv.symm (equivShrink F.ColimitType) : (a : Shrink.{u, max u v} F.ColimitType) → F.ColimitType)
          ((equivShrink F.ColimitType : (a : F.ColimitType) → Shrink.{u, max u v} F.ColimitType)
            (F.ιColimitType i xi)) :
        F.ColimitType)
      ((Equiv.symm (equivShrink F.ColimitType) : (a : Shrink.{u, max u v} F.ColimitType) → F.ColimitType)
          ((equivShrink F.ColimitType : (a : F.ColimitType) → Shrink.{u, max u v} F.ColimitType)
            (F.ιColimitType j xj)) :
        F.ColimitType) ↔
    FilteredColimit.Rel F (Sigma.mk (β := fun (j : J) ↦ F.obj j) i xi) (Sigma.mk (β := fun (j : J) ↦ F.obj j) j xj)
rw₁ :
  F.ιColimitType i xi =
      (Equiv.symm (equivShrink F.ColimitType) : (a : Shrink.{u, max u v} F.ColimitType) → F.ColimitType)
        ((equivShrink F.ColimitType : (a : F.ColimitType) → Shrink.{u, max u v} F.ColimitType) (F.ιColimitType j xj)) ↔
    FilteredColimit.Rel F (Sigma.mk (β := fun (j : J) ↦ F.obj j) i xi) (Sigma.mk (β := fun (j : J) ↦ F.obj j) j xj)
rw₂ :
  F.ιColimitType i xi = F.ιColimitType j xj ↔
    FilteredColimit.Rel F (Sigma.mk (β := fun (j : J) ↦ F.obj j) i xi) (Sigma.mk (β := fun (j : J) ↦ F.obj j) j xj)
rw₃ :
  Relation.EqvGen F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) i xi)
      (Sigma.mk (β := fun (j : J) ↦ F.obj j) j xj) ↔
    FilteredColimit.Rel F (Sigma.mk (β := fun (j : J) ↦ F.obj j) i xi) (Sigma.mk (β := fun (j : J) ↦ F.obj j) j xj)
⊢ Eq.{u + 1} (α := Shrink.{u, max u v} F.ColimitType)
      ((equivShrink F.ColimitType : (a : F.ColimitType) → Shrink.{u, max u v} F.ColimitType) (F.ιColimitType i xi) :
        Shrink.{u, max u v} F.ColimitType)
      ((equivShrink F.ColimitType : (a : F.ColimitType) → Shrink.{u, max u v} F.ColimitType) (F.ιColimitType j xj) :
        Shrink.{u, max u v} F.ColimitType) ↔
    FilteredColimit.Rel F (Sigma.mk (β := fun (j : J) ↦ F.obj j) i xi) (Sigma.mk (β := fun (j : J) ↦ F.obj j) j xj)
have rw₄ : Relation.EqvGen F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) i xi)
    (Sigma.mk (β := fun (j : J) ↦ F.obj j) j xj) ↔
  Relation.EqvGen F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) i xi)
    (Sigma.mk (β := fun (j : J) ↦ F.obj j) j xj)
Tactic: rw [← (equivShrink _).symm.injective.eq_iff, Equiv.symm_apply_apply, Equiv.symm_apply_apply,
    Functor.ιColimitType_eq_iff, FilteredColimit.rel_eq_eqvGen_colimitTypeRel]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Filtered (hypothesis)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
⊢ Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i))
      ((hom (FC := TypeCat.Fun) (t.ι.app i) :
            (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
          xi :
        (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i))
      ((hom (FC := TypeCat.Fun) (t.ι.app j) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
          xj :
        (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j)) ↔
    ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
      Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
            xi :
          (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj k))
            xj :
          (fun (X : Type u) ↦ X) (F.obj k))
have this : HasColimit F
Tactic: have : HasColimit F := ⟨_, ht⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Filtered (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
⊢ Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i))
      ((hom (FC := TypeCat.Fun) (t.ι.app i) :
            (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
          xi :
        (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i))
      ((hom (FC := TypeCat.Fun) (t.ι.app j) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
          xj :
        (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j)) ↔
    ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
      Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
            xi :
          (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj k))
            xj :
          (fun (X : Type u) ↦ X) (F.obj k))
have refine : Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i))
    ((hom (FC := TypeCat.Fun) (t.ι.app i) :
          (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
        xi :
      (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i))
    ((hom (FC := TypeCat.Fun) (t.ι.app j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
        xj :
      (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j)) ↔
  Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i))
    ((hom (FC := TypeCat.Fun) ((colimitCocone F).ι.app i) :
          (a : (fun (X : Type u) ↦ X) (F.obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj (colimitCocone F).pt).obj i))
        xi :
      (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i))
    ((hom (FC := TypeCat.Fun) ((colimitCocone F).ι.app j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj (colimitCocone F).pt).obj j))
        xj :
      (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) j))
Tactic: refine Iff.trans ?_ (colimit_eq_iff_aux F)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Filtered (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i j : J
xi : F.obj i
xj : F.obj j
this : HasColimit F
⊢ Eq (α := (colimitCocone F).pt)
      ((Iso.toEquiv (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)) : (a : t.pt) → (colimitCocone F).pt)
          ((hom (FC := TypeCat.Fun) (t.ι.app i) :
                (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
              xi :
            (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i)) :
        (colimitCocone F).pt)
      ((Iso.toEquiv (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)) : (a : t.pt) → (colimitCocone F).pt)
          ((hom (FC := TypeCat.Fun) (t.ι.app j) :
                (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
              xj :
            (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j)) :
        (colimitCocone F).pt) ↔
    Eq (α :=
      (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i))
      ((hom (FC := TypeCat.Fun) ((colimitCocone F).ι.app i) :
            (a : (fun (X : Type u) ↦ X) (F.obj i)) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj (colimitCocone F).pt).obj i))
          xi :
        (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i))
      ((hom (FC := TypeCat.Fun) ((colimitCocone F).ι.app j) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj (colimitCocone F).pt).obj j))
          xj :
        (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) j))
have h : (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i) =
    (colimitCocone F).pt →
  Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i))
    ((hom (FC := TypeCat.Fun) ((colimitCocone F).ι.app i) :
          (a : (fun (X : Type u) ↦ X) (F.obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj (colimitCocone F).pt).obj i))
        xi :
      (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) (colimitCocone F).pt) i))
    ((Iso.toEquiv (ht.coconePointUniqueUpToIso (colimitCoconeIsColimit F)) : (a : t.pt) → (colimitCocone F).pt)
        ((hom (FC := TypeCat.Fun) (t.ι.app i) :
              (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
            xi :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i)) :
      (colimitCocone F).pt)
Tactic: convert! Iff.rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Filtered (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
⊢ Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i))
      ((hom (FC := TypeCat.Fun) (t.ι.app i) :
            (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
          x :
        (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i))
      ((hom (FC := TypeCat.Fun) (t.ι.app i) :
            (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj i))
          y :
        (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) i)) ↔
    ∃ (j : J) (f : i ⟶ j),
      Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
            x :
          (fun (X : Type u) ↦ X) (F.obj j))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
            y :
          (fun (X : Type u) ↦ X) (F.obj j))
have rw : (∃ (k : J) (f : i ⟶ k) (g : i ⟶ k),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
      ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
          x :
        (fun (X : Type u) ↦ X) (F.obj k))
      ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
          y :
        (fun (X : Type u) ↦ X) (F.obj k))) ↔
  ∃ (j : J) (f : i ⟶ j),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
          x :
        (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
          y :
        (fun (X : Type u) ↦ X) (F.obj j))
Tactic: rw [isColimit_eq_iff _ ht]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Filtered (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
⊢ (∃ (k : J) (f : i ⟶ k) (g : i ⟶ k),
      Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
            x :
          (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
            y :
          (fun (X : Type u) ↦ X) (F.obj k))) ↔
    ∃ (j : J) (f : i ⟶ j),
      Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
            x :
          (fun (X : Type u) ↦ X) (F.obj j))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
            y :
          (fun (X : Type u) ↦ X) (F.obj j))
have mp : (∃ (k : J) (f : i ⟶ k) (g : i ⟶ k),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
      ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
          x :
        (fun (X : Type u) ↦ X) (F.obj k))
      ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
          y :
        (fun (X : Type u) ↦ X) (F.obj k))) →
  ∃ (j : J) (f : i ⟶ j),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
          x :
        (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
          y :
        (fun (X : Type u) ↦ X) (F.obj j))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Filtered (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
mp :
  (∃ (k : J) (f : i ⟶ k) (g : i ⟶ k),
      Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
            x :
          (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
            y :
          (fun (X : Type u) ↦ X) (F.obj k))) →
    ∃ (j : J) (f : i ⟶ j),
      Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
            x :
          (fun (X : Type u) ↦ X) (F.obj j))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
            y :
          (fun (X : Type u) ↦ X) (F.obj j))
⊢ (∃ (k : J) (f : i ⟶ k) (g : i ⟶ k),
      Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
            x :
          (fun (X : Type u) ↦ X) (F.obj k))
        ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
            y :
          (fun (X : Type u) ↦ X) (F.obj k))) ↔
    ∃ (j : J) (f : i ⟶ j),
      Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
            x :
          (fun (X : Type u) ↦ X) (F.obj j))
        ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
            y :
          (fun (X : Type u) ↦ X) (F.obj j))
have mpr : (∃ (j : J) (f : i ⟶ j),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
          x :
        (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
          y :
        (fun (X : Type u) ↦ X) (F.obj j))) →
  ∃ (k : J) (f : i ⟶ k) (g : i ⟶ k),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
      ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
          x :
        (fun (X : Type u) ↦ X) (F.obj k))
      ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k))
          y :
        (fun (X : Type u) ↦ X) (F.obj k))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Filtered (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k)) x :
      (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k)) y :
      (fun (X : Type u) ↦ X) (F.obj k))
⊢ ∃ (j : J) (f : i ⟶ j),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
          x :
        (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj j))
          y :
        (fun (X : Type u) ↦ X) (F.obj j))
have mp : Eq (α := (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
  ((hom (FC := TypeCat.Fun) (F.map (f ≫ IsFiltered.coeqHom f g)) :
        (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
      x :
    (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
  ((hom (FC := TypeCat.Fun) (F.map (f ≫ IsFiltered.coeqHom f g)) :
        (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
      y :
    (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
Tactic: refine ⟨IsFiltered.coeq f g, f ≫ IsFiltered.coeqHom f g, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Filtered (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k)) x :
      (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k)) y :
      (fun (X : Type u) ↦ X) (F.obj k))
| ((hom (FC := TypeCat.Fun) (F.map (f ≫ IsFiltered.coeqHom f g)) :
        (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
      y :
    (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
have rw : ((hom (FC := TypeCat.Fun) (F.map (g ≫ IsFiltered.coeqHom f g)) :
      (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
    y :
  (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
Tactic: rw [IsFiltered.coeq_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Filtered (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k)) x :
      (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj k)) y :
      (fun (X : Type u) ↦ X) (F.obj k))
⊢ Eq (α := (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
    ((hom (FC := TypeCat.Fun) (F.map (f ≫ IsFiltered.coeqHom f g)) :
          (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
        x :
      (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
    ((hom (FC := TypeCat.Fun) (F.map (f ≫ IsFiltered.coeqHom f g)) :
          (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
        y :
      (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
have mp : Eq (α := (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
  ((hom (FC := TypeCat.Fun) (F.map (f ≫ IsFiltered.coeqHom f g)) :
        (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
      x :
    (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
  ((hom (FC := TypeCat.Fun) (F.map (g ≫ IsFiltered.coeqHom f g)) :
        (a : (fun (X : Type u) ↦ X) (F.obj i)) → (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
      y :
    (fun (X : Type u) ↦ X) (F.obj (IsFiltered.coeq f g)))
Tactic: conv_rhs => rw [IsFiltered.coeq_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Filtered (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
x₁ x₂ : t.pt
⊢ ∃ (j : J) (x₁' : F.obj j) (x₂' : F.obj j),
    (hom (FC := TypeCat.Fun) (t.ι.app j) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
          x₁' =
        x₁ ∧
      (hom (FC := TypeCat.Fun) (t.ι.app j) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
          x₂' =
        x₂
have obtain : ∀ (j₁ : J) (x₁ : F.obj j₁),
  ∃ (j : J) (x₁' : F.obj j) (x₂' : F.obj j),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j))
        ((hom (FC := TypeCat.Fun) (t.ι.app j) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
            x₁' :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j))
        ((hom (FC := TypeCat.Fun) (t.ι.app j₁) :
              (a : (fun (X : Type u) ↦ X) (F.obj j₁)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j₁))
            x₁ :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j₁)) ∧
      (hom (FC := TypeCat.Fun) (t.ι.app j) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
          x₂' =
        x₂
Tactic: obtain ⟨j₁, x₁, rfl⟩ := Types.jointly_surjective_of_isColimit ht x₁
Cleared hypotheses: x₁