-- Mathlib/Geometry/Manifold/WhitneyEmbedding.lean
theorem exists_immersion_euclidean {ι : Type*} [Finite ι] (f : SmoothBumpCovering ι I M) :
    ∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)),
      ContMDiff I (𝓡 n) ∞ e ∧ Injective e ∧ ∀ x : M, Injective (mfderiv I (𝓡 n) e x)

Proof state:
case intro
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
ι : Type u_1
inst✝ : Finite ι
f : SmoothBumpCovering ι I M
val✝ : Fintype ι
F : Type := EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))
this✝ : IsNoetherian ℝ (E × ℝ) := IsNoetherian.iff_fg.mpr inferInstance
this : FiniteDimensional ℝ (ι → E × ℝ) := IsNoetherian.iff_fg.mp inferInstance
eEF : (ι → E × ℝ) ≃L[ℝ] F := ContinuousLinearEquiv.ofFinrankEq ⋯
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ Injective e ∧ ∀ (x : M), Injective ⇑(mfderiv I (𝓡 n) e x)

Tactic:
refine ⟨_, eEF ∘ f.embeddingPiTangent,
  eEF.toDiffeomorph.contMDiff.comp f.embeddingPiTangent.contMDiff,
  eEF.injective.comp f.embeddingPiTangent_injective, fun x => ?_⟩

Result:
case intro
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
ι : Type u_1
inst✝ : Finite ι
f : SmoothBumpCovering ι I M
val✝ : Fintype ι
F : Type := EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))
this✝ : IsNoetherian ℝ (E × ℝ) := IsNoetherian.iff_fg.mpr inferInstance
this : FiniteDimensional ℝ (ι → E × ℝ) := IsNoetherian.iff_fg.mp inferInstance
eEF : (ι → E × ℝ) ≃L[ℝ] F := ContinuousLinearEquiv.ofFinrankEq ⋯
x : M
⊢ Injective ⇑(mfderiv I (𝓡 finrank ℝ (ι → E × ℝ)) (⇑eEF ∘ ⇑f.embeddingPiTangent) x)

Proof state:
case intro
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
ι : Type u_1
inst✝ : Finite ι
f : SmoothBumpCovering ι I M
val✝ : Fintype ι
F : Type := EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ Injective e ∧ ∀ (x : M), Injective ⇑(mfderiv I (𝓡 n) e x)

Tactic:
letI : IsNoetherian ℝ (E × ℝ) := IsNoetherian.iff_fg.2 inferInstance

Result:
case intro
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
ι : Type u_1
inst✝ : Finite ι
f : SmoothBumpCovering ι I M
val✝ : Fintype ι
F : Type := EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))
this : IsNoetherian ℝ (E × ℝ) := IsNoetherian.iff_fg.mpr inferInstance
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ Injective e ∧ ∀ (x : M), Injective ⇑(mfderiv I (𝓡 n) e x)

Proof state:
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
ι : Type u_1
inst✝ : Finite ι
f : SmoothBumpCovering ι I M
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ Injective e ∧ ∀ (x : M), Injective ⇑(mfderiv I (𝓡 n) e x)

Tactic:
cases nonempty_fintype ι

Result:
case intro
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
ι : Type u_1
inst✝ : Finite ι
f : SmoothBumpCovering ι I M
val✝ : Fintype ι
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ Injective e ∧ ∀ (x : M), Injective ⇑(mfderiv I (𝓡 n) e x)