feat: some simp lemmas to compute more cardinals (#7660)

leanprover-community · Oct 15, 2023 · a577026 · a577026
1 parent 84f5ad0
commit a577026
Show file tree

Hide file tree

Showing 3 changed files with 47 additions and 4 deletions.
diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean
@@ -1656,6 +1656,16 @@ theorem nat_mul_aleph0 {n : ℕ} (hn : n ≠ 0) : ↑n * ℵ₀ = ℵ₀ :=
 theorem aleph0_mul_nat {n : ℕ} (hn : n ≠ 0) : ℵ₀ * n = ℵ₀ := by rw [mul_comm, nat_mul_aleph0 hn]
 #align cardinal.aleph_0_mul_nat Cardinal.aleph0_mul_nat
 
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem ofNat_mul_aleph0 {n : ℕ} [Nat.AtLeastTwo n] : no_index (OfNat.ofNat n) * ℵ₀ = ℵ₀ :=
+  nat_mul_aleph0 (OfNat.ofNat_ne_zero n)
+
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem aleph0_mul_ofNat {n : ℕ} [Nat.AtLeastTwo n] : ℵ₀ * no_index (OfNat.ofNat n) = ℵ₀ :=
+  aleph0_mul_nat (OfNat.ofNat_ne_zero n)
+
 @[simp]
 theorem add_le_aleph0 {c₁ c₂ : Cardinal} : c₁ + c₂ ≤ ℵ₀ ↔ c₁ ≤ ℵ₀ ∧ c₂ ≤ ℵ₀ :=
   ⟨fun h => ⟨le_self_add.trans h, le_add_self.trans h⟩, fun h =>
@@ -1671,6 +1681,16 @@ theorem aleph0_add_nat (n : ℕ) : ℵ₀ + n = ℵ₀ :=
 theorem nat_add_aleph0 (n : ℕ) : ↑n + ℵ₀ = ℵ₀ := by rw [add_comm, aleph0_add_nat]
 #align cardinal.nat_add_aleph_0 Cardinal.nat_add_aleph0
 
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem ofNat_add_aleph0 {n : ℕ} [Nat.AtLeastTwo n] : no_index (OfNat.ofNat n) + ℵ₀ = ℵ₀ :=
+  nat_add_aleph0 n
+
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem aleph0_add_ofNat {n : ℕ} [Nat.AtLeastTwo n] : ℵ₀ + no_index (OfNat.ofNat n) = ℵ₀ :=
+  aleph0_add_nat n
+
 /-- This function sends finite cardinals to the corresponding natural, and infinite cardinals
   to 0. -/
 def toNat : ZeroHom Cardinal ℕ where

diff --git a/Mathlib/SetTheory/Cardinal/Continuum.lean b/Mathlib/SetTheory/Cardinal/Continuum.lean
@@ -27,7 +27,7 @@ open Cardinal
 
 /-- Cardinality of continuum. -/
 def continuum : Cardinal.{u} :=
-  2 ^ aleph0.{u}
+  2 ^ ℵ₀
 #align cardinal.continuum Cardinal.continuum
 
 -- mathport name: Cardinal.continuum
@@ -131,19 +131,29 @@ theorem continuum_add_aleph0 : 𝔠 + ℵ₀ = 𝔠 :=
 
 @[simp]
 theorem continuum_add_self : 𝔠 + 𝔠 = 𝔠 :=
-  add_eq_right aleph0_le_continuum le_rfl
+  add_eq_self aleph0_le_continuum
 #align cardinal.continuum_add_self Cardinal.continuum_add_self
 
 @[simp]
 theorem nat_add_continuum (n : ℕ) : ↑n + 𝔠 = 𝔠 :=
-  add_eq_right aleph0_le_continuum (nat_lt_continuum n).le
+  nat_add_eq n aleph0_le_continuum
 #align cardinal.nat_add_continuum Cardinal.nat_add_continuum
 
 @[simp]
 theorem continuum_add_nat (n : ℕ) : 𝔠 + n = 𝔠 :=
   (add_comm _ _).trans (nat_add_continuum n)
 #align cardinal.continuum_add_nat Cardinal.continuum_add_nat
 
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem ofNat_add_continuum {n : ℕ} [Nat.AtLeastTwo n] : no_index (OfNat.ofNat n) + 𝔠 = 𝔠 :=
+  nat_add_continuum n
+
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem continuum_add_ofNat {n : ℕ} [Nat.AtLeastTwo n] : 𝔠 + no_index (OfNat.ofNat n) = 𝔠 :=
+  continuum_add_nat n
+
 /-!
 ### Multiplication
 -/
@@ -174,6 +184,16 @@ theorem continuum_mul_nat {n : ℕ} (hn : n ≠ 0) : 𝔠 * n = 𝔠 :=
   (mul_comm _ _).trans (nat_mul_continuum hn)
 #align cardinal.continuum_mul_nat Cardinal.continuum_mul_nat
 
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem ofNat_mul_continuum {n : ℕ} [Nat.AtLeastTwo n] : no_index (OfNat.ofNat n) * 𝔠 = 𝔠 :=
+  nat_mul_continuum (OfNat.ofNat_ne_zero n)
+
+-- See note [no_index around OfNat.ofNat]
+@[simp]
+theorem continuum_mul_ofNat {n : ℕ} [Nat.AtLeastTwo n] : 𝔠 * no_index (OfNat.ofNat n) = 𝔠 :=
+  continuum_mul_nat (OfNat.ofNat_ne_zero n)
+
 /-!
 ### Power
 -/

diff --git a/Mathlib/SetTheory/Cardinal/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Ordinal.lean
@@ -810,8 +810,11 @@ theorem add_nat_eq {a : Cardinal} (n : ℕ) (ha : ℵ₀ ≤ a) : a + n = a :=
   add_eq_left ha ((nat_lt_aleph0 _).le.trans ha)
 #align cardinal.add_nat_eq Cardinal.add_nat_eq
 
+theorem nat_add_eq {a : Cardinal} (n : ℕ) (ha : ℵ₀ ≤ a) : n + a = a := by
+  rw [add_comm, add_nat_eq n ha]
+
 theorem add_one_eq {a : Cardinal} (ha : ℵ₀ ≤ a) : a + 1 = a :=
-  add_eq_left ha (one_le_aleph0.trans ha)
+  add_one_of_aleph0_le ha
 #align cardinal.add_one_eq Cardinal.add_one_eq
 
 --Porting note: removed `simp`, `simp` can prove it