-- 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
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)
have refine_1 : (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))))
    (PSigma.mk (β := fun (i : C) ↦ i ⟶ j) l (li ≫ ij)))
Tactic: refine ⟨⟨l, lk ≫ kj⟩, e ▸ ?_, ?_⟩