-- Mathlib/Topology/PartitionOfUnity.lean
theorem exists_continuous_sum_one_of_isOpen_isCompact [T2Space X] [LocallyCompactSpace X]
    {n : ℕ} {t : Set X} {s : Fin n → Set X} (hs : ∀ (i : Fin n), IsOpen (s i)) (htcp : IsCompact t)
    (hst : t ⊆ ⋃ i, s i) :
    ∃ f : Fin n → C(X, ℝ), (∀ (i : Fin n), tsupport (f i) ⊆ s i) ∧ EqOn (∑ i, f i) 1 t
      ∧ (∀ (i : Fin n), ∀ (x : X), f i x ∈ Icc (0 : ℝ) 1)
      ∧ (∀ (i : Fin n), HasCompactSupport (f i))

Proof state:
case h.refine_1
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ i, s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate s
hfcp : ∀ (i : Fin n), HasCompactSupport ⇑(f i)
⊢ EqOn (∑ i : Fin n, ⇑(f i)) 1 t

Tactic:
intro x hx

Result:
case h.refine_1
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ i, s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate s
hfcp : ∀ (i : Fin n), HasCompactSupport ⇑(f i)
x : X
hx : x ∈ t
⊢ (∑ i : Fin n, ⇑(f i)) x = 1 x

Proof state:
case h.refine_1
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ i, s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate s
hfcp : ∀ (i : Fin n), HasCompactSupport ⇑(f i)
x : X
hx : x ∈ t
⊢ (∑ i : Fin n, ⇑(f i)) x = 1 x

Tactic:
simp only [Finset.sum_apply, Pi.one_apply]

Result:
case h.refine_1
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ i, s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate s
hfcp : ∀ (i : Fin n), HasCompactSupport ⇑(f i)
x : X
hx : x ∈ t
⊢ ∑ c : Fin n, (f c) x = 1

Proof state:
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ i, s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate s
hfcp : ∀ (i : Fin n), HasCompactSupport ⇑(f i)
x : X
hx : x ∈ t
h : ∑ i ∈ Finset.filter (fun x_1 => ¬(f.toFun x_1) x = 0) Finset.univ, (f.toFun i) x = 1
j : Fin n
hju : j ∈ Finset.univ
hj : (f.toFun j) x = 0
⊢ (f j) x = 0

Tactic:
exact hj

Result:
no goals

Proof state:
case h.refine_1
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ i, s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate s
hfcp : ∀ (i : Fin n), HasCompactSupport ⇑(f i)
x : X
hx : x ∈ t
⊢ ∑ c : Fin n, (f c) x = 1

Tactic:
have h := f.sum_eq_one' x hx

Result:
case h.refine_1
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ i, s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate s
hfcp : ∀ (i : Fin n), HasCompactSupport ⇑(f i)
x : X
hx : x ∈ t
h : ∑ᶠ (i : Fin n), (f.toFun i) x = 1
⊢ ∑ c : Fin n, (f c) x = 1

Proof state:
case h.refine_1
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ i, s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate s
hfcp : ∀ (i : Fin n), HasCompactSupport ⇑(f i)
x : X
hx : x ∈ t
h : ∑ i ∈ Finset.filter (fun x_1 => ¬(f.toFun x_1) x = 0) Finset.univ, (f.toFun i) x = 1
⊢ ∑ x_1 ∈ Finset.filter (fun j => ¬(f.toFun j) x = 0) Finset.univ, (f x_1) x =
    ∑ i ∈ Finset.filter (fun x_1 => ¬(f.toFun x_1) x = 0) Finset.univ, (f.toFun i) x

Tactic:
rfl

Result:
no goals

Proof state:
case h
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ i, s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate s
hfcp : ∀ (i : Fin n), HasCompactSupport ⇑(f i)
⊢ (∀ (i : Fin n), tsupport ⇑(f i) ⊆ s i) ∧
    EqOn (∑ i : Fin n, ⇑(f i)) 1 t ∧
      (∀ (i : Fin n) (x : X), (f i) x ∈ Icc 0 1) ∧ ∀ (i : Fin n), HasCompactSupport ⇑(f i)

Tactic:
refine ⟨fun i ↦ hfsub i, ?_, ?_, fun i => hfcp i⟩

Result:
case h.refine_1
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ i, s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate s
hfcp : ∀ (i : Fin n), HasCompactSupport ⇑(f i)
⊢ EqOn (∑ i : Fin n, ⇑(f i)) 1 t

case h.refine_2
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ i, s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate s
hfcp : ∀ (i : Fin n), HasCompactSupport ⇑(f i)
⊢ ∀ (i : Fin n) (x : X), (f i) x ∈ Icc 0 1

Proof state:
case h.refine_1
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ i, s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate s
hfcp : ∀ (i : Fin n), HasCompactSupport ⇑(f i)
x : X
hx : x ∈ t
h : ∑ i ∈ Finset.filter (fun x_1 => ¬(f.toFun x_1) x = 0) Finset.univ, (f.toFun i) x = 1
⊢ ∑ c : Fin n, (f c) x = 1

Tactic:
rw [← h, ← Finset.sum_subset
  (Finset.subset_univ (Finset.filter (fun (j : Fin n) ↦ ¬(f.toFun j) x = 0) Finset.univ))
  (by intro j hju hj
      simp only [Finset.mem_filter, Finset.mem_univ, true_and, Decidable.not_not] at hj
      exact hj)]

Result:
case h.refine_1
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
n : ℕ
t : Set X
s : Fin n → Set X
hs : ∀ (i : Fin n), IsOpen (s i)
htcp : IsCompact t
hst : t ⊆ ⋃ i, s i
f : PartitionOfUnity (Fin n) X t
hfsub : f.IsSubordinate s
hfcp : ∀ (i : Fin n), HasCompactSupport ⇑(f i)
x : X
hx : x ∈ t
h : ∑ i ∈ Finset.filter (fun x_1 => ¬(f.toFun x_1) x = 0) Finset.univ, (f.toFun i) x = 1
⊢ ∑ x_1 ∈ Finset.filter (fun j => ¬(f.toFun j) x = 0) Finset.univ, (f x_1) x =
    ∑ i ∈ Finset.filter (fun x_1 => ¬(f.toFun x_1) x = 0) Finset.univ, (f.toFun i) x