-- Module: Mathlib.Order.DirectedInverseSystem
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))
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))
                    ⋯ :
                  { 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)) :
          (l : (↑(Iio i) : Type u_6)) → F (↑l : ι))
        x =
      (↑t : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) 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 }))
      ((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

Tactic:
ext