-- Mathlib/Geometry/Manifold/BumpFunction.lean
theorem contMDiff_smul {G} [NormedAddCommGroup G] [NormedSpace ℝ G] {g : M → G}
    (hg : ContMDiffOn I 𝓘(ℝ, G) ∞ g (chartAt H c).source) :
    ContMDiff I 𝓘(ℝ, G) ∞ fun x => f x • g x

Proof state:
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
H : Type uH
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : T2Space M
inst✝² : IsManifold I ∞ M
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : M → G
hg : ContMDiffOn I 𝓘(ℝ, G) ∞ g (chartAt H c).source
⊢ ContMDiff I 𝓘(ℝ, G) ∞ fun x => ↑f x • g x

Tactic:
refine contMDiff_of_tsupport fun x hx => ?_

Result:
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
H : Type uH
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : T2Space M
inst✝² : IsManifold I ∞ M
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : M → G
hg : ContMDiffOn I 𝓘(ℝ, G) ∞ g (chartAt H c).source
x : M
hx : x ∈ tsupport fun x => ↑f x • g x
⊢ ContMDiffAt I 𝓘(ℝ, G) ∞ (fun x => ↑f x • g x) x

Proof state:
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
H : Type uH
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : T2Space M
inst✝² : IsManifold I ∞ M
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : M → G
hg : ContMDiffOn I 𝓘(ℝ, G) ∞ g (chartAt H c).source
x : M
hx : x ∈ tsupport fun x => ↑f x • g x
⊢ ContMDiffAt I 𝓘(ℝ, G) ∞ (fun x => ↑f x • g x) x

Tactic:
have : x ∈ (chartAt H c).source :=
f.tsupport_subset_chartAt_source <| tsupport_smul_subset_left _ _ hx

Result:
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
H : Type uH
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : T2Space M
inst✝² : IsManifold I ∞ M
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : M → G
hg : ContMDiffOn I 𝓘(ℝ, G) ∞ g (chartAt H c).source
x : M
hx : x ∈ tsupport fun x => ↑f x • g x
this : x ∈ (chartAt H c).source
⊢ ContMDiffAt I 𝓘(ℝ, G) ∞ (fun x => ↑f x • g x) x

Proof state:
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
H : Type uH
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : T2Space M
inst✝² : IsManifold I ∞ M
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
g : M → G
hg : ContMDiffOn I 𝓘(ℝ, G) ∞ g (chartAt H c).source
x : M
hx : x ∈ tsupport fun x => ↑f x • g x
this : x ∈ (chartAt H c).source
⊢ ContMDiffAt I 𝓘(ℝ, G) ∞ (fun x => ↑f x • g x) x

Tactic:
exact f.contMDiffAt.smul ((hg _ this).contMDiffAt <| (chartAt _ _).open_source.mem_nhds this)

Result:
no goals