[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
hs : x ∈ (chartAt H c).toLocalEquiv.source
hd : dist (↑(extChartAt I c) x) (↑(extChartAt I c) c) ≤ f.rIn
⊢ ↑f x = 1
[PROOFSTEP]
simp only [f.eqOn_source hs, (· ∘ ·), f.one_of_mem_closedBall hd]
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
⊢ support ↑f = (chartAt H c).toLocalEquiv.source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rOut
[PROOFSTEP]
rw [coe_def, support_indicator, support_comp_eq_preimage, ← extChartAt_source I, ←
  (extChartAt I c).symm_image_target_inter_eq', ← (extChartAt I c).symm_image_target_inter_eq', f.support_eq]
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
⊢ IsOpen (support ↑f)
[PROOFSTEP]
rw [support_eq_inter_preimage]
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
⊢ IsOpen ((chartAt H c).toLocalEquiv.source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rOut)
[PROOFSTEP]
exact isOpen_extChartAt_preimage I c isOpen_ball
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
⊢ support ↑f = ↑(LocalEquiv.symm (extChartAt I c)) '' (ball (↑(extChartAt I c) c) f.rOut ∩ range ↑I)
[PROOFSTEP]
rw [f.support_eq_inter_preimage, ← extChartAt_source I, ← (extChartAt I c).symm_image_target_inter_eq', inter_comm,
  ball_inter_range_eq_ball_inter_target]
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
⊢ support ↑f ⊆ (chartAt H c).toLocalEquiv.source
[PROOFSTEP]
rw [f.support_eq_inter_preimage, ← extChartAt_source I]
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
⊢ (extChartAt I c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rOut ⊆ (extChartAt I c).source
[PROOFSTEP]
exact inter_subset_left _ _
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
s : Set M
hs : s ⊆ support ↑f
⊢ ↑(extChartAt I c) '' s =
    closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I ∩ ↑(LocalEquiv.symm (extChartAt I c)) ⁻¹' s
[PROOFSTEP]
rw [support_eq_inter_preimage, subset_inter_iff, ← extChartAt_source I, ← image_subset_iff] at hs 
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
s : Set M
hs : s ⊆ (extChartAt I c).source ∧ ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
⊢ ↑(extChartAt I c) '' s =
    closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I ∩ ↑(LocalEquiv.symm (extChartAt I c)) ⁻¹' s
[PROOFSTEP]
cases' hs with hse hsf
[GOAL]
case intro
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
c : M
f : SmoothBumpFunction I c
x : M
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
⊢ ↑(extChartAt I c) '' s =
    closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I ∩ ↑(LocalEquiv.symm (extChartAt I c)) ⁻¹' s
[PROOFSTEP]
apply Subset.antisymm
[GOAL]
case intro.h₁
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
c : M
f : SmoothBumpFunction I c
x : M
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
⊢ ↑(extChartAt I c) '' s ⊆
    closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I ∩ ↑(LocalEquiv.symm (extChartAt I c)) ⁻¹' s
[PROOFSTEP]
refine' subset_inter (subset_inter (hsf.trans ball_subset_closedBall) _) _
[GOAL]
case intro.h₁.refine'_1
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
c : M
f : SmoothBumpFunction I c
x : M
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
⊢ ↑(extChartAt I c) '' s ⊆ range ↑I
[PROOFSTEP]
rintro _ ⟨x, -, rfl⟩
[GOAL]
case intro.h₁.refine'_1.intro.intro
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
c : M
f : SmoothBumpFunction I c
x✝ : M
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
x : M
⊢ ↑(extChartAt I c) x ∈ range ↑I
[PROOFSTEP]
exact mem_range_self _
[GOAL]
case intro.h₁.refine'_2
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
c : M
f : SmoothBumpFunction I c
x : M
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
⊢ ↑(extChartAt I c) '' s ⊆ ↑(LocalEquiv.symm (extChartAt I c)) ⁻¹' s
[PROOFSTEP]
rw [(extChartAt I c).image_eq_target_inter_inv_preimage hse]
[GOAL]
case intro.h₁.refine'_2
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
c : M
f : SmoothBumpFunction I c
x : M
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
⊢ (extChartAt I c).target ∩ ↑(LocalEquiv.symm (extChartAt I c)) ⁻¹' s ⊆ ↑(LocalEquiv.symm (extChartAt I c)) ⁻¹' s
[PROOFSTEP]
exact inter_subset_right _ _
[GOAL]
case intro.h₂
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
c : M
f : SmoothBumpFunction I c
x : M
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
⊢ closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I ∩ ↑(LocalEquiv.symm (extChartAt I c)) ⁻¹' s ⊆
    ↑(extChartAt I c) '' s
[PROOFSTEP]
refine' Subset.trans (inter_subset_inter_left _ f.closedBall_subset) _
[GOAL]
case intro.h₂
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
c : M
f : SmoothBumpFunction I c
x : M
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
⊢ (extChartAt I c).target ∩ ↑(LocalEquiv.symm (extChartAt I c)) ⁻¹' s ⊆ ↑(extChartAt I c) '' s
[PROOFSTEP]
rw [(extChartAt I c).image_eq_target_inter_inv_preimage hse]
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
⊢ ↑f x ∈ Icc 0 1
[PROOFSTEP]
have : f x = 0 ∨ f x = _ := indicator_eq_zero_or_self _ _ _
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
this : ↑f x = 0 ∨ ↑f x = (↑f.toContDiffBump ∘ ↑(extChartAt I c)) x
⊢ ↑f x ∈ Icc 0 1
[PROOFSTEP]
cases' this with h h
[GOAL]
case inl
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
c : M
f : SmoothBumpFunction I c
x : M
h : ↑f x = 0
⊢ ↑f x ∈ Icc 0 1
[PROOFSTEP]
rw [h]
[GOAL]
case inr
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
c : M
f : SmoothBumpFunction I c
x : M
h : ↑f x = (↑f.toContDiffBump ∘ ↑(extChartAt I c)) x
⊢ ↑f x ∈ Icc 0 1
[PROOFSTEP]
rw [h]
[GOAL]
case inl
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
c : M
f : SmoothBumpFunction I c
x : M
h : ↑f x = 0
⊢ 0 ∈ Icc 0 1
case inr
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
c : M
f : SmoothBumpFunction I c
x : M
h : ↑f x = (↑f.toContDiffBump ∘ ↑(extChartAt I c)) x
⊢ (↑f.toContDiffBump ∘ ↑(extChartAt I c)) x ∈ Icc 0 1
[PROOFSTEP]
exacts [left_mem_Icc.2 zero_le_one, ⟨f.nonneg, f.le_one⟩]
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
hs : x ∈ (chartAt H c).toLocalEquiv.source
hd : dist (↑(extChartAt I c) x) (↑(extChartAt I c) c) < f.rIn
⊢ ↑f =ᶠ[𝓝 x] 1
[PROOFSTEP]
filter_upwards [IsOpen.mem_nhds (isOpen_extChartAt_preimage I c isOpen_ball) ⟨hs, hd⟩]
[GOAL]
case h
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
c : M
f : SmoothBumpFunction I c
x : M
hs : x ∈ (chartAt H c).toLocalEquiv.source
hd : dist (↑(extChartAt I c) x) (↑(extChartAt I c) c) < f.rIn
⊢ ∀ (a : M),
    a ∈ (chartAt H c).toLocalEquiv.source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rIn →
      ↑f a = OfNat.ofNat 1 a
[PROOFSTEP]
rintro z ⟨hzs, hzd⟩
[GOAL]
case h.intro
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
c : M
f : SmoothBumpFunction I c
x : M
hs : x ∈ (chartAt H c).toLocalEquiv.source
hd : dist (↑(extChartAt I c) x) (↑(extChartAt I c) c) < f.rIn
z : M
hzs : z ∈ (chartAt H c).toLocalEquiv.source
hzd : z ∈ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rIn
⊢ ↑f z = OfNat.ofNat 1 z
[PROOFSTEP]
exact f.one_of_dist_le hzs <| le_of_lt hzd
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
⊢ dist (↑(extChartAt I c) c) (↑(extChartAt I c) c) < f.rIn
[PROOFSTEP]
rw [dist_self]
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
⊢ 0 < f.rIn
[PROOFSTEP]
exact f.rIn_pos
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x✝ x : M
hx : ↑f x = OfNat.ofNat 1 x
⊢ ↑f x ≠ 0
[PROOFSTEP]
rw [hx]
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x✝ x : M
hx : ↑f x = OfNat.ofNat 1 x
⊢ OfNat.ofNat 1 x ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
⊢ HasBasis (𝓝[range ↑I] ↑(extChartAt I c) c) (fun x => True) fun f => closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I
[PROOFSTEP]
refine'
  ((nhdsWithin_hasBasis nhds_basis_closedBall _).restrict_subset (extChartAt_target_mem_nhdsWithin _ _)).to_has_basis' _
    _
[GOAL]
case refine'_1
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
c : M
f : SmoothBumpFunction I c
x : M
⊢ ∀ (i : ℝ),
    0 < i ∧ closedBall (↑(extChartAt I c) c) i ∩ range ↑I ⊆ (extChartAt I c).target →
      ∃ i', True ∧ closedBall (↑(extChartAt I c) c) i'.rOut ∩ range ↑I ⊆ closedBall (↑(extChartAt I c) c) i ∩ range ↑I
[PROOFSTEP]
rintro R ⟨hR0, hsub⟩
[GOAL]
case refine'_1.intro
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
c : M
f : SmoothBumpFunction I c
x : M
R : ℝ
hR0 : 0 < R
hsub : closedBall (↑(extChartAt I c) c) R ∩ range ↑I ⊆ (extChartAt I c).target
⊢ ∃ i', True ∧ closedBall (↑(extChartAt I c) c) i'.rOut ∩ range ↑I ⊆ closedBall (↑(extChartAt I c) c) R ∩ range ↑I
[PROOFSTEP]
exact ⟨⟨⟨R / 2, R, half_pos hR0, half_lt_self hR0⟩, hsub⟩, trivial, Subset.rfl⟩
[GOAL]
case refine'_2
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
c : M
f : SmoothBumpFunction I c
x : M
⊢ ∀ (i' : SmoothBumpFunction I c),
    True → closedBall (↑(extChartAt I c) c) i'.rOut ∩ range ↑I ∈ 𝓝[range ↑I] ↑(extChartAt I c) c
[PROOFSTEP]
exact fun f _ => inter_mem (mem_nhdsWithin_of_mem_nhds <| closedBall_mem_nhds _ f.rOut_pos) self_mem_nhdsWithin
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
s : Set M
hsc : IsClosed s
hs : s ⊆ support ↑f
⊢ IsClosed (↑(extChartAt I c) '' s)
[PROOFSTEP]
rw [f.image_eq_inter_preimage_of_subset_support hs]
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
s : Set M
hsc : IsClosed s
hs : s ⊆ support ↑f
⊢ IsClosed (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I ∩ ↑(LocalEquiv.symm (extChartAt I c)) ⁻¹' s)
[PROOFSTEP]
refine' ContinuousOn.preimage_closed_of_closed ((continuousOn_extChartAt_symm _ _).mono f.closedBall_subset) _ hsc
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
s : Set M
hsc : IsClosed s
hs : s ⊆ support ↑f
⊢ IsClosed (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)
[PROOFSTEP]
exact IsClosed.inter isClosed_ball I.closed_range
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
s : Set M
hsc : IsClosed s
hs : s ⊆ support ↑f
⊢ ∃ r, r ∈ Ioo 0 f.rOut ∧ s ⊆ (chartAt H c).toLocalEquiv.source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) r
[PROOFSTEP]
set e := extChartAt I c
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
s : Set M
hsc : IsClosed s
hs : s ⊆ support ↑f
e : LocalEquiv M E := extChartAt I c
⊢ ∃ r, r ∈ Ioo 0 f.rOut ∧ s ⊆ (chartAt H c).toLocalEquiv.source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) r
[PROOFSTEP]
have : IsClosed (e '' s) := f.isClosed_image_of_isClosed hsc hs
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
s : Set M
hsc : IsClosed s
hs : s ⊆ support ↑f
e : LocalEquiv M E := extChartAt I c
this : IsClosed (↑e '' s)
⊢ ∃ r, r ∈ Ioo 0 f.rOut ∧ s ⊆ (chartAt H c).toLocalEquiv.source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) r
[PROOFSTEP]
rw [support_eq_inter_preimage, subset_inter_iff, ← image_subset_iff] at hs 
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
s : Set M
hsc : IsClosed s
hs : s ⊆ (chartAt H c).toLocalEquiv.source ∧ ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
e : LocalEquiv M E := extChartAt I c
this : IsClosed (↑e '' s)
⊢ ∃ r, r ∈ Ioo 0 f.rOut ∧ s ⊆ (chartAt H c).toLocalEquiv.source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) r
[PROOFSTEP]
rcases exists_pos_lt_subset_ball f.rOut_pos this hs.2 with ⟨r, hrR, hr⟩
[GOAL]
case intro.intro
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
c : M
f : SmoothBumpFunction I c
x : M
s : Set M
hsc : IsClosed s
hs : s ⊆ (chartAt H c).toLocalEquiv.source ∧ ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
e : LocalEquiv M E := extChartAt I c
this : IsClosed (↑e '' s)
r : ℝ
hrR : r ∈ Ioo 0 f.rOut
hr : ↑e '' s ⊆ ball (↑(extChartAt I c) c) r
⊢ ∃ r, r ∈ Ioo 0 f.rOut ∧ s ⊆ (chartAt H c).toLocalEquiv.source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) r
[PROOFSTEP]
exact ⟨r, hrR, subset_inter hs.1 (image_subset_iff.1 hr)⟩
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
r : ℝ
hr : r ∈ Ioo 0 f.rOut
⊢ support ↑(updateRIn f r hr) = support ↑f
[PROOFSTEP]
simp only [support_eq_inter_preimage, updateRIn_rOut]
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
inst✝ : T2Space M
⊢ tsupport ↑f ⊆ ↑(LocalEquiv.symm (extChartAt I c)) '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)
[PROOFSTEP]
rw [tsupport, support_eq_symm_image]
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
inst✝ : T2Space M
⊢ closure (↑(LocalEquiv.symm (extChartAt I c)) '' (ball (↑(extChartAt I c) c) f.rOut ∩ range ↑I)) ⊆
    ↑(LocalEquiv.symm (extChartAt I c)) '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)
[PROOFSTEP]
exact
  closure_minimal (image_subset _ <| inter_subset_inter_left _ ball_subset_closedBall) f.isClosed_symm_image_closedBall
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
inst✝ : T2Space M
⊢ tsupport ↑f ⊆ (chartAt H c).toLocalEquiv.source
[PROOFSTEP]
simpa only [extChartAt_source] using f.tsupport_subset_extChartAt_source
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
inst✝ : T2Space M
⊢ HasBasis (𝓝 c) (fun x => True) fun f => tsupport ↑f
[PROOFSTEP]
have :
  (𝓝 c).HasBasis (fun _ : SmoothBumpFunction I c => True) fun f =>
    (extChartAt I c).symm '' (closedBall (extChartAt I c c) f.rOut ∩ range I) :=
  by
  rw [← map_extChartAt_symm_nhdsWithin_range I c]
  exact nhdsWithin_range_basis.map _
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
inst✝ : T2Space M
⊢ HasBasis (𝓝 c) (fun x => True) fun f =>
    ↑(LocalEquiv.symm (extChartAt I c)) '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)
[PROOFSTEP]
rw [← map_extChartAt_symm_nhdsWithin_range I c]
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
inst✝ : T2Space M
⊢ HasBasis (map (↑(LocalEquiv.symm (extChartAt I c))) (𝓝[range ↑I] ↑(extChartAt I c) c)) (fun x => True) fun f =>
    ↑(LocalEquiv.symm (extChartAt I c)) '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)
[PROOFSTEP]
exact nhdsWithin_range_basis.map _
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
inst✝ : T2Space M
this :
  HasBasis (𝓝 c) (fun x => True) fun f =>
    ↑(LocalEquiv.symm (extChartAt I c)) '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)
⊢ HasBasis (𝓝 c) (fun x => True) fun f => tsupport ↑f
[PROOFSTEP]
refine'
  this.to_has_basis' (fun f _ => ⟨f, trivial, f.tsupport_subset_symm_image_closedBall⟩) fun f _ => f.tsupport_mem_nhds
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
inst✝¹ : T2Space M
inst✝ : SmoothManifoldWithCorners I M
⊢ Smooth I 𝓘(ℝ, ℝ) ↑f
[PROOFSTEP]
refine' contMDiff_of_support fun x hx => _
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x✝ : M
inst✝¹ : T2Space M
inst✝ : SmoothManifoldWithCorners I M
x : M
hx : x ∈ tsupport ↑f
⊢ ContMDiffAt I 𝓘(ℝ, ℝ) ⊤ (↑f) x
[PROOFSTEP]
have : x ∈ (chartAt H c).source := f.tsupport_subset_chartAt_source hx
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x✝ : M
inst✝¹ : T2Space M
inst✝ : SmoothManifoldWithCorners I M
x : M
hx : x ∈ tsupport ↑f
this : x ∈ (chartAt H c).toLocalEquiv.source
⊢ ContMDiffAt I 𝓘(ℝ, ℝ) ⊤ (↑f) x
[PROOFSTEP]
refine'
  ContMDiffAt.congr_of_eventuallyEq _ <|
    f.eqOn_source.eventuallyEq_of_mem <| IsOpen.mem_nhds (chartAt H c).open_source this
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x✝ : M
inst✝¹ : T2Space M
inst✝ : SmoothManifoldWithCorners I M
x : M
hx : x ∈ tsupport ↑f
this : x ∈ (chartAt H c).toLocalEquiv.source
⊢ ContMDiffAt I 𝓘(ℝ, ℝ) ⊤ (↑f.toContDiffBump ∘ ↑(extChartAt I c)) x
[PROOFSTEP]
exact f.contDiffAt.contMDiffAt.comp _ (contMDiffAt_extChartAt' this)
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x : M
inst✝³ : T2Space M
inst✝² : SmoothManifoldWithCorners I M
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : M → G
hg : SmoothOn I 𝓘(ℝ, G) g (chartAt H c).toLocalEquiv.source
⊢ Smooth I 𝓘(ℝ, G) fun x => ↑f x • g x
[PROOFSTEP]
refine contMDiff_of_support fun x hx => ?_
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x✝ : M
inst✝³ : T2Space M
inst✝² : SmoothManifoldWithCorners I M
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : M → G
hg : SmoothOn I 𝓘(ℝ, G) g (chartAt H c).toLocalEquiv.source
x : M
hx : x ∈ tsupport fun x => ↑f x • g x
⊢ ContMDiffAt I 𝓘(ℝ, G) ⊤ (fun x => ↑f x • g x) x
[PROOFSTEP]
have : x ∈ (chartAt H c).source
[GOAL]
case this
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
c : M
f : SmoothBumpFunction I c
x✝ : M
inst✝³ : T2Space M
inst✝² : SmoothManifoldWithCorners I M
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : M → G
hg : SmoothOn I 𝓘(ℝ, G) g (chartAt H c).toLocalEquiv.source
x : M
hx : x ∈ tsupport fun x => ↑f x • g x
⊢ x ∈ (chartAt H c).toLocalEquiv.source
[PROOFSTEP]
exact f.tsupport_subset_chartAt_source <| tsupport_smul_subset_left _ _ hx
[GOAL]
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
c : M
f : SmoothBumpFunction I c
x✝ : M
inst✝³ : T2Space M
inst✝² : SmoothManifoldWithCorners I M
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : M → G
hg : SmoothOn I 𝓘(ℝ, G) g (chartAt H c).toLocalEquiv.source
x : M
hx : x ∈ tsupport fun x => ↑f x • g x
this : x ∈ (chartAt H c).toLocalEquiv.source
⊢ ContMDiffAt I 𝓘(ℝ, G) ⊤ (fun x => ↑f x • g x) x
[PROOFSTEP]
exact f.smoothAt.smul ((hg _ this).contMDiffAt <| IsOpen.mem_nhds (chartAt _ _).open_source this)
