-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
l : Ordinal.{u_4}
lLim : IsSuccLimit l
motive : (↑(Iio l) : Type (u_4 + 1)) → Sort u_5
o : (↑(Iio l) : Type (u_4 + 1))
H₁ : motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) 0 ⋯)
H₂ :
  (o : (↑(Iio l) : Type (u_4 + 1))) →
    motive o → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) (succ (↑o : Ordinal.{u_4})) ⋯)
H₃ :
  (o : (↑(Iio l) : Type (u_4 + 1))) →
    IsSuccLimit (↑o : Ordinal.{u_4}) → ((o' : (↑(Iio l) : Type (u_4 + 1))) → o' < o → motive o') → motive o
oLim : IsSuccLimit (↑o : Ordinal.{u_4})
⊢ limitRecOn (motive := fun (o : Ordinal.{u_4}) ↦
      (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho)) (↑o : Ordinal.{u_4})
      (fun (ho : 0 ∈ Iio l) ↦ H₁)
      (fun (o : Ordinal.{u_4})
          (IH : (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho))
          (ho : o + 1 ∈ Iio l) ↦
        H₂ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ⋯) (IH ⋯))
      (fun (o : Ordinal.{u_4}) (ho' : IsSuccLimit o)
          (IH :
            (o' : Ordinal.{u_4}) →
              o' < o → (ho : o' ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o' ho))
          (ho : o ∈ Iio l) ↦
        H₃ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ho'
          fun (a : (↑(Iio l) : Type (u_4 + 1))) (ha : a < Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ↦
          IH (↑a : Ordinal.{u_4}) ha ⋯)
      ⋯ =
    H₃ o oLim fun (x : (↑(Iio l) : Type (u_4 + 1))) (x_1 : x < o) ↦ boundedLimitRecOn lLim (motive := motive) x H₁ H₂ H₃
have rw : (H₃ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) (↑o : Ordinal.{u_4}) sorry) oLim
    fun (a : (↑(Iio l) : Type (u_4 + 1)))
      (ha : a < Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) (↑o : Ordinal.{u_4}) sorry) ↦
    (fun (x : Ordinal.{u_4}) (_h : x < (↑o : Ordinal.{u_4})) ↦
        (limitRecOn (motive := fun (o : Ordinal.{u_4}) ↦
            (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho)) x
            (fun (ho : 0 ∈ Iio l) ↦ H₁)
            (fun (o : Ordinal.{u_4})
                (IH : (ho : o ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho))
                (ho : o + 1 ∈ Iio l) ↦
              H₂ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o sorry) (IH sorry))
            fun (o : Ordinal.{u_4}) (ho' : IsSuccLimit o)
              (IH :
                (o' : Ordinal.{u_4}) →
                  o' < o → (ho : o' ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o' ho))
              (ho : o ∈ Iio l) ↦
            H₃ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ho'
              fun (a : (↑(Iio l) : Type (u_4 + 1)))
                (ha : a < Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) o ho) ↦
              IH (↑a : Ordinal.{u_4}) ha sorry :
          (ho : x ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) x ho)))
      (↑a : Ordinal.{u_4}) ha sorry) =
  H₃ o oLim fun (x : (↑(Iio l) : Type (u_4 + 1))) (x_1 : x < o) ↦ boundedLimitRecOn lLim (motive := motive) x H₁ H₂ H₃
Tactic: rw [limitRecOn_limit]