feat(ENat): add several lemmas (#10508)

Add lemmas needed for #10472
leanprover-community · Feb 14, 2024 · 5cc14ef · 5cc14ef
1 parent e862bf8
commit 5cc14ef
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 2 deletions.
diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean
@@ -114,6 +114,8 @@ theorem toNat_top : toNat ⊤ = 0 :=
   rfl
 #align enat.to_nat_top ENat.toNat_top
 
+@[simp] theorem toNat_eq_zero : toNat n = 0 ↔ n = 0 ∨ n = ⊤ := WithTop.untop'_eq_self_iff
+
 --Porting note: new definition copied from `WithTop`
 /-- Recursor for `ENat` using the preferred forms `⊤` and `↑a`. -/
 @[elab_as_elim]

diff --git a/Mathlib/SetTheory/Cardinal/ENat.lean b/Mathlib/SetTheory/Cardinal/ENat.lean
@@ -170,10 +170,13 @@ lemma toENatAux_gc : GaloisConnection (↑) toENatAux := fun n x ↦ by
   | inl hx => lift x to ℕ using hx; simp
   | inr hx => simp [toENatAux_eq_top hx, (ofENat_le_aleph0 n).trans hx]
 
-lemma toENatAux_eq_nat {x : Cardinal} {n : ℕ} : toENatAux x = n ↔ x = n := by
+theorem toENatAux_le_nat {x : Cardinal} {n : ℕ} : toENatAux x ≤ n ↔ x ≤ n := by
   cases lt_or_le x ℵ₀ with
   | inl hx => lift x to ℕ using hx; simp
-  | inr hx => simpa [toENatAux_eq_top hx] using ((nat_lt_aleph0 n).trans_le hx).ne'
+  | inr hx => simp [toENatAux_eq_top hx, (nat_lt_aleph0 n).trans_le hx]
+
+lemma toENatAux_eq_nat {x : Cardinal} {n : ℕ} : toENatAux x = n ↔ x = n := by
+  simp only [le_antisymm_iff, toENatAux_le_nat, ← toENatAux_gc _, ofENat_nat]
 
 lemma toENatAux_eq_zero {x : Cardinal} : toENatAux x = 0 ↔ x = 0 := toENatAux_eq_nat
 
@@ -237,15 +240,26 @@ lemma ofENat_toENat_eq_self {a : Cardinal} : toENat a = a ↔ a ≤ ℵ₀ := by
 
 lemma toENat_nat (n : ℕ) : toENat n = n := map_natCast _ n
 
+@[simp] lemma toENat_le_nat {a : Cardinal} {n : ℕ} : toENat a ≤ n ↔ a ≤ n := toENatAux_le_nat
 @[simp] lemma toENat_eq_nat {a : Cardinal} {n : ℕ} : toENat a = n ↔ a = n := toENatAux_eq_nat
 @[simp] lemma toENat_eq_zero {a : Cardinal} : toENat a = 0 ↔ a = 0 := toENatAux_eq_zero
+@[simp] lemma toENat_le_one {a : Cardinal} : toENat a ≤ 1 ↔ a ≤ 1 := toENat_le_nat
 @[simp] lemma toENat_eq_one {a : Cardinal} : toENat a = 1 ↔ a = 1 := toENat_eq_nat
 
+@[simp] lemma toENat_le_ofNat {a : Cardinal} {n : ℕ} [n.AtLeastTwo] :
+    toENat a ≤ no_index (OfNat.ofNat n) ↔ a ≤ OfNat.ofNat n := toENat_le_nat
+
 @[simp] lemma toENat_eq_ofNat {a : Cardinal} {n : ℕ} [n.AtLeastTwo] :
     toENat a = no_index (OfNat.ofNat n) ↔ a = OfNat.ofNat n := toENat_eq_nat
 
 @[simp] lemma toENat_eq_top {a : Cardinal} : toENat a = ⊤ ↔ ℵ₀ ≤ a := enat_gc.u_eq_top
 
+@[simp]
+theorem toENat_lift {a : Cardinal.{v}} : toENat (lift.{u} a) = toENat a := by
+  cases le_total a ℵ₀ with
+  | inl ha => lift a to ℕ∞ using ha; simp
+  | inr ha => simp [toENat_eq_top.2, ha]
+
 @[simp, norm_cast]
 lemma ofENat_add (m n : ℕ∞) : ofENat (m + n) = m + n := by apply toENat_injOn <;> simp