data.finset.lattice mathlib4#1606

Stream: mathlib4

[Johan Commelin]

I'm working on this PR for a bit

[Johan Commelin]

I pushed.

[Johan Commelin]

There is some trouble aabout moving back and forth to OrderDual. We used to convert a lot of stuff. That no longer works because irreducible, I guess?

[Johan Commelin]

Is there a standard way too approach this now?

[Kevin Buzzard]

docs4#OrderDual

[Kevin Buzzard]

It doesn't look irreducible to me?

[Johan Commelin]

Huh! Then I don't know what's going on.

[Yaël Dillies]

Different order of elaboration is what's happening.

[Ruben Van de Velde]

I pushed alternative proofs for some of the OrderDual issues. Still some errors and name changes needed, if someone wants to pick it up

[Johan Commelin]

one error left

[Johan Commelin]

Should supr now always be renamed to sup\i?

[Johan Commelin]

final error fixed

[Johan Commelin]

There is one linter complaint.

[Johan Commelin]

@[simp]
theorem sup_attach (s : Finset β) (f : β → α) : (s.attach.sup fun x => f x) = s.sup f :=
-- LHS does not simplify

[Johan Commelin]

Which I don't understand because

example (s : Finset β) (f : β → α) : (s.attach.sup fun x => f x) = a := by
  simp? -- simp only [sup_attach]
  -- goal is now `sup s f = a`

[Johan Commelin]

I think this one is ready for review

[Heather Macbeth]

Johan Commelin said:

There is some trouble aabout moving back and forth to OrderDual. We used to convert a lot of stuff. That no longer works because irreducible, I guess?

Maybe it's just that convert is broken generally? Do the issues look like these ones?
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/convert.20failures