awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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
⊢ ∃ (i : Fin 2), x ∈ if i = 0 then s₀ᶜ else s₁ᶜ
have 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₁ᶜ
Tactic: rw [← subset_compl_iff_disjoint_right, ← compl_compl s₀, compl_subset_iff_union] at disj
Cleared hypotheses: disj, hst, so, hso, soopen, x, hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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₁ᶜ
have rw : Membership.mem (γ := Set X) univ x
Tactic: rw [← mem_union, disj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (hypothesis)
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
⊢ ∃ (i : Fin 2), x ∈ if i = 0 then s₀ᶜ else s₁ᶜ
have h : x ∈ s₀ᶜ ∨ x ∈ s₁ᶜ
Tactic: have h : x ∈ s₀ᶜ ∨ x ∈ s₁ᶜ := by
      rw [← mem_union, disj]
      exact mem_univ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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₁ᶜ
⊢ ∃ (i : Fin 2), x ∈ if i = 0 then s₀ᶜ else s₁ᶜ
have left : x ∈ s₀ᶜ → ∃ (i : Fin 2), x ∈ if i = 0 then s₀ᶜ else s₁ᶜ
Tactic: apply Or.elim h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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₁ᶜ
⊢ ∃ (i : Fin 2), x ∈ if i = 0 then s₀ᶜ else s₁ᶜ
have right : x ∈ s₁ᶜ → ∃ (i : Fin 2), x ∈ if i = 0 then s₀ᶜ else s₁ᶜ
Tactic: apply Or.elim h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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₀ᶜ
⊢ ∃ (i : Fin 2), x ∈ if i = 0 then s₀ᶜ else s₁ᶜ
have h₁ : x ∈ if Eq (α := Fin 2) 0 0 then s₀ᶜ else s₁ᶜ
Tactic: use 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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₁ᶜ
⊢ ∃ (i : Fin 2), x ∈ if i = 0 then s₀ᶜ else s₁ᶜ
have h₁ : x ∈ if Eq (α := Fin 2) 1 0 then s₀ᶜ else s₁ᶜ
Tactic: use 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (hypothesis)
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)
⊢ ∃ (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
have hsot : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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₀ : 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
have 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
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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) → ℝ)
⊢ ∃ (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
have h : EqOn (β := ℝ≥0) (⇑{ toContinuousMap := f 1, hasCompactSupport' := sorry : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) 1 s₀ ∧
  EqOn (β := ℝ≥0) (⇑{ toContinuousMap := f 0, hasCompactSupport' := sorry : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) 1 s₁ ∧
    EqOn (β := ℝ≥0)
      (⇑({ toContinuousMap := f 1, hasCompactSupport' := sorry : X →C_c ℝ }.nnrealPart +
            { toContinuousMap := f 0, hasCompactSupport' := sorry : X →C_c ℝ }.nnrealPart) :
        (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, ℝ)))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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) → ℝ)
⊢ 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
have h : EqOn (β := ℝ≥0) (⇑{ toContinuousMap := f 1, hasCompactSupport' := sorry : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) 1 s₀ ∧
  EqOn (β := ℝ≥0) (⇑{ toContinuousMap := f 0, hasCompactSupport' := sorry : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) 1 s₁ ∧
    EqOn
      (HAdd.hAdd (α := (a : X) → ℝ≥0)
        (⇑{ toContinuousMap := f 1, hasCompactSupport' := sorry : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0)
        (⇑{ toContinuousMap := f 0, hasCompactSupport' := sorry : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0))
      1 t
Tactic: simp only [Fin.isValue, CompactlySupportedContinuousMap.coe_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (hypothesis)
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) → ℝ)
⊢ 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
have sum_one_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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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
have h : EqOn (β := ℝ≥0) (⇑{ toContinuousMap := f 1, hasCompactSupport' := sorry : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) 1 s₀
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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₀
⊢ 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
have h₁ : EqOn (β := ℝ≥0) (⇑{ toContinuousMap := f 0, hasCompactSupport' := sorry : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) 1 s₁
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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₁
⊢ 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
have h₂ : EqOn
  (HAdd.hAdd (α := (a : X) → ℝ≥0)
    (⇑{ toContinuousMap := f 1, hasCompactSupport' := sorry : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0)
    (⇑{ toContinuousMap := f 0, hasCompactSupport' := sorry : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0))
  1 t
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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
x : X
hx : x ∈ s₀
⊢ Eq (α := ℝ≥0) (({ toContinuousMap := f 1, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) x : ℝ≥0)
    (1 x : ℝ≥0)
have h : Eq (α := ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) (1 : ℝ)
Tactic: simp only [Fin.isValue, nnrealPart_apply,
      CompactlySupportedContinuousMap.coe_mk, Pi.one_apply, Real.toNNReal_eq_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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
x : X
hx : x ∈ s₀
⊢ Eq (α := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) (0 : ℝ)
have rw : x ∉ support (M := ℝ) (⇑(f 0) : (a : X) → ℝ)
Tactic: rw [← notMem_support]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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
x : X
hx : x ∈ s₀
⊢ s₀ ⊆ (tsupport (α := ℝ) (⇑(f 0) : (a : X) → ℝ))ᶜ
have apply : s₀ ⊆ (so 0)ᶜ
Tactic: apply subset_trans _ (compl_subset_compl.mpr (f_supp_in_so 0))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (hypothesis)
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
x : X
hx : x ∈ s₀
⊢ x ∉ support (M := ℝ) (⇑(f 0) : (a : X) → ℝ)
have this : s₀ ⊆ (tsupport (α := ℝ) (⇑(f 0) : (a : X) → ℝ))ᶜ
Tactic: have : s₀ ⊆ (tsupport (f 0))ᶜ := by
        apply subset_trans _ (compl_subset_compl.mpr (f_supp_in_so 0))
        rw [hso]
        simp only [Fin.isValue, ↓reduceIte, compl_compl, subset_refl]