supr over units ℤ

Stream: Is there code for X?

[Eric Wieser]

Do we have this anywhere?

lemma supr_units_int {α : Type*} (f : units ℤ → α) [complete_lattice α] :
  ⨆ i : units ℤ,  f i = f 1 ⊔ f (-1) :=
sorry

docs#supr_bool_eq is close, but I'm not sure of the easiest way to glue it

[Johan Commelin]

Shouldn't there be general machinery for fintypes that folds over finset.univ or something like that?

[Johan Commelin]

Doing this just for units ℤ seems too specific. If I take the sup indexed by fin 5, I want 3 well-chosen simp/rw lemmas to turn it into

f 0 ⊔ f 1 ⊔ f 2 ⊔ f 3 ⊔ f 4

etc...

[Anne Baanen]

I know there's something along the lines of docs#int.units_eq_one_or, (EDIT:) and we have docs#units_int.univ

[Eric Wieser]

Converting to finset.sup sounds like the way to go

[Eric Wieser]

docs#finset.sup_eq_supr?

[Yaël Dillies]

Yup

[Anne Baanen]

And then perhaps docs#finset.sup_insert?