-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem IsOpen.exists_msmooth_support_eq {s : Set M} (hs : IsOpen s) :
    ∃ f : M → ℝ, f.support = s ∧ ContMDiff I 𝓘(ℝ) ∞ f ∧ ∀ x, 0 ≤ f x

Proof state:
case intro.refine_2
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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x => (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
⊢ ContMDiff I 𝓘(ℝ, ℝ) ∞ fun x => ∑ᶠ (c : M), (f c) x * g c (↑(chartAt H c) x)

Tactic:
apply SmoothPartitionOfUnity.contMDiff_finsum_smul

Result:
case intro.refine_2.hg
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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x => (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
⊢ ∀ (i x : M), x ∈ tsupport ⇑(f i) → ContMDiffAt I 𝓘(ℝ, ℝ) ∞ (fun x => g i (↑(chartAt H i) 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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x => (chartAt H x).source
i : M
⊢ ∃ g, support g = (chartAt H i).target ∩ ↑(chartAt H i).symm ⁻¹' s ∧ ContMDiff I 𝓘(ℝ, ℝ) ∞ g ∧ range g ⊆ Icc 0 1

Tactic:
apply IsOpen.exists_msmooth_support_eq_aux

Result:
case hs
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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x => (chartAt H x).source
i : M
⊢ IsOpen ((chartAt H i).target ∩ ↑(chartAt H i).symm ⁻¹' s)

Proof state:
case pos
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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x => (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x c : M
Hx : x ∈ tsupport ⇑(f c)
hx : x ∈ ↑(chartAt H c) ⁻¹' (chartAt H c).target ∩ ↑(chartAt H c) ⁻¹' (↑(chartAt H c).symm ⁻¹' s)
⊢ x ∈ s

Tactic:
simp only [mem_inter_iff, mem_preimage, (chartAt H c).left_inv (hf c Hx)] at hx

Result:
case pos
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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x => (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x c : M
Hx : x ∈ tsupport ⇑(f c)
hx : ↑(chartAt H c) x ∈ (chartAt H c).target ∧ x ∈ s
⊢ x ∈ s

Proof state:
case intro
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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x => (chartAt H x).source
⊢ ∃ f, support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) ∞ f ∧ ∀ (x : M), 0 ≤ f x

Tactic:
have A : ∀ (c : M), ∃ g : H → ℝ,
    g.support = (chartAt H c).target ∩ (chartAt H c).symm ⁻¹' s ∧
    ContMDiff I 𝓘(ℝ) ∞ g ∧ Set.range g ⊆ Set.Icc 0 1 := by
  intro i
  apply IsOpen.exists_msmooth_support_eq_aux
  exact PartialHomeomorph.isOpen_inter_preimage_symm _ hs

Result:
case intro
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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x => (chartAt H x).source
A :
  ∀ (c : M),
    ∃ g, support g = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s ∧ ContMDiff I 𝓘(ℝ, ℝ) ∞ g ∧ range g ⊆ Icc 0 1
⊢ ∃ f, support f = s ∧ ContMDiff I 𝓘(ℝ, ℝ) ∞ f ∧ ∀ (x : M), 0 ≤ 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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x => (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∈ s
c : M
hc : 0 < (f c) x
⊢ g c (↑(chartAt H c) x) ≠ 0

Tactic:
rw [← mem_support, g_supp, ← mem_preimage, preimage_inter]

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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x => (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∈ s
c : M
hc : 0 < (f c) x
⊢ x ∈ ↑(chartAt H c) ⁻¹' (chartAt H c).target ∩ ↑(chartAt H c) ⁻¹' (↑(chartAt H c).symm ⁻¹' s)