Induction fails with let binding

Stream: lean4

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Is this a known issue?

inductive P : Nat → Prop
  | zero : P 0
  | succ {n : Nat} : P n → P (n + 1)

example : P (n + 1) → P n := by
  let m := n + 1; rw [← (show m = n + 1 from rfl)]
  intro h
  induction h
/-
Type mismatch when assigning motive
  let m := n + 1;
  fun h => P n
has type
  let m := n + 1;
  P m → Prop
but is expected to have type
  (a : Nat) → P a → Prop
-/

[Kenny Lau]

you can only induct on a free variable; you're meant to use generalize to convert it to a free variable.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Yeah, I know :) I was just wondering if this has been discussed before, but it seems like it has, also here.