-- Mathlib/Data/Int/Basic.lean
lemma strongRec_of_ge :
    ∀ hn : m ≤ n, m.strongRec lt ge n = ge n hn fun k _ ↦ m.strongRec lt ge k

Proof state:
case e_a.refine_3.h.h
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝¹ : n ≥ m
hn : m ≤ n
k : ℤ
hkm : k ≤ m
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x => Int.strongRec lt ge k) →
    (k.inductionOn' m lt (fun _n a ih l a => if hlm : l < m then lt l hlm else ge l ⋯ fun k_1 x => ih k_1 ⋯)
        fun n x hn l x => hn l ⋯) =
      fun k_1 x => Int.strongRec lt ge k_1
x✝ : ∀ (k_1 : ℤ), k_1 < k - 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x => Int.strongRec lt ge k
l : ℤ
hl : l < k - 1
⊢ (k - 1).inductionOn' m lt (fun _n a ih l a => if hlm : l < m then lt l hlm else ge l ⋯ fun k_1 x => ih k_1 ⋯)
      (fun n x hn l x => hn l ⋯) l hl =
    Int.strongRec lt ge l

Tactic:
rw [inductionOn'_sub_one hkm, ih']

Result:
case e_a.refine_3.h.h
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝¹ : n ≥ m
hn : m ≤ n
k : ℤ
hkm : k ≤ m
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x => Int.strongRec lt ge k) →
    (k.inductionOn' m lt (fun _n a ih l a => if hlm : l < m then lt l hlm else ge l ⋯ fun k_1 x => ih k_1 ⋯)
        fun n x hn l x => hn l ⋯) =
      fun k_1 x => Int.strongRec lt ge k_1
x✝ : ∀ (k_1 : ℤ), k_1 < k - 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x => Int.strongRec lt ge k
l : ℤ
hl : l < k - 1
⊢ ∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x => Int.strongRec lt ge k

Proof state:
case pos
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x => Int.strongRec lt ge k) →
    (k.inductionOn' m lt (fun _n a ih l a => if hlm : l < m then lt l hlm else ge l ⋯ fun k_1 x => ih k_1 ⋯)
        fun n x hn l x => hn l ⋯) =
      fun k_1 x => Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x => Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
hlm : l < m
⊢ lt l hlm = Int.strongRec lt ge l

Tactic:
rw [strongRec_of_lt hlm]

Result:
no goals

Proof state:
case e_a.refine_2.h.h
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x => Int.strongRec lt ge k) →
    (k.inductionOn' m lt (fun _n a ih l a => if hlm : l < m then lt l hlm else ge l ⋯ fun k_1 x => ih k_1 ⋯)
        fun n x hn l x => hn l ⋯) =
      fun k_1 x => Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x => Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
⊢ (k + 1).inductionOn' m lt (fun _n a ih l a => if hlm : l < m then lt l hlm else ge l ⋯ fun k_1 x => ih k_1 ⋯)
      (fun n x hn l x => hn l ⋯) l hl =
    Int.strongRec lt ge l

Tactic:
rw [inductionOn'_add_one hmk]

Result:
case e_a.refine_2.h.h
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x => Int.strongRec lt ge k) →
    (k.inductionOn' m lt (fun _n a ih l a => if hlm : l < m then lt l hlm else ge l ⋯ fun k_1 x => ih k_1 ⋯)
        fun n x hn l x => hn l ⋯) =
      fun k_1 x => Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x => Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
⊢ (if hlm : l < m then lt l hlm
    else
      ge l ⋯ fun k_1 x =>
        k.inductionOn' m lt (fun _n a ih l a => if hlm : l < m then lt l hlm else ge l ⋯ fun k_2 x => ih k_2 ⋯)
          (fun n x hn l x => hn l ⋯) k_1 ⋯) =
    Int.strongRec lt ge l

Proof state:
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
ih : ∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x => Int.strongRec lt ge k_1
hn : m ≤ n
⊢ ge n ⋯
      (n.inductionOn' m lt (fun _n a ih l a => if hlm : l < m then lt l hlm else ge l ⋯ fun k x => ih k ⋯)
        fun n_1 x hn l x => hn l ⋯) =
    ge n hn fun k x => Int.strongRec lt ge k

Tactic:
congr

Result:
case e_a
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
ih : ∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x => Int.strongRec lt ge k_1
hn : m ≤ n
⊢ (n.inductionOn' m lt (fun _n a ih l a => if hlm : l < m then lt l hlm else ge l ⋯ fun k x => ih k ⋯)
      fun n_1 x hn l x => hn l ⋯) =
    fun k x => Int.strongRec lt ge k

Proof state:
m n : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
⊢ ∀ (hn : m ≤ n), Int.strongRec lt ge n = ge n hn fun k x => Int.strongRec lt ge k

Tactic:
refine m.strongRec (fun n hnm hmn ↦ (Int.not_lt.mpr hmn hnm).elim) (fun n _ ih hn ↦ ?_) n

Result:
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
ih : ∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x => Int.strongRec lt ge k_1
hn : m ≤ n
⊢ Int.strongRec lt ge n = ge n hn fun k x => Int.strongRec lt ge k