-- 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)
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₁))
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₁))
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
⊢ Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₃)))
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₃)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
      s)
    y
have refine_1 : ∀ (y : F.obj j₄)
  (hy :
    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₃))
          y :
        (fun (X : Type v) ↦ X) (F.obj 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₁))
          ((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₃))
              y :
            (fun (X : Type v) ↦ X) (F.obj j₃)) :
        (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.obj j₃)) (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₃)))
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₃)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
      s)
    ((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₃))
        y :
      (fun (X : Type v) ↦ X) (F.obj j₃))
Tactic: obtain ⟨y, rfl⟩ := F.mem_eventualRange_iff.1 hy f₄
Cleared hypotheses: y, hy, h₃