Commit 2026-09-15 16:52 d87564e8

View on Github →

refactor(Data/SetLike): generalise IsConcreteLE (#42666)

  • Generalise IsConcreteLE typeclass from SetLike to Membership
  • Generalise the API where possible
  • Rename theorems to match generalisation AI usage disclosure: Codex was used to fix long line lints. All changes were manually reviewed.

Estimated changes

added def LE.ofMembership
deleted def LE.ofSetLike
modified theorem SetLike.coe_ssubset_coe
modified theorem SetLike.coe_subset_coe
deleted theorem SetLike.exists_of_lt
deleted theorem SetLike.le_def
deleted theorem SetLike.not_le_iff_exists