[GOAL]
ι : Type uι
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : T2Space M
hi : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
⊢ InjOn (↑(embeddingPiTangent f)) s
[PROOFSTEP]
intro x hx y _ h
[GOAL]
ι : Type uι
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : T2Space M
hi : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h : ↑(embeddingPiTangent f) x = ↑(embeddingPiTangent f) y
⊢ x = y
[PROOFSTEP]
simp only [embeddingPiTangent_coe, funext_iff] at h 
[GOAL]
ι : Type uι
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : T2Space M
hi : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (a : ι),
    (↑(toFun s f a) x • ↑(extChartAt I (c s f a)) x, ↑(toFun s f a) x) =
      (↑(toFun s f a) y • ↑(extChartAt I (c s f a)) y, ↑(toFun s f a) y)
⊢ x = y
[PROOFSTEP]
obtain ⟨h₁, h₂⟩ := Prod.mk.inj_iff.1 (h (f.ind x hx))
[GOAL]
case intro
ι : Type uι
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : T2Space M
hi : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (a : ι),
    (↑(toFun s f a) x • ↑(extChartAt I (c s f a)) x, ↑(toFun s f a) x) =
      (↑(toFun s f a) y • ↑(extChartAt I (c s f a)) y, ↑(toFun s f a) y)
h₁ :
  ↑(toFun s f (ind f x hx)) x • ↑(extChartAt I (c s f (ind f x hx))) x =
    ↑(toFun s f (ind f x hx)) y • ↑(extChartAt I (c s f (ind f x hx))) y
h₂ : ↑(toFun s f (ind f x hx)) x = ↑(toFun s f (ind f x hx)) y
⊢ x = y
[PROOFSTEP]
rw [f.apply_ind x hx] at h₂ 
[GOAL]
case intro
ι : Type uι
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : T2Space M
hi : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (a : ι),
    (↑(toFun s f a) x • ↑(extChartAt I (c s f a)) x, ↑(toFun s f a) x) =
      (↑(toFun s f a) y • ↑(extChartAt I (c s f a)) y, ↑(toFun s f a) y)
h₁ :
  ↑(toFun s f (ind f x hx)) x • ↑(extChartAt I (c s f (ind f x hx))) x =
    ↑(toFun s f (ind f x hx)) y • ↑(extChartAt I (c s f (ind f x hx))) y
h₂ : 1 = ↑(toFun s f (ind f x hx)) y
⊢ x = y
[PROOFSTEP]
rw [← h₂, f.apply_ind x hx, one_smul, one_smul] at h₁ 
[GOAL]
case intro
ι : Type uι
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : T2Space M
hi : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (a : ι),
    (↑(toFun s f a) x • ↑(extChartAt I (c s f a)) x, ↑(toFun s f a) x) =
      (↑(toFun s f a) y • ↑(extChartAt I (c s f a)) y, ↑(toFun s f a) y)
h₁ : ↑(extChartAt I (c s f (ind f x hx))) x = ↑(extChartAt I (c s f (ind f x hx))) y
h₂ : 1 = ↑(toFun s f (ind f x hx)) y
⊢ x = y
[PROOFSTEP]
have := f.mem_extChartAt_source_of_eq_one h₂.symm
[GOAL]
case intro
ι : Type uι
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : T2Space M
hi : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (a : ι),
    (↑(toFun s f a) x • ↑(extChartAt I (c s f a)) x, ↑(toFun s f a) x) =
      (↑(toFun s f a) y • ↑(extChartAt I (c s f a)) y, ↑(toFun s f a) y)
h₁ : ↑(extChartAt I (c s f (ind f x hx))) x = ↑(extChartAt I (c s f (ind f x hx))) y
h₂ : 1 = ↑(toFun s f (ind f x hx)) y
this : y ∈ (extChartAt I (c s f (ind f x hx))).source
⊢ x = y
[PROOFSTEP]
exact (extChartAt I (f.c _)).injOn (f.mem_extChartAt_ind_source x hx) this h₁
[GOAL]
ι : Type uι
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : T2Space M
hi : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ ContinuousLinearMap.comp
      (ContinuousLinearMap.comp (ContinuousLinearMap.fst ℝ E ℝ) (ContinuousLinearMap.proj (ind f x hx)))
      (mfderiv I 𝓘(ℝ, ι → E × ℝ) (↑(embeddingPiTangent f)) x) =
    mfderiv I I (↑(chartAt H (c s f (ind f x hx)))) x
[PROOFSTEP]
set L :=
  (ContinuousLinearMap.fst ℝ E ℝ).comp
    (@ContinuousLinearMap.proj ℝ _ ι (fun _ => E × ℝ) _ _ (fun _ => inferInstance) (f.ind x hx))
[GOAL]
ι : Type uι
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : T2Space M
hi : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
L : (ι → E × ℝ) →L[ℝ] E :=
  ContinuousLinearMap.comp (ContinuousLinearMap.fst ℝ E ℝ) (ContinuousLinearMap.proj (ind f x hx))
⊢ ContinuousLinearMap.comp L (mfderiv I 𝓘(ℝ, ι → E × ℝ) (↑(embeddingPiTangent f)) x) =
    mfderiv I I (↑(chartAt H (c s f (ind f x hx)))) x
[PROOFSTEP]
have := L.hasMFDerivAt.comp x f.embeddingPiTangent.smooth.mdifferentiableAt.hasMFDerivAt
[GOAL]
ι : Type uι
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : T2Space M
hi : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
L : (ι → E × ℝ) →L[ℝ] E :=
  ContinuousLinearMap.comp (ContinuousLinearMap.fst ℝ E ℝ) (ContinuousLinearMap.proj (ind f x hx))
this :
  HasMFDerivAt I 𝓘(ℝ, E) (↑L ∘ ↑(embeddingPiTangent f)) x
    (ContinuousLinearMap.comp L (mfderiv I 𝓘(ℝ, ι → E × ℝ) (↑(embeddingPiTangent f)) x))
⊢ ContinuousLinearMap.comp L (mfderiv I 𝓘(ℝ, ι → E × ℝ) (↑(embeddingPiTangent f)) x) =
    mfderiv I I (↑(chartAt H (c s f (ind f x hx)))) x
[PROOFSTEP]
convert hasMFDerivAt_unique this _
[GOAL]
case convert_2
ι : Type uι
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : T2Space M
hi : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
L : (ι → E × ℝ) →L[ℝ] E :=
  ContinuousLinearMap.comp (ContinuousLinearMap.fst ℝ E ℝ) (ContinuousLinearMap.proj (ind f x hx))
this :
  HasMFDerivAt I 𝓘(ℝ, E) (↑L ∘ ↑(embeddingPiTangent f)) x
    (ContinuousLinearMap.comp L (mfderiv I 𝓘(ℝ, ι → E × ℝ) (↑(embeddingPiTangent f)) x))
⊢ HasMFDerivAt I 𝓘(ℝ, E) (↑L ∘ ↑(embeddingPiTangent f)) x (mfderiv I I (↑(chartAt H (c s f (ind f x hx)))) x)
[PROOFSTEP]
refine' (hasMFDerivAt_extChartAt I (f.mem_chartAt_ind_source x hx)).congr_of_eventuallyEq _
[GOAL]
case convert_2
ι : Type uι
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : T2Space M
hi : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
L : (ι → E × ℝ) →L[ℝ] E :=
  ContinuousLinearMap.comp (ContinuousLinearMap.fst ℝ E ℝ) (ContinuousLinearMap.proj (ind f x hx))
this :
  HasMFDerivAt I 𝓘(ℝ, E) (↑L ∘ ↑(embeddingPiTangent f)) x
    (ContinuousLinearMap.comp L (mfderiv I 𝓘(ℝ, ι → E × ℝ) (↑(embeddingPiTangent f)) x))
⊢ ↑L ∘ ↑(embeddingPiTangent f) =ᶠ[𝓝 x] ↑(extChartAt I (c s f (ind f x hx)))
[PROOFSTEP]
refine' (f.eventuallyEq_one x hx).mono fun y hy => _
[GOAL]
case convert_2
ι : Type uι
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : T2Space M
hi : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
L : (ι → E × ℝ) →L[ℝ] E :=
  ContinuousLinearMap.comp (ContinuousLinearMap.fst ℝ E ℝ) (ContinuousLinearMap.proj (ind f x hx))
this :
  HasMFDerivAt I 𝓘(ℝ, E) (↑L ∘ ↑(embeddingPiTangent f)) x
    (ContinuousLinearMap.comp L (mfderiv I 𝓘(ℝ, ι → E × ℝ) (↑(embeddingPiTangent f)) x))
y : M
hy : ↑(toFun s f (ind f x hx)) y = OfNat.ofNat 1 y
⊢ (↑L ∘ ↑(embeddingPiTangent f)) y = ↑(extChartAt I (c s f (ind f x hx))) y
[PROOFSTEP]
simp only [embeddingPiTangent_coe, ContinuousLinearMap.coe_comp', (· ∘ ·), ContinuousLinearMap.coe_fst',
  ContinuousLinearMap.proj_apply]
[GOAL]
case convert_2
ι : Type uι
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : T2Space M
hi : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
L : (ι → E × ℝ) →L[ℝ] E :=
  ContinuousLinearMap.comp (ContinuousLinearMap.fst ℝ E ℝ) (ContinuousLinearMap.proj (ind f x hx))
this :
  HasMFDerivAt I 𝓘(ℝ, E) (↑L ∘ ↑(embeddingPiTangent f)) x
    (ContinuousLinearMap.comp L (mfderiv I 𝓘(ℝ, ι → E × ℝ) (↑(embeddingPiTangent f)) x))
y : M
hy : ↑(toFun s f (ind f x hx)) y = OfNat.ofNat 1 y
⊢ ↑(toFun s f (ind f x hx)) y • ↑(extChartAt I (c s f (ind f x hx))) y = ↑(extChartAt I (c s f (ind f x hx))) y
[PROOFSTEP]
rw [hy, Pi.one_apply, one_smul]
[GOAL]
ι : Type uι
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : T2Space M
hi : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ LinearMap.ker (mfderiv I 𝓘(ℝ, ι → E × ℝ) (↑(embeddingPiTangent f)) x) = ⊥
[PROOFSTEP]
apply bot_unique
[GOAL]
case h
ι : Type uι
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : T2Space M
hi : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ LinearMap.ker (mfderiv I 𝓘(ℝ, ι → E × ℝ) (↑(embeddingPiTangent f)) x) ≤ ⊥
[PROOFSTEP]
rw [← (mdifferentiable_chart I (f.c (f.ind x hx))).ker_mfderiv_eq_bot (f.mem_chartAt_ind_source x hx), ←
  comp_embeddingPiTangent_mfderiv]
[GOAL]
case h
ι : Type uι
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✝¹ : SmoothManifoldWithCorners I M
inst✝ : T2Space M
hi : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ LinearMap.ker (mfderiv I 𝓘(ℝ, ι → E × ℝ) (↑(embeddingPiTangent f)) x) ≤
    LinearMap.ker
      (ContinuousLinearMap.comp
        (ContinuousLinearMap.comp (ContinuousLinearMap.fst ℝ E ℝ) (ContinuousLinearMap.proj (ind f x hx)))
        (mfderiv I 𝓘(ℝ, ι → E × ℝ) (↑(embeddingPiTangent f)) x))
[PROOFSTEP]
exact LinearMap.ker_le_ker_comp _ _
[GOAL]
ι : Type uι
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✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
hi : Fintype ι
s : Set M
f✝ : SmoothBumpCovering ι I M s
inst✝ : Finite ι
f : SmoothBumpCovering ι I M univ
⊢ ∃ n e,
    Smooth I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e ∧
      Injective e ∧ ∀ (x : M), Injective ↑(mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e x)
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
ι : Type uι
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✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
hi : Fintype ι
s : Set M
f✝ : SmoothBumpCovering ι I M s
inst✝ : Finite ι
f : SmoothBumpCovering ι I M univ
val✝ : Fintype ι
⊢ ∃ n e,
    Smooth I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e ∧
      Injective e ∧ ∀ (x : M), Injective ↑(mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e x)
[PROOFSTEP]
set F := EuclideanSpace ℝ (Fin <| finrank ℝ (ι → E × ℝ))
[GOAL]
case intro
ι : Type uι
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✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
hi : Fintype ι
s : Set M
f✝ : SmoothBumpCovering ι I M s
inst✝ : Finite ι
f : SmoothBumpCovering ι I M univ
val✝ : Fintype ι
F : Type := EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))
⊢ ∃ n e,
    Smooth I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e ∧
      Injective e ∧ ∀ (x : M), Injective ↑(mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e x)
[PROOFSTEP]
letI : IsNoetherian ℝ (E × ℝ) := IsNoetherian.iff_fg.2 inferInstance
[GOAL]
case intro
ι : Type uι
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✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
hi : Fintype ι
s : Set M
f✝ : SmoothBumpCovering ι I M s
inst✝ : Finite ι
f : SmoothBumpCovering ι I M univ
val✝ : Fintype ι
F : Type := EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))
this : IsNoetherian ℝ (E × ℝ) := Iff.mpr IsNoetherian.iff_fg inferInstance
⊢ ∃ n e,
    Smooth I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e ∧
      Injective e ∧ ∀ (x : M), Injective ↑(mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e x)
[PROOFSTEP]
letI : FiniteDimensional ℝ (ι → E × ℝ) := IsNoetherian.iff_fg.1 inferInstance
[GOAL]
case intro
ι : Type uι
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✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
hi : Fintype ι
s : Set M
f✝ : SmoothBumpCovering ι I M s
inst✝ : Finite ι
f : SmoothBumpCovering ι I M univ
val✝ : Fintype ι
F : Type := EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))
this✝ : IsNoetherian ℝ (E × ℝ) := Iff.mpr IsNoetherian.iff_fg inferInstance
this : FiniteDimensional ℝ (ι → E × ℝ) := Iff.mp IsNoetherian.iff_fg inferInstance
⊢ ∃ n e,
    Smooth I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e ∧
      Injective e ∧ ∀ (x : M), Injective ↑(mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e x)
[PROOFSTEP]
set eEF : (ι → E × ℝ) ≃L[ℝ] F := ContinuousLinearEquiv.ofFinrankEq finrank_euclideanSpace_fin.symm
[GOAL]
case intro
ι : Type uι
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✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
hi : Fintype ι
s : Set M
f✝ : SmoothBumpCovering ι I M s
inst✝ : Finite ι
f : SmoothBumpCovering ι I M univ
val✝ : Fintype ι
F : Type := EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))
this✝ : IsNoetherian ℝ (E × ℝ) := Iff.mpr IsNoetherian.iff_fg inferInstance
this : FiniteDimensional ℝ (ι → E × ℝ) := Iff.mp IsNoetherian.iff_fg inferInstance
eEF : (ι → E × ℝ) ≃L[ℝ] F :=
  ContinuousLinearEquiv.ofFinrankEq
    (_ : finrank ℝ (ι → E × ℝ) = finrank ℝ (EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))))
⊢ ∃ n e,
    Smooth I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e ∧
      Injective e ∧ ∀ (x : M), Injective ↑(mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e x)
[PROOFSTEP]
refine
  ⟨_, eEF ∘ f.embeddingPiTangent, eEF.toDiffeomorph.smooth.comp f.embeddingPiTangent.smooth,
    eEF.injective.comp f.embeddingPiTangent_injective, fun x => ?_⟩
[GOAL]
case intro
ι : Type uι
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✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
hi : Fintype ι
s : Set M
f✝ : SmoothBumpCovering ι I M s
inst✝ : Finite ι
f : SmoothBumpCovering ι I M univ
val✝ : Fintype ι
F : Type := EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))
this✝ : IsNoetherian ℝ (E × ℝ) := Iff.mpr IsNoetherian.iff_fg inferInstance
this : FiniteDimensional ℝ (ι → E × ℝ) := Iff.mp IsNoetherian.iff_fg inferInstance
eEF : (ι → E × ℝ) ≃L[ℝ] F :=
  ContinuousLinearEquiv.ofFinrankEq
    (_ : finrank ℝ (ι → E × ℝ) = finrank ℝ (EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))))
x : M
⊢ Injective ↑(mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))) (↑eEF ∘ ↑(embeddingPiTangent f)) x)
[PROOFSTEP]
rw [mfderiv_comp _ eEF.differentiableAt.mdifferentiableAt f.embeddingPiTangent.smooth.mdifferentiableAt, eEF.mfderiv_eq]
[GOAL]
case intro
ι : Type uι
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✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
hi : Fintype ι
s : Set M
f✝ : SmoothBumpCovering ι I M s
inst✝ : Finite ι
f : SmoothBumpCovering ι I M univ
val✝ : Fintype ι
F : Type := EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))
this✝ : IsNoetherian ℝ (E × ℝ) := Iff.mpr IsNoetherian.iff_fg inferInstance
this : FiniteDimensional ℝ (ι → E × ℝ) := Iff.mp IsNoetherian.iff_fg inferInstance
eEF : (ι → E × ℝ) ≃L[ℝ] F :=
  ContinuousLinearEquiv.ofFinrankEq
    (_ : finrank ℝ (ι → E × ℝ) = finrank ℝ (EuclideanSpace ℝ (Fin (finrank ℝ (ι → E × ℝ)))))
x : M
⊢ Injective ↑(ContinuousLinearMap.comp (↑eEF) (mfderiv I 𝓘(ℝ, ι → E × ℝ) (↑(embeddingPiTangent f)) x))
[PROOFSTEP]
exact eEF.injective.comp (f.embeddingPiTangent_injective_mfderiv _ trivial)
[GOAL]
ι : Type uι
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✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : CompactSpace M
⊢ ∃ n e,
    Smooth I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e ∧
      ClosedEmbedding e ∧ ∀ (x : M), Injective ↑(mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e x)
[PROOFSTEP]
rcases SmoothBumpCovering.exists_isSubordinate I isClosed_univ fun (x : M) _ => univ_mem with ⟨ι, f, -⟩
[GOAL]
case intro.intro
ι✝ : Type uι
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✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : CompactSpace M
ι : Type uM
f : SmoothBumpCovering ι I M univ
⊢ ∃ n e,
    Smooth I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e ∧
      ClosedEmbedding e ∧ ∀ (x : M), Injective ↑(mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e x)
[PROOFSTEP]
haveI := f.fintype
[GOAL]
case intro.intro
ι✝ : Type uι
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✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : CompactSpace M
ι : Type uM
f : SmoothBumpCovering ι I M univ
this : Fintype ι
⊢ ∃ n e,
    Smooth I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e ∧
      ClosedEmbedding e ∧ ∀ (x : M), Injective ↑(mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e x)
[PROOFSTEP]
rcases f.exists_immersion_euclidean with ⟨n, e, hsmooth, hinj, hinj_mfderiv⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
ι✝ : Type uι
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✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : CompactSpace M
ι : Type uM
f : SmoothBumpCovering ι I M univ
this : Fintype ι
n : ℕ
e : M → EuclideanSpace ℝ (Fin n)
hsmooth : Smooth I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e
hinj : Injective e
hinj_mfderiv : ∀ (x : M), Injective ↑(mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e x)
⊢ ∃ n e,
    Smooth I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e ∧
      ClosedEmbedding e ∧ ∀ (x : M), Injective ↑(mfderiv I 𝓘(ℝ, EuclideanSpace ℝ (Fin n)) e x)
[PROOFSTEP]
exact ⟨n, e, hsmooth, hsmooth.continuous.closedEmbedding hinj, hinj_mfderiv⟩
