case zero
m n k : ℕ
C : ℕ → Sort u
next : {k : ℕ} → C k → C (k + 1)
h : zero ≤ zero
x : C zero
⊢ (_ : zero = 0) ▸ x = x

case succ
m n k : ℕ
C : ℕ → Sort u
next : {k : ℕ} → C k → C (k + 1)
n✝ : ℕ
h : succ n✝ ≤ succ n✝
x : C (succ n✝)
⊢ (Or.by_cases (_ : succ n✝ ≤ n✝ ∨ succ n✝ = succ n✝) (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x))
      fun h => h ▸ x) =
    x
m n✝ k : ℕ
C : ℕ → Sort u
n : ℕ
h : n ≤ n
next : {k : ℕ} → C k → C (k + 1)
x : C n
⊢ leRecOn h (fun {k} => next) x = x
cases n <;> unfold leRecOn Eq.recOn
no goals
case zero
m n k : ℕ
C : ℕ → Sort u
next : {k : ℕ} → C k → C (k + 1)
h : zero ≤ zero
x : C zero
⊢ (_ : zero = 0) ▸ x = x
simp
case succ
m n k : ℕ
C : ℕ → Sort u
next : {k : ℕ} → C k → C (k + 1)
n✝ : ℕ
h : succ n✝ ≤ succ n✝
x : C (succ n✝)
⊢ (if hp : succ n✝ ≤ n✝ then (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x)) hp
    else (fun h => h ▸ x) (_ : succ n✝ = succ n✝)) =
    x
case succ
m n k : ℕ
C : ℕ → Sort u
next : {k : ℕ} → C k → C (k + 1)
n✝ : ℕ
h : succ n✝ ≤ succ n✝
x : C (succ n✝)
⊢ (Or.by_cases (_ : succ n✝ ≤ n✝ ∨ succ n✝ = succ n✝) (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x))
      fun h => h ▸ x) =
    x
unfold Or.by_cases
no goals
case succ
m n k : ℕ
C : ℕ → Sort u
next : {k : ℕ} → C k → C (k + 1)
n✝ : ℕ
h : succ n✝ ≤ succ n✝
x : C (succ n✝)
⊢ (if hp : succ n✝ ≤ n✝ then (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x)) hp
    else (fun h => h ▸ x) (_ : succ n✝ = succ n✝)) =
    x
rw [dif_neg (Nat.not_succ_le_self _)]