Commit 2024-02-28 10:54 a66bd9db

View on Github →

chore(Order/Lattice): Resolve porting notes (#11034)

  • The dsimp issue has been resolved.
  • I knew that the lemmas provable by simp were provable by simp in Lean 3, but the simp nf linter was more lax. Now there's definitely no need to tag them.
  • ematch is not coming back (and was already completely unused for years in Lean 3).
  • Unification has changed in Lean 4, so it's really unsurprising that we need to provide an extra argument to sup_ind. It's not expectable that this will ever change, neither is it necessary.
  • Dot notation on Function.update is still broken. This is the last remaining porting note.

Estimated changes

modified theorem inf_idem
modified theorem inf_left_idem
modified theorem inf_right_idem