unexpected eliminator resulting type

Stream: mathlib4

[Maxwell Thum]

In Logic.Encodable.Lattice,

@[elab_as_elim]
theorem Union_decode₂_cases {f : β → Set α} {C : Set α → Prop} (H0 : C ∅) (H1 : ∀ b, C (f b)) {n} :
    C (⋃ b ∈ decode₂ β n, f b)

gives me the error

unexpected eliminator resulting type
  C (unionᵢ fun b => unionᵢ fun h => f b)

[Maxwell Thum]

Is this an issue with elab_as_elim? Perhaps a feature?

[Eric Wieser]

I think in Lean 3, elab_as_elim was often just ignored

[Maxwell Thum]

Is it safe to just comment it out or delete it then?

[Eric Wieser]

Commenting out with a porting note seems fine

[Eric Wieser]

But maybe this is a feature that Lean could support