-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem contMDiffAt_finsum {x₀ : M} {g : ι → M → F}
    (hφ : ∀ i, x₀ ∈ tsupport (f i) → ContMDiffAt I 𝓘(ℝ, F) n (g i) x₀) :
    ContMDiffAt I 𝓘(ℝ, F) n (fun x ↦ ∑ᶠ i, f i x • g i x) x₀

Proof state:
case neg
ι : Type uι
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
F : Type uF
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x₀ : M
g : ι → M → F
hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt I 𝓘(ℝ, F) (↑n) (g i) x₀
i : ι
hx : x₀ ∉ tsupport ⇑(f i)
⊢ ContMDiffAt I 𝓘(ℝ, F) (↑n) (fun x => (f i) x • g i x) x₀

Tactic:
exact contMDiffAt_of_not_mem (compl_subset_compl.mpr
  (tsupport_smul_subset_left (f i) (g i)) hx) n

Result:
no goals

Proof state:
ι : Type uι
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
F : Type uF
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x₀ : M
g : ι → M → F
hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt I 𝓘(ℝ, F) (↑n) (g i) x₀
⊢ ContMDiffAt I 𝓘(ℝ, F) (↑n) (fun x => ∑ᶠ (i : ι), (f i) x • g i x) x₀

Tactic:
refine _root_.contMDiffAt_finsum (f.locallyFinite.smul_left _) fun i ↦ ?_

Result:
ι : Type uι
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
F : Type uF
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x₀ : M
g : ι → M → F
hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt I 𝓘(ℝ, F) (↑n) (g i) x₀
i : ι
⊢ ContMDiffAt I 𝓘(ℝ, F) (↑n) (fun x => (f i) x • g i x) x₀

Proof state:
case pos
ι : Type uι
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
F : Type uF
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x₀ : M
g : ι → M → F
hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt I 𝓘(ℝ, F) (↑n) (g i) x₀
i : ι
hx : x₀ ∈ tsupport ⇑(f i)
⊢ ContMDiffAt I 𝓘(ℝ, F) (↑n) (fun x => (f i) x • g i x) x₀

Tactic:
exact ContMDiffAt.smul ((f i).contMDiff.of_le (mod_cast le_top)).contMDiffAt (hφ i hx)

Result:
no goals

Proof state:
ι : Type uι
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
F : Type uF
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x₀ : M
g : ι → M → F
hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt I 𝓘(ℝ, F) (↑n) (g i) x₀
i : ι
⊢ ContMDiffAt I 𝓘(ℝ, F) (↑n) (fun x => (f i) x • g i x) x₀

Tactic:
by_cases hx : x₀ ∈ tsupport (f i)

Result:
case pos
ι : Type uι
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
F : Type uF
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x₀ : M
g : ι → M → F
hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt I 𝓘(ℝ, F) (↑n) (g i) x₀
i : ι
hx : x₀ ∈ tsupport ⇑(f i)
⊢ ContMDiffAt I 𝓘(ℝ, F) (↑n) (fun x => (f i) x • g i x) x₀

case neg
ι : Type uι
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
F : Type uF
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x₀ : M
g : ι → M → F
hφ : ∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContMDiffAt I 𝓘(ℝ, F) (↑n) (g i) x₀
i : ι
hx : x₀ ∉ tsupport ⇑(f i)
⊢ ContMDiffAt I 𝓘(ℝ, F) (↑n) (fun x => (f i) x • g i x) x₀