non-variable induction fails on two-argument induction principles

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

When using induction h : x, hx using or induction x, hx using, the generalization appears to be applied incorrectly.

Context

I am trying to simplify the lift tactic in mathlib to be a macro for induction.

Steps to Reproduce

1. Run the following code:

import Lean

theorem Nat.induction_pos {motive : (n : Nat) → 0 < n → Prop}
    (one : motive 1 (by omega))
    (succ_pos : ∀ n hn, motive n hn → motive (n + 1) (by omega)) :
    ∀ n hn, motive n hn :=
  fun _ hn => Nat.le.rec one @succ_pos hn

theorem broken {n : Nat} : (n + 1) ≠ 0 := by
  have hn : 0 < n + 1 := by omega
  induction n + 1, hn using Nat.induction_pos  -- fails

theorem broken_h {n : Nat} : (n + 1) ≠ 0 := by
  have hn : 0 < n + 1 := by omega
  induction h : n + 1, hn using Nat.induction_pos  -- fails

theorem ok {n : Nat} : (n + 1) ≠ 0 := by
  have hn : 0 < n + 1 := by omega
  generalize n + 1 = m at *
  induction m, hn using Nat.induction_pos -- ok
  all_goals sorry

theorem ok_h {n : Nat} : (n + 1) ≠ 0 := by
  have hn : 0 < n + 1 := by omega
  generalize h : n + 1 = m at *
  induction m, hn using Nat.induction_pos -- ok
  all_goals sorry

Expected behavior: induction succeeds in all cases

Actual behavior: The broken cases errors with

target
  hn
has type
  0 < n + 1 : Prop
but is expected to have type
  0 < x✝ : Prop

where the origin of x✝ is unclear.

Versions

[Output of #version or #eval Lean.versionString]
[OS version, if not using live.lean-lang.org.]

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the minimal reproduction in live.lean-lang.org or against the latest Lean nightly, focusing on the broken and broken_h induction cases using Nat.induction_pos. Compare them with the working generalize cases and confirm that induction succeeds without producing the x✝ type mismatch.