-- Mathlib/Data/Nat/Basic.lean
lemma leRecOn_surjective {C : ℕ → Sort*} {n m} (hnm : n ≤ m) (next : ∀ {k}, C k → C (k + 1))
    (Hnext : ∀ n, Surjective (@next n)) : Surjective (@leRecOn C n m hnm next)

Proof state:
case step.intro
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} => next)
w : C m✝
⊢ ∃ a, leRecOn ⋯ (fun {k} => next) a = next w

Tactic:
obtain ⟨x, rfl⟩ := ih w

Result:
case step.intro.intro
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} => next)
x : C n
⊢ ∃ a, leRecOn ⋯ (fun {k} => next) a = next (leRecOn hnm (fun {k} => next) x)

Proof state:
case step.intro.intro
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} => next)
x : C n
⊢ leRecOn ⋯ (fun {k} => next) x = next (leRecOn hnm (fun {k} => next) x)

Tactic:
rw [leRecOn_succ]

Result:
no goals

Proof state:
case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
x : C n
⊢ leRecOn ⋯ (fun {k} => next) x = x

Tactic:
rw [leRecOn_self]

Result:
no goals

Proof state:
case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
x : C n
⊢ ∃ a, leRecOn ⋯ (fun {k} => next) a = x

Tactic:
refine ⟨x, ?_⟩

Result:
case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
x : C n
⊢ leRecOn ⋯ (fun {k} => next) x = x

Proof state:
C : ℕ → Sort u_1
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
⊢ Surjective (leRecOn hnm fun {k} => next)

Tactic:
induction hnm with
| refl =>
  intro x
  refine ⟨x, ?_⟩
  rw [leRecOn_self]
| step hnm ih =>
  intro x
  obtain ⟨w, rfl⟩ := Hnext _ x
  obtain ⟨x, rfl⟩ := ih w
  refine ⟨x, ?_⟩
  rw [leRecOn_succ]

Result:
no goals

Proof state:
case step.intro.intro
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} => next)
x : C n
⊢ ∃ a, leRecOn ⋯ (fun {k} => next) a = next (leRecOn hnm (fun {k} => next) x)

Tactic:
refine ⟨x, ?_⟩

Result:
case step.intro.intro
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} => next)
x : C n
⊢ leRecOn ⋯ (fun {k} => next) x = next (leRecOn hnm (fun {k} => next) x)

Proof state:
case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} => next)
x : C m✝.succ
⊢ ∃ a, leRecOn ⋯ (fun {k} => next) a = x

Tactic:
obtain ⟨w, rfl⟩ := Hnext _ x

Result:
case step.intro
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} => next)
w : C m✝
⊢ ∃ a, leRecOn ⋯ (fun {k} => next) a = next w

Proof state:
case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} => next)
⊢ Surjective (leRecOn ⋯ fun {k} => next)

Tactic:
intro x

Result:
case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} => next)
x : C m✝.succ
⊢ ∃ a, leRecOn ⋯ (fun {k} => next) a = x

Proof state:
case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
⊢ Surjective (leRecOn ⋯ fun {k} => next)

Tactic:
intro x

Result:
case refl
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
x : C n
⊢ ∃ a, leRecOn ⋯ (fun {k} => next) a = x