-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} C (Type u_1)
j : C
x x_1 : (i : C) ×' (i ⟶ j)
i : C
ij : i ⟶ j
k : C
kj : k ⟶ j
⊢ ∃ (z : (i : C) ×' (i ⟶ j)),
    (fun (x1 x2 : Set ((fun (X : Type u_1) ↦ X) (F.obj j))) ↦ x1 ⊇ x2)
        ((fun (f : (i : C) ×' (i ⟶ j)) ↦
            (Set.range (ι := (fun (X : Type u_1) ↦ X) (F.obj (f.fst (β := fun (i : C) ↦ i ⟶ j))))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : C) ↦ i ⟶ j)))) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj f.fst)) → (fun (X : Type u_1) ↦ X) (F.obj j)) :
              Set ((fun (X : Type u_1) ↦ X) (F.obj j))))
          (PSigma.mk (β := fun (i : C) ↦ i ⟶ j) i ij))
        ((fun (f : (i : C) ×' (i ⟶ j)) ↦
            (Set.range (ι := (fun (X : Type u_1) ↦ X) (F.obj (f.fst (β := fun (i : C) ↦ i ⟶ j))))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : C) ↦ i ⟶ j)))) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj f.fst)) → (fun (X : Type u_1) ↦ X) (F.obj j)) :
              Set ((fun (X : Type u_1) ↦ X) (F.obj j))))
          z) ∧
      (fun (x1 x2 : Set ((fun (X : Type u_1) ↦ X) (F.obj j))) ↦ x1 ⊇ x2)
        ((fun (f : (i : C) ×' (i ⟶ j)) ↦
            (Set.range (ι := (fun (X : Type u_1) ↦ X) (F.obj (f.fst (β := fun (i : C) ↦ i ⟶ j))))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : C) ↦ i ⟶ j)))) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj f.fst)) → (fun (X : Type u_1) ↦ X) (F.obj j)) :
              Set ((fun (X : Type u_1) ↦ X) (F.obj j))))
          (PSigma.mk (β := fun (i : C) ↦ i ⟶ j) k kj))
        ((fun (f : (i : C) ×' (i ⟶ j)) ↦
            (Set.range (ι := (fun (X : Type u_1) ↦ X) (F.obj (f.fst (β := fun (i : C) ↦ i ⟶ j))))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : C) ↦ i ⟶ j)))) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj f.fst)) → (fun (X : Type u_1) ↦ X) (F.obj j)) :
              Set ((fun (X : Type u_1) ↦ X) (F.obj j))))
          z)
have let : ∀ (l : C) (li : l ⟶ i) (lk : l ⟶ k) (e : li ≫ ij = lk ≫ kj),
  ∃ (z : (i : C) ×' (i ⟶ j)),
    (fun (x1 x2 : Set ((fun (X : Type u_1) ↦ X) (F.obj j))) ↦ x1 ⊇ x2)
        ((fun (f : (i : C) ×' (i ⟶ j)) ↦
            (Set.range (ι := (fun (X : Type u_1) ↦ X) (F.obj (f.fst (β := fun (i : C) ↦ i ⟶ j))))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : C) ↦ i ⟶ j)))) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj f.fst)) → (fun (X : Type u_1) ↦ X) (F.obj j)) :
              Set ((fun (X : Type u_1) ↦ X) (F.obj j))))
          (PSigma.mk (β := fun (i : C) ↦ i ⟶ j) i ij))
        ((fun (f : (i : C) ×' (i ⟶ j)) ↦
            (Set.range (ι := (fun (X : Type u_1) ↦ X) (F.obj (f.fst (β := fun (i : C) ↦ i ⟶ j))))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : C) ↦ i ⟶ j)))) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj f.fst)) → (fun (X : Type u_1) ↦ X) (F.obj j)) :
              Set ((fun (X : Type u_1) ↦ X) (F.obj j))))
          z) ∧
      (fun (x1 x2 : Set ((fun (X : Type u_1) ↦ X) (F.obj j))) ↦ x1 ⊇ x2)
        ((fun (f : (i : C) ×' (i ⟶ j)) ↦
            (Set.range (ι := (fun (X : Type u_1) ↦ X) (F.obj (f.fst (β := fun (i : C) ↦ i ⟶ j))))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : C) ↦ i ⟶ j)))) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj f.fst)) → (fun (X : Type u_1) ↦ X) (F.obj j)) :
              Set ((fun (X : Type u_1) ↦ X) (F.obj j))))
          (PSigma.mk (β := fun (i : C) ↦ i ⟶ j) k kj))
        ((fun (f : (i : C) ×' (i ⟶ j)) ↦
            (Set.range (ι := (fun (X : Type u_1) ↦ X) (F.obj (f.fst (β := fun (i : C) ↦ i ⟶ j))))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : C) ↦ i ⟶ j)))) :
                  (a : (fun (X : Type u_1) ↦ X) (F.obj f.fst)) → (fun (X : Type u_1) ↦ X) (F.obj j)) :
              Set ((fun (X : Type u_1) ↦ X) (F.obj j))))
          z)
Tactic: let ⟨l, li, lk, e⟩ := cospan ij kj