-- 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 ι
inst_4 : InverseSystem (F := F) f
hi : ¬IsMax i
e : PEquivOn (F := F) (X := X) f equivSucc (Iic i)
H : ∀ ⦃i : ι⦄ (hi : ¬IsMax i) (x : F i⁺), ((equivSucc hi : (a : F i⁺) → F i × X i) x).1 = f ⋯ x
i_2 : ι
hsj : i_2⁺ ∈ Iic i⁺
hj : ¬IsMax i_2
x : F (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)
lt : i_2⁺ < i⁺
inr :
  Eq.{u_8 + 1} (α :=
    X
      (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
        ι))
    ((((piSplitLE (X := fun (i : ι) ↦ F i ≃ piLT X i) :
                (a : piLT (fun (i : ι) ↦ F i ≃ piLT X i) i⁺ × (F i⁺ ≃ piLT X i⁺)) →
                  (j : (↑(Iic i⁺) : Type u_6)) → F (↑j : ι) ≃ piLT X (↑j : ι))
              (fun (j : (↑(Iio i⁺) : Type u_6)) ↦
                e.equiv (F := F) (X := X) (s := Iic i) (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) (↑j : ι) ⋯),
                (equivSucc hi).trans
                  (Equiv.trans
                    (Equiv.prodCongr
                      (e.equiv (F := F) (X := X) (s := Iic i) (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i ⋯))
                      (Equiv.refl (X i)))
                    (Equiv.trans (piSplitLE (X := X))
                      (Equiv.piCongrSet (W := X) (s :=
                        Iic (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i ⋯ : { x : ι // x ∈ Iic i }) : ι)) (t :=
                        Iio i⁺) ⋯))))
              (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) :
            F (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι) ≃
              piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) :
          (a : F (↑⟨i_2⁺, hsj⟩ : ι)) → piLT X (↑⟨i_2⁺, hsj⟩ : ι))
        x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
      X
        (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
          ι))
    (((equivSucc hj : (a : F i_2⁺) → F i_2 × X i_2) x).2 : X i_2)
inr₁ :
  Eq.{u_8 + 1} (α :=
    X
      (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
        ι))
    (((fun (j : (↑(Iio i⁺) : Type u_6)) ↦
                e.equiv (F := F) (X := X) (s := Iic i) (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) (↑j : ι) ⋯),
                (equivSucc hi).trans
                  (Equiv.trans
                    (Equiv.prodCongr
                      (e.equiv (F := F) (X := X) (s := Iic i) (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i ⋯))
                      (Equiv.refl (X i)))
                    (Equiv.trans (piSplitLE (X := X))
                      (Equiv.piCongrSet (W := X) (s :=
                        Iic (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i ⋯ : { x : ι // x ∈ Iic i }) : ι)) (t :=
                        Iio i⁺) ⋯)))).1
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i⁺) i_2⁺ lt) :
          (a : F (↑⟨i_2⁺, hsj⟩ : ι)) → piLT X (↑⟨i_2⁺, hsj⟩ : ι))
        x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
      X
        (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
          ι))
    (((equivSucc hj : (a : F i_2⁺) → F i_2 × X i_2) x).2 : X i_2)
inr₂ : i_2⁺ < i⁺
⊢ Eq.{u_8 + 1} (α :=
    X
      (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
        ι))
    ((piEquivSucc (F := F) (X := X) (e.equiv (F := F) (X := X) (s := Iic i)) (equivSucc hi) hi
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) :
          (a : F (↑⟨i_2⁺, hsj⟩ : ι)) → piLT X (↑⟨i_2⁺, hsj⟩ : ι))
        x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
      X
        (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 ⋯) :
          ι))
    (((equivSucc hj : (a : F i_2⁺) → F i_2 × X i_2) x).2 : X i_2)
have inr₃ : Eq.{u_8 + 1} (α :=
  X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) i_2⁺ hsj) : ι)) i_2 sorry) : ι))
  ((equivSucc hj : (a : F i_2⁺) → F i_2 × X i_2) x).2 ((equivSucc hj : (a : F i_2⁺) → F i_2 × X i_2) x).2
Tactic: rwa [piEquivSucc, piSplitLE_lt, e.compat]