-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
mn : m ≤ n
msn : m ≤ n + 1
⊢ Eq.{u_1} (α := motive m msn)
    (leRec (motive := fun {n : ℕ} (mn : m ≤ n) ↦
        {motive : (m : ℕ) → m ≤ n → Sort u_1} →
          (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → (self : motive n ⋯) → motive m mn)
        (fun {motive : (m_1 : ℕ) → m_1 ≤ m → Sort u_1} (of_succ : (k : ℕ) → (h : k < m) → motive (k + 1) h → motive k ⋯)
            (self : motive m ⋯) ↦
          self)
        (fun ⦃k : ℕ⦄ (h : m ≤ k)
            (ih :
              {motive : (m : ℕ) → m ≤ k → Sort u_1} →
                (of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯) →
                  (self : motive k ⋯) → motive m h)
            {motive : (m : ℕ) → m ≤ k + 1 → Sort u_1}
            (of_succ : (k_1 : ℕ) → (h : k_1 < k + 1) → motive (k_1 + 1) h → motive k_1 ⋯) (self : motive (k + 1) ⋯) ↦
          ih (motive := fun {m : ℕ} (h : m ≤ k) ↦ motive m ⋯) (fun (i : ℕ) (hi : i < k) ↦ of_succ i ⋯)
            (of_succ k ⋯ self))
        msn (motive := motive) of_succ self :
      motive m msn)
    (leRec (motive := fun {n : ℕ} (mn : m ≤ n) ↦
        {motive : (m : ℕ) → m ≤ n → Sort u_1} →
          (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) → (self : motive n ⋯) → motive m mn)
        (fun {motive : (m_1 : ℕ) → m_1 ≤ m → Sort u_1} (of_succ : (k : ℕ) → (h : k < m) → motive (k + 1) h → motive k ⋯)
            (self : motive m ⋯) ↦
          self)
        (fun ⦃k : ℕ⦄ (h : m ≤ k)
            (ih :
              {motive : (m : ℕ) → m ≤ k → Sort u_1} →
                (of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯) →
                  (self : motive k ⋯) → motive m h)
            {motive : (m : ℕ) → m ≤ k + 1 → Sort u_1}
            (of_succ : (k_1 : ℕ) → (h : k_1 < k + 1) → motive (k_1 + 1) h → motive k_1 ⋯) (self : motive (k + 1) ⋯) ↦
          ih (motive := fun {m : ℕ} (h : m ≤ k) ↦ motive m ⋯) (fun (i : ℕ) (hi : i < k) ↦ of_succ i ⋯)
            (of_succ k ⋯ self))
        mn (motive := fun (m : ℕ) (h : m ≤ n) ↦ motive m ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (of_succ n ⋯ self) :
      motive m ⋯)
have rw : Eq.{u_1} (α := motive m msn)
  (leRec (motive := fun {n : ℕ} (mn : m ≤ n) ↦
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k sorry) → (self : motive n sorry) → motive m mn)
      (fun {motive : (m_1 : ℕ) → m_1 ≤ m → Sort u_1} (of_succ : (k : ℕ) → (h : k < m) → motive (k + 1) h → motive k sorry)
          (self : motive m sorry) ↦
        self)
      (fun ⦃k : ℕ⦄ (h : m ≤ k)
          (ih :
            {motive : (m : ℕ) → m ≤ k → Sort u_1} →
              (of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 sorry) →
                (self : motive k sorry) → motive m h)
          {motive : (m : ℕ) → m ≤ k + 1 → Sort u_1}
          (of_succ : (k_1 : ℕ) → (h : k_1 < k + 1) → motive (k_1 + 1) h → motive k_1 sorry) (self : motive (k + 1) sorry) ↦
        ih (motive := fun {m : ℕ} (h : m ≤ k) ↦ motive m sorry) (fun (i : ℕ) (hi : i < k) ↦ of_succ i sorry) (of_succ k sorry self))
      mn (motive := fun {m : ℕ} (h : m ≤ n) ↦ motive m sorry) (fun (i : ℕ) (hi : i < n) ↦ of_succ i sorry) (of_succ n sorry self) :
    motive m sorry)
  (leRec (motive := fun {n : ℕ} (mn : m ≤ n) ↦
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k sorry) → (self : motive n sorry) → motive m mn)
      (fun {motive : (m_1 : ℕ) → m_1 ≤ m → Sort u_1} (of_succ : (k : ℕ) → (h : k < m) → motive (k + 1) h → motive k sorry)
          (self : motive m sorry) ↦
        self)
      (fun ⦃k : ℕ⦄ (h : m ≤ k)
          (ih :
            {motive : (m : ℕ) → m ≤ k → Sort u_1} →
              (of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 sorry) →
                (self : motive k sorry) → motive m h)
          {motive : (m : ℕ) → m ≤ k + 1 → Sort u_1}
          (of_succ : (k_1 : ℕ) → (h : k_1 < k + 1) → motive (k_1 + 1) h → motive k_1 sorry) (self : motive (k + 1) sorry) ↦
        ih (motive := fun {m : ℕ} (h : m ≤ k) ↦ motive m sorry) (fun (i : ℕ) (hi : i < k) ↦ of_succ i sorry) (of_succ k sorry self))
      mn (motive := fun (m : ℕ) (h : m ≤ n) ↦ motive m sorry) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x sorry) (of_succ n sorry self) :
    motive m sorry)
Tactic: rw [leRec_succ]