-- Module: Mathlib.CategoryTheory.Filtered.Basic
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
refine_1 :
  Superset.{u_1} (α := Set ((fun (X : Type u_1) ↦ X) (F.obj j)))
    ((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)))
refine_2 :
  (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))))
      (PSigma.mk (β := fun (i : C) ↦ i ⟶ j) l (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:
refine ⟨⟨l, lk ≫ kj⟩, e ▸ ?_, ?_⟩