Order.SupIndep mathlib4#1627

Stream: mathlib4

[Ruben Van de Velde]

I'm stuck on

def Independent {ι : Sort _} {α : Type _} [CompleteLattice α] (t : ι → α) : Prop :=
  ∀ i : ι, Disjoint (t i) (⨆ (j) (_ : j ≠ i), t j)

with error

elaboration function for 'Lean.Parser.Command.«termExpand_binders%(_=>_)_,_»' has not been implemented
  expand_binders% (f✝ => supᵢ✝ f✝) (_ : j ≠ i), t j

Any thoughts?

[Patrick Massot]

def Independent {ι : Sort _} {α : Type _} [CompleteLattice α] (t : ι → α) : Prop :=
  ∀ i : ι, Disjoint (t i) (⨆ (j) (_H : j ≠ i), t j)

will work, but maybe we now have a better solution (that was the state of the art solution one month ago).

[Patrick Massot]

At least this will get you unstuck.

[Ruben Van de Velde]

Huh, I thought I tried that. Thanks

[Patrick Massot]

Don't forget to let a porting note flagging this (unless @Mario Carneiro tells us there is a better solution now).

[Mario Carneiro]

oh, that's just a simple bug in the implementation, I hadn't heard about this before