-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
m n_1 : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
h : n ≥ m
hn : m ≤ n
e_a :
  (∀ (k : ℤ),
      k < m →
        ∀ (hn : m ≤ k),
          Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k =
            ge k hn fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1) →
    Eq.{u_1} (α := (k : ℤ) → k < m → P k)
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) m m lt
          (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
            if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
          fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
        (k : ℤ) → k < m → P k)
      fun (k : ℤ) (x : k < m) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
e_a₁ :
  ∀ (k : ℤ) (hmk : m ≤ k)
    (ih' :
      ∀
        (ih :
          ∀ (k_1 : ℤ),
            k_1 < k →
              ∀ (hn : m ≤ k_1),
                Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
                  ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k),
        Eq.{u_1} (α := (k_1 : ℤ) → k_1 < k → P k_1)
          (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) k m lt
              (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
                if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
              fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
            (k_1 : ℤ) → k_1 < k → P k_1)
          fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1)
    (ih :
      ∀ (k_1 : ℤ),
        k_1 < k + 1 →
          ∀ (hn : m ≤ k_1),
            Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
              ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k),
    Eq.{u_1} (α := (k_1 : ℤ) → k_1 < k + 1 → P k_1)
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) (k + 1) m lt
          (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
            if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
          fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
        (k_1 : ℤ) → k_1 < k + 1 → P k_1)
      fun (k_1 : ℤ) (x : k_1 < k + 1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1
⊢ ∀
    (ih :
      ∀ (k : ℤ),
        k < n →
          ∀ (hn : m ≤ k),
            Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k =
              ge k hn fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1),
    Eq.{u_1} (α := (k : ℤ) → k < n → P k)
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) n m lt
          (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
            if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
          fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
        (k : ℤ) → k < n → P k)
      fun (k : ℤ) (x : k < n) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
have e_a₂ : ∀ (k : ℤ) (hkm : k ≤ m)
  (ih' :
    ∀
      (ih :
        ∀ (k_1 : ℤ),
          k_1 < k →
            ∀ (hn : m ≤ k_1),
              Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
                ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k),
      Eq.{u_1} (α := (k_1 : ℤ) → k_1 < k → P k_1)
        (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) k m lt
            (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
              if hlm : l < m then lt l hlm else ge l sorry fun (k : ℤ) (x : k < l) ↦ ih k sorry)
            fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l sorry :
          (k_1 : ℤ) → k_1 < k → P k_1)
        fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1),
  (∀ (k_1 : ℤ),
      k_1 < k - 1 →
        ∀ (hn : m ≤ k_1),
          Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
            ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k) →
    Eq.{u_1} (α := (k_1 : ℤ) → k_1 < k - 1 → P k_1)
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) (k - 1) m lt
          (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
            if hlm : l < m then lt l hlm else ge l sorry fun (k : ℤ) (x : k < l) ↦ ih k sorry)
          fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l sorry :
        (k_1 : ℤ) → k_1 < k - 1 → P k_1)
      fun (k_1 : ℤ) (x : k_1 < k - 1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1
Tactic: refine n.inductionOn' m (fun _ ↦ ?_) (fun k hmk ih' ih ↦ ?_) (fun k hkm ih' _ ↦ ?_)