-- 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_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

Tactic:
split_ifs with hlm

Result:
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

case neg
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
⊢ (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:
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
hn : m ≤ n
⊢ (∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x => Int.strongRec lt ge k_1) →
    (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

Tactic:
refine n.inductionOn' m (fun _ ↦ ?_) (fun k hmk ih' ih ↦ ?_) (fun k hkm ih' _ ↦ ?_) <;> ext l hl

Result:
case e_a.refine_1.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
x✝ : ∀ (k : ℤ), k < m → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x => Int.strongRec lt ge k_1
l : ℤ
hl : l < m
⊢ m.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 x hn l x => hn l ⋯) l hl =
    Int.strongRec lt ge l

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

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

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 : ℤ), 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

Tactic:
exact fun l hlk hml ↦ (Int.not_lt.mpr hkm <| Int.lt_of_le_of_lt hml hlk).elim

Result:
no goals

Proof state:
case e_a.refine_1.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
x✝ : ∀ (k : ℤ), k < m → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x => Int.strongRec lt ge k_1
l : ℤ
hl : l < m
⊢ m.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 x hn l x => hn l ⋯) l hl =
    Int.strongRec lt ge l

Tactic:
rw [inductionOn'_self, strongRec_of_lt hl]

Result:
no goals

Proof state:
case neg
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
⊢ (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

Tactic:
rw [ih' fun l hl ↦ ih l (Int.lt_trans hl k.lt_succ), ih _ hl]

Result:
no goals