feat: a replacement for Nat.leRecOn' that works with induction (#14431)

Before this PR, we had:
* `theorem Nat.le.rec`: induct on `a ≤ b`, but using an annoying `a.le b` spelling
* `theorem Nat.le_induction`: induct on `a ≤ b`
* `def Nat.leRecOn'`, which is `Nat.le.rec` that works in `Sort*` but does not work with the `induction` keyword. There are no lemmas about this definition.
* `def Nat.leRecOn`, a weaker version of `Nat.leRecOn'` that also doesn't work with `induction`. There are lots of lemmas about this definition

This PR introduces `Nat.leRec`, which is a `Sort*`-valued version of `Nat.le.rec`, with a signature that coincides in the `Prop` case.
Where appropriate, the lemmas about `Nat.leRecOn` are recovered as special cases of lemmas about this new definition.
`Nat.leRecOn'` is then deprecated, as it is strictly less useful than `Nat.leRec`.

This also changes the signature of `Nat.decreasingInduction` to be usable with the `induction` tactic, with no deprecated alias since there are very few uses.

`Nat.decreasingInduction'` is left alone, as it is unclear to me how to state it in a way understood by `induction`.

Author: eric-wieser

Mathlib/Data/Nat/Choose/Basic.lean

@@ -304,12 +304,10 @@ theorem choose_le_succ_of_lt_half_left {r n : ℕ} (h : r < n / 2) :
 
 /-- Show that for small values of the right argument, the middle value is largest. -/
 private theorem choose_le_middle_of_le_half_left {n r : ℕ} (hr : r ≤ n / 2) :
-    choose n r ≤ choose n (n / 2) :=
-  decreasingInduction
-    (fun _ k a =>
-      (eq_or_lt_of_le a).elim (fun t => t.symm ▸ le_rfl) fun h =>
-        (choose_le_succ_of_lt_half_left h).trans (k h))
-    hr (fun _ => le_rfl) hr
+    choose n r ≤ choose n (n / 2) := by
+  induction hr using decreasingInduction with
+  | self => rfl
+  | of_succ k hk ih => exact (choose_le_succ_of_lt_half_left hk).trans ih
 
 /-- `choose n r` is maximised when `r` is `n/2`. -/
 theorem choose_le_middle (r n : ℕ) : choose n r ≤ choose n (n / 2) := by

Mathlib/Data/Nat/Defs.lean

@@ -854,52 +854,112 @@ lemma rec_add_one {C : ℕ → Sort*} (h0 : C 0) (h : ∀ n, C n → C (n + 1))
     Nat.rec (motive := C) h0 h 1 = h 0 h0 := rfl
 
 /-- Recursion starting at a non-zero number: given a map `C k → C (k+1)` for each `k ≥ n`,
-there is a map from `C n` to each `C m`, `n ≤ m`. -/
+there is a map from `C n` to each `C m`, `n ≤ m`.
+
+This is a version of `Nat.le.rec` that works for `Sort u`.
+Similarly to `Nat.le.rec`, it can be used as
+```
+induction hle using Nat.leRec with
+| refl => sorry
+| le_succ_of_le hle ih => sorry
+```
+-/
 @[elab_as_elim]
-def leRecOn' {C : ℕ → Sort*} : ∀ {m}, n ≤ m → (∀ ⦃k⦄, n ≤ k → C k → C (k + 1)) → C n → C m
-  | 0, H, _, x => Eq.recOn (Nat.eq_zero_of_le_zero H) x
-  | m + 1, H, next, x => (le_succ_iff.1 H).by_cases (fun h : n ≤ m ↦ next h <| leRecOn' h next x)
-      fun h : n = m + 1 ↦ Eq.recOn h x
+def leRec {n} {motive : (m : ℕ) → n ≤ m → Sort*}
+    (refl : motive n le_rfl)
+    (le_succ_of_le : ∀ ⦃k⦄ (h : n ≤ k), motive k h → motive (k + 1) (le_succ_of_le h)) :
+    ∀ {m} (h : n ≤ m), motive m h
+  | 0, H => Nat.eq_zero_of_le_zero H ▸ refl
+  | m + 1, H =>
+    (le_succ_iff.1 H).by_cases
+      (fun h : n ≤ m ↦ le_succ_of_le h <| leRec refl le_succ_of_le h)
+      (fun h : n = m + 1 ↦ h ▸ refl)
+
+-- This verifies the signatures of the recursor matches the builtin one, as promised in the
+-- above.
+theorem leRec_eq_leRec : @Nat.leRec.{0} = @Nat.le.rec := rfl
+
+@[simp]
+lemma leRec_self {n} {motive : (m : ℕ) → n ≤ m → Sort*}
+    (refl : motive n le_rfl)
+    (le_succ_of_le : ∀ ⦃k⦄ (h : n ≤ k), motive k h → motive (k + 1) (le_succ_of_le h)) :
+    (leRec (motive := motive) refl le_succ_of_le le_rfl : motive n le_rfl) = refl := by
+  cases n <;> simp [leRec, Or.by_cases, dif_neg]
+
+@[simp]
+lemma leRec_succ {n} {motive : (m : ℕ) → n ≤ m → Sort*}
+    (refl : motive n le_rfl)
+    (le_succ_of_le : ∀ ⦃k⦄ (h : n ≤ k), motive k h → motive (k + 1) (le_succ_of_le h))
+    (h1 : n ≤ m) {h2 : n ≤ m + 1} :
+    (leRec (motive := motive) refl le_succ_of_le h2) =
+      le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1) := by
+  conv =>
+    lhs
+    rw [leRec, Or.by_cases, dif_pos h1]
+
+lemma leRec_succ' {n} {motive : (m : ℕ) → n ≤ m → Sort*} (refl le_succ_of_le) :
+    (leRec (motive := motive) refl le_succ_of_le (le_succ _)) = le_succ_of_le _ refl := by
+  rw [leRec_succ, leRec_self]
+
+lemma leRec_trans {n m k} {motive : (m : ℕ) → n ≤ m → Sort*} (refl le_succ_of_le)
+    (hnm : n ≤ m) (hmk : m ≤ k) :
+    leRec (motive := motive) refl le_succ_of_le (Nat.le_trans hnm hmk) =
+      leRec
+        (leRec refl (fun _ h => le_succ_of_le h) hnm)
+        (fun _ h => le_succ_of_le <| Nat.le_trans hnm h) hmk := by
+  induction hmk with
+  | refl => rw [leRec_self]
+  | step hmk ih => rw [leRec_succ _ _ (Nat.le_trans hnm hmk), ih, leRec_succ]
+
+lemma leRec_succ_left {motive : (m : ℕ) → n ≤ m → Sort*}
+    (refl le_succ_of_le) {m} (h1 : n ≤ m) (h2 : n + 1 ≤ m) :
+    -- the `@` is needed for this to elaborate, even though we only provide explicit arguments!
+    @leRec _ _ (le_succ_of_le le_rfl refl) (fun k h ih => le_succ_of_le (le_of_succ_le h) ih) _ h2 =
+      leRec (motive := motive) refl le_succ_of_le h1 := by
+  rw [leRec_trans _ _ (le_succ n) h2, leRec_succ']
+
+/-- Recursion starting at a non-zero number: given a map `C k → C (k+1)` for each `k ≥ n`,
+there is a map from `C n` to each `C m`, `n ≤ m`.
+
+Prefer `Nat.leRec`, which can be used as `induction h using Nat.leRec`. -/
+@[elab_as_elim, deprecated Nat.leRec (since := "2024-07-05")]
+def leRecOn' {C : ℕ → Sort*} : ∀ {m}, n ≤ m → (∀ ⦃k⦄, n ≤ k → C k → C (k + 1)) → C n → C m :=
+  fun h of_succ self => Nat.leRec self of_succ h
 #align nat.le_rec_on' Nat.leRecOn'
 
 /-- Recursion starting at a non-zero number: given a map `C k → C (k + 1)` for each `k`,
 there is a map from `C n` to each `C m`, `n ≤ m`. For a version where the assumption is only made
-when `k ≥ n`, see `Nat.leRecOn'`. -/
+when `k ≥ n`, see `Nat.leRec`. -/
 @[elab_as_elim]
-def leRecOn {C : ℕ → Sort*} {n : ℕ} : ∀ {m}, n ≤ m → (∀ {k}, C k → C (k + 1)) → C n → C m
-  | 0, H, _, x => Eq.recOn (Nat.eq_zero_of_le_zero H) x
-  | m + 1, H, next, x => (le_succ_iff.1 H).by_cases (fun h : n ≤ m ↦ next <| leRecOn h next x)
-      fun h : n = m + 1 ↦ Eq.recOn h x
+def leRecOn {C : ℕ → Sort*} {n : ℕ} : ∀ {m}, n ≤ m → (∀ {k}, C k → C (k + 1)) → C n → C m :=
+  fun h of_succ self => Nat.leRec self (fun _ _ => @of_succ _) h
 #align nat.le_rec_on Nat.leRecOn
 
 lemma leRecOn_self {C : ℕ → Sort*} {n} {next : ∀ {k}, C k → C (k + 1)} (x : C n) :
-    (leRecOn n.le_refl next x : C n) = x := by cases n <;> simp [leRecOn, Or.by_cases, dif_neg]
+    (leRecOn n.le_refl next x : C n) = x :=
+  leRec_self _ _
 #align nat.le_rec_on_self Nat.leRecOn_self
 
 lemma leRecOn_succ {C : ℕ → Sort*} {n m} (h1 : n ≤ m) {h2 : n ≤ m + 1} {next} (x : C n) :
-    (leRecOn h2 next x : C (m + 1)) = next (leRecOn h1 next x : C m) := by
-  conv =>
-    lhs
-    rw [leRecOn, Or.by_cases, dif_pos h1]
+    (leRecOn h2 next x : C (m + 1)) = next (leRecOn h1 next x : C m) :=
+  leRec_succ _ _ _
 #align nat.le_rec_on_succ Nat.leRecOn_succ
 
 lemma leRecOn_succ' {C : ℕ → Sort*} {n} {h : n ≤ n + 1} {next : ∀ {k}, C k → C (k + 1)} (x : C n) :
-    (leRecOn h next x : C (n + 1)) = next x := by rw [leRecOn_succ (le_refl n), leRecOn_self]
+    (leRecOn h next x : C (n + 1)) = next x :=
+  leRec_succ' _ _
 #align nat.le_rec_on_succ' Nat.leRecOn_succ'
 
 lemma leRecOn_trans {C : ℕ → Sort*} {n m k} (hnm : n ≤ m) (hmk : m ≤ k) {next} (x : C n) :
     (leRecOn (Nat.le_trans hnm hmk) (@next) x : C k) =
-      leRecOn hmk (@next) (leRecOn hnm (@next) x) := by
-  induction hmk with
-  | refl => rw [leRecOn_self]
-  | step hmk ih => rw [leRecOn_succ (Nat.le_trans hnm hmk), ih, leRecOn_succ]
+      leRecOn hmk (@next) (leRecOn hnm (@next) x) :=
+  leRec_trans _ _ _ _
 #align nat.le_rec_on_trans Nat.leRecOn_trans
 
-lemma leRecOn_succ_left {C : ℕ → Sort*} {n m} (h1 : n ≤ m) (h2 : n + 1 ≤ m)
-    {next : ∀ {k}, C k → C (k + 1)} (x : C n) :
-    (leRecOn h2 next (next x) : C m) = (leRecOn h1 next x : C m) := by
-  rw [Subsingleton.elim h1 (Nat.le_trans (le_succ n) h2), leRecOn_trans (le_succ n) h2,
-    leRecOn_succ']
+lemma leRecOn_succ_left {C : ℕ → Sort*} {n m}
+    {next : ∀ {k}, C k → C (k + 1)} (x : C n) (h1 : n ≤ m) (h2 : n + 1 ≤ m) :
+    (leRecOn h2 next (next x) : C m) = (leRecOn h1 next x : C m) :=
+  leRec_succ_left (motive := fun n _ => C n) _ (fun _ _ => @next _) _ _
 #align nat.le_rec_on_succ_left Nat.leRecOn_succ_left
 
 lemma leRecOn_injective {C : ℕ → Sort*} {n m} (hnm : n ≤ m) (next : ∀ {k}, C k → C (k + 1))
@@ -946,62 +1006,69 @@ lemma strongRecOn'_beta {P : ℕ → Sort*} {h} :
   simp only [strongRecOn']; rw [Nat.strongRec']
 #align nat.strong_rec_on_beta' Nat.strongRecOn'_beta
 
-/-- Induction principle starting at a non-zero number. For maps to a `Sort*` see `leRecOn`.
+/-- Induction principle starting at a non-zero number.
 To use in an induction proof, the syntax is `induction n, hn using Nat.le_induction` (or the same
-for `induction'`). -/
+for `induction'`).
+
+This is an alias of `Nat.leRec`, specialized to `Prop`. -/
 @[elab_as_elim]
 lemma le_induction {m : ℕ} {P : ∀ n, m ≤ n → Prop} (base : P m m.le_refl)
-    (succ : ∀ n hmn, P n hmn → P (n + 1) (le_succ_of_le hmn)) : ∀ n hmn, P n hmn := fun n hmn ↦ by
-  apply Nat.le.rec
-  · exact base
-  · intros n hn
-    apply succ n hn
+    (succ : ∀ n hmn, P n hmn → P (n + 1) (le_succ_of_le hmn)) : ∀ n hmn, P n hmn :=
+  @Nat.leRec (motive := P) base succ
 #align nat.le_induction Nat.le_induction
 
-/-- Decreasing induction: if `P (k+1)` implies `P k`, then `P n` implies `P m` for all `m ≤ n`.
-Also works for functions to `Sort*`. For m version assuming only the assumption for `k < n`, see
-`decreasing_induction'`. -/
+/-- Decreasing induction: if `P (k+1)` implies `P k` for all `k < n`, then `P n` implies `P m` for
+all `m ≤ n`.
+Also works for functions to `Sort*`.
+
+For a version also assuming `m ≤ k`, see `Nat.decreasingInduction'`. -/
 @[elab_as_elim]
-def decreasingInduction {P : ℕ → Sort*} (h : ∀ n, P (n + 1) → P n) (mn : m ≤ n) (hP : P n) : P m :=
-  leRecOn mn (fun {k} ih hsk ↦ ih <| h k hsk) (fun h ↦ h) hP
+def decreasingInduction {n} {motive : (m : ℕ) → m ≤ n → Sort*}
+    (of_succ : ∀ k (h : k < n), motive (k + 1) h → motive k (le_of_succ_le h))
+    (self : motive n le_rfl) {m} (mn : m ≤ n) : motive m mn := by
+  induction mn using leRec with
+  | refl => exact self
+  | @le_succ_of_le k _ ih =>
+    apply ih (fun i hi => of_succ i (le_succ_of_le hi)) (of_succ k (lt_succ_self _) self)
 #align nat.decreasing_induction Nat.decreasingInduction
 
 @[simp]
-lemma decreasingInduction_self {P : ℕ → Sort*} (h : ∀ n, P (n + 1) → P n) (nn : n ≤ n)
-    (hP : P n) :
-    (decreasingInduction h nn hP : P n) = hP := by
+lemma decreasingInduction_self {n} {motive : (m : ℕ) → m ≤ n → Sort*} (of_succ self) :
+    (decreasingInduction (motive := motive) of_succ self le_rfl) = self := by
   dsimp only [decreasingInduction]
-  rw [leRecOn_self]
+  rw [leRec_self]
 #align nat.decreasing_induction_self Nat.decreasingInduction_self
 
-lemma decreasingInduction_succ {P : ℕ → Sort*} (h : ∀ n, P (n + 1) → P n) (mn : m ≤ n)
-    (msn : m ≤ n + 1) (hP : P (n + 1)) :
-    (decreasingInduction h msn hP : P m) = decreasingInduction h mn (h n hP) := by
-  dsimp only [decreasingInduction]; rw [leRecOn_succ]
+lemma decreasingInduction_succ {n} {motive : (m : ℕ) → m ≤ n + 1 → Sort*} (of_succ self)
+    (mn : m ≤ n) (msn : m ≤ n + 1) :
+    (decreasingInduction (motive := motive) of_succ self msn : motive m msn) =
+      decreasingInduction (motive := fun m h => motive m (le_succ_of_le h))
+        (fun i hi => of_succ _ _) (of_succ _ _ self) mn := by
+  dsimp only [decreasingInduction]; rw [leRec_succ]
 #align nat.decreasing_induction_succ Nat.decreasingInduction_succ
 
 @[simp]
-lemma decreasingInduction_succ' {P : ℕ → Sort*} (h : ∀ n, P (n + 1) → P n) {m : ℕ}
-    (msm : m ≤ m + 1) (hP : P (m + 1)) : decreasingInduction h msm hP = h m hP := by
-  dsimp only [decreasingInduction]; rw [leRecOn_succ']
+lemma decreasingInduction_succ' {n} {motive : (m : ℕ) → m ≤ n + 1 → Sort*} (of_succ self) :
+    decreasingInduction (motive := motive) of_succ self n.le_succ = of_succ _ _ self := by
+  dsimp only [decreasingInduction]; rw [leRec_succ']
 #align nat.decreasing_induction_succ' Nat.decreasingInduction_succ'
 
-lemma decreasingInduction_trans {P : ℕ → Sort*} (h : ∀ n, P (n + 1) → P n)
-    (hmn : m ≤ n) (hnk : n ≤ k) (hP : P k) :
-    (decreasingInduction h (Nat.le_trans hmn hnk) hP : P m) =
-    decreasingInduction h hmn (decreasingInduction h hnk hP) := by
+lemma decreasingInduction_trans {motive : (m : ℕ) → m ≤ k → Sort*} (hmn : m ≤ n) (hnk : n ≤ k)
+    (of_succ self) :
+    (decreasingInduction (motive := motive) of_succ self (Nat.le_trans hmn hnk) : motive m _) =
+    decreasingInduction (fun n ih => of_succ _ _) (decreasingInduction of_succ self hnk) hmn := by
   induction hnk with
   | refl => rw [decreasingInduction_self]
   | step hnk ih =>
-      rw [decreasingInduction_succ h (Nat.le_trans hmn hnk), ih, decreasingInduction_succ]
+      rw [decreasingInduction_succ _ _ (Nat.le_trans hmn hnk), ih, decreasingInduction_succ]
 #align nat.decreasing_induction_trans Nat.decreasingInduction_trans
 
-lemma decreasingInduction_succ_left {P : ℕ → Sort*} (h : ∀ n, P (n + 1) → P n)
-    (smn : m + 1 ≤ n) (mn : m ≤ n) (hP : P n) :
-    decreasingInduction h mn hP = h m (decreasingInduction h smn hP) := by
+lemma decreasingInduction_succ_left  {motive : (m : ℕ) → m ≤ n → Sort*} (of_succ self)
+    (smn : m + 1 ≤ n) (mn : m ≤ n) :
+    decreasingInduction (motive := motive) of_succ self mn =
+      of_succ m smn (decreasingInduction of_succ self smn) := by
   rw [Subsingleton.elim mn (Nat.le_trans (le_succ m) smn), decreasingInduction_trans,
     decreasingInduction_succ']
-  apply Nat.le_succ
 #align nat.decreasing_induction_succ_left Nat.decreasingInduction_succ_left
 
 /-- Given `P : ℕ → ℕ → Sort*`, if for all `m n : ℕ` we can extend `P` from the rectangle
@@ -1029,18 +1096,16 @@ def pincerRecursion {P : ℕ → ℕ → Sort*} (Ha0 : ∀ m : ℕ, P m 0) (H0b
 #align nat.pincer_recursion Nat.pincerRecursion
 
 /-- Decreasing induction: if `P (k+1)` implies `P k` for all `m ≤ k < n`, then `P n` implies `P m`.
-Also works for functions to `Sort*`. Weakens the assumptions of `decreasing_induction`. -/
+Also works for functions to `Sort*`.
+
+Weakens the assumptions of `Nat.decreasingInduction`. -/
 @[elab_as_elim]
 def decreasingInduction' {P : ℕ → Sort*} (h : ∀ k < n, m ≤ k → P (k + 1) → P k)
     (mn : m ≤ n) (hP : P n) : P m := by
-  revert h hP
-  refine leRecOn' mn ?_ ?_
-  · intro n mn ih h hP
-    apply ih
-    · exact fun k hk ↦ h k (Nat.lt.step hk)
-    · exact h n (lt_succ_self n) mn hP
-  · intro _ hP
-    exact hP
+  induction mn using decreasingInduction with
+  | self => exact hP
+  | of_succ k hk ih =>
+    exact h _ (lt_of_succ_le hk) le_rfl (ih fun k' hk' h'' => h k' hk' <| le_of_succ_le h'')
 #align nat.decreasing_induction' Nat.decreasingInduction'
 
 /-- Given a predicate on two naturals `P : ℕ → ℕ → Prop`, `P a b` is true for all `a < b` if

Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

@@ -211,8 +211,7 @@ private theorem toStepOfLE'.succ (m n : ℕ) (h : m ≤ n) :
     toStepOfLE' k m (Nat.succ n) (h.trans n.le_succ) =
     (toStepSucc k n) ∘ toStepOfLE' k m n h := by
   ext x
-  convert Nat.leRecOn_succ h x
-  exact h.trans n.le_succ
+  exact Nat.leRecOn_succ h x
 
 /-- The canonical ring homomorphism to a step with a greater index. -/
 def toStepOfLE (m n : ℕ) (h : m ≤ n) : Step k m →+* Step k n where

Mathlib/LinearAlgebra/Matrix/Transvection.lean

@@ -370,13 +370,13 @@ def listTransvecRow : List (Matrix (Sum (Fin r) Unit) (Sum (Fin r) Unit) 𝕜) :
 /-- Multiplying by some of the matrices in `listTransvecCol M` does not change the last row. -/
 theorem listTransvecCol_mul_last_row_drop (i : Sum (Fin r) Unit) {k : ℕ} (hk : k ≤ r) :
     (((listTransvecCol M).drop k).prod * M) (inr unit) i = M (inr unit) i := by
-  -- Porting note: `apply` didn't work anymore, because of the implicit arguments
-  refine Nat.decreasingInduction' ?_ hk ?_
-  · intro n hn _ IH
+  induction hk using Nat.decreasingInduction with
+  | of_succ n hn IH =>
     have hn' : n < (listTransvecCol M).length := by simpa [listTransvecCol] using hn
     rw [List.drop_eq_getElem_cons hn']
     simpa [listTransvecCol, Matrix.mul_assoc]
-  · simp only [listTransvecCol, List.length_ofFn, le_refl, List.drop_eq_nil_of_le, List.prod_nil,
+  | self =>
+    simp only [listTransvecCol, List.length_ofFn, le_refl, List.drop_eq_nil_of_le, List.prod_nil,
       Matrix.one_mul]
 #align matrix.pivot.list_transvec_col_mul_last_row_drop Matrix.Pivot.listTransvecCol_mul_last_row_drop
 
@@ -397,9 +397,8 @@ theorem listTransvecCol_mul_last_col (hM : M (inr unit) (inr unit) ≠ 0) (i : F
           if k ≤ i then 0 else M (inl i) (inr unit) by
     simpa only [List.drop, _root_.zero_le, ite_true] using H 0 (zero_le _)
   intro k hk
-  -- Porting note: `apply` didn't work anymore, because of the implicit arguments
-  refine Nat.decreasingInduction' ?_ hk ?_
-  · intro n hn hk IH
+  induction hk using Nat.decreasingInduction with
+  | of_succ n hn IH =>
     have hn' : n < (listTransvecCol M).length := by simpa [listTransvecCol] using hn
     let n' : Fin r := ⟨n, hn⟩
     rw [List.drop_eq_getElem_cons hn']
@@ -427,7 +426,8 @@ theorem listTransvecCol_mul_last_col (hM : M (inr unit) (inr unit) ≠ 0) (i : F
       · rw [if_neg, if_neg]
         · simpa only [hni.symm, not_le, or_false_iff] using Nat.lt_succ_iff_lt_or_eq.1 hi
         · simpa only [not_le] using hi
-  · simp only [listTransvecCol, List.length_ofFn, le_refl, List.drop_eq_nil_of_le, List.prod_nil,
+  | self =>
+    simp only [listTransvecCol, List.length_ofFn, le_refl, List.drop_eq_nil_of_le, List.prod_nil,
       Matrix.one_mul]
     rw [if_neg]
     simpa only [not_le] using i.2

Mathlib/Order/Interval/Finset/Nat.lean

@@ -310,7 +310,7 @@ variable {P : ℕ → Prop} (h : ∀ n, P (n + 1) → P n)
 
 theorem Nat.decreasing_induction_of_not_bddAbove (hP : ¬BddAbove { x | P x }) (n : ℕ) : P n :=
   let ⟨_, hm, hl⟩ := not_bddAbove_iff.1 hP n
-  decreasingInduction h hl.le hm
+  decreasingInduction (fun _ _ => h _) hm hl.le
 #align nat.decreasing_induction_of_not_bdd_above Nat.decreasing_induction_of_not_bddAbove
 
 @[elab_as_elim]