-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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})
rw :
  (H₃ (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) (↑o : Ordinal.{u_4}) ⋯) 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}) ⋯) ↦
      (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 ⋯) (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 ⋯ :
            (ho : x ∈ Iio l) → motive (Subtype.mk (p := fun (x : Ordinal.{u_4}) ↦ x ∈ Iio l) x ho)))
        (↑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₃
h : 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₃

Tactic:
rw [limitRecOn_limit]

Premises used: Ordinal.limitRecOn_limit