-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem exists_contMDiffOn_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t x))
    (Hloc : ∀ x : M, ∃ U ∈ 𝓝 x, ∃ g : M → F, ContMDiffOn I 𝓘(ℝ, F) n g U ∧ ∀ y ∈ U, g y ∈ t y) :
    ∃ g : C^n⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x

Proof state:
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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
ht : ∀ (x : M), Convex ℝ (t x)
Hloc : ∀ (x : M), ∃ U ∈ 𝓝 x, ∃ g, ContMDiffOn I 𝓘(ℝ, F) (↑n) g U ∧ ∀ y ∈ U, g y ∈ t y
⊢ ∃ g, ∀ (x : M), g x ∈ t x

Tactic:
choose U hU g hgs hgt using Hloc

Result:
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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
ht : ∀ (x : M), Convex ℝ (t x)
U : M → Set M
hU : ∀ (x : M), U x ∈ 𝓝 x
g : M → M → F
hgs : ∀ (x : M), ContMDiffOn I 𝓘(ℝ, F) (↑n) (g x) (U x)
hgt : ∀ (x y : M), y ∈ U x → g x y ∈ t y
⊢ ∃ g, ∀ (x : M), g x ∈ t x

Proof state:
case intro
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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
ht : ∀ (x : M), Convex ℝ (t x)
U : M → Set M
hU : ∀ (x : M), U x ∈ 𝓝 x
g : M → M → F
hgs : ∀ (x : M), ContMDiffOn I 𝓘(ℝ, F) (↑n) (g x) (U x)
hgt : ∀ (x y : M), y ∈ U x → g x y ∈ t y
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x => interior (U x)
x i : M
hi : (f i) x ≠ 0
⊢ x ∈ U i

Tactic:
exact interior_subset (hf _ <| subset_closure hi)

Result:
no goals

Proof state:
case intro
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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
ht : ∀ (x : M), Convex ℝ (t x)
U : M → Set M
hU : ∀ (x : M), U x ∈ 𝓝 x
g : M → M → F
hgs : ∀ (x : M), ContMDiffOn I 𝓘(ℝ, F) (↑n) (g x) (U x)
hgt : ∀ (x y : M), y ∈ U x → g x y ∈ t y
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x => interior (U x)
⊢ ∃ g, ∀ (x : M), g x ∈ t x

Tactic:
refine ⟨⟨fun x => ∑ᶠ i, f i x • g i x,
    hf.contMDiff_finsum_smul (fun i => isOpen_interior) fun i => (hgs i).mono interior_subset⟩,
  fun x => f.finsum_smul_mem_convex (mem_univ x) (fun i hi => hgt _ _ ?_) (ht _)⟩

Result:
case intro
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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
ht : ∀ (x : M), Convex ℝ (t x)
U : M → Set M
hU : ∀ (x : M), U x ∈ 𝓝 x
g : M → M → F
hgs : ∀ (x : M), ContMDiffOn I 𝓘(ℝ, F) (↑n) (g x) (U x)
hgt : ∀ (x y : M), y ∈ U x → g x y ∈ t y
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x => interior (U x)
x i : M
hi : (f i) x ≠ 0
⊢ x ∈ U i

Proof state:
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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
ht : ∀ (x : M), Convex ℝ (t x)
U : M → Set M
hU : ∀ (x : M), U x ∈ 𝓝 x
g : M → M → F
hgs : ∀ (x : M), ContMDiffOn I 𝓘(ℝ, F) (↑n) (g x) (U x)
hgt : ∀ (x y : M), y ∈ U x → g x y ∈ t y
⊢ ∃ g, ∀ (x : M), g x ∈ t x

Tactic:
obtain ⟨f, hf⟩ :=
  SmoothPartitionOfUnity.exists_isSubordinate I isClosed_univ (fun x => interior (U x))
    (fun x => isOpen_interior) fun x _ => mem_iUnion.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x)⟩

Result:
case intro
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
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
ht : ∀ (x : M), Convex ℝ (t x)
U : M → Set M
hU : ∀ (x : M), U x ∈ 𝓝 x
g : M → M → F
hgs : ∀ (x : M), ContMDiffOn I 𝓘(ℝ, F) (↑n) (g x) (U x)
hgt : ∀ (x y : M), y ∈ U x → g x y ∈ t y
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x => interior (U x)
⊢ ∃ g, ∀ (x : M), g x ∈ t x