-- 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 := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_8))
⊢ (↑((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 }))
          ((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 }))
            t)) :
      (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) =
    (↑t : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
have a : ∀ (x : (↑(Iio i) : Type u_6)),
  (↑((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 }))
            ((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 }))
              t)) :
        (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
      x =
    (↑t : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) x
Tactic: ext1