-- 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)
x : X
hx : x ∈ t
h : ∑ i ∈ ⋯.toFinset, (f.toFun i) x = 1
⊢ ∑ c : Fin n, (f c) x = 1

Tactic:
simp only [Finite.toFinset_setOf, ne_eq] at h

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
⊢ ∑ 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,
    (∀ (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:
obtain ⟨f, hfsub, hfcp⟩ := PartitionOfUnity.exists_isSubordinate_of_locallyFinite_t2space htcp s
  hs (locallyFinite_of_finite _) hst

Result:
case intro.intro
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)
⊢ ∃ f,
    (∀ (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)

Proof state:
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

Tactic:
exact ⟨f.nonneg i x, PartitionOfUnity.le_one f i x⟩

Result:
no goals

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 : j ∉ Finset.filter (fun j => ¬(f.toFun j) x = 0) Finset.univ
⊢ (f j) x = 0

Tactic:
simp only [Finset.mem_filter, Finset.mem_univ, true_and, Decidable.not_not] at hj

Result:
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

Proof state:
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

Tactic:
intro i x

Result:
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 : Fin n), (f.toFun i) x = 1
⊢ ∑ c : Fin n, (f c) x = 1

Tactic:
rw [finsum_eq_sum (fun i => (f.toFun i) x)
  (Finite.subset finite_univ (subset_univ (support fun i ↦ (f.toFun i) x)))] at h

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 ∈ ⋯.toFinset, (f.toFun i) x = 1
⊢ ∑ c : Fin n, (f c) x = 1

Proof state:
case intro.intro
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)
⊢ ∃ f,
    (∀ (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:
use f

Result:
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)

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
⊢ ∀ x_1 ∈ Finset.univ, x_1 ∉ Finset.filter (fun j => ¬(f.toFun j) x = 0) Finset.univ → (f x_1) x = 0

Tactic:
intro j hju hj

Result:
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 : j ∉ Finset.filter (fun j => ¬(f.toFun j) x = 0) Finset.univ
⊢ (f j) x = 0