-- Module: Mathlib.Data.Nat.Init
Goal:
m n k : ℕ
hmn : m ≤ n
m_1 : ℕ
hnk : n.le m_1
ih :
  ∀ {motive : (m : ℕ) → m ≤ m_1 → Sort u_1} (of_succ : (k : ℕ) → (h : k < m_1) → motive (k + 1) h → motive k ⋯)
    (self : motive m_1 ⋯),
    decreasingInduction (motive := motive) of_succ self ⋯ =
      decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1) ↦ motive x ⋯) of_succ self hnk) hmn
motive : (m : ℕ) → m ≤ m_1.succ → Sort u_1
of_succ : (k : ℕ) → (h : k < m_1.succ) → motive (k + 1) h → motive k ⋯
self : motive m_1.succ ⋯
step :
  Eq.{u_1} (α := motive m ⋯)
    (decreasingInduction (motive := fun (m : ℕ) (h : m ≤ m_1) ↦ motive m ⋯) (fun (x : ℕ) (x_1 : x < m_1) ↦ of_succ x ⋯)
        (of_succ m_1 ⋯ self) ⋯ :
      motive m ⋯)
    (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1.succ) ↦ motive x ⋯) of_succ self ⋯) hmn :
      motive m ⋯)
step₁ :
  Eq.{u_1} (α := motive m ⋯)
    (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1) ↦ motive x ⋯)
          (fun (x : ℕ) (x_1 : x < m_1) ↦ of_succ x ⋯) (of_succ m_1 ⋯ self) hnk)
        hmn :
      motive m ⋯)
    (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1.succ) ↦ motive x ⋯) of_succ self ⋯) hmn :
      motive m ⋯)
step₂ :
  Eq.{u_1} (α := motive m ⋯)
    (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1) ↦ motive x ⋯)
          (fun (x : ℕ) (x_1 : x < m_1) ↦ of_succ x ⋯) (of_succ m_1 ⋯ self) hnk)
        hmn :
      motive m ⋯)
    (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (m : ℕ) (h : m ≤ m_1) ↦ motive m ⋯)
          (fun (x : ℕ) (x_1 : x < m_1) ↦ of_succ x ⋯) (of_succ m_1 ⋯ self) hnk)
        hmn :
      motive m ⋯)
step₃ : n ≤ m_1
step₄ :
  Eq.{u_1} (α := motive m ⋯)
    (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1) ↦ motive x ⋯)
          (fun (x : ℕ) (x_1 : x < m_1) ↦ of_succ x ⋯) (of_succ m_1 ⋯ self) hnk)
        hmn :
      motive m ⋯)
    (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (m : ℕ) (h : m ≤ m_1) ↦ motive m ⋯)
          (fun (x : ℕ) (x_1 : x < m_1) ↦ of_succ x ⋯) (of_succ m_1 ⋯ self) hnk)
        hmn :
      motive m ⋯)
step₅ : n ≤ m_1
⊢ decreasingInduction (motive := motive) of_succ self ⋯ =
    decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
      (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1.succ) ↦ motive x ⋯) of_succ self ⋯) hmn

Tactic:
rw [decreasingInduction_succ _ _ (Nat.le_trans hmn hnk), ih, decreasingInduction_succ]

Premises used: Nat.le_trans, Nat.decreasingInduction_succ