-- 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 : ι_1
h_1 : i_1 ≤ j_1
ι : 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 : ι))
j k : ι
hj : j ∈ Iio i
hk : k ∈ Iio i
h : k ≤ j
rw :
  ∀ (x : F j),
    Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) k hk) : ι))
      (((↑(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 : ι)) ⋯))
                    ⋯) :
                (l : (↑(Iio i) : Type u_6)) → piLT (fun (j : ι) ↦ F j ≃ piLT X j) (↑l : ι))
              (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑(hi.mid ⋯) : ι) ⋯)
              (Subtype.mk (p := fun (x : ι) ↦
                x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑(hi.mid ⋯) : ι) ⋯) : ι))
                (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) k hk) : ι) ⋯) :
            (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
          (f h x) :
        piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) k hk) : ι))
      (piLTProj (X := X) h
          ((((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) j hj) :
                (fun (j : ι) ↦ F j ≃ piLT X j) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) j hj) : ι)) :
              (a : F (↑⟨j, hj⟩ : ι)) → piLT X (↑⟨j, hj⟩ : ι))
            x) :
        piLT X k)
k₁ : (↑(Iio i) : Type u_6)
⊢ ∀ (x : F j),
    Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) k hk) : ι))
      ((((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) k hk) :
              (fun (j : ι) ↦ F j ≃ piLT X j) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) k hk) : ι)) :
            (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
          (f h x) :
        piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) k hk) : ι))
      (piLTProj (X := X) h
          ((((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) j hj) :
                (fun (j : ι) ↦ F j ≃ piLT X j) (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) j hj) : ι)) :
              (a : F (↑⟨j, hj⟩ : ι)) → piLT X (↑⟨j, hj⟩ : ι))
            x) :
        piLT X k)
have hl : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) k hk) : ι) <
  (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑(hi.mid sorry) : ι) sorry) : ι)
Tactic: rw [piLTLim_symm_apply]