feat(set_theory/cardinal): lt_omega_of_fintype (#13365)

Author: vihdzp

archive/100-theorems-list/82_cubing_a_cube.lean

@@ -509,7 +509,7 @@ omit h
 /-- The infinite sequence of cubes contradicts the finiteness of the family. -/
 theorem not_correct : ¬correct cs :=
 begin
-  intro h, apply not_le_of_lt (lt_omega_iff_fintype.mpr ⟨_inst_1⟩),
+  intro h, apply (lt_omega_of_fintype ι).not_le,
   rw [omega, lift_id], fapply mk_le_of_injective, exact λ n, (sequence_of_cubes h n).1,
   intros n m hnm, apply strict_mono.injective (strict_mono_sequence_of_cubes h),
   dsimp only [decreasing_sequence], rw hnm

src/data/W/cardinal.lean

@@ -69,7 +69,7 @@ calc cardinal.sum (λ a : α, m ^ #(β a))
   mul_le_mul' (le_max_left _ _) le_rfl
 ... = m : mul_eq_left.{u} (le_max_right _ _)
   (cardinal.sup_le (λ i, begin
-    cases lt_omega.1 (lt_omega_iff_fintype.2 ⟨show fintype (β i), by apply_instance⟩) with n hn,
+    cases lt_omega.1 (lt_omega_of_fintype (β i)) with n hn,
     rw [hn],
     exact power_nat_le (le_max_right _ _)
   end))

src/data/mv_polynomial/cardinal.lean

@@ -84,11 +84,8 @@ calc #(mv_polynomial_fun σ R) = #R + #σ + #(ulift bool) :
 ... ≤ max (max (#R + #σ) (#(ulift bool))) ω : add_le_max _ _
 ... ≤ max (max (max (max (#R) (#σ)) ω) (#(ulift bool))) ω :
   max_le_max (max_le_max (add_le_max _ _) le_rfl) le_rfl
-... ≤ _ : begin
-  have : #(ulift.{u} bool) ≤ ω,
-    from le_of_lt (lt_omega_iff_fintype.2 ⟨infer_instance⟩),
-  simp only [max_comm omega.{u}, max_assoc, max_left_comm omega.{u}, max_self, max_eq_left this],
-end
+... ≤ _ : by simp only [max_comm omega.{u}, max_assoc, max_left_comm omega.{u}, max_self,
+            max_eq_left (lt_omega_of_fintype (ulift.{u} bool)).le]
 
 namespace mv_polynomial
 

src/data/polynomial/cardinal.lean

@@ -22,9 +22,6 @@ lemma cardinal_mk_le_max {R : Type u} [comm_semiring R] : #R[X] ≤ max (#R) ω
 calc #R[X] = #(mv_polynomial punit.{u + 1} R) :
   cardinal.eq.2 ⟨(mv_polynomial.punit_alg_equiv.{u u} R).to_equiv.symm⟩
 ... ≤ _ : mv_polynomial.cardinal_mk_le_max
-... ≤ _ : begin
-  have : #(punit.{u + 1}) ≤ ω, from le_of_lt (lt_omega_iff_fintype.2 ⟨infer_instance⟩),
-  rw [max_assoc, max_eq_right this]
-end
+... ≤ _ : by rw [max_assoc, max_eq_right (lt_omega_of_fintype punit).le]
 
 end polynomial

src/field_theory/is_alg_closed/classification.lean

@@ -192,9 +192,9 @@ begin
       from ring_hom.injective _) with t ht,
   have : #s = #t,
   { rw [← cardinal_eq_cardinal_transcendence_basis_of_omega_lt _ hs
-      (le_of_lt $ lt_omega_iff_fintype.2 ⟨infer_instance⟩) hK,
+      (lt_omega_of_fintype (zmod p)).le hK,
         ← cardinal_eq_cardinal_transcendence_basis_of_omega_lt _ ht
-      (le_of_lt $ lt_omega_iff_fintype.2 ⟨infer_instance⟩), hKL],
+      (lt_omega_of_fintype (zmod p)).le, hKL],
     rwa ← hKL },
   cases cardinal.eq.1 this with e,
   exact ⟨equiv_of_transcendence_basis _ _ e hs ht⟩

src/linear_algebra/finsupp_vector_space.lean

@@ -199,7 +199,7 @@ lemma cardinal_lt_omega_of_finite_dimensional [fintype K] [finite_dimensional K
 begin
   letI : is_noetherian K V := is_noetherian.iff_fg.2 infer_instance,
   rw cardinal_mk_eq_cardinal_mk_field_pow_dim K V,
-  exact cardinal.power_lt_omega (cardinal.lt_omega_iff_fintype.2 ⟨infer_instance⟩)
+  exact cardinal.power_lt_omega (cardinal.lt_omega_of_fintype K)
     (is_noetherian.dim_lt_omega K V),
 end
 

src/set_theory/cardinal.lean

@@ -918,6 +918,9 @@ lt_omega.trans ⟨λ ⟨n, e⟩, begin
   exact ⟨fintype.of_equiv _ f.symm⟩
 end, λ ⟨_⟩, by exactI ⟨_, mk_fintype _⟩⟩
 
+theorem lt_omega_of_fintype (α : Type u) [fintype α] : #α < ω :=
+lt_omega_iff_fintype.2 ⟨infer_instance⟩
+
 theorem lt_omega_iff_finite {α} {S : set α} : #S < ω ↔ finite S :=
 lt_omega_iff_fintype.trans finite_def.symm