chore(set_theory/cardinal): rename is_empty/nonempty lemmas (#9668)

* add `is_empty_pi`, `is_empty_prod`, `is_empty_pprod`, `is_empty_sum`;
* rename `cardinal.eq_zero_of_is_empty` to `cardinal.mk_eq_zero`, make
  the argument `α : Type u` explicit;
* rename `cardinal.eq_zero_iff_is_empty` to `cardinal.mk_eq_zero_iff`;
* rename `cardinal.ne_zero_iff_nonempty` to `cardinal.mk_ne_zero_iff`;
* add `@[simp]` lemma `cardinal.mk_ne_zero`;
* fix compile errors caused by these changes, golf a few proofs.

src/data/W/cardinal.lean

@@ -55,7 +55,7 @@ lemma cardinal_mk_le_max_omega_of_fintype [Π a, fintype (β a)] : #(W_type β)
 (is_empty_or_nonempty α).elim
   (begin
     introI h,
-    rw [@cardinal.eq_zero_of_is_empty (W_type β)],
+    rw [cardinal.mk_eq_zero (W_type β)],
     exact zero_le _
   end) $
 λ hn,

src/logic/is_empty.lean

@@ -98,6 +98,21 @@ end is_empty
 @[simp] lemma not_is_empty_iff : ¬ is_empty α ↔ nonempty α :=
 not_iff_comm.mp not_nonempty_iff
 
+@[simp] lemma is_empty_pi {π : α → Sort*} : is_empty (Π a, π a) ↔ ∃ a, is_empty (π a) :=
+by simp only [← not_nonempty_iff, classical.nonempty_pi, not_forall]
+
+@[simp] lemma is_empty_prod {α β : Type*} : is_empty (α × β) ↔ is_empty α ∨ is_empty β :=
+by simp only [← not_nonempty_iff, nonempty_prod, not_and_distrib]
+
+@[simp] lemma is_empty_pprod : is_empty (pprod α β) ↔ is_empty α ∨ is_empty β :=
+by simp only [← not_nonempty_iff, nonempty_pprod, not_and_distrib]
+
+@[simp] lemma is_empty_sum {α β} : is_empty (α ⊕ β) ↔ is_empty α ∧ is_empty β :=
+by simp only [← not_nonempty_iff, nonempty_sum, not_or_distrib]
+
+@[simp] lemma is_empty_psum {α β} : is_empty (psum α β) ↔ is_empty α ∧ is_empty β :=
+by simp only [← not_nonempty_iff, nonempty_psum, not_or_distrib]
+
 variables (α)
 
 lemma is_empty_or_nonempty : is_empty α ∨ nonempty α :=

src/set_theory/cardinal.lean

@@ -94,6 +94,9 @@ localized "notation `#` := cardinal.mk" in cardinal
 instance can_lift_cardinal_Type : can_lift cardinal.{u} (Type u) :=
 ⟨mk, λ c, true, λ c _, quot.induction_on c $ λ α, ⟨α, rfl⟩⟩
 
+protected lemma induction_on {p : cardinal → Prop} (c : cardinal) (h : ∀ α, p (#α)) : p c :=
+quotient.induction_on c h
+
 protected lemma eq : #α = #β ↔ nonempty (α ≃ β) := quotient.eq
 
 @[simp] theorem mk_def (α : Type u) : @eq cardinal ⟦α⟧ (#α) := rfl
@@ -204,25 +207,23 @@ instance : has_zero cardinal.{u} := ⟨#pempty⟩
 
 instance : inhabited cardinal.{u} := ⟨0⟩
 
+@[simp] lemma mk_eq_zero (α : Type u) [is_empty α] : #α = 0 :=
+(equiv.equiv_pempty α).cardinal_eq
+
 @[simp] theorem lift_zero : lift 0 = 0 :=
 quotient.sound ⟨equiv.equiv_pempty _⟩
 
-@[simp]
-lemma eq_zero_of_is_empty {α : Type u} [is_empty α] : #α = 0 :=
-(equiv.equiv_pempty α).cardinal_eq
+lemma mk_eq_zero_iff {α : Type u} : #α = 0 ↔ is_empty α :=
+⟨λ e, let ⟨h⟩ := quotient.exact e in h.is_empty, @mk_eq_zero α⟩
 
-lemma eq_zero_iff_is_empty {α : Type u} : #α = 0 ↔ is_empty α :=
-⟨λ e, let ⟨h⟩ := quotient.exact e in
-  equiv.equiv_empty_equiv α $ h.trans equiv.empty_equiv_pempty.symm,
-  @eq_zero_of_is_empty _⟩
+theorem mk_ne_zero_iff {α : Type u} : #α ≠ 0 ↔ nonempty α :=
+(not_iff_not.2 mk_eq_zero_iff).trans not_is_empty_iff
 
-theorem ne_zero_iff_nonempty {α : Type u} : #α ≠ 0 ↔ nonempty α :=
-(not_iff_not.2 eq_zero_iff_is_empty).trans not_is_empty_iff
+@[simp] lemma mk_ne_zero (α : Type u) [nonempty α] : #α ≠ 0 := mk_ne_zero_iff.2 ‹_›
 
 instance : has_one cardinal.{u} := ⟨⟦punit⟧⟩
 
-instance : nontrivial cardinal.{u} :=
-⟨⟨1, 0, ne_zero_iff_nonempty.2 ⟨punit.star⟩⟩⟩
+instance : nontrivial cardinal.{u} := ⟨⟨1, 0, mk_ne_zero _⟩⟩
 
 theorem le_one_iff_subsingleton {α : Type u} : #α ≤ 1 ↔ subsingleton α :=
 ⟨λ ⟨f⟩, ⟨λ a b, f.injective (subsingleton.elim _ _)⟩,
@@ -278,13 +279,10 @@ quotient.induction_on₃ a b c $ assume α β γ, quotient.sound ⟨equiv.prod_s
 protected theorem eq_zero_or_eq_zero_of_mul_eq_zero  {a b : cardinal.{u}} :
   a * b = 0 → a = 0 ∨ b = 0 :=
 begin
-  refine quotient.induction_on b _,
-  refine quotient.induction_on a _,
-  intros a b h,
-  contrapose h,
-  simp_rw [not_or_distrib, ← ne.def] at h,
-  have := @prod.nonempty a b (ne_zero_iff_nonempty.mp h.1) (ne_zero_iff_nonempty.mp h.2),
-  exact ne_zero_iff_nonempty.mpr this
+  induction a using cardinal.induction_on with α,
+  induction b using cardinal.induction_on with β,
+  simp only [mul_def, mk_eq_zero_iff, is_empty_prod],
+  exact id
 end
 
 instance : comm_semiring cardinal.{u} :=
@@ -338,14 +336,12 @@ quotient.induction_on a $ assume α, quotient.sound
 quot.sound ⟨equiv.ulift.trans $ equiv.Prop_equiv_bool.trans equiv.bool_equiv_punit_sum_punit⟩
 
 @[simp] theorem zero_power {a : cardinal} : a ≠ 0 → 0 ^ a = 0 :=
-quotient.induction_on a $ assume α heq,
-(ne_zero_iff_nonempty.1 heq).elim $ assume a,
-by { haveI : nonempty α := ⟨a⟩, exact quotient.sound ⟨equiv.equiv_pempty _⟩ }
+quotient.induction_on a $ assume α heq, mk_eq_zero_iff.2 $ is_empty_pi.2 $
+let ⟨a⟩ := mk_ne_zero_iff.1 heq in ⟨a, pempty.is_empty⟩
 
 theorem power_ne_zero {a : cardinal} (b) : a ≠ 0 → a ^ b ≠ 0 :=
 quotient.induction_on₂ a b $ λ α β h,
-let ⟨a⟩ := ne_zero_iff_nonempty.1 h in
-ne_zero_iff_nonempty.2 ⟨λ _, a⟩
+let ⟨a⟩ := mk_ne_zero_iff.1 h in mk_ne_zero_iff.2 ⟨λ _, a⟩
 
 theorem mul_power {a b c : cardinal} : (a * b) ^ c = a ^ c * b ^ c :=
 quotient.induction_on₃ a b c $ assume α β γ,
@@ -429,7 +425,7 @@ by { by_cases h : c = 0, rw [h, power_zero], rw [zero_power h], apply zero_le }
 
 theorem power_le_power_left : ∀{a b c : cardinal}, a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c :=
 by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ hα ⟨e⟩; exact
-  let ⟨a⟩ := ne_zero_iff_nonempty.1 hα in
+  let ⟨a⟩ := mk_ne_zero_iff.1 hα in
   ⟨@embedding.arrow_congr_right _ _ _ ⟨a⟩ e⟩
 
 theorem power_le_max_power_one {a b c : cardinal} (h : b ≤ c) : a ^ b ≤ max (a ^ c) 1 :=
@@ -580,15 +576,11 @@ theorem prod_le_prod {ι} (f g : ι → cardinal) (H : ∀ i, f i ≤ g i) : pro
 ⟨embedding.Pi_congr_right $ λ i, classical.choice $
   by have := H i; rwa [← mk_out (f i), ← mk_out (g i)] at this⟩
 
-theorem prod_ne_zero {ι} (f : ι → cardinal) : prod f ≠ 0 ↔ ∀ i, f i ≠ 0 :=
-begin
-  suffices : nonempty (Π i, (f i).out) ↔ ∀ i, nonempty (f i).out,
-  { simpa [← ne_zero_iff_nonempty, prod] },
-  exact classical.nonempty_pi
-end
+theorem prod_eq_zero {ι} (f : ι → cardinal.{u}) : prod f = 0 ↔ ∃ i, f i = 0 :=
+by { lift f to ι → Type u using λ _, trivial, simp [mk_eq_zero_iff] }
 
-theorem prod_eq_zero {ι} (f : ι → cardinal) : prod f = 0 ↔ ∃ i, f i = 0 :=
-not_iff_not.1 $ by simpa using prod_ne_zero f
+theorem prod_ne_zero {ι} (f : ι → cardinal) : prod f ≠ 0 ↔ ∀ i, f i ≠ 0 :=
+by simp [prod_eq_zero]
 
 @[simp] theorem lift_prod {ι : Type u} (c : ι → cardinal.{v}) :
   lift.{w} (prod c) = prod (λ i, lift.{w} (c i)) :=
@@ -715,8 +707,7 @@ localized "notation `ω` := cardinal.omega" in cardinal
 
 lemma mk_nat : #ℕ = ω := (lift_id _).symm
 
-theorem omega_ne_zero : ω ≠ 0 :=
-ne_zero_iff_nonempty.2 ⟨⟨0⟩⟩
+theorem omega_ne_zero : ω ≠ 0 := mk_ne_zero _
 
 theorem omega_pos : 0 < ω :=
 pos_iff_ne_zero.2 omega_ne_zero
@@ -907,7 +898,7 @@ calc #α = 1 ↔ #α ≤ 1 ∧ ¬#α < 1 : eq_iff_le_not_lt
 begin
   apply and_congr le_one_iff_subsingleton,
   push_neg,
-  rw [one_le_iff_ne_zero, ne_zero_iff_nonempty]
+  rw [one_le_iff_ne_zero, mk_ne_zero_iff]
 end
 
 theorem infinite_iff {α : Type u} : infinite α ↔ ω ≤ #α :=
@@ -1082,10 +1073,10 @@ end
 /-- **König's theorem** -/
 theorem sum_lt_prod {ι} (f g : ι → cardinal) (H : ∀ i, f i < g i) : sum f < prod g :=
 lt_of_not_ge $ λ ⟨F⟩, begin
-  have : inhabited (Π (i : ι), (g i).out),
-  { refine ⟨λ i, classical.choice $ ne_zero_iff_nonempty.1 _⟩,
+  haveI : inhabited (Π (i : ι), (g i).out),
+  { refine ⟨λ i, classical.choice $ mk_ne_zero_iff.1 _⟩,
     rw mk_out,
-    exact ne_of_gt (lt_of_le_of_lt (zero_le _) (H i)) }, resetI,
+    exact (H i).ne_bot },
   let G := inv_fun F,
   have sG : surjective G := inv_fun_surjective F.2,
   choose C hc using show ∀ i, ∃ b, ∀ a, G ⟨i, a⟩ i ≠ b,

src/set_theory/cofinality.lean

@@ -197,7 +197,7 @@ le_antisymm (by simpa using cof_le_card 0) (cardinal.zero_le _)
 ⟨induction_on o $ λ α r _ z, by exactI
   let ⟨S, hl, e⟩ := cof_eq r in type_eq_zero_iff_is_empty.2 $
   ⟨λ a, let ⟨b, h, _⟩ := hl a in
-    (eq_zero_iff_is_empty.1 (e.trans z)).elim' ⟨_, h⟩⟩,
+    (mk_eq_zero_iff.1 (e.trans z)).elim' ⟨_, h⟩⟩,
 λ e, by simp [e]⟩
 
 @[simp] theorem cof_succ (o) : cof (succ o) = 1 :=
@@ -218,7 +218,7 @@ end
 ⟨induction_on o $ λ α r _ z, begin
   resetI,
   rcases cof_eq r with ⟨S, hl, e⟩, rw z at e,
-  cases ne_zero_iff_nonempty.1 (by rw e; exact one_ne_zero) with a,
+  cases mk_ne_zero_iff.1 (by rw e; exact one_ne_zero) with a,
   refine ⟨typein r a, eq.symm $ quotient.sound
     ⟨rel_iso.of_surjective (rel_embedding.of_monotone _
       (λ x y, _)) (λ x, _)⟩⟩,

src/set_theory/ordinal_arithmetic.lean

@@ -150,19 +150,19 @@ by simp only [le_antisymm_iff, add_le_add_iff_right]
 @[simp] theorem card_eq_zero {o} : card o = 0 ↔ o = 0 :=
 ⟨induction_on o $ λ α r _ h, begin
   refine le_antisymm (le_of_not_lt $
-    λ hn, ne_zero_iff_nonempty.2 _ h) (ordinal.zero_le _),
+    λ hn, mk_ne_zero_iff.2 _ h) (ordinal.zero_le _),
   rw [← succ_le, succ_zero] at hn, cases hn with f,
   exact ⟨f punit.star⟩
 end, λ e, by simp only [e, card_zero]⟩
 
 @[simp] theorem type_eq_zero_of_empty [is_well_order α r] [is_empty α] : type r = 0 :=
-card_eq_zero.symm.mpr eq_zero_of_is_empty
+card_eq_zero.symm.mpr (mk_eq_zero _)
 
 @[simp] theorem type_eq_zero_iff_is_empty [is_well_order α r] : type r = 0 ↔ is_empty α :=
-(@card_eq_zero (type r)).symm.trans eq_zero_iff_is_empty
+(@card_eq_zero (type r)).symm.trans mk_eq_zero_iff
 
 theorem type_ne_zero_iff_nonempty [is_well_order α r] : type r ≠ 0 ↔ nonempty α :=
-(not_congr (@card_eq_zero (type r))).symm.trans ne_zero_iff_nonempty
+(not_congr (@card_eq_zero (type r))).symm.trans mk_ne_zero_iff
 
 protected lemma one_ne_zero : (1 : ordinal) ≠ 0 :=
 type_ne_zero_iff_nonempty.2 ⟨punit.star⟩