-- Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean
lemma exists_continuous_add_one_of_isCompact_nnreal
    {s₀ s₁ : Set X} {t : Set X} (s₀_compact : IsCompact s₀) (s₁_compact : IsCompact s₁)
    (t_compact : IsCompact t) (disj : Disjoint s₀ s₁) (hst : s₀ ∪ s₁ ⊆ t) :
    ∃ (f₀ f₁ : C_c(X, ℝ≥0)), EqOn f₀ 1 s₀ ∧ EqOn f₁ 1 s₁ ∧ EqOn (f₀ + f₁) 1 t

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : s₀ᶜ ∪ s₁ᶜ = univ
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j => if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j => if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
⊢ ∃ i, x ∈ if i = 0 then s₀ᶜ else s₁ᶜ

Tactic:
have h : x ∈ s₀ᶜ ∨ x ∈ s₁ᶜ := by
  rw [← mem_union, disj]
  exact mem_univ _

Result:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : s₀ᶜ ∪ s₁ᶜ = univ
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j => if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j => if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
h : x ∈ s₀ᶜ ∨ x ∈ s₁ᶜ
⊢ ∃ i, x ∈ if i = 0 then s₀ᶜ else s₁ᶜ

Proof state:
case h
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j => if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j => if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ j, so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport ⇑(f i) ⊆ so i
sum_f_one_on_t : EqOn (∑ i : Fin 2, ⇑(f i)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), (f i) x ∈ Icc 0 1
f_hcs : ∀ (i : Fin 2), HasCompactSupport ⇑(f i)
⊢ EqOn (⇑{ toContinuousMap := f 1, hasCompactSupport' := ⋯ }.nnrealPart) 1 s₀ ∧
    EqOn (⇑{ toContinuousMap := f 0, hasCompactSupport' := ⋯ }.nnrealPart) 1 s₁ ∧
      EqOn
        (⇑{ toContinuousMap := f 1, hasCompactSupport' := ⋯ }.nnrealPart +
          ⇑{ toContinuousMap := f 0, hasCompactSupport' := ⋯ }.nnrealPart)
        1 t

Tactic:
have sum_one_x (x : X) (hx : x ∈ t) : (f 0) x + (f 1) x = 1 := by
  simpa only [Finset.sum_apply, Fin.sum_univ_two, Fin.isValue, Pi.one_apply]
    using sum_f_one_on_t hx

Result:
case h
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j => if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j => if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ j, so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport ⇑(f i) ⊆ so i
sum_f_one_on_t : EqOn (∑ i : Fin 2, ⇑(f i)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), (f i) x ∈ Icc 0 1
f_hcs : ∀ (i : Fin 2), HasCompactSupport ⇑(f i)
sum_one_x : ∀ x ∈ t, (f 0) x + (f 1) x = 1
⊢ EqOn (⇑{ toContinuousMap := f 1, hasCompactSupport' := ⋯ }.nnrealPart) 1 s₀ ∧
    EqOn (⇑{ toContinuousMap := f 0, hasCompactSupport' := ⋯ }.nnrealPart) 1 s₁ ∧
      EqOn
        (⇑{ toContinuousMap := f 1, hasCompactSupport' := ⋯ }.nnrealPart +
          ⇑{ toContinuousMap := f 0, hasCompactSupport' := ⋯ }.nnrealPart)
        1 t

Proof state:
case right
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : s₀ᶜ ∪ s₁ᶜ = univ
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j => if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j => if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
h : x ∈ s₀ᶜ ∨ x ∈ s₁ᶜ
⊢ x ∈ s₁ᶜ → ∃ i, x ∈ if i = 0 then s₀ᶜ else s₁ᶜ

Tactic:
intro h1

Result:
case right
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : s₀ᶜ ∪ s₁ᶜ = univ
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j => if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j => if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
h : x ∈ s₀ᶜ ∨ x ∈ s₁ᶜ
h1 : x ∈ s₁ᶜ
⊢ ∃ i, x ∈ if i = 0 then s₀ᶜ else s₁ᶜ

Proof state:
case h.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ⊆ t ∧ s₁ ⊆ t
so : Fin 2 → Set X := fun j => if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j => if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ j, so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport ⇑(f i) ⊆ so i
sum_f_one_on_t : EqOn (∑ i : Fin 2, ⇑(f i)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), (f i) x ∈ Icc 0 1
f_hcs : ∀ (i : Fin 2), HasCompactSupport ⇑(f i)
sum_one_x : ∀ x ∈ t, (f 0) x + (f 1) x = 1
x : X
hx : x ∈ s₁
this : (f 1) x = 0
⊢ (f 0) x = 1

Tactic:
rw [← sum_one_x x (mem_of_subset_of_mem hst.2 hx), this]

Result:
case h.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ⊆ t ∧ s₁ ⊆ t
so : Fin 2 → Set X := fun j => if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j => if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ j, so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport ⇑(f i) ⊆ so i
sum_f_one_on_t : EqOn (∑ i : Fin 2, ⇑(f i)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), (f i) x ∈ Icc 0 1
f_hcs : ∀ (i : Fin 2), HasCompactSupport ⇑(f i)
sum_one_x : ∀ x ∈ t, (f 0) x + (f 1) x = 1
x : X
hx : x ∈ s₁
this : (f 1) x = 0
⊢ (f 0) x = (f 0) x + 0

Proof state:
case h.refine_1
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j => if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j => if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ j, so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport ⇑(f i) ⊆ so i
sum_f_one_on_t : EqOn (∑ i : Fin 2, ⇑(f i)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), (f i) x ∈ Icc 0 1
f_hcs : ∀ (i : Fin 2), HasCompactSupport ⇑(f i)
sum_one_x : ∀ x ∈ t, (f 0) x + (f 1) x = 1
x : X
hx : x ∈ s₀
⊢ { toContinuousMap := f 1, hasCompactSupport' := ⋯ }.nnrealPart x = 1 x

Tactic:
simp only [Fin.isValue, nnrealPart_apply,
  CompactlySupportedContinuousMap.coe_mk, Pi.one_apply, Real.toNNReal_eq_one]

Result:
case h.refine_1
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j => if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j => if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ j, so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport ⇑(f i) ⊆ so i
sum_f_one_on_t : EqOn (∑ i : Fin 2, ⇑(f i)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), (f i) x ∈ Icc 0 1
f_hcs : ∀ (i : Fin 2), HasCompactSupport ⇑(f i)
sum_one_x : ∀ x ∈ t, (f 0) x + (f 1) x = 1
x : X
hx : x ∈ s₀
⊢ (f 1) x = 1