From 5cbe3c4ff5b9d121c9a047f02946f5c49d4f8e0c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mar=C3=ADa=20In=C3=A9s=20de=20Frutos-Fern=C3=A1ndez?= Date: Wed, 14 Sep 2022 16:17:53 +0000 Subject: [PATCH] chore(data/finset/powerset): generalize powerset_len_nonempty (#16429) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `powerset_len_nonempty` holds for `n ≤ s.card`. --- src/data/finset/powerset.lean | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/data/finset/powerset.lean b/src/data/finset/powerset.lean index 8e4f0e13f3896..fc7401ccb03fc 100644 --- a/src/data/finset/powerset.lean +++ b/src/data/finset/powerset.lean @@ -195,15 +195,17 @@ begin simp [card_insert_of_not_mem this, nat.succ_inj'] end -lemma powerset_len_nonempty {n : ℕ} {s : finset α} (h : n < s.card) : +lemma powerset_len_nonempty {n : ℕ} {s : finset α} (h : n ≤ s.card) : (powerset_len n s).nonempty := begin classical, induction s using finset.induction_on with x s hx IH generalizing n, - { simpa using h }, + { rw [card_empty, le_zero_iff] at h, + rw [h, powerset_len_zero], + exact finset.singleton_nonempty _, }, { cases n, { simp }, - { rw [card_insert_of_not_mem hx, nat.succ_lt_succ_iff] at h, + { rw [card_insert_of_not_mem hx, nat.succ_le_succ_iff] at h, rw powerset_len_succ_insert hx, refine nonempty.mono _ ((IH h).image (insert x)), convert (subset_union_right _ _) } } @@ -247,7 +249,8 @@ begin { refine ⟨insert x t, _, mem_insert_self _ _⟩, rw [←insert_erase hx, powerset_len_succ_insert (not_mem_erase _ _)], exact mem_union_right _ (mem_image_of_mem _ ht) }, - { rwa [card_erase_of_mem hx, lt_tsub_iff_right] } } } + { rw [card_erase_of_mem hx], + exact nat.le_pred_of_lt hn, } } } end @[simp]