-- 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)
i : J
s : Set (F.obj i)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ :
  F.eventualRange j₁ =
    range (ι := (fun (X : Type v) ↦ X) (F.obj j₂))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx :
  Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₂)))
    (⋂ (f : j₂ ⟶ i),
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
    x
this :
  Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj j₁)) (F.eventualRange j₁)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))
obtain :
  ∀ (y : F.obj j₃) (hy : y ∈ F.eventualRange j₃)
    (h₃ :
      Eq (α := (fun (X : Type v) ↦ X) (F.obj j₁))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₃ ≫ f₂)) :
              (a : (fun (X : Type v) ↦ X) (F.obj j₃)) → (fun (X : Type v) ↦ X) (F.obj j₁))
            y :
          (fun (X : Type v) ↦ X) (F.obj j₁))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂) :
              (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
            x :
          (fun (X : Type v) ↦ X) (F.obj j₁))),
    Membership.mem (α := (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)) (γ :=
      Set ((fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
      (range (ι := (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j₃))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((F.toPreimages s).map (f₃ ≫ f₂ ≫ f₁))) :
          (a : (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j₃)) → (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.toPreimages s).map (f₂ ≫ f₁)) :
            (a : (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j₂)) → (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j))
          (Subtype.mk (p := fun (x : (fun (X : Type v) ↦ X) (F.obj j₂)) ↦
            Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₂)))
              (⋂ (f : j₂ ⟶ i),
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
                    (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
                  s)
              x)
            x hx) :
        (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j))
⊢ Membership.mem (α := (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)) (γ :=
    Set ((fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
    (range (ι := (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j₃))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((F.toPreimages s).map (f₃ ≫ f₂ ≫ f₁))) :
        (a : (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j₃)) → (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.toPreimages s).map (f₂ ≫ f₁)) :
          (a : (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j₂)) → (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j))
        (Subtype.mk (p := fun (x : (fun (X : Type v) ↦ X) (F.obj j₂)) ↦
          Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₂)))
            (⋂ (f : j₂ ⟶ i),
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
                  (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
                s)
            x)
          x hx) :
      (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j))

Tactic:
obtain ⟨y, hy, h₃⟩ := h.subset_image_eventualRange F (f₃ ≫ f₂) this

Premises used: CategoryTheory.Functor.IsMittagLeffler.subset_image_eventualRange, CategoryTheory.CategoryStruct.comp