-- Mathlib/Geometry/Manifold/WhitneyEmbedding.lean
theorem exists_embedding_euclidean_of_compact [T2Space M] [CompactSpace M] :
    ∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)),
      ContMDiff I (𝓡 n) ∞ e ∧ IsClosedEmbedding e ∧ ∀ x : M, Injective (mfderiv I (𝓡 n) e x)

Proof state:
case intro.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
inst✝ : CompactSpace M
ι : Type uM
f : SmoothBumpCovering ι I M
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ IsClosedEmbedding e ∧ ∀ (x : M), Injective ⇑(mfderiv I (𝓡 n) e x)

Tactic:
haveI := f.fintype

Result:
case intro.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
inst✝ : CompactSpace M
ι : Type uM
f : SmoothBumpCovering ι I M
this : Fintype ι
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ IsClosedEmbedding e ∧ ∀ (x : M), Injective ⇑(mfderiv I (𝓡 n) e x)

Proof state:
case intro.intro.intro.intro.intro.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
inst✝ : CompactSpace M
ι : Type uM
f : SmoothBumpCovering ι I M
this : Fintype ι
n : ℕ
e : M → EuclideanSpace ℝ (Fin n)
hsmooth : ContMDiff I (𝓡 n) ∞ e
hinj : Injective e
hinj_mfderiv : ∀ (x : M), Injective ⇑(mfderiv I (𝓡 n) e x)
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ IsClosedEmbedding e ∧ ∀ (x : M), Injective ⇑(mfderiv I (𝓡 n) e x)

Tactic:
exact ⟨n, e, hsmooth, hsmooth.continuous.isClosedEmbedding hinj, hinj_mfderiv⟩

Result:
no goals

Proof state:
case intro.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
inst✝ : CompactSpace M
ι : Type uM
f : SmoothBumpCovering ι I M
this : Fintype ι
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ IsClosedEmbedding e ∧ ∀ (x : M), Injective ⇑(mfderiv I (𝓡 n) e x)

Tactic:
rcases f.exists_immersion_euclidean with ⟨n, e, hsmooth, hinj, hinj_mfderiv⟩

Result:
case intro.intro.intro.intro.intro.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
inst✝ : CompactSpace M
ι : Type uM
f : SmoothBumpCovering ι I M
this : Fintype ι
n : ℕ
e : M → EuclideanSpace ℝ (Fin n)
hsmooth : ContMDiff I (𝓡 n) ∞ e
hinj : Injective e
hinj_mfderiv : ∀ (x : M), Injective ⇑(mfderiv I (𝓡 n) e x)
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ IsClosedEmbedding 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
inst✝ : CompactSpace M
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ IsClosedEmbedding e ∧ ∀ (x : M), Injective ⇑(mfderiv I (𝓡 n) e x)

Tactic:
rcases SmoothBumpCovering.exists_isSubordinate I isClosed_univ fun (x : M) _ => univ_mem with
  ⟨ι, f, -⟩

Result:
case intro.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
inst✝ : CompactSpace M
ι : Type uM
f : SmoothBumpCovering ι I M
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ IsClosedEmbedding e ∧ ∀ (x : M), Injective ⇑(mfderiv I (𝓡 n) e x)