Commit 2025-08-16 00:47 efa1ad90

feat: add @[simp] to Multiset.cons_le_cons and Finset.insert_subset_insert (#28285) I see some other similar theorems such as List.cons_sublist_cons and Finset.cons_subset_cons are already marked with @[simp] annotations. Doing this enables the following statements to be proved simpler with a single simp, which in turn makes proofs more easily found by proof search tactics:

example a b c : {a, b} ≤ ({a, b, c} : Multiset ℝ) := by
  simp
example a b : {a, b} ≤ ({a, a, b, b} : Multiset ℝ) := by
  simp
example a b c : {a, b} ⊆ ({a, b, c} : Finset ℝ) := by
  simp