-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (hypothesis)
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))
⊢ ¬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))
have this : ¬sorry.toFinset (s :=
      range (ι := (fun (X : Type v) ↦ X) (F.obj k'))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g')) :
          (a : (fun (X : Type v) ↦ X) (F.obj k')) → (fun (X : Type v) ↦ X) (F.obj j))) <
    m
Tactic: have := hmin _ ⟨k', g', (m.finite_toSet.subset <| hm.substr hl).coe_toFinset⟩