-- 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
inst_2 : SuccOrder ι
equivSucc : ⦃i : ι⦄ → ¬IsMax i → F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i)
s t : Set ι
inst_3 : WellFoundedLT ι
hi : IsSuccPrelimit i
e : (j : (↑(Iio i) : Type u_6)) → PEquivOn (F := F) (X := X) f equivSucc (Iic (↑j : ι))
i_2 : ι
hj : i_2⁺ ∈ Iio i
k : (↑(Ioo i_2⁺ i) : Type u_6)
⊢ ∀ (hi_1 : ¬IsMax i_2) (x : F (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ hj) : ι)),
    Eq.{u_8 + 1} (α :=
      X
        (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ hj) : ι)) i_2 ⋯) :
          ι))
      ((((Equiv.symm (piLTLim (X := fun (j : ι) ↦ F j ≃ piLT X j) hi) :
                  (a : (↑(limit piLTProj i) : Type (max u_6 (max u_6 u_7) u_8))) →
                    piLT (fun (j : ι) ↦ F j ≃ piLT X j) i)
                (Subtype.mk (p := fun (x : (l : (↑(Iio i) : Type u_6)) → piLT (fun (j : ι) ↦ F j ≃ piLT X j) (↑l : ι)) ↦
                  Membership.mem (γ := Set ((l : (↑(Iio i) : Type u_6)) → piLT (fun (j : ι) ↦ F j ≃ piLT X j) (↑l : ι)))
                    (limit (F := piLT fun (j : ι) ↦ F j ≃ piLT X j) (piLTProj (X := fun (j : ι) ↦ F j ≃ piLT X j)) i) x)
                  (fun (j : (↑(Iio i) : Type u_6)) ↦
                    PEquivOn.equiv (F := F) (X := X) (s := Iio (↑j : ι))
                      ((e j).restrict (F := F) (X := X) (s := Iio (↑j : ι)) (t := Iic (↑j : ι)) ⋯))
                  ⋯)
                (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ hj) :
              (fun (j : ι) ↦ F j ≃ piLT X j) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ hj) : ι)) :
            (a : F (↑⟨i_2⁺, hj⟩ : ι)) → piLT X (↑⟨i_2⁺, hj⟩ : ι))
          x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ hj) : ι)) i_2 ⋯) :
        X
          (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ hj) : ι)) i_2 ⋯) :
            ι))
      (((equivSucc hi_1 : (a : F i_2⁺) → F i_2 × X i_2) x).2 : X i_2)
have rw : ∀ (hi : ¬IsMax i_2) (x : F (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ hj) : ι)),
  Eq.{u_8 + 1} (α :=
    X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ hj) : ι)) i_2 sorry) : ι))
    (((↑(Subtype.mk (p := fun (x : (l : (↑(Iio i) : Type u_6)) → piLT (fun (j : ι) ↦ F j ≃ piLT X j) (↑l : ι)) ↦
                  Membership.mem (γ := Set ((l : (↑(Iio i) : Type u_6)) → piLT (fun (j : ι) ↦ F j ≃ piLT X j) (↑l : ι)))
                    (limit (F := piLT fun (j : ι) ↦ F j ≃ piLT X j) (piLTProj (X := fun (j : ι) ↦ F j ≃ piLT X j)) i) x)
                  (fun (j : (↑(Iio i) : Type u_6)) ↦
                    PEquivOn.equiv (F := F) (X := X) (s := Iio (↑j : ι))
                      ((e j).restrict (F := F) (X := X) (s := Iio (↑j : ι)) (t := Iic (↑j : ι)) sorry))
                  sorry) :
              (l : (↑(Iio i) : Type u_6)) → piLT (fun (j : ι) ↦ F j ≃ piLT X j) (↑l : ι))
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) sorry)
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) sorry) : ι))
              (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ hj) : ι) sorry) :
          (a : F (↑⟨i_2⁺, hj⟩ : ι)) → piLT X (↑⟨i_2⁺, hj⟩ : ι))
        x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ hj) : ι)) i_2 sorry) :
      X
        (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) i_2⁺ hj) : ι)) i_2 sorry) :
          ι))
    (((equivSucc hi : (a : F i_2⁺) → F i_2 × X i_2) x).2 : X i_2)
Tactic: rw [piLTLim_symm_apply hi ⟨_, k.2.2⟩ (by exact k.2.1)]