awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
⊢ IsClosed s₀

Tactic:
IsCompact.isClosed <| s₀_compact

Premises used: IsCompact.isClosed
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
⊢ IsClosed s₀

Tactic:
exact IsCompact.isClosed <| s₀_compact

Premises used: IsCompact.isClosed
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
1 : IsClosed s₁
⊢ IsOpen (so ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))

Tactic:
simp only [hso, Fin.isValue, Fin.mk_one, one_ne_zero, ↓reduceIte, isOpen_compl_iff]

Premises used: Fin.mk_one, Fin.isValue, reduceIte, one_ne_zero, isOpen_compl_iff
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
⊢ IsClosed s₁

Tactic:
IsCompact.isClosed <| s₁_compact

Premises used: IsCompact.isClosed
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
⊢ IsClosed s₁

Tactic:
exact IsCompact.isClosed <| s₁_compact

Premises used: IsCompact.isClosed
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
⊢ ∀ (j : Fin 2), IsOpen (so j)

Tactic:
have soopen (j : Fin 2) : IsOpen (so j) := by
    fin_cases j
    · simp only [hso, Fin.zero_eta, Fin.isValue, ↓reduceIte, isOpen_compl_iff]
      exact IsCompact.isClosed <| s₀_compact
    · simp only [hso, Fin.isValue, Fin.mk_one, one_ne_zero, ↓reduceIte, isOpen_compl_iff]
      exact IsCompact.isClosed <| s₁_compact
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
rw : t ⊆ ⋃ (j : Fin 2), (fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ) j
⊢ t ⊆ ⋃ (j : Fin 2), so j

Tactic:
rw [hso]
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
rw : ∃ (i : Fin 2), x ∈ if i = 0 then s₀ᶜ else s₁ᶜ
⊢ Membership.mem (γ := Set X) (⋃ (j : Fin 2), if j = 0 then s₀ᶜ else s₁ᶜ) x

Tactic:
rw [mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
rw :
  ∀ (disj : s₀ᶜ ∪ s₁ᶜ = univ) (hst : s₀ ∪ s₁ ⊆ t),
    let so : Fin 2 → Set X := fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ;
    ∀ (hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ) (soopen : ∀ (j : Fin 2), IsOpen (so j)) ⦃x : X⦄
      (hx : x ∈ t), ∃ (i : Fin 2), x ∈ if i = 0 then s₀ᶜ else s₁ᶜ
⊢ ∃ (i : Fin 2), x ∈ if i = 0 then s₀ᶜ else s₁ᶜ

Tactic:
rw [← subset_compl_iff_disjoint_right, ← compl_compl s₀, compl_subset_iff_union] at disj

Premises used: compl_compl, Set.subset_compl_iff_disjoint_right, Set.compl_subset_iff_union
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
rw : Membership.mem (γ := Set X) univ x
⊢ x ∈ s₀ᶜ ∨ x ∈ s₁ᶜ

Tactic:
rw [← mem_union, disj]

Premises used: Set.mem_union
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
⊢ Membership.mem (γ := Set X) univ x

Tactic:
mem_univ _

Premises used: Set.mem_univ
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
⊢ Membership.mem (γ := Set X) univ x

Tactic:
exact mem_univ _

Premises used: Set.mem_univ
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
⊢ x ∈ s₀ᶜ ∨ x ∈ s₁ᶜ

Tactic:
have h : x ∈ s₀ᶜ ∨ x ∈ s₁ᶜ := by
      rw [← mem_union, disj]
      exact mem_univ _
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
h : x ∈ s₀ᶜ ∨ x ∈ s₁ᶜ
left : x ∈ s₀ᶜ → ∃ (i : Fin 2), x ∈ if i = 0 then s₀ᶜ else s₁ᶜ
right : x ∈ s₁ᶜ → ∃ (i : Fin 2), x ∈ if i = 0 then s₀ᶜ else s₁ᶜ
⊢ ∃ (i : Fin 2), x ∈ if i = 0 then s₀ᶜ else s₁ᶜ

Tactic:
apply Or.elim h

Premises used: Or.elim
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
h : x ∈ s₀ᶜ ∨ x ∈ s₁ᶜ
h0 : x ∈ s₀ᶜ
h₁ : x ∈ if Eq (α := Fin 2) 0 0 then s₀ᶜ else s₁ᶜ
⊢ ∃ (i : Fin 2), x ∈ if i = 0 then s₀ᶜ else s₁ᶜ

Tactic:
use 0
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
h : x ∈ s₀ᶜ ∨ x ∈ s₁ᶜ
h0 : x ∈ s₀ᶜ
⊢ x ∈ s₀ᶜ

Tactic:
h0
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
h : x ∈ s₀ᶜ ∨ x ∈ s₁ᶜ
h0 : x ∈ s₀ᶜ
⊢ x ∈ s₀ᶜ

Tactic:
exact h0
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ 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₁ᶜ
h₁ : x ∈ if Eq (α := Fin 2) 1 0 then s₀ᶜ else s₁ᶜ
⊢ ∃ (i : Fin 2), x ∈ if i = 0 then s₀ᶜ else s₁ᶜ

Tactic:
use 1
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ 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₁ᶜ
⊢ x ∈ s₁ᶜ

Tactic:
h1
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ 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₁ᶜ
⊢ x ∈ s₁ᶜ

Tactic:
exact h1
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
⊢ t ⊆ ⋃ (j : Fin 2), so j

Tactic:
have hsot : t ⊆ ⋃ j, so j := by
    rw [hso]
    simp only [Fin.isValue]
    intro x hx
    rw [mem_iUnion]
    rw [← subset_compl_iff_disjoint_right, ← compl_compl s₀, compl_subset_iff_union] at disj
    have h : x ∈ s₀ᶜ ∨ x ∈ s₁ᶜ := by
      rw [← mem_union, disj]
      exact mem_univ _
    apply Or.elim h
    · intro h0
      use 0
      simp only [Fin.isValue, ↓reduceIte]
      exact h0
    · intro h1
      use 1
      simp only [Fin.isValue, one_ne_zero, ↓reduceIte]
      exact h1
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ (j : Fin 2), so j
obtain :
  ∀ (f : Fin 2 → C(X, ℝ)) (f_supp_in_so : ∀ (i : Fin 2), tsupport (α := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ so i)
    (sum_f_one_on_t : EqOn (β := ℝ) (∑ i : Fin 2, (⇑(f i) : (a : X) → ℝ)) 1 t)
    (f_in_icc : ∀ (i : Fin 2) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ))
    (f_hcs : ∀ (i : Fin 2), HasCompactSupport (α := X) (β := ℝ) (⇑(f i) : (a : X) → ℝ)),
    ∃ (f₀ : X →C_c ℝ≥0) (f₁ : X →C_c ℝ≥0),
      EqOn (β := ℝ≥0) (⇑f₀ : (a : X) → ℝ≥0) 1 s₀ ∧
        EqOn (β := ℝ≥0) (⇑f₁ : (a : X) → ℝ≥0) 1 s₁ ∧ EqOn (β := ℝ≥0) (⇑(f₀ + f₁) : (a : X) → ℝ≥0) 1 t
⊢ ∃ (f₀ : X →C_c ℝ≥0) (f₁ : X →C_c ℝ≥0),
    EqOn (β := ℝ≥0) (⇑f₀ : (a : X) → ℝ≥0) 1 s₀ ∧
      EqOn (β := ℝ≥0) (⇑f₁ : (a : X) → ℝ≥0) 1 s₁ ∧ EqOn (β := ℝ≥0) (⇑(f₀ + f₁) : (a : X) → ℝ≥0) 1 t

Tactic:
obtain ⟨f, f_supp_in_so, sum_f_one_on_t, f_in_icc, f_hcs⟩ :=
    exists_continuous_sum_one_of_isOpen_isCompact soopen t_compact hsot

Premises used: exists_continuous_sum_one_of_isOpen_isCompact
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ (j : Fin 2), so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport (α := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ so i
sum_f_one_on_t : EqOn (β := ℝ) (∑ i : Fin 2, (⇑(f i) : (a : X) → ℝ)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ)
f_hcs : ∀ (i : Fin 2), HasCompactSupport (α := X) (β := ℝ) (⇑(f i) : (a : X) → ℝ)
h :
  EqOn (β := ℝ≥0) (⇑{ toContinuousMap := f 1, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) 1 s₀ ∧
    EqOn (β := ℝ≥0) (⇑{ toContinuousMap := f 0, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) 1 s₁ ∧
      EqOn (β := ℝ≥0)
        (⇑({ toContinuousMap := f 1, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart +
              { toContinuousMap := f 0, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart) :
          (a : X) → ℝ≥0)
        1 t
⊢ ∃ (f₀ : X →C_c ℝ≥0) (f₁ : X →C_c ℝ≥0),
    EqOn (β := ℝ≥0) (⇑f₀ : (a : X) → ℝ≥0) 1 s₀ ∧
      EqOn (β := ℝ≥0) (⇑f₁ : (a : X) → ℝ≥0) 1 s₁ ∧ EqOn (β := ℝ≥0) (⇑(f₀ + f₁) : (a : X) → ℝ≥0) 1 t

Tactic:
use (nnrealPart (⟨f 1, f_hcs 1⟩ : C_c(X, ℝ))),
    (nnrealPart (⟨f 0, f_hcs 0⟩ : C_c(X, ℝ)))

Premises used: CompactlySupportedContinuousMap.nnrealPart, OfNat.ofNat, CompactlySupportedContinuousMap.mk
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ (j : Fin 2), so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport (α := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ so i
sum_f_one_on_t : EqOn (β := ℝ) (∑ i : Fin 2, (⇑(f i) : (a : X) → ℝ)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ)
f_hcs : ∀ (i : Fin 2), HasCompactSupport (α := X) (β := ℝ) (⇑(f i) : (a : X) → ℝ)
h :
  EqOn (β := ℝ≥0) (⇑{ toContinuousMap := f 1, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) 1 s₀ ∧
    EqOn (β := ℝ≥0) (⇑{ toContinuousMap := f 0, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) 1 s₁ ∧
      EqOn
        (HAdd.hAdd (α := (a : X) → ℝ≥0)
          (⇑{ toContinuousMap := f 1, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0)
          (⇑{ toContinuousMap := f 0, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0))
        1 t
⊢ EqOn (β := ℝ≥0) (⇑{ toContinuousMap := f 1, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) 1 s₀ ∧
    EqOn (β := ℝ≥0) (⇑{ toContinuousMap := f 0, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) 1 s₁ ∧
      EqOn (β := ℝ≥0)
        (⇑({ toContinuousMap := f 1, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart +
              { toContinuousMap := f 0, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart) :
          (a : X) → ℝ≥0)
        1 t

Tactic:
simp only [Fin.isValue, CompactlySupportedContinuousMap.coe_add]

Premises used: Fin.isValue, CompactlySupportedContinuousMap.coe_add
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ (j : Fin 2), so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport (α := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ so i
sum_f_one_on_t : EqOn (β := ℝ) (∑ i : Fin 2, (⇑(f i) : (a : X) → ℝ)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ)
f_hcs : ∀ (i : Fin 2), HasCompactSupport (α := X) (β := ℝ) (⇑(f i) : (a : X) → ℝ)
x : X
hx : x ∈ t
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) = 1

Tactic:
simpa only [Finset.sum_apply, Fin.sum_univ_two, Fin.isValue, Pi.one_apply]
      using sum_f_one_on_t hx

Premises used: Pi.one_apply, Finset.sum_apply, Fin.isValue, Fin.sum_univ_two
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ (j : Fin 2), so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport (α := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ so i
sum_f_one_on_t : EqOn (β := ℝ) (∑ i : Fin 2, (⇑(f i) : (a : X) → ℝ)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ)
f_hcs : ∀ (i : Fin 2), HasCompactSupport (α := X) (β := ℝ) (⇑(f i) : (a : X) → ℝ)
⊢ ∀ (x : X) (hx : x ∈ t), HAdd.hAdd (α := ℝ) (β := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) = 1

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
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ (j : Fin 2), so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport (α := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ so i
sum_f_one_on_t : EqOn (β := ℝ) (∑ i : Fin 2, (⇑(f i) : (a : X) → ℝ)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ)
f_hcs : ∀ (i : Fin 2), HasCompactSupport (α := X) (β := ℝ) (⇑(f i) : (a : X) → ℝ)
sum_one_x :
  ∀ (x : X) (hx : x ∈ t), HAdd.hAdd (α := ℝ) (β := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) = 1
⊢ EqOn (β := ℝ≥0) (⇑{ toContinuousMap := f 1, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) 1 s₀ ∧
    EqOn (β := ℝ≥0) (⇑{ toContinuousMap := f 0, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) 1 s₁ ∧
      EqOn
        (HAdd.hAdd (α := (a : X) → ℝ≥0)
          (⇑{ toContinuousMap := f 1, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0)
          (⇑{ toContinuousMap := f 0, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0))
        1 t

Tactic:
⟨?_, ?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : 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 : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ (j : Fin 2), so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport (α := ℝ) (⇑(f i) : (a : X) → ℝ) ⊆ so i
sum_f_one_on_t : EqOn (β := ℝ) (∑ i : Fin 2, (⇑(f i) : (a : X) → ℝ)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f i : (a : X) → ℝ) x : ℝ)
f_hcs : ∀ (i : Fin 2), HasCompactSupport (α := X) (β := ℝ) (⇑(f i) : (a : X) → ℝ)
sum_one_x :
  ∀ (x : X) (hx : x ∈ t), HAdd.hAdd (α := ℝ) (β := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) = 1
h : EqOn (β := ℝ≥0) (⇑{ toContinuousMap := f 1, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) 1 s₀
h₁ : EqOn (β := ℝ≥0) (⇑{ toContinuousMap := f 0, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) 1 s₁
h₂ :
  EqOn
    (HAdd.hAdd (α := (a : X) → ℝ≥0)
      (⇑{ toContinuousMap := f 1, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0)
      (⇑{ toContinuousMap := f 0, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0))
    1 t
⊢ EqOn (β := ℝ≥0) (⇑{ toContinuousMap := f 1, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) 1 s₀ ∧
    EqOn (β := ℝ≥0) (⇑{ toContinuousMap := f 0, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) 1 s₁ ∧
      EqOn
        (HAdd.hAdd (α := (a : X) → ℝ≥0)
          (⇑{ toContinuousMap := f 1, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0)
          (⇑{ toContinuousMap := f 0, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0))
        1 t

Tactic:
refine ⟨?_, ?_, ?_⟩