feat(set_theory/ordinal/basic): tweak theorems on order type of empty…

… relation (#14650)

We move the theorems on the order type of an empty relation much earlier, and golf them. We also remove other redundant theorems.

`zero_eq_type_empty` is made redundant by `type_eq_zero_of_empty`, while `zero_eq_lift_type_empty`  is made redundant by the former lemma and `lift_zero`.

src/order/rel_iso.lean

@@ -486,6 +486,10 @@ lemma mul_apply (e₁ e₂ : r ≃r r) (x : α) : (e₁ * e₂) x = e₁ (e₂ x
 
 @[simp] lemma apply_inv_self (e : r ≃r r) (x) : e (e⁻¹ x) = x := e.apply_symm_apply x
 
+/-- Two relations on empty types are isomorphic. -/
+def rel_iso_of_is_empty (r : α → α → Prop) (s : β → β → Prop) [is_empty α] [is_empty β] : r ≃r s :=
+⟨equiv.equiv_of_is_empty α β, is_empty_elim⟩
+
 end rel_iso
 
 /-- `subrel r p` is the inherited relation on a subset. -/

src/set_theory/ordinal/arithmetic.lean

@@ -153,17 +153,8 @@ by simp only [le_antisymm_iff, add_le_add_iff_right]
   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 (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 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 mk_ne_zero_iff
-
 protected lemma one_ne_zero : (1 : ordinal) ≠ 0 :=
-type_ne_zero_iff_nonempty.2 ⟨punit.star⟩
+type_ne_zero_of_nonempty _
 
 instance : nontrivial ordinal.{u} :=
 ⟨⟨1, 0, ordinal.one_ne_zero⟩⟩

src/set_theory/ordinal/basic.lean

@@ -746,8 +746,17 @@ instance : has_zero ordinal :=
 
 instance : inhabited ordinal := ⟨0⟩
 
-theorem zero_eq_type_empty : 0 = @type empty empty_relation _ :=
-quotient.sound ⟨⟨equiv_of_is_empty  _ _, λ _ _, iff.rfl⟩⟩
+@[simp] theorem type_eq_zero_of_empty (r) [is_well_order α r] [is_empty α] : type r = 0 :=
+(rel_iso.rel_iso_of_is_empty r _).ordinal_type_eq
+
+@[simp] theorem type_eq_zero_iff_is_empty [is_well_order α r] : type r = 0 ↔ is_empty α :=
+⟨λ h, let ⟨s⟩ := type_eq.1 h in s.to_equiv.is_empty, @type_eq_zero_of_empty α r _⟩
+
+theorem type_ne_zero_iff_nonempty [is_well_order α r] : type r ≠ 0 ↔ nonempty α :=
+by simp
+
+theorem type_ne_zero_of_nonempty (r) [is_well_order α r] [h : nonempty α] : type r ≠ 0 :=
+type_ne_zero_iff_nonempty.2 h
 
 @[simp] theorem card_zero : card 0 = 0 := rfl
 
@@ -863,9 +872,6 @@ by simp only [lt_iff_le_not_le, lift_le]
 quotient.sound ⟨(rel_iso.preimage equiv.ulift _).trans
  ⟨equiv_of_is_empty  _ _, λ a b, iff.rfl⟩⟩
 
-theorem zero_eq_lift_type_empty : 0 = lift.{u} (@type empty empty_relation _) :=
-by rw [← zero_eq_type_empty, lift_zero]
-
 @[simp] theorem lift_one : lift 1 = 1 :=
 quotient.sound ⟨(rel_iso.preimage equiv.ulift _).trans
  ⟨punit_equiv_punit, λ a b, iff.rfl⟩⟩