chore(fintype/card_embedding): generalize instances (#12775)

Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

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`.

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

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

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⟩