Commit 2024-11-21 08:54 1e5f38b9
View on Github →feat: Measure.count s = 0 ↔ s = ∅ unconditionally (#19287)
By moving cases around, we can remove all side conditions from the lemma stating count s = 0 ↔ s = ∅. As a result, a few pairs of lemmas are unified.
From LeanAPAP