-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι_1 : Type u_1
inst : Preorder ι_1
F₁ : ι_1 → Type u_2
F₂ : ι_1 → Type u_3
F_1 : ι_1 → Type u_4
X_1 : ι_1 → Type u_5
f_1 : ⦃i j : ι_1⦄ → i ≤ j → F_1 j → F_1 i
i_1 j : ι_1
h : i_1 ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst_1 : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : (↑(Iio i) : Type u_6)) → F (↑j : ι) ≃ piLT X (↑j : ι)
nat : IsNatEquiv (F := F) (X := X) f (s := Iio i) equiv
t : (↑(limit (F := F) f i) : Type (max u_6 u_7))
⊢ (fun (t : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_8))) ↦
        (Subtype.mk (p := fun (x : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) ↦ x ∈ limit (F := F) f i)
            (fun (l : (↑(Iio i) : Type u_6)) ↦
              ((equiv l).symm : (a : piLT X (↑l : ι)) → F (↑l : ι))
                ((↑t : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) l))
            ⋯ :
          { x : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι) // x ∈ limit (F := F) f i }))
      ((fun (t : (↑(limit (F := F) f i) : Type (max u_6 u_7))) ↦
          (Subtype.mk (p := fun (x : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) ↦
              Membership.mem (γ := Set ((l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)))
                (limit (F := piLT X) (piLTProj (X := X)) i) x)
              (fun (l : (↑(Iio i) : Type u_6)) ↦
                (equiv l : (a : F (↑l : ι)) → piLT X (↑l : ι)) ((↑t : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) l))
              ⋯ :
            { x : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι) //
              Membership.mem (γ := Set ((l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)))
                (limit (F := piLT X) (piLTProj (X := X)) i) x }))
        t) =
    t
have a : ∀ (x : (↑(Iio i) : Type u_6)),
  (↑((fun (t : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_8))) ↦
              (Subtype.mk (p := fun (x : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) ↦ x ∈ limit (F := F) f i)
                  (fun (l : (↑(Iio i) : Type u_6)) ↦
                    ((equiv l).symm : (a : piLT X (↑l : ι)) → F (↑l : ι))
                      ((↑t : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) l))
                  sorry :
                { x : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι) // x ∈ limit (F := F) f i }))
            ((fun (t : (↑(limit (F := F) f i) : Type (max u_6 u_7))) ↦
                (Subtype.mk (p := fun (x : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) ↦
                    Membership.mem (γ := Set ((l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)))
                      (limit (F := piLT X) (piLTProj (X := X)) i) x)
                    (fun (l : (↑(Iio i) : Type u_6)) ↦
                      (equiv l : (a : F (↑l : ι)) → piLT X (↑l : ι))
                        ((↑t : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) l))
                    sorry :
                  { x : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι) //
                    Membership.mem (γ := Set ((l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)))
                      (limit (F := piLT X) (piLTProj (X := X)) i) x }))
              t)) :
        (l : (↑(Iio i) : Type u_6)) → F (↑l : ι))
      x =
    (↑t : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) x
Tactic: ext