[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⟩


[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
⊢ Injective ContMDiffSection.toFun
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ h
[GOAL]
case mk.mk
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
toFun✝¹ : (x : M) → V x
contMDiff_toFun✝¹ : ContMDiff I (ModelWithCorners.prod I 𝓘(𝕜, F)) n fun x => TotalSpace.mk' F x (toFun✝¹ x)
toFun✝ : (x : M) → V x
contMDiff_toFun✝ : ContMDiff I (ModelWithCorners.prod I 𝓘(𝕜, F)) n fun x => TotalSpace.mk' F x (toFun✝ x)
h :
  { toFun := toFun✝¹, contMDiff_toFun := contMDiff_toFun✝¹ }.toFun =
    { toFun := toFun✝, contMDiff_toFun := contMDiff_toFun✝ }.toFun
⊢ { toFun := toFun✝¹, contMDiff_toFun := contMDiff_toFun✝¹ } = { toFun := toFun✝, contMDiff_toFun := contMDiff_toFun✝ }
[PROOFSTEP]
congr
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s t : Cₛ^n⟮I; F, V⟯
⊢ Add Cₛ^n⟮I; F, V⟯
[PROOFSTEP]
refine' ⟨fun s t => ⟨s + t, _⟩⟩
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t✝ s t : Cₛ^n⟮I; F, V⟯
⊢ ContMDiff I (ModelWithCorners.prod I 𝓘(𝕜, F)) n fun x => TotalSpace.mk' F x ((↑s + ↑t) x)
[PROOFSTEP]
intro x₀
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t✝ s t : Cₛ^n⟮I; F, V⟯
x₀ : M
⊢ ContMDiffAt I (ModelWithCorners.prod I 𝓘(𝕜, F)) n (fun x => TotalSpace.mk' F x ((↑s + ↑t) x)) x₀
[PROOFSTEP]
have hs := s.contMDiff x₀
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t✝ s t : Cₛ^n⟮I; F, V⟯
x₀ : M
hs : ContMDiffAt I (ModelWithCorners.prod I 𝓘(𝕜, F)) n (fun x => TotalSpace.mk' F x (↑s x)) x₀
⊢ ContMDiffAt I (ModelWithCorners.prod I 𝓘(𝕜, F)) n (fun x => TotalSpace.mk' F x ((↑s + ↑t) x)) x₀
[PROOFSTEP]
have ht := t.contMDiff x₀
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t✝ s t : Cₛ^n⟮I; F, V⟯
x₀ : M
hs : ContMDiffAt I (ModelWithCorners.prod I 𝓘(𝕜, F)) n (fun x => TotalSpace.mk' F x (↑s x)) x₀
ht : ContMDiffAt I (ModelWithCorners.prod I 𝓘(𝕜, F)) n (fun x => TotalSpace.mk' F x (↑t x)) x₀
⊢ ContMDiffAt I (ModelWithCorners.prod I 𝓘(𝕜, F)) n (fun x => TotalSpace.mk' F x ((↑s + ↑t) x)) x₀
[PROOFSTEP]
rw [contMDiffAt_section] at hs ht ⊢
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t✝ s t : Cₛ^n⟮I; F, V⟯
x₀ : M
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑(trivializationAt F V x₀) { proj := x, snd := ↑s x }).snd) x₀
ht : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑(trivializationAt F V x₀) { proj := x, snd := ↑t x }).snd) x₀
⊢ ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑(trivializationAt F V x₀) { proj := x, snd := (↑s + ↑t) x }).snd) x₀
[PROOFSTEP]
set e := trivializationAt F V x₀
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t✝ s t : Cₛ^n⟮I; F, V⟯
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑s x }).snd) x₀
ht : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑t x }).snd) x₀
⊢ ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := (↑s + ↑t) x }).snd) x₀
[PROOFSTEP]
refine' (hs.add ht).congr_of_eventuallyEq _
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t✝ s t : Cₛ^n⟮I; F, V⟯
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑s x }).snd) x₀
ht : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑t x }).snd) x₀
⊢ (fun x => (↑e { proj := x, snd := (↑s + ↑t) x }).snd) =ᶠ[nhds x₀]
    (fun x => (↑e { proj := x, snd := ↑s x }).snd) + fun x => (↑e { proj := x, snd := ↑t x }).snd
[PROOFSTEP]
refine' eventually_of_mem (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀) _
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t✝ s t : Cₛ^n⟮I; F, V⟯
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑s x }).snd) x₀
ht : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑t x }).snd) x₀
⊢ ∀ (x : M),
    x ∈ e.baseSet →
      (fun x => (↑e { proj := x, snd := (↑s + ↑t) x }).snd) x =
        ((fun x => (↑e { proj := x, snd := ↑s x }).snd) + fun x => (↑e { proj := x, snd := ↑t x }).snd) x
[PROOFSTEP]
intro x hx
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t✝ s t : Cₛ^n⟮I; F, V⟯
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑s x }).snd) x₀
ht : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑t x }).snd) x₀
x : M
hx : x ∈ e.baseSet
⊢ (fun x => (↑e { proj := x, snd := (↑s + ↑t) x }).snd) x =
    ((fun x => (↑e { proj := x, snd := ↑s x }).snd) + fun x => (↑e { proj := x, snd := ↑t x }).snd) x
[PROOFSTEP]
apply (e.linear 𝕜 hx).1
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s t : Cₛ^n⟮I; F, V⟯
⊢ Sub Cₛ^n⟮I; F, V⟯
[PROOFSTEP]
refine' ⟨fun s t => ⟨s - t, _⟩⟩
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t✝ s t : Cₛ^n⟮I; F, V⟯
⊢ ContMDiff I (ModelWithCorners.prod I 𝓘(𝕜, F)) n fun x => TotalSpace.mk' F x ((↑s - ↑t) x)
[PROOFSTEP]
intro x₀
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t✝ s t : Cₛ^n⟮I; F, V⟯
x₀ : M
⊢ ContMDiffAt I (ModelWithCorners.prod I 𝓘(𝕜, F)) n (fun x => TotalSpace.mk' F x ((↑s - ↑t) x)) x₀
[PROOFSTEP]
have hs := s.contMDiff x₀
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t✝ s t : Cₛ^n⟮I; F, V⟯
x₀ : M
hs : ContMDiffAt I (ModelWithCorners.prod I 𝓘(𝕜, F)) n (fun x => TotalSpace.mk' F x (↑s x)) x₀
⊢ ContMDiffAt I (ModelWithCorners.prod I 𝓘(𝕜, F)) n (fun x => TotalSpace.mk' F x ((↑s - ↑t) x)) x₀
[PROOFSTEP]
have ht := t.contMDiff x₀
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t✝ s t : Cₛ^n⟮I; F, V⟯
x₀ : M
hs : ContMDiffAt I (ModelWithCorners.prod I 𝓘(𝕜, F)) n (fun x => TotalSpace.mk' F x (↑s x)) x₀
ht : ContMDiffAt I (ModelWithCorners.prod I 𝓘(𝕜, F)) n (fun x => TotalSpace.mk' F x (↑t x)) x₀
⊢ ContMDiffAt I (ModelWithCorners.prod I 𝓘(𝕜, F)) n (fun x => TotalSpace.mk' F x ((↑s - ↑t) x)) x₀
[PROOFSTEP]
rw [contMDiffAt_section] at hs ht ⊢
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t✝ s t : Cₛ^n⟮I; F, V⟯
x₀ : M
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑(trivializationAt F V x₀) { proj := x, snd := ↑s x }).snd) x₀
ht : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑(trivializationAt F V x₀) { proj := x, snd := ↑t x }).snd) x₀
⊢ ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑(trivializationAt F V x₀) { proj := x, snd := (↑s - ↑t) x }).snd) x₀
[PROOFSTEP]
set e := trivializationAt F V x₀
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t✝ s t : Cₛ^n⟮I; F, V⟯
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑s x }).snd) x₀
ht : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑t x }).snd) x₀
⊢ ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := (↑s - ↑t) x }).snd) x₀
[PROOFSTEP]
refine' (hs.sub ht).congr_of_eventuallyEq _
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t✝ s t : Cₛ^n⟮I; F, V⟯
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑s x }).snd) x₀
ht : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑t x }).snd) x₀
⊢ (fun x => (↑e { proj := x, snd := (↑s - ↑t) x }).snd) =ᶠ[nhds x₀] fun x =>
    (↑e { proj := x, snd := ↑s x }).snd - (↑e { proj := x, snd := ↑t x }).snd
[PROOFSTEP]
refine' eventually_of_mem (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀) _
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t✝ s t : Cₛ^n⟮I; F, V⟯
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑s x }).snd) x₀
ht : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑t x }).snd) x₀
⊢ ∀ (x : M),
    x ∈ e.baseSet →
      (fun x => (↑e { proj := x, snd := (↑s - ↑t) x }).snd) x =
        (fun x => (↑e { proj := x, snd := ↑s x }).snd - (↑e { proj := x, snd := ↑t x }).snd) x
[PROOFSTEP]
intro x hx
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t✝ s t : Cₛ^n⟮I; F, V⟯
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑s x }).snd) x₀
ht : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑t x }).snd) x₀
x : M
hx : x ∈ e.baseSet
⊢ (fun x => (↑e { proj := x, snd := (↑s - ↑t) x }).snd) x =
    (fun x => (↑e { proj := x, snd := ↑s x }).snd - (↑e { proj := x, snd := ↑t x }).snd) x
[PROOFSTEP]
apply (e.linear 𝕜 hx).map_sub
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s t : Cₛ^n⟮I; F, V⟯
⊢ SMul 𝕜 Cₛ^n⟮I; F, V⟯
[PROOFSTEP]
refine' ⟨fun c s => ⟨c • ⇑s, _⟩⟩
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t : Cₛ^n⟮I; F, V⟯
c : 𝕜
s : Cₛ^n⟮I; F, V⟯
⊢ ContMDiff I (ModelWithCorners.prod I 𝓘(𝕜, F)) n fun x => TotalSpace.mk' F x ((c • ↑s) x)
[PROOFSTEP]
intro x₀
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t : Cₛ^n⟮I; F, V⟯
c : 𝕜
s : Cₛ^n⟮I; F, V⟯
x₀ : M
⊢ ContMDiffAt I (ModelWithCorners.prod I 𝓘(𝕜, F)) n (fun x => TotalSpace.mk' F x ((c • ↑s) x)) x₀
[PROOFSTEP]
have hs := s.contMDiff x₀
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t : Cₛ^n⟮I; F, V⟯
c : 𝕜
s : Cₛ^n⟮I; F, V⟯
x₀ : M
hs : ContMDiffAt I (ModelWithCorners.prod I 𝓘(𝕜, F)) n (fun x => TotalSpace.mk' F x (↑s x)) x₀
⊢ ContMDiffAt I (ModelWithCorners.prod I 𝓘(𝕜, F)) n (fun x => TotalSpace.mk' F x ((c • ↑s) x)) x₀
[PROOFSTEP]
rw [contMDiffAt_section] at hs ⊢
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t : Cₛ^n⟮I; F, V⟯
c : 𝕜
s : Cₛ^n⟮I; F, V⟯
x₀ : M
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑(trivializationAt F V x₀) { proj := x, snd := ↑s x }).snd) x₀
⊢ ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑(trivializationAt F V x₀) { proj := x, snd := (c • ↑s) x }).snd) x₀
[PROOFSTEP]
set e := trivializationAt F V x₀
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t : Cₛ^n⟮I; F, V⟯
c : 𝕜
s : Cₛ^n⟮I; F, V⟯
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑s x }).snd) x₀
⊢ ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := (c • ↑s) x }).snd) x₀
[PROOFSTEP]
refine' (contMDiffAt_const.smul hs).congr_of_eventuallyEq _
[GOAL]
case refine'_1
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t : Cₛ^n⟮I; F, V⟯
c : 𝕜
s : Cₛ^n⟮I; F, V⟯
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑s x }).snd) x₀
⊢ 𝕜
[PROOFSTEP]
exact c
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t : Cₛ^n⟮I; F, V⟯
c : 𝕜
s : Cₛ^n⟮I; F, V⟯
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑s x }).snd) x₀
⊢ (fun x => (↑e { proj := x, snd := (c • ↑s) x }).snd) =ᶠ[nhds x₀] fun p => c • (↑e { proj := p, snd := ↑s p }).snd
[PROOFSTEP]
refine' eventually_of_mem (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀) _
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t : Cₛ^n⟮I; F, V⟯
c : 𝕜
s : Cₛ^n⟮I; F, V⟯
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑s x }).snd) x₀
⊢ ∀ (x : M),
    x ∈ e.baseSet →
      (fun x => (↑e { proj := x, snd := (c • ↑s) x }).snd) x = (fun p => c • (↑e { proj := p, snd := ↑s p }).snd) x
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t : Cₛ^n⟮I; F, V⟯
c : 𝕜
s : Cₛ^n⟮I; F, V⟯
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑s x }).snd) x₀
x : M
hx : x ∈ e.baseSet
⊢ (fun x => (↑e { proj := x, snd := (c • ↑s) x }).snd) x = (fun p => c • (↑e { proj := p, snd := ↑s p }).snd) x
[PROOFSTEP]
apply (e.linear 𝕜 hx).2
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s t : Cₛ^n⟮I; F, V⟯
⊢ Neg Cₛ^n⟮I; F, V⟯
[PROOFSTEP]
refine' ⟨fun s => ⟨-s, _⟩⟩
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n⟮I; F, V⟯
⊢ ContMDiff I (ModelWithCorners.prod I 𝓘(𝕜, F)) n fun x => TotalSpace.mk' F x ((-↑s) x)
[PROOFSTEP]
intro x₀
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n⟮I; F, V⟯
x₀ : M
⊢ ContMDiffAt I (ModelWithCorners.prod I 𝓘(𝕜, F)) n (fun x => TotalSpace.mk' F x ((-↑s) x)) x₀
[PROOFSTEP]
have hs := s.contMDiff x₀
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n⟮I; F, V⟯
x₀ : M
hs : ContMDiffAt I (ModelWithCorners.prod I 𝓘(𝕜, F)) n (fun x => TotalSpace.mk' F x (↑s x)) x₀
⊢ ContMDiffAt I (ModelWithCorners.prod I 𝓘(𝕜, F)) n (fun x => TotalSpace.mk' F x ((-↑s) x)) x₀
[PROOFSTEP]
rw [contMDiffAt_section] at hs ⊢
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n⟮I; F, V⟯
x₀ : M
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑(trivializationAt F V x₀) { proj := x, snd := ↑s x }).snd) x₀
⊢ ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑(trivializationAt F V x₀) { proj := x, snd := (-↑s) x }).snd) x₀
[PROOFSTEP]
set e := trivializationAt F V x₀
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n⟮I; F, V⟯
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑s x }).snd) x₀
⊢ ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := (-↑s) x }).snd) x₀
[PROOFSTEP]
refine' hs.neg.congr_of_eventuallyEq _
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n⟮I; F, V⟯
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑s x }).snd) x₀
⊢ (fun x => (↑e { proj := x, snd := (-↑s) x }).snd) =ᶠ[nhds x₀] fun x => -(↑e { proj := x, snd := ↑s x }).snd
[PROOFSTEP]
refine' eventually_of_mem (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀) _
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n⟮I; F, V⟯
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑s x }).snd) x₀
⊢ ∀ (x : M),
    x ∈ e.baseSet →
      (fun x => (↑e { proj := x, snd := (-↑s) x }).snd) x = (fun x => -(↑e { proj := x, snd := ↑s x }).snd) x
[PROOFSTEP]
intro x hx
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n⟮I; F, V⟯
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffAt I 𝓘(𝕜, F) n (fun x => (↑e { proj := x, snd := ↑s x }).snd) x₀
x : M
hx : x ∈ e.baseSet
⊢ (fun x => (↑e { proj := x, snd := (-↑s) x }).snd) x = (fun x => -(↑e { proj := x, snd := ↑s x }).snd) x
[PROOFSTEP]
apply (e.linear 𝕜 hx).map_neg
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n⟮I; F, V⟯
k : ℕ
⊢ ↑(k • s) = k • ↑s
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n⟮I; F, V⟯
⊢ ↑(Nat.zero • s) = Nat.zero • ↑s
[PROOFSTEP]
simp_rw [Nat.zero_eq, zero_smul]
[GOAL]
case zero
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n⟮I; F, V⟯
⊢ ↑(0 • s) = 0
[PROOFSTEP]
rfl
[GOAL]
case succ
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n⟮I; F, V⟯
k : ℕ
ih : ↑(k • s) = k • ↑s
⊢ ↑(Nat.succ k • s) = Nat.succ k • ↑s
[PROOFSTEP]
simp_rw [succ_nsmul, ← ih]
[GOAL]
case succ
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n⟮I; F, V⟯
k : ℕ
ih : ↑(k • s) = k • ↑s
⊢ ↑(Nat.succ k • s) = ↑s + ↑(k • s)
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n⟮I; F, V⟯
z : ℤ
⊢ ↑(z • s) = z • ↑s
[PROOFSTEP]
cases' z with n n
[GOAL]
case ofNat
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n✝ : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n✝⟮I; F, V⟯
n : ℕ
⊢ ↑(Int.ofNat n • s) = Int.ofNat n • ↑s
case negSucc
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n✝ : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n✝⟮I; F, V⟯
n : ℕ
⊢ ↑(Int.negSucc n • s) = Int.negSucc n • ↑s
[PROOFSTEP]
refine' (coe_nsmul s n).trans _
[GOAL]
case ofNat
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n✝ : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n✝⟮I; F, V⟯
n : ℕ
⊢ n • ↑s = Int.ofNat n • ↑s
case negSucc
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n✝ : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n✝⟮I; F, V⟯
n : ℕ
⊢ ↑(Int.negSucc n • s) = Int.negSucc n • ↑s
[PROOFSTEP]
simp only [Int.ofNat_eq_coe, coe_nat_zsmul]
[GOAL]
case negSucc
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n✝ : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n✝⟮I; F, V⟯
n : ℕ
⊢ ↑(Int.negSucc n • s) = Int.negSucc n • ↑s
[PROOFSTEP]
refine' (congr_arg Neg.neg (coe_nsmul s (n + 1))).trans _
[GOAL]
case negSucc
𝕜 : Type u_1
inst✝²⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁴ : NormedAddCommGroup E
inst✝²³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝²² : NormedAddCommGroup E'
inst✝²¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝²⁰ : TopologicalSpace H
H' : Type u_5
inst✝¹⁹ : TopologicalSpace H'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace H M
M' : Type u_7
inst✝¹⁶ : TopologicalSpace M'
inst✝¹⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝¹² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹¹ : TopologicalSpace M''
inst✝¹⁰ : ChartedSpace H'' M''
inst✝⁹ : SmoothManifoldWithCorners I M
F : Type u_11
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
n✝ : ℕ∞
V : M → Type u_12
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : SmoothVectorBundle F V I
s✝ t s : Cₛ^n✝⟮I; F, V⟯
n : ℕ
⊢ -((n + 1) • ↑s) = Int.negSucc n • ↑s
[PROOFSTEP]
simp only [negSucc_zsmul, neg_inj]