Is `omit` broken?

Stream: mathlib4

[Sébastien Gouëzel]

In the following mwe, the instance uses hi while I said to omit it explicitely. Is there a way around? (Note that this is a real issue in current mathlib, the sigma finiteness assumption is included while it shouldn't)

import Mathlib

open MeasureTheory
variable {ι X : Type*} [MeasurableSpace X] [Fintype ι] {μ : ι → Measure X}

variable [hi : ∀ i, SigmaFinite (μ i)]

omit hi in
instance pi.instIsFiniteMeasure' [∀ i, IsFiniteMeasure (μ i)] :
    IsFiniteMeasure (Measure.pi μ) :=
  ⟨Measure.pi_univ μ ▸ ENNReal.prod_lt_top (fun i _ ↦ measure_lt_top (μ i) _)⟩

[Andrew Yang]

I think omit only works for theorem/lemma. I don’t know anyway around this and I would love a solution too.

[Kyle Miller]

Andrew's observation suggests a workaround:

omit hi in
@[instance] theorem pi.instIsFiniteMeasure' [∀ i, IsFiniteMeasure (μ i)] :
    IsFiniteMeasure (Measure.pi μ) :=
  ⟨Measure.pi_univ μ ▸ ENNReal.prod_lt_top (fun i _ ↦ measure_lt_top (μ i) _)⟩

Would someone mind creating a mathlib-free example and making a Lean 4 issue?

[Sébastien Gouëzel]

lean4#9597