-- 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 → Type u_4
X_1 : ι_1 → Type u_5
f_1 : ⦃i j : ι_1⦄ → i ≤ j → F j → F i
i_1 j_1 : ι_1
h : i_1 ≤ j_1
ι : Type u_6
inst_1 : LinearOrder ι
X : ι → Type u_7
i : ι
hi : IsSuccPrelimit i
f : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_7))
j : (↑(Iio i) : Type u_6)
l : (↑(Iio (↑j : ι)) : Type u_6)
k : (↑(Ioo (↑l : ι) i) : Type u_6) := hi.mid ⋯
a :
  ∀ (le : j ≤ Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯),
    (↑((fun (f : piLT X i) ↦
                (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 (j : (↑(Iio i) : Type u_6)) ↦ piLTProj (X := X) ⋯ f) ⋯ :
                  { 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 (f : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_7)))
                    (l : (↑(Iio i) : Type u_6)) ↦
                  let k := hi.mid ⋯;
                  (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
                    (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯)
                    (Subtype.mk (p := fun (x : ι) ↦
                      x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯) : ι)) (↑l : ι) ⋯))
                f)) :
          (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
        j l =
      (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) j l
⊢ (↑((fun (f : piLT X i) ↦
              (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 (j : (↑(Iio i) : Type u_6)) ↦ piLTProj (X := X) ⋯ f) ⋯ :
                { 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 (f : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_7)))
                  (l : (↑(Iio i) : Type u_6)) ↦
                let k := hi.mid ⋯;
                (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯)
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) ⋯) : ι))
                    (↑l : ι) ⋯))
              f)) :
        (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
      j l =
    (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) j l
have a₁ : ∀ (le : Subtype.mk (p := fun (x : ι) ↦ x ∈ Iio i) (↑k : ι) sorry ≤ j),
  (↑((fun (f : piLT X i) ↦
              (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 (j : (↑(Iio i) : Type u_6)) ↦ piLTProj (X := X) sorry f) sorry :
                { 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 (f : (↑(limit (F := piLT X) (piLTProj (X := X)) i) : Type (max u_6 u_7)))
                  (l : (↑(Iio i) : Type u_6)) ↦
                let k := hi.mid sorry;
                (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑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) : ι))
                    (↑l : ι) sorry))
              f)) :
        (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι))
      j l =
    (↑f : (l : (↑(Iio i) : Type u_6)) → piLT X (↑l : ι)) j l
Tactic: obtain le | le := le_total j ⟨k, k.2.2⟩