-- Module: Mathlib.CategoryTheory.CofilteredSystem
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))
this :
  ¬⋯.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
rwa :
  ∀
    (this :
      ¬⋯.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),
    ¬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))
rwa₁ :
  ∀
    (this :
      ¬(↑(⋯.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)))) :
            Set (F.obj j)) ⊂
          (↑m : Set (F.obj j))),
    ¬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))
rwa₂ :
  ∀
    (this :
      ¬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 : Set (F.obj j))),
    ¬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))
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀
    (this :
      ¬SSubset (α := Set (F.obj j))
          (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)))
          (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)))),
    ¬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))
⊢ ¬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:
rwa [Finset.lt_iff_ssubset, ← Finset.coe_ssubset, Set.Finite.coe_toFinset, hm] at this

Premises used: Set.Finite.coe_toFinset, Finset.coe_ssubset, Finset.lt_iff_ssubset