lint(geometry/manifold/whitney_embedding): assume [finite _] (#17628)

Author: urkud

src/geometry/manifold/whitney_embedding.lean

@@ -45,7 +45,8 @@ In this section we prove a version of the Whitney embedding theorem: for any com
 `M`, for sufficiently large `n` there exists a smooth embedding `M → ℝ^n`.
 -/
 
-variables [t2_space M] [fintype ι] {s : set M} (f : smooth_bump_covering ι I M s)
+variables [t2_space M] [hi : fintype ι] {s : set M} (f : smooth_bump_covering ι I M s)
+include hi
 
 /-- Smooth embedding of `M` into `(E × ℝ) ^ ι`. -/
 def embedding_pi_tangent : C^∞⟮I, M; 𝓘(ℝ, ι → (E × ℝ)), ι → (E × ℝ)⟯ :=
@@ -103,13 +104,16 @@ lemma embedding_pi_tangent_injective_mfderiv (x : M) (hx : x ∈ s) :
   injective (mfderiv I 𝓘(ℝ, ι → (E × ℝ)) f.embedding_pi_tangent x) :=
 linear_map.ker_eq_bot.1 (f.embedding_pi_tangent_ker_mfderiv x hx)
 
-/-- Baby version of the Whitney weak embedding theorem: if `M` admits a finite covering by
+omit hi
+
+/-- Baby version of the **Whitney weak embedding theorem**: if `M` admits a finite covering by
 supports of bump functions, then for some `n` it can be immersed into the `n`-dimensional
 Euclidean space. -/
-lemma exists_immersion_euclidean (f : smooth_bump_covering ι I M) :
+lemma exists_immersion_euclidean [finite ι] (f : smooth_bump_covering ι I M) :
   ∃ (n : ℕ) (e : M → euclidean_space ℝ (fin n)), smooth I (𝓡 n) e ∧
     injective e ∧ ∀ x : M, injective (mfderiv I (𝓡 n) e x) :=
 begin
+  casesI nonempty_fintype ι,
   set F := euclidean_space ℝ (fin $ finrank ℝ (ι → (E × ℝ))),
   letI : is_noetherian ℝ (E × ℝ) := is_noetherian.iff_fg.2 infer_instance,
   letI : finite_dimensional ℝ (ι → E × ℝ) := is_noetherian.iff_fg.1 infer_instance,