chore(SetTheory/Cardinal): remove explicit argument to nat_lt_aleph0 (leanprover-community#33990)

It is almost never used. Also rename to `natCast_lt_aleph0` and add `natCast_le_aleph0`.

Author: YaelDillies

Mathlib/Algebra/Lie/CartanExists.lean

@@ -377,7 +377,7 @@ lemma exists_isCartanSubalgebra_engel_of_finrank_le_card (h : finrank K L ≤ #K
 lemma exists_isCartanSubalgebra_engel [Infinite K] :
     ∃ x : L, IsCartanSubalgebra (engel K x) := by
   apply exists_isCartanSubalgebra_engel_of_finrank_le_card
-  exact (Cardinal.nat_lt_aleph0 _).le.trans <| Cardinal.infinite_iff.mp ‹Infinite K›
+  exact natCast_le_aleph0.trans <| Cardinal.infinite_iff.mp ‹Infinite K›
 
 end Field
 

Mathlib/Algebra/Module/LinearMap/Polynomial.lean

@@ -556,7 +556,7 @@ lemma exists_isNilRegular_of_finrank_le_card (h : finrank R M ≤ #R) :
 
 lemma exists_isNilRegular [Infinite R] : ∃ x : L, IsNilRegular φ x := by
   apply exists_isNilRegular_of_finrank_le_card
-  exact (Cardinal.nat_lt_aleph0 _).le.trans <| Cardinal.infinite_iff.mp ‹Infinite R›
+  exact Cardinal.natCast_le_aleph0.trans <| Cardinal.infinite_iff.mp ‹Infinite R›
 
 end IsDomain
 

Mathlib/FieldTheory/CardinalEmb.lean

@@ -219,7 +219,7 @@ instance (i : ι) : Algebra.IsSeparable (E⟮<i⟯) (E⟮<i⟯⟮b (φ i)⟯) :=
 
 open Field in
 theorem two_le_deg (i : ι) : 2 ≤ #(X i) := by
-  rw [← Nat.cast_ofNat, ← toNat_le_iff_le_of_lt_aleph0 (nat_lt_aleph0 _) (deg_lt_aleph0 i),
+  rw [← Nat.cast_ofNat, ← toNat_le_iff_le_of_lt_aleph0 natCast_lt_aleph0 (deg_lt_aleph0 i),
     toNat_natCast, ← Nat.card, ← finSepDegree, finSepDegree_eq_finrank_of_isSeparable,
     Nat.succ_le_iff]
   by_contra!
@@ -327,7 +327,7 @@ theorem cardinal_eq_two_pow_rank [Algebra.IsSeparable F E]
   haveI := Fact.mk rank_inf
   rw [Emb.Cardinal.embEquivPi.cardinal_eq, mk_pi]
   apply le_antisymm
-  · rw [← power_eq_two_power rank_inf (nat_lt_aleph0 2).le rank_inf]
+  · rw [← power_eq_two_power rank_inf natCast_le_aleph0 rank_inf]
     conv_rhs => rw [← mk_ord_toType (Module.rank F E), ← prod_const']
     exact prod_le_prod _ _ fun i ↦ (Emb.Cardinal.deg_lt_aleph0 _).le
   · conv_lhs => rw [← mk_ord_toType (Module.rank F E), ← prod_const']

Mathlib/FieldTheory/Cardinality.lean

@@ -66,5 +66,5 @@ theorem Field.nonempty_iff {α : Type u} : Nonempty (Field α) ↔ IsPrimePow #
   rw [Cardinal.isPrimePow_iff]
   obtain h | h := fintypeOrInfinite α
   · simpa only [Cardinal.mk_fintype, Nat.cast_inj, exists_eq_left',
-      (Cardinal.nat_lt_aleph0 _).not_ge, false_or] using Fintype.nonempty_field_iff
+      Cardinal.natCast_lt_aleph0.not_ge, false_or] using Fintype.nonempty_field_iff
   · simpa only [← Cardinal.infinite_iff, h, true_or, iff_true] using Infinite.nonempty_field

Mathlib/FieldTheory/Finite/Polynomial.lean

@@ -199,11 +199,8 @@ theorem rank_R [Fintype σ] : Module.rank K (R σ K) = Fintype.card (σ → K) :
 
 instance [Finite σ] : FiniteDimensional K (R σ K) := by
   cases nonempty_fintype σ
-  classical
-  exact
-    IsNoetherian.iff_fg.1
-      (IsNoetherian.iff_rank_lt_aleph0.mpr <| by
-        simpa only [rank_R] using Cardinal.nat_lt_aleph0 (Fintype.card (σ → K)))
+  rw [FiniteDimensional, ← IsNoetherian.iff_fg, IsNoetherian.iff_rank_lt_aleph0]
+  simpa only [rank_R] using Cardinal.natCast_lt_aleph0
 
 open Classical in
 theorem finrank_R [Fintype σ] : Module.finrank K (R σ K) = Fintype.card (σ → K) :=

Mathlib/FieldTheory/Fixed.lean

@@ -276,7 +276,7 @@ instance isSeparable : Algebra.IsSeparable (FixedPoints.subfield G F) F := by
 instance : FiniteDimensional (subfield G F) F := by
   cases nonempty_fintype G
   exact IsNoetherian.iff_fg.1
-      (IsNoetherian.iff_rank_lt_aleph0.2 <| (rank_le_card G F).trans_lt <| Cardinal.nat_lt_aleph0 _)
+    (IsNoetherian.iff_rank_lt_aleph0.2 <| (rank_le_card G F).trans_lt Cardinal.natCast_lt_aleph0)
 
 end Finite
 

Mathlib/FieldTheory/SeparableClosure.lean

@@ -389,7 +389,7 @@ lemma exists_finset_maximalFor_isTranscendenceBasis_separableClosure
   have hs := d.argminOn_mem _ Hexists
   refine ⟨s, hs, fun t ht ↦ not_lt_iff_le_imp_ge.mp fun H ↦ ?_⟩
   have : t.Finite := by
-    simp [Set.Finite, ← Cardinal.mk_lt_aleph0_iff, ht.cardinalMk_eq hs, Cardinal.nat_lt_aleph0]
+    simp [Set.Finite, ← Cardinal.mk_lt_aleph0_iff, ht.cardinalMk_eq hs, Cardinal.natCast_lt_aleph0]
   lift t to Finset E using this
   have : Module.Finite (adjoin F (s : Set E)) E := by
     apply (config := { allowSynthFailures := true }) Algebra.finite_of_essFiniteType_of_isAlgebraic

Mathlib/GroupTheory/CoprodI.lean

@@ -1051,8 +1051,7 @@ theorem _root_.FreeGroup.injective_lift_of_ping_pong : Function.Injective (FreeG
   use Inhabited.default
   simp only [H]
   rw [FreeGroup.freeGroupUnitEquivInt.cardinal_eq, Cardinal.mk_denumerable]
-  apply le_of_lt
-  exact nat_lt_aleph0 3
+  exact natCast_le_aleph0
 
 end PingPongLemma
 

Mathlib/LinearAlgebra/Dimension/Constructions.lean

@@ -433,7 +433,7 @@ theorem rank_span_finset_le (s : Finset M) : Module.rank R (span R (s : Set M))
   simpa using rank_span_le (s : Set M)
 
 theorem rank_span_of_finset (s : Finset M) : Module.rank R (span R (s : Set M)) < ℵ₀ :=
-  (rank_span_finset_le s).trans_lt (Cardinal.nat_lt_aleph0 _)
+  (rank_span_finset_le s).trans_lt natCast_lt_aleph0
 
 open Submodule Module
 

Mathlib/LinearAlgebra/Dimension/ErdosKaplansky.lean

@@ -57,7 +57,7 @@ theorem max_aleph0_card_le_rank_fun_nat : max ℵ₀ #K ≤ Module.rank K (ℕ 
         ← MulOpposite.opEquiv.cardinal_eq] at card_K ⊢
     apply power_nat_le
     contrapose! card_K
-    exact (power_lt_aleph0 card_K <| nat_lt_aleph0 _).le
+    exact (power_lt_aleph0 card_K natCast_lt_aleph0).le
   obtain ⟨e⟩ := lift_mk_le'.mp (card_ιL.trans_eq (lift_uzero #ιL).symm)
   have rep_e := bK.linearCombination_repr (bL ∘ e)
   rw [Finsupp.linearCombination_apply, Finsupp.sum] at rep_e
@@ -68,7 +68,7 @@ theorem max_aleph0_card_le_rank_fun_nat : max ℵ₀ #K ≤ Module.rank K (ℕ 
     have := h.cardinal_lift_le_rank
     rw [lift_uzero, (LinearEquiv.piCongrRight fun _ ↦ MulOpposite.opLinearEquiv Lᵐᵒᵖ).rank_eq,
         rank_fun'] at this
-    exact (nat_lt_aleph0 _).not_ge this
+    exact natCast_lt_aleph0.not_ge this
   obtain ⟨t, g, eq0, i, hi, hgi⟩ := not_linearIndependent_iff.mp this
   refine hgi (linearIndependent_iff'.mp (bL.linearIndependent.comp e e.injective) t g ?_ i hi)
   clear_value c s