case refl
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
⊢ Function.Surjective (leRecOn (_ : Nat.le n n) fun {k} => next)

case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
⊢ Function.Surjective (leRecOn (_ : Nat.le n (succ m)) fun {k} => next)
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
⊢ Function.Surjective (leRecOn hnm fun {k} => next)
induction' hnm with m hnm ih
case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
x : C (succ m)
⊢ ∃ a, leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) a = x
case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
⊢ Function.Surjective (leRecOn (_ : Nat.le n (succ m)) fun {k} => next)
intro x
case step.intro
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
w : C m
⊢ ∃ a, leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) a = next w
case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
x : C (succ m)
⊢ ∃ a, leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) a = x
rcases Hnext _ x with ⟨w, rfl⟩
case step.intro.intro
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
x : C n
⊢ ∃ a, leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) a = next (leRecOn hnm (fun {k} => next) x)
case step.intro
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
w : C m
⊢ ∃ a, leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) a = next w
rcases ih w with ⟨x, rfl⟩
case step.intro.intro
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
x : C n
⊢ leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) x = next (leRecOn hnm (fun {k} => next) x)
case step.intro.intro
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
x : C n
⊢ ∃ a, leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) a = next (leRecOn hnm (fun {k} => next) x)
use x
no goals
case step.intro.intro
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
x : C n
⊢ leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) x = next (leRecOn hnm (fun {k} => next) x)
rw [leRecOn_succ]
case refl
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
x : C n
⊢ ∃ a, leRecOn (_ : Nat.le n n) (fun {k} => next) a = x
case refl
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
⊢ Function.Surjective (leRecOn (_ : Nat.le n n) fun {k} => next)
intro x
case refl
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
x : C n
⊢ leRecOn (_ : Nat.le n n) (fun {k} => next) x = x
case refl
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
x : C n
⊢ ∃ a, leRecOn (_ : Nat.le n n) (fun {k} => next) a = x
use x
no goals
case refl
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
x : C n
⊢ leRecOn (_ : Nat.le n n) (fun {k} => next) x = x
rw [leRecOn_self]