-- 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 := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_8))
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))
                    ⋯ :
                  { 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 : ι))
        x =
      (↑t : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) x
⊢ (↑((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 : ι))

Tactic:
ext1