-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_1 : SuccOrder ι
equiv : (j : (↑(Iic i) : Type u_6)) → F (↑j : ι) ≃ piLT X (↑j : ι)
e : F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i)
hi : ¬IsMax i
inst_2 : InverseSystem (F := F) f
H : ∀ (x : F i⁺), ((e : (a : F i⁺) → F i × X i) x).1 = f ⋯ x
nat : IsNatEquiv (F := F) (X := X) f (s := Iic i) equiv
j k : ι
hj_1 : j ∈ Iic i⁺
hk : k ∈ Iic i⁺
h : k ≤ j
x : F j
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : j ≤ i
inr :
  Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    ((((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)) ↦ equiv (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) (↑j : ι) ⋯),
                e.trans
                  (Equiv.trans
                    (Equiv.prodCongr (equiv (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⁺) k hk) :
            F (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι) ≃
              piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι)) :
          (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
        (f h x) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    (piLTProj (X := X) h
        ((((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)) ↦ equiv (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) (↑j : ι) ⋯),
                  e.trans
                    (Equiv.trans
                      (Equiv.prodCongr (equiv (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⁺) j hj_1) :
              F (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) j hj_1) : ι) ≃
                piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) j hj_1) : ι)) :
            (a : F (↑⟨j, hj_1⟩ : ι)) → piLT X (↑⟨j, hj_1⟩ : ι))
          x) :
      piLT X k)
⊢ Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) :
          (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
        (f h x) :
      piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
    (piLTProj (X := X) h
        ((piEquivSucc (F := F) (X := X) equiv e hi (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) j hj_1) :
            (a : F (↑⟨j, hj_1⟩ : ι)) → piLT X (↑⟨j, hj_1⟩ : ι))
          x) :
      piLT X k)
have inr₁ : Eq (α := piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
  (((fun (j : (↑(Iio i⁺) : Type u_6)) ↦ equiv (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) (↑j : ι) sorry),
              e.trans
                (Equiv.trans
                  (Equiv.prodCongr (equiv (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i sorry)) (Equiv.refl (X i)))
                  (Equiv.trans (piSplitLE (X := X))
                    (Equiv.piCongrSet (W := X) (s :=
                      Iic (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i sorry : { x : ι // x ∈ Iic i }) : ι)) (t := Iio i⁺)
                      sorry)))).1
          (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i⁺) k sorry) :
        (a : F (↑⟨k, hk⟩ : ι)) → piLT X (↑⟨k, hk⟩ : ι))
      (f h x) :
    piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) k hk) : ι))
  (piLTProj (X := X) h
      ((((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)) ↦ equiv (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) (↑j : ι) sorry),
                e.trans
                  (Equiv.trans
                    (Equiv.prodCongr (equiv (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i sorry)) (Equiv.refl (X i)))
                    (Equiv.trans (piSplitLE (X := X))
                      (Equiv.piCongrSet (W := X) (s :=
                        Iic (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i) i sorry : { x : ι // x ∈ Iic i }) : ι)) (t :=
                        Iio i⁺) sorry))))
              (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) j hj_1) :
            F (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) j hj_1) : ι) ≃
              piLT X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic i⁺) j hj_1) : ι)) :
          (a : F (↑⟨j, hj_1⟩ : ι)) → piLT X (↑⟨j, hj_1⟩ : ι))
        x) :
    piLT X k)
Tactic: rw [piEquivSucc, piSplitLE_lt (h.trans_lt <| lt_succ hj), nat hj, piSplitLE_lt (lt_succ hj)]