-- Mathlib/Analysis/Convex/PartitionOfUnity.lean
theorem exists_continuous_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t x))
    (H : ∀ x : X, ∃ U ∈ 𝓝 x, ∃ g : X → E, ContinuousOn g U ∧ ∀ y ∈ U, g y ∈ t y) :
    ∃ g : C(X, E), ∀ x, g x ∈ t x

Proof state:
X : Type u_2
E : Type u_3
inst✝⁷ : TopologicalSpace X
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : NormalSpace X
inst✝³ : ParacompactSpace X
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
H : ∀ (x : X), ∃ U ∈ 𝓝 x, ∃ g, ContinuousOn g U ∧ ∀ y ∈ U, g y ∈ t y
⊢ ∃ g, ∀ (x : X), g x ∈ t x

Tactic:
choose U hU g hgc hgt using H

Result:
X : Type u_2
E : Type u_3
inst✝⁷ : TopologicalSpace X
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : NormalSpace X
inst✝³ : ParacompactSpace X
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
g : X → X → E
hgc : ∀ (x : X), ContinuousOn (g x) (U x)
hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y
⊢ ∃ g, ∀ (x : X), g x ∈ t x

Proof state:
case intro
X : Type u_2
E : Type u_3
inst✝⁷ : TopologicalSpace X
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : NormalSpace X
inst✝³ : ParacompactSpace X
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
g : X → X → E
hgc : ∀ (x : X), ContinuousOn (g x) (U x)
hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y
f : PartitionOfUnity X X
hf : f.IsSubordinate fun x => interior (U x)
x i : X
hi : (f i) x ≠ 0
⊢ x ∈ U i

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

Result:
no goals

Proof state:
case intro
X : Type u_2
E : Type u_3
inst✝⁷ : TopologicalSpace X
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : NormalSpace X
inst✝³ : ParacompactSpace X
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
g : X → X → E
hgc : ∀ (x : X), ContinuousOn (g x) (U x)
hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y
f : PartitionOfUnity X X
hf : f.IsSubordinate fun x => interior (U x)
⊢ ∃ g, ∀ (x : X), g x ∈ t x

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

Result:
case intro
X : Type u_2
E : Type u_3
inst✝⁷ : TopologicalSpace X
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : NormalSpace X
inst✝³ : ParacompactSpace X
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
g : X → X → E
hgc : ∀ (x : X), ContinuousOn (g x) (U x)
hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y
f : PartitionOfUnity X X
hf : f.IsSubordinate fun x => interior (U x)
x i : X
hi : (f i) x ≠ 0
⊢ x ∈ U i

Proof state:
X : Type u_2
E : Type u_3
inst✝⁷ : TopologicalSpace X
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : NormalSpace X
inst✝³ : ParacompactSpace X
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
g : X → X → E
hgc : ∀ (x : X), ContinuousOn (g x) (U x)
hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y
⊢ ∃ g, ∀ (x : X), g x ∈ t x

Tactic:
obtain ⟨f, hf⟩ := PartitionOfUnity.exists_isSubordinate 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
X : Type u_2
E : Type u_3
inst✝⁷ : TopologicalSpace X
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : NormalSpace X
inst✝³ : ParacompactSpace X
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
g : X → X → E
hgc : ∀ (x : X), ContinuousOn (g x) (U x)
hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y
f : PartitionOfUnity X X
hf : f.IsSubordinate fun x => interior (U x)
⊢ ∃ g, ∀ (x : X), g x ∈ t x