feat(logic/is_empty): add some simp lemmas and unique instances (#7832)

There are a handful of lemmas about `(h : ¬nonempty a)` that if restated in terms of `[is_empty a]` become suitable for `simp` or as `instance`s. This adjusts some of those lemmas.

Author: eric-wieser

src/data/finset/basic.lean

@@ -366,6 +366,10 @@ classical.by_cases or.inl (λ h, or.inr (nonempty_of_ne_empty h))
   (s : set α) = ∅ ↔ s = ∅ :=
 by rw [← coe_empty, coe_inj]
 
+/-- A `finset` for an empty type is empty. -/
+lemma eq_empty_of_is_empty [is_empty α] (s : finset α) : s = ∅ :=
+finset.eq_empty_of_forall_not_mem is_empty_elim
+
 /-- A `finset` for an empty type is empty. -/
 lemma eq_empty_of_not_nonempty (h : ¬ nonempty α) (s : finset α) : s = ∅ :=
 finset.eq_empty_of_forall_not_mem $ λ x, false.elim $ not_nonempty_iff_imp_false.1 h x

src/data/matrix/basic.lean

@@ -114,11 +114,13 @@ lemma map_smul [has_scalar R α] [has_scalar R β] (f : α →[R] β) (r : R)
   (M : matrix m n α) : (r • M).map f = r • (M.map f) :=
 by { ext, simp, }
 
-lemma subsingleton_of_empty_left (hm : ¬ nonempty m) : subsingleton (matrix m n α) :=
-⟨λ M N, by { ext, contrapose! hm, use i }⟩
+-- TODO[gh-6025]: make this an instance once safe to do so
+lemma subsingleton_of_empty_left [is_empty m] : subsingleton (matrix m n α) :=
+⟨λ M N, by { ext, exact is_empty_elim i }⟩
 
-lemma subsingleton_of_empty_right (hn : ¬ nonempty n) : subsingleton (matrix m n α) :=
-⟨λ M N, by { ext, contrapose! hn, use j }⟩
+-- TODO[gh-6025]: make this an instance once safe to do so
+lemma subsingleton_of_empty_right [is_empty n] : subsingleton (matrix m n α) :=
+⟨λ M N, by { ext, exact is_empty_elim j }⟩
 
 end matrix
 

src/data/matrix/dmatrix.lean

@@ -104,11 +104,13 @@ lemma map_sub [∀ i j, add_group (α i j)] {β : m → n → Type w} [∀ i j,
   (M - N).map (λ i j, @f i j) = M.map (λ i j, @f i j) - N.map (λ i j, @f i j) :=
 by { ext, simp }
 
-lemma subsingleton_of_empty_left (hm : ¬ nonempty m) : subsingleton (dmatrix m n α) :=
-⟨λ M N, by { ext, contrapose! hm, use i }⟩
+-- TODO[gh-6025]: make this an instance once safe to do so
+lemma subsingleton_of_empty_left [is_empty m] : subsingleton (dmatrix m n α) :=
+⟨λ M N, by { ext, exact is_empty_elim i }⟩
 
-lemma subsingleton_of_empty_right (hn : ¬ nonempty n) : subsingleton (dmatrix m n α) :=
-⟨λ M N, by { ext, contrapose! hn, use j }⟩
+-- TODO[gh-6025]: make this an instance once safe to do so
+lemma subsingleton_of_empty_right [is_empty n] : subsingleton (dmatrix m n α) :=
+⟨λ M N, by { ext, exact is_empty_elim j }⟩
 
 end dmatrix
 

src/data/set/basic.lean

@@ -375,6 +375,14 @@ theorem eq_empty_of_subset_empty {s : set α} : s ⊆ ∅ → s = ∅ := subset_
 theorem eq_empty_of_not_nonempty (h : ¬nonempty α) (s : set α) : s = ∅ :=
 eq_empty_of_subset_empty $ λ x hx, h ⟨x⟩
 
+theorem eq_empty_of_is_empty [is_empty α] (s : set α) : s = ∅ :=
+eq_empty_of_subset_empty $ λ x hx, is_empty_elim x
+
+/-- There is exactly one set of a type that is empty. -/
+-- TODO[gh-6025]: make this an instance once safe to do so
+def unique_empty [is_empty α] : unique (set α) :=
+{ default := ∅, uniq := eq_empty_of_is_empty }
+
 lemma not_nonempty_iff_eq_empty {s : set α} : ¬s.nonempty ↔ s = ∅ :=
 by simp only [set.nonempty, eq_empty_iff_forall_not_mem, not_exists]
 

src/linear_algebra/char_poly/coeff.lean

@@ -182,9 +182,8 @@ end
 @[simp] lemma finite_field.char_poly_pow_card {K : Type*} [field K] [fintype K] (M : matrix n n K) :
   char_poly (M ^ (fintype.card K)) = char_poly M :=
 begin
-  by_cases hn : nonempty n,
-  { haveI := hn,
-    cases char_p.exists K with p hp, letI := hp,
+  casesI (is_empty_or_nonempty n).symm,
+  { cases char_p.exists K with p hp, letI := hp,
     rcases finite_field.card K p with ⟨⟨k, kpos⟩, ⟨hp, hk⟩⟩,
     haveI : fact p.prime := ⟨hp⟩,
     dsimp at hk, rw hk at *,
@@ -193,12 +192,13 @@ begin
     rw ← finite_field.expand_card,
     unfold char_poly, rw [alg_hom.map_det, ← is_monoid_hom.map_pow],
     apply congr_arg det,
-    apply mat_poly_equiv.injective, swap, { apply_instance },
-    rw [← mat_poly_equiv.coe_alg_hom, alg_hom.map_pow, mat_poly_equiv.coe_alg_hom,
-          mat_poly_equiv_char_matrix, hk, sub_pow_char_pow_of_commute, ← C_pow],
+    refine mat_poly_equiv.injective _,
+    rw [alg_equiv.map_pow, mat_poly_equiv_char_matrix, hk, sub_pow_char_pow_of_commute, ← C_pow],
     { exact (id (mat_poly_equiv_eq_X_pow_sub_C (p ^ k) M) : _) },
     { exact (C M).commute_X } },
-  { apply congr_arg, apply @subsingleton.elim _ (subsingleton_of_empty_left hn) _ _, },
+  { -- TODO[gh-6025]: remove this `haveI` once `subsingleton_of_empty_right` is a global instance
+    haveI : subsingleton (matrix n n K) := matrix.subsingleton_of_empty_right,
+    exact congr_arg _ (subsingleton.elim _ _), },
 end
 
 @[simp] lemma zmod.char_poly_pow_card (M : matrix n n (zmod p)) :

src/logic/embedding.lean

@@ -98,6 +98,10 @@ protected noncomputable def equiv_of_surjective {α β} (f : α ↪ β) (hf : su
   α ≃ β :=
 equiv.of_bijective f ⟨f.injective, hf⟩
 
+/-- There is always an embedding from an empty type. --/
+protected def of_is_empty {α β} [is_empty α] : α ↪ β :=
+⟨is_empty_elim, is_empty_elim⟩
+
 protected def of_not_nonempty {α β} (hα : ¬ nonempty α) : α ↪ β :=
 ⟨λa, (hα ⟨a⟩).elim, assume a, (hα ⟨a⟩).elim⟩
 

src/logic/is_empty.lean

@@ -44,6 +44,15 @@ instance [is_empty α] [is_empty β] : is_empty (psum α β) :=
 ⟨λ x, psum.rec is_empty.false is_empty.false x⟩
 instance {α β} [is_empty α] [is_empty β] : is_empty (α ⊕ β) :=
 ⟨λ x, sum.rec is_empty.false is_empty.false x⟩
+/-- subtypes of an empty type are empty -/
+instance [is_empty α] (p : α → Prop) : is_empty (subtype p) :=
+⟨λ x, is_empty.false x.1⟩
+/-- subtypes by an all-false predicate are false. -/
+lemma subtype.is_empty_of_false {p : α → Prop} (hp : ∀ a, ¬(p a)) : is_empty (subtype p) :=
+⟨λ x, hp _ x.2⟩
+/-- subtypes by false are false. -/
+instance subtype.is_empty_false : is_empty {a : α // false} :=
+subtype.is_empty_of_false (λ a, id)
 
 /- Test that `pi.is_empty` finds this instance. -/
 example [h : nonempty α] [is_empty β] : is_empty (α → β) := by apply_instance

src/order/filter/basic.lean

@@ -533,16 +533,25 @@ nonempty_of_exists $ nonempty_of_mem_sets (univ_mem_sets : univ ∈ f)
 lemma compl_not_mem_sets {f : filter α} {s : set α} [ne_bot f] (h : s ∈ f) : sᶜ ∉ f :=
 λ hsc, (nonempty_of_mem_sets (inter_mem_sets h hsc)).ne_empty $ inter_compl_self s
 
+lemma filter_eq_bot_of_is_empty [is_empty α] (f : filter α) : f = ⊥ :=
+empty_in_sets_eq_bot.mp $ univ_mem_sets' is_empty_elim
+
 lemma filter_eq_bot_of_not_nonempty (f : filter α) (ne : ¬ nonempty α) : f = ⊥ :=
 empty_in_sets_eq_bot.mp $ univ_mem_sets' $ assume x, false.elim (ne ⟨x⟩)
 
+/-- There is exactly one filter on an empty type. --/
+-- TODO[gh-6025]: make this globally an instance once safe to do so
+local attribute [instance]
+protected def unique [is_empty α] : unique (filter α) :=
+{ default := ⊥, uniq := filter_eq_bot_of_is_empty }
+
 lemma forall_sets_nonempty_iff_ne_bot {f : filter α} :
   (∀ (s : set α), s ∈ f → s.nonempty) ↔ ne_bot f :=
 ⟨λ h, ⟨λ hf, empty_not_nonempty (h ∅ $ hf.symm ▸ mem_bot_sets)⟩, @nonempty_of_mem_sets _ _⟩
 
 lemma nontrivial_iff_nonempty : nontrivial (filter α) ↔ nonempty α :=
 ⟨λ ⟨⟨f, g, hfg⟩⟩, by_contra $
-  λ h, hfg $ (filter_eq_bot_of_not_nonempty f h).trans (filter_eq_bot_of_not_nonempty g h).symm,
+  λ h, hfg $ by haveI : is_empty α := not_nonempty_iff.1 h; exact subsingleton.elim _ _,
   λ ⟨x⟩, ⟨⟨⊤, ⊥, ne_bot.ne $ forall_sets_nonempty_iff_ne_bot.1 $ λ s hs,
     by rwa [mem_top_sets.1 hs, ← nonempty_iff_univ_nonempty]⟩⟩⟩
 

src/set_theory/cardinal.lean

@@ -140,10 +140,14 @@ instance : has_zero cardinal.{u} := ⟨⟦pempty⟧⟩
 
 instance : inhabited cardinal.{u} := ⟨0⟩
 
+@[simp]
+lemma eq_zero_of_is_empty {α : Type u} [is_empty α] : mk α = 0 :=
+quotient.sound ⟨equiv.equiv_pempty α⟩
+
 lemma eq_zero_iff_is_empty {α : Type u} : mk α = 0 ↔ is_empty α :=
 ⟨λ e, let ⟨h⟩ := quotient.exact e in
   equiv.equiv_empty_equiv α $ h.trans equiv.empty_equiv_pempty.symm,
-  λ h, by exactI quotient.sound ⟨equiv.equiv_pempty α⟩⟩
+  @eq_zero_of_is_empty _⟩
 
 theorem ne_zero_iff_nonempty {α : Type u} : mk α ≠ 0 ↔ nonempty α :=
 (not_iff_not.2 eq_zero_iff_is_empty).trans not_is_empty_iff
@@ -280,7 +284,7 @@ section order_properties
 open sum
 
 protected theorem zero_le : ∀(a : cardinal), 0 ≤ a :=
-by rintro ⟨α⟩; exact ⟨embedding.of_not_nonempty $ λ ⟨a⟩, a.elim⟩
+by rintro ⟨α⟩; exact ⟨embedding.of_is_empty⟩
 
 protected theorem add_le_add : ∀{a b c d : cardinal}, a ≤ b → c ≤ d → a + c ≤ b + d :=
 by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨δ⟩ ⟨e₁⟩ ⟨e₂⟩; exact ⟨e₁.sum_map e₂⟩

src/set_theory/ordinal.lean

@@ -736,9 +736,7 @@ quotient.sound ⟨⟨empty_equiv_pempty.symm, λ _ _, iff.rfl⟩⟩
 @[simp] theorem card_zero : card 0 = 0 := rfl
 
 protected theorem zero_le (o : ordinal) : 0 ≤ o :=
-induction_on o $ λ α r _,
-⟨⟨⟨embedding.of_not_nonempty $ λ ⟨a⟩, a.elim,
-  λ a, a.elim⟩, λ a, a.elim⟩⟩
+induction_on o $ λ α r _, ⟨⟨⟨embedding.of_is_empty, is_empty_elim⟩, is_empty_elim⟩⟩
 
 @[simp] protected theorem le_zero {o : ordinal} : o ≤ 0 ↔ o = 0 :=
 by simp only [le_antisymm_iff, ordinal.zero_le, and_true]