-- Mathlib/Geometry/Manifold/BumpFunction.lean
theorem contMDiff : ContMDiff I 𝓘(ℝ) ∞ f

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
x : M
hx : x ∈ tsupport ↑f
this : x ∈ (chartAt H c).source
⊢ ContMDiffAt I 𝓘(ℝ, ℝ) ∞ (↑f) x

Tactic:
refine ContMDiffAt.congr_of_eventuallyEq ?_ <| f.eqOn_source.eventuallyEq_of_mem <|
  (chartAt H c).open_source.mem_nhds this

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
x : M
hx : x ∈ tsupport ↑f
this : x ∈ (chartAt H c).source
⊢ ContMDiffAt I 𝓘(ℝ, ℝ) ∞ (↑f.toContDiffBump ∘ ↑(extChartAt I c)) 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
x : M
hx : x ∈ tsupport ↑f
⊢ ContMDiffAt I 𝓘(ℝ, ℝ) ∞ (↑f) x

Tactic:
have : x ∈ (chartAt H c).source := f.tsupport_subset_chartAt_source 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
x : M
hx : x ∈ tsupport ↑f
this : x ∈ (chartAt H c).source
⊢ ContMDiffAt I 𝓘(ℝ, ℝ) ∞ (↑f) 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
⊢ ContMDiff I 𝓘(ℝ, ℝ) ∞ ↑f

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
x : M
hx : x ∈ tsupport ↑f
⊢ ContMDiffAt I 𝓘(ℝ, ℝ) ∞ (↑f) 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
x : M
hx : x ∈ tsupport ↑f
this : x ∈ (chartAt H c).source
⊢ ContMDiffAt I 𝓘(ℝ, ℝ) ∞ (↑f.toContDiffBump ∘ ↑(extChartAt I c)) x

Tactic:
exact f.contDiffAt.contMDiffAt.comp _ (contMDiffAt_extChartAt' this)

Result:
no goals