chore(data/fintype/basic): add fintype instance for is_empty (#7692)

Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>

src/analysis/mean_inequalities.lean

@@ -197,24 +197,24 @@ by exact_mod_cast real.geom_mean_le_arith_mean_weighted _ _ _ (λ i _, (w i).coe
 for two `nnreal` numbers. -/
 theorem geom_mean_le_arith_mean2_weighted (w₁ w₂ p₁ p₂ : ℝ≥0) :
   w₁ + w₂ = 1 → p₁ ^ (w₁:ℝ) * p₂ ^ (w₂:ℝ) ≤ w₁ * p₁ + w₂ * p₂ :=
-by simpa only [fin.prod_univ_succ, fin.sum_univ_succ, fin.prod_univ_zero, fin.sum_univ_zero,
-  fin.cons_succ, fin.cons_zero, add_zero, mul_one]
+by simpa only [fin.prod_univ_succ, fin.sum_univ_succ, finset.prod_empty, finset.sum_empty,
+  fintype.univ_of_is_empty, fin.cons_succ, fin.cons_zero, add_zero, mul_one]
 using geom_mean_le_arith_mean_weighted (univ : finset (fin 2))
   (fin.cons w₁ $ fin.cons w₂ fin_zero_elim) (fin.cons p₁ $ fin.cons p₂ $ fin_zero_elim)
 
 theorem geom_mean_le_arith_mean3_weighted (w₁ w₂ w₃ p₁ p₂ p₃ : ℝ≥0) :
   w₁ + w₂ + w₃ = 1 → p₁ ^ (w₁:ℝ) * p₂ ^ (w₂:ℝ) * p₃ ^ (w₃:ℝ) ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃ :=
-by simpa only  [fin.prod_univ_succ, fin.sum_univ_succ, fin.prod_univ_zero, fin.sum_univ_zero,
-  fin.cons_succ, fin.cons_zero, add_zero, mul_one, ← add_assoc, mul_assoc]
+by simpa only  [fin.prod_univ_succ, fin.sum_univ_succ, finset.prod_empty, finset.sum_empty,
+  fintype.univ_of_is_empty, fin.cons_succ, fin.cons_zero, add_zero, mul_one, ← add_assoc, mul_assoc]
 using geom_mean_le_arith_mean_weighted (univ : finset (fin 3))
   (fin.cons w₁ $ fin.cons w₂ $ fin.cons w₃ fin_zero_elim)
   (fin.cons p₁ $ fin.cons p₂ $ fin.cons p₃ fin_zero_elim)
 
 theorem geom_mean_le_arith_mean4_weighted (w₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : ℝ≥0) :
   w₁ + w₂ + w₃ + w₄ = 1 → p₁ ^ (w₁:ℝ) * p₂ ^ (w₂:ℝ) * p₃ ^ (w₃:ℝ)* p₄ ^ (w₄:ℝ) ≤
     w₁ * p₁ + w₂ * p₂ + w₃ * p₃ + w₄ * p₄ :=
-by simpa only  [fin.prod_univ_succ, fin.sum_univ_succ, fin.prod_univ_zero, fin.sum_univ_zero,
-  fin.cons_succ, fin.cons_zero, add_zero, mul_one, ← add_assoc, mul_assoc]
+by simpa only  [fin.prod_univ_succ, fin.sum_univ_succ, finset.prod_empty, finset.sum_empty,
+  fintype.univ_of_is_empty, fin.cons_succ, fin.cons_zero, add_zero, mul_one, ← add_assoc, mul_assoc]
 using geom_mean_le_arith_mean_weighted (univ : finset (fin 4))
   (fin.cons w₁ $ fin.cons w₂ $ fin.cons w₃ $ fin.cons w₄ fin_zero_elim)
   (fin.cons p₁ $ fin.cons p₂ $ fin.cons p₃ $ fin.cons p₄ fin_zero_elim)

src/data/fintype/basic.lean

@@ -51,6 +51,9 @@ univ_nonempty_iff.2 ‹_›
 lemma univ_eq_empty : (univ : finset α) = ∅ ↔ ¬nonempty α :=
 by rw [← univ_nonempty_iff, nonempty_iff_ne_empty, ne.def, not_not]
 
+lemma univ_eq_empty' : (univ : finset α) = ∅ ↔ is_empty α :=
+univ_eq_empty.trans (not_nonempty_iff)
+
 @[simp] theorem subset_univ (s : finset α) : s ⊆ univ := λ a _, mem_univ a
 
 instance : order_top (finset α) :=
@@ -483,16 +486,27 @@ arbitrary `fintype` instances, use either `fintype.card_le_one_iff_subsingleton`
   fintype.card α = 1 :=
 subsingleton.elim (of_subsingleton $ default α) h ▸ card_of_subsingleton _
 
+@[priority 100] -- see Note [lower instance priority]
+instance of_is_empty [is_empty α] : fintype α := ⟨∅, is_empty_elim⟩
+
+/-- Note: this lemma is specifically about `fintype.of_is_empty`. For a statement about
+arbitrary `fintype` instances, use `fintype.univ_eq_empty'`. -/
+@[simp] theorem univ_of_is_empty [is_empty α] : @univ α _ = ∅ := rfl
+
+/-- Note: this lemma is specifically about `fintype.of_is_empty`. For a statement about
+arbitrary `fintype` instances, use `fintype.card_eq_zero_iff`. -/
+@[simp] theorem card_of_is_empty [is_empty α] : fintype.card α = 0 := rfl
+
 open_locale classical
 variables (α)
 
 /-- Any subsingleton type is (noncomputably) a fintype (with zero or one terms). -/
-@[priority 100]
+@[priority 5] -- see Note [lower instance priority]
 noncomputable instance of_subsingleton' [subsingleton α] : fintype α :=
 if h : nonempty α then
   of_subsingleton (nonempty.some h)
 else
-  ⟨∅, (λ a, false.elim (h ⟨a⟩))⟩
+  @fintype.of_is_empty _ $ not_nonempty_iff.mp h
 
 end fintype
 
@@ -651,14 +665,10 @@ fintype.of_subsingleton (default α)
 @[simp] lemma univ_unique {α : Type*} [unique α] [f : fintype α] : @finset.univ α _ = {default α} :=
 by rw [subsingleton.elim f (@unique.fintype α _)]; refl
 
-instance : fintype empty := ⟨∅, empty.rec _⟩
-
 @[simp] theorem fintype.univ_empty : @univ empty _ = ∅ := rfl
 
 @[simp] theorem fintype.card_empty : fintype.card empty = 0 := rfl
 
-instance : fintype pempty := ⟨∅, pempty.rec _⟩
-
 @[simp] theorem fintype.univ_pempty : @univ pempty _ = ∅ := rfl
 
 @[simp] theorem fintype.card_pempty : fintype.card pempty = 0 := rfl
@@ -1076,8 +1086,6 @@ by { ext, simp only [set.mem_univ, mem_univ, set.mem_to_finset] }
   s.to_finset = ∅ ↔ s = ∅ :=
 by simp [ext_iff, set.ext_iff]
 
-instance : fintype (∅ : set α) := ⟨∅, subtype.property⟩
-
 @[simp] lemma set.to_finset_empty :
   (∅ : set α).to_finset = ∅ :=
 set.to_finset_eq_empty_iff.mpr rfl
@@ -1535,7 +1543,7 @@ instance function.embedding.is_empty {α β} [infinite α] [fintype β] : is_emp
 ⟨λ f, let ⟨x, y, ne, feq⟩ := fintype.exists_ne_map_eq_of_infinite f in ne $ f.injective feq⟩
 
 @[priority 100]
-noncomputable instance function.embedding.fintype'' {α β : Type*} [fintype β] : fintype (α ↪ β) :=
+noncomputable instance function.embedding.fintype' {α β : Type*} [fintype β] : fintype (α ↪ β) :=
 begin
   by_cases h : infinite α,
   { resetI, apply_instance },
@@ -1571,10 +1579,6 @@ assume (hf : surjective f),
 have H : infinite α := infinite.of_surjective f hf,
 by exactI not_fintype α
 
--- the instance generated by `is_empty → subsingleton → fintype is non-computable
-instance function.embedding.fintype' {α β} [infinite α] [fintype β] : fintype (α ↪ β) :=
-{ elems := finset.empty, complete := is_empty_elim }
-
 instance nat.infinite : infinite ℕ :=
 ⟨λ ⟨s, hs⟩, finset.not_mem_range_self $ s.subset_range_sup_succ (hs _)⟩
 

src/data/fintype/card.lean

@@ -126,7 +126,7 @@ theorem fin.prod_of_fn [comm_monoid β] {n : ℕ} (f : fin n → β) :
 by rw [list.of_fn_eq_map, fin.prod_univ_def]
 
 /-- A product of a function `f : fin 0 → β` is `1` because `fin 0` is empty -/
-@[simp, to_additive "A sum of a function `f : fin 0 → β` is `0` because `fin 0` is empty"]
+@[to_additive "A sum of a function `f : fin 0 → β` is `0` because `fin 0` is empty"]
 theorem fin.prod_univ_zero [comm_monoid β] (f : fin 0 → β) : ∏ i, f i = 1 := rfl
 
 /-- A product of a function `f : fin (n + 1) → β` over all `fin (n + 1)`

test/matrix.lean

@@ -62,9 +62,10 @@ example {α : Type*} [comm_ring α] {a b c d : α} :
 begin
   simp [matrix.det_succ_row_zero, fin.sum_univ_succ],
   /-
-  Try this: simp only [matrix.det_succ_row_zero, fin.sum_univ_succ, det_fin_zero,
-      finset.sum_singleton, fin.sum_univ_zero, minor_apply, cons_val_zero, cons_val_succ,
-      fin.succ_above_zero, fin.coe_succ, fin.coe_zero],
+  Try this: simp only [det_succ_row_zero, fin.sum_univ_succ, neg_mul_eq_neg_mul_symm, mul_one,
+  fin.default_eq_zero, fin.coe_zero, one_mul, cons_val_one, fin.coe_succ, univ_unique, minor_apply,
+  pow_one, fin.zero_succ_above, fin.succ_succ_above_zero,  finset.sum_singleton, cons_val_zero,
+  cons_val_succ, det_fin_zero, pow_zero]
   -/
   ring
 end
@@ -75,10 +76,11 @@ example {α : Type*} [comm_ring α] (A : matrix (fin 3) (fin 3) α) {a b c d e f
 begin
   simp [matrix.det_succ_row_zero, fin.sum_univ_succ],
   /-
-  Try this: simp only [matrix.det_succ_row_zero, fin.sum_univ_succ, det_fin_zero,
-      finset.sum_singleton, fin.sum_univ_zero, minor_apply, cons_val_zero, cons_val_succ,
-      fin.succ_above_zero, fin.succ_succ_above_zero, fin.succ_succ_above_succ,
-      fin.coe_zero, fin.coe_succ, pow_zero, pow_add],
+  Try this: simp only [det_succ_row_zero, fin.sum_univ_succ, neg_mul_eq_neg_mul_symm, cons_append,
+  mul_one, fin.default_eq_zero, fin.coe_zero, cons_vec_bit0_eq_alt0, one_mul, cons_val_one,
+  cons_vec_alt0, fin.succ_succ_above_one, fin.coe_succ, univ_unique, minor_apply, pow_one,
+  fin.zero_succ_above, fin.succ_zero_eq_one, fin.succ_succ_above_zero, nat.neg_one_sq,
+  finset.sum_singleton, cons_val_zero, cons_val_succ, det_fin_zero, head_cons, pow_zero]
    -/
   ring
 end