`omit` not working for Prop-valued instances

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

Currently, lemmas only use variables in the context that are referred to in the statement, while definitions use variables that are refereed to in the statement and in the body. I would expect that Prop-valued instances behave like lemmas, and data-carrying instances behave like definitions, but this is not the case: omit does not work for Prop-valued instances.

Context

This issue is a minimization of an issue showing up in mathlib, see discussion at #mathlib4 > Is `omit` broken? @ 💬

Steps to Reproduce

Run the following code:

class A (α : Type) : Prop where
class B (α : Type) : Prop where
class C (α : Type) : Prop where

instance BtoC (α : Type) [B α] : C α := {}
instance AtoC (α : Type) [A α] : C α := {}

variable (α : Type) [h : A α]

omit h in
instance myinst [B α] : C α := by
  infer_instance

#check myinst -- myinst (α : Type) [h : A α] [B α] : C α

Expected behavior: Since myinst is a Prop-valued instance, I expect the line omit h to work, and the infer_instance line to use BtoC, as there should be no assumption [A α] in the context.

Actual behavior: h is not omitted, so [A α] is available in the proof of myinst, and is used in the infer_instance line. In the end, myinst requires both [A α] and [B α].

Versions

Lean 4.23.0-nightly-2025-07-28
Target: x86_64-unknown-linux-gnu

Additional Information

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 the issue against the stated Lean nightly version, then trace the implementation of omit for Prop-valued instances. Done means h is absent from myinst and the proof uses BtoC, leaving myinst dependent only on [B α].