Commit 2026-04-27 15:18 16c33f09

View on Github →

chore(Data/Finset/Card): use section variables rather than fresh arguments in three lemmas (#37796)

Estimated changes

Modified Mathlib/Data/Finset/Card.lean

modified theorem Finset.card_sdiff_add_card_eq_card

modified theorem Finset.eq_of_subset_of_card_le

modified theorem Finset.exists_eq_insert_iff