`induction` passes wrong instance to function application

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

induction will use instances on the original variable in function applications on the new variable. The tactic will succeed, and indeed create new goals, but the proof will have a type error.

Context

This was discovered during usage of https://github.com/leanprover-community/repl, where we found a successful sequence of tactics resulting in an unsuccessful proof.

Steps to Reproduce

/--
warning: declaration uses 'sorry'
---
error: application type mismatch
  @Fin.instOfNat n inst✝
argument has type
  NeZero n✝
but function has type
  [inst : NeZero n] → {i : Nat} → OfNat (Fin n) i
-/
#guard_msgs in
example (n: Nat) [NeZero n] : (0 : Fin n) = 0 := by
  induction n <;> sorry

Expected behavior: An error on the tactic as it should try to synthesize NeZero 0 and NeZero n (where the original n is succ of this n) and both should fail.

Actual behavior: The tactic uses the original NeZero n✝ instance to synthesize Fin.instOfNat, for the new (0 : Fin n), which is not type-correct. Yet the tactic does not fail.

Versions

Lean 4.16.0-rc1
Target: x86_64-unknown-linux-gnu
live.lean-lang.org

Additional Information

Initially, https://github.com/leanprover/lean4/issues/4246 looked similar, but I think it's not the same.

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 Lean example in the issue and inspect the induction tactic's handling of instances for the new variable. Done means the tactic reports an error when it cannot synthesize NeZero 0 or NeZero n, rather than creating a proof that later has a type error.