-- Module: Mathlib.Data.Nat.Init
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
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 ⋯) → (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 (i : ℕ) (hi : i < n) ↦ of_succ i ⋯)
        (of_succ n ⋯ self) :
      motive m ⋯)
    (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 ⋯)
h1 : m ≤ n
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 ⋯) → (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 (i : ℕ) (hi : i < n) ↦ of_succ i ⋯)
        (of_succ n ⋯ self) :
      motive m ⋯)
    (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 ⋯)
h1₁ : m ≤ n
⊢ 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 ⋯)

Tactic:
rw [leRec_succ]

Premises used: Nat.leRec_succ