From 0faebd2af05ae55f707572c2ed9e88472b58a4c4 Mon Sep 17 00:00:00 2001 From: Eric Rodriguez Date: Thu, 24 Mar 2022 10:12:31 +0000 Subject: [PATCH] chore(fintype/card_embedding): generalize instances (#12775) Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com> Co-authored-by: Yury G. Kudryashov --- src/data/fintype/basic.lean | 23 +++++++--- src/data/fintype/card_embedding.lean | 66 ++++++++-------------------- src/data/set/finite.lean | 4 -- src/logic/embedding.lean | 8 ++++ 4 files changed, 45 insertions(+), 56 deletions(-) diff --git a/src/data/fintype/basic.lean b/src/data/fintype/basic.lean index e9bc941398cbd..a4f21e5e73191 100644 --- a/src/data/fintype/basic.lean +++ b/src/data/fintype/basic.lean @@ -661,14 +661,15 @@ by simp [finset.subset_iff, set.subset_def] @[simp, mono] theorem to_finset_strict_mono {s t : set α} [fintype s] [fintype t] : s.to_finset ⊂ t.to_finset ↔ s ⊂ t := -begin - rw [←lt_eq_ssubset, ←finset.lt_iff_ssubset, lt_iff_le_and_ne, lt_iff_le_and_ne], - simp -end +by simp only [finset.ssubset_def, to_finset_mono, ssubset_def] @[simp] theorem to_finset_disjoint_iff [decidable_eq α] {s t : set α} [fintype s] [fintype t] : disjoint s.to_finset t.to_finset ↔ disjoint s t := -⟨λ h x hx, h (by simpa using hx), λ h x hx, h (by simpa using hx)⟩ +by simp only [disjoint_iff_disjoint_coe, coe_to_finset] + +theorem to_finset_compl [decidable_eq α] [fintype α] (s : set α) [fintype s] [fintype ↥sᶜ] : + (sᶜ).to_finset = s.to_finsetᶜ := +by { ext a, simp } lemma filter_mem_univ_eq_to_finset [fintype α] (s : set α) [fintype s] [decidable_pred (∈ s)] : finset.univ.filter (∈ s) = s.to_finset := @@ -711,6 +712,13 @@ lemma finset.card_compl [decidable_eq α] [fintype α] (s : finset α) : sᶜ.card = fintype.card α - s.card := finset.card_univ_diff s +lemma fintype.card_compl_set [fintype α] (s : set α) [fintype s] [fintype ↥sᶜ] : + fintype.card ↥sᶜ = fintype.card α - fintype.card s := +begin + classical, + rw [← set.to_finset_card, ← set.to_finset_card, ← finset.card_compl, set.to_finset_compl] +end + instance (n : ℕ) : fintype (fin n) := ⟨finset.fin_range n, finset.mem_fin_range⟩ @@ -969,6 +977,11 @@ lemma card_range_le {α β : Type*} (f : α → β) [fintype α] [fintype (set.r fintype.card (set.range f) ≤ fintype.card α := fintype.card_le_of_surjective (λ a, ⟨f a, by simp⟩) (λ ⟨_, a, ha⟩, ⟨a, by simpa using ha⟩) +lemma card_range {α β F : Type*} [embedding_like F α β] (f : F) [fintype α] + [fintype (set.range f)] : + fintype.card (set.range f) = fintype.card α := +eq.symm $ fintype.card_congr $ equiv.of_injective _ $ embedding_like.injective f + /-- The pigeonhole principle for finitely many pigeons and pigeonholes. This is the `fintype` version of `finset.exists_ne_map_eq_of_card_lt_of_maps_to`. diff --git a/src/data/fintype/card_embedding.lean b/src/data/fintype/card_embedding.lean index efa216dadf65b..dac7ab5948cd6 100644 --- a/src/data/fintype/card_embedding.lean +++ b/src/data/fintype/card_embedding.lean @@ -16,63 +16,35 @@ This file establishes the cardinality of `α ↪ β` in full generality. local notation `|` x `|` := finset.card x local notation `‖` x `‖` := fintype.card x -open_locale nat - -local attribute [semireducible] function.embedding.fintype +open function +open_locale nat big_operators namespace fintype --- We need the separate `fintype α` instance as it contains data, --- and may not match definitionally with the instance coming from `unique.fintype`. -lemma card_embedding_eq_of_unique - {α β : Type*} [unique α] [fintype α] [fintype β] [decidable_eq α] [decidable_eq β]: -‖α ↪ β‖ = ‖β‖ := card_congr equiv.unique_embedding_equiv_result - -private lemma card_embedding_aux {n : ℕ} {β} [fintype β] [decidable_eq β] (h : n ≤ ‖β‖) : - ‖fin n ↪ β‖ = ‖β‖.desc_factorial n := -begin - induction n with n hn, - { nontriviality (fin 0 ↪ β), - rw [nat.desc_factorial_zero, fintype.card_eq_one_iff], - refine ⟨nonempty.some nontrivial.to_nonempty, λ x, function.embedding.ext fin.elim0⟩ }, - - rw [nat.succ_eq_add_one, ←card_congr (equiv.embedding_congr fin_sum_fin_equiv (equiv.refl β)), - card_congr equiv.sum_embedding_equiv_sigma_embedding_restricted], - -- these `rw`s create goals for instances, which it doesn't infer for some reason - all_goals { try { apply_instance } }, - -- however, this needs to be done here instead of at the end - -- else, a later `simp`, which depends on the `fintype` instance, won't work. - - have : ∀ (f : fin n ↪ β), ‖fin 1 ↪ ((set.range f)ᶜ : set β)‖ = ‖β‖ - n, - { intro f, - rw card_embedding_eq_of_unique, - rw card_of_finset' (finset.map f finset.univ)ᶜ, - { rw [finset.card_compl, finset.card_map, finset.card_fin] }, - { simp } }, - - -- putting `card_sigma` in `simp` causes it to not fully simplify - rw card_sigma, - simp only [this, finset.sum_const, finset.card_univ, nsmul_eq_mul, nat.cast_id], - - replace h := (nat.lt_of_succ_le h).le, - rw [nat.desc_factorial_succ, hn h, mul_comm] -end +lemma card_embedding_eq_of_unique {α β : Type*} [unique α] [fintype β] [fintype (α ↪ β)] : + ‖α ↪ β‖ = ‖β‖ := card_congr equiv.unique_embedding_equiv_result /- Establishes the cardinality of the type of all injections between two finite types. -/ -@[simp] theorem card_embedding_eq {α β} [fintype α] [fintype β] [decidable_eq α] [decidable_eq β] : -‖α ↪ β‖ = (‖β‖.desc_factorial ‖α‖) := +@[simp] theorem card_embedding_eq {α β} [fintype α] [fintype β] [fintype (α ↪ β)] : + ‖α ↪ β‖ = (‖β‖.desc_factorial ‖α‖) := begin - obtain h | h := lt_or_ge (‖β‖) (‖α‖), - { rw [card_eq_zero_iff.mpr (function.embedding.is_empty_of_card_lt h), - nat.desc_factorial_eq_zero_iff_lt.mpr h] }, - { trunc_cases fintype.trunc_equiv_fin α with eq, - rw fintype.card_congr (equiv.embedding_congr eq (equiv.refl β)), - exact card_embedding_aux h } + classical, + unfreezingI { induction ‹fintype α› using fintype.induction_empty_option' + with α₁ α₂ h₂ e ih α h ih }, + { letI := fintype.of_equiv _ e.symm, + rw [← card_congr (equiv.embedding_congr e (equiv.refl β)), ih, card_congr e] }, + { rw [card_pempty, nat.desc_factorial_zero, card_eq_one_iff], + exact ⟨embedding.of_is_empty, λ x, fun_like.ext _ _ is_empty_elim⟩ }, + { rw [card_option, nat.desc_factorial_succ, card_congr (embedding.option_embedding_equiv α β), + card_sigma, ← ih], + simp only [fintype.card_compl_set, fintype.card_range, finset.sum_const, finset.card_univ, + smul_eq_mul, mul_comm] }, end /- The cardinality of embeddings from an infinite type to a finite type is zero. This is a re-statement of the pigeonhole principle. -/ -@[simp] lemma card_embedding_eq_of_infinite {α β} [infinite α] [fintype β] : ‖α ↪ β‖ = 0 := +@[simp] lemma card_embedding_eq_of_infinite {α β} [infinite α] [fintype β] [fintype (α ↪ β)] : + ‖α ↪ β‖ = 0 := card_eq_zero_iff.mpr function.embedding.is_empty end fintype diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean index 142ffc1c0dd59..3a7af5e50e47d 100644 --- a/src/data/set/finite.lean +++ b/src/data/set/finite.lean @@ -776,10 +776,6 @@ let ⟨a, has, haf⟩ := (hs.diff f.finite_to_set).nonempty in ⟨a, has, λ h, section decidable_eq -lemma to_finset_compl {α : Type*} [fintype α] [decidable_eq α] - (s : set α) [fintype (sᶜ : set α)] [fintype s] : sᶜ.to_finset = (s.to_finset)ᶜ := -by ext; simp - lemma to_finset_inter {α : Type*} [decidable_eq α] (s t : set α) [fintype (s ∩ t : set α)] [fintype s] [fintype t] : (s ∩ t).to_finset = s.to_finset ∩ t.to_finset := by ext; simp diff --git a/src/logic/embedding.lean b/src/logic/embedding.lean index 7ac3bd7eca87c..700845176f34e 100644 --- a/src/logic/embedding.lean +++ b/src/logic/embedding.lean @@ -175,6 +175,14 @@ def coe_with_top {α} : α ↪ with_top α := { to_fun := coe, ..embedding.some} option α ↪ β := ⟨λ o, o.elim x f, option.injective_iff.2 ⟨f.2, h⟩⟩ +/-- Equivalence between embeddings of `option α` and a sigma type over the embeddings of `α`. -/ +@[simps] +def option_embedding_equiv (α β) : (option α ↪ β) ≃ Σ f : α ↪ β, ↥(set.range f)ᶜ := +{ to_fun := λ f, ⟨coe_option.trans f, f none, λ ⟨x, hx⟩, option.some_ne_none x $ f.injective hx⟩, + inv_fun := λ f, f.1.option_elim f.2 f.2.2, + left_inv := λ f, ext $ by { rintro (_|_); simp [option.coe_def] }, + right_inv := λ ⟨f, y, hy⟩, by { ext; simp [option.coe_def] } } + /-- Embedding of a `subtype`. -/ def subtype {α} (p : α → Prop) : subtype p ↪ α := ⟨coe, λ _ _, subtype.ext_val⟩