-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h :
  ∀ (j : J),
    ∃ (i : J) (f : i ⟶ j),
      Set.Finite (α := (fun (X : Type v) ↦ X) (F.obj j))
        (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j)))
j i_1 : J
hi : i_1 ⟶ j
hf :
  Set.Finite (α := (fun (X : Type v) ↦ X) (F.obj j))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj i_1))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map hi)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i_1)) → (fun (X : Type v) ↦ X) (F.obj j)))
m : Finset (F.obj j)
hmin :
  ∀ (x : Finset (F.obj j)),
    Membership.mem (γ := Set (Finset (F.obj j)))
        {s : Finset (F.obj j) |
          ∃ (i : J) (f : i ⟶ j),
            (↑s : Set ((fun (X : Type v) ↦ X) (F.obj j))) =
              range (ι := (fun (X : Type v) ↦ X) (F.obj i))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
                  (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))}
        x →
      ¬x < m
i : J
f : i ⟶ j
hm :
  (↑m : Set ((fun (X : Type v) ↦ X) (F.obj j))) =
    range (ι := (fun (X : Type v) ↦ X) (F.obj i))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
k : J
g : k ⟶ j
k' : J
g' : k' ⟶ j
hl :
  LE.le.{v} (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
    ((fun (f : (i : J) ×' (i ⟶ j)) ↦
        (range (ι := (fun (X : Type v) ↦ X) (F.obj (f.fst (β := fun (i : J) ↦ i ⟶ j))))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : J) ↦ i ⟶ j)))) :
              (a : (fun (X : Type v) ↦ X) (F.obj f.fst)) → (fun (X : Type v) ↦ X) (F.obj j)) :
          Set ((fun (X : Type v) ↦ X) (F.obj j))))
      (PSigma.mk (β := fun (i : J) ↦ i ⟶ j) k' g'))
    ((fun (f : (i : J) ×' (i ⟶ j)) ↦
        (range (ι := (fun (X : Type v) ↦ X) (F.obj (f.fst (β := fun (i : J) ↦ i ⟶ j))))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : J) ↦ i ⟶ j)))) :
              (a : (fun (X : Type v) ↦ X) (F.obj f.fst)) → (fun (X : Type v) ↦ X) (F.obj j)) :
          Set ((fun (X : Type v) ↦ X) (F.obj j))))
      (PSigma.mk (β := fun (i : J) ↦ i ⟶ j) i f))
⊢ LE.le.{v} (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
    ((fun (f : (i : J) ×' (i ⟶ j)) ↦
        (range (ι := (fun (X : Type v) ↦ X) (F.obj (f.fst (β := fun (i : J) ↦ i ⟶ j))))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : J) ↦ i ⟶ j)))) :
              (a : (fun (X : Type v) ↦ X) (F.obj f.fst)) → (fun (X : Type v) ↦ X) (F.obj j)) :
          Set ((fun (X : Type v) ↦ X) (F.obj j))))
      (PSigma.mk (β := fun (i : J) ↦ i ⟶ j) i f))
    ((fun (f : (i : J) ×' (i ⟶ j)) ↦
        (range (ι := (fun (X : Type v) ↦ X) (F.obj (f.fst (β := fun (i : J) ↦ i ⟶ j))))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : J) ↦ i ⟶ j)))) :
              (a : (fun (X : Type v) ↦ X) (F.obj f.fst)) → (fun (X : Type v) ↦ X) (F.obj j)) :
          Set ((fun (X : Type v) ↦ X) (F.obj j))))
      (PSigma.mk (β := fun (i : J) ↦ i ⟶ j) k' g'))
have refine : ¬LT.lt.{v} (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
    ((fun (f : (i : J) ×' (i ⟶ j)) ↦
        (range (ι := (fun (X : Type v) ↦ X) (F.obj (f.fst (β := fun (i : J) ↦ i ⟶ j))))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : J) ↦ i ⟶ j)))) :
              (a : (fun (X : Type v) ↦ X) (F.obj f.fst)) → (fun (X : Type v) ↦ X) (F.obj j)) :
          Set ((fun (X : Type v) ↦ X) (F.obj j))))
      (PSigma.mk (β := fun (i : J) ↦ i ⟶ j) k' g'))
    ((fun (f : (i : J) ×' (i ⟶ j)) ↦
        (range (ι := (fun (X : Type v) ↦ X) (F.obj (f.fst (β := fun (i : J) ↦ i ⟶ j))))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : J) ↦ i ⟶ j)))) :
              (a : (fun (X : Type v) ↦ X) (F.obj f.fst)) → (fun (X : Type v) ↦ X) (F.obj j)) :
          Set ((fun (X : Type v) ↦ X) (F.obj j))))
      (PSigma.mk (β := fun (i : J) ↦ i ⟶ j) i f))
Tactic: refine (eq_of_le_of_not_lt hl ?_).ge