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₁ᶜ
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 1) : (a : X) → ℝ))ᶜ

Tactic:
have : s₁ ⊆ (tsupport (f 1))ᶜ := by
        apply subset_trans _ (compl_subset_compl.mpr (f_supp_in_so 1))
        rw [hso]
        simp only [Fin.isValue, one_ne_zero, ↓reduceIte, compl_compl, subset_refl]
-- 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
x : X
hx : x ∈ s₁
this : s₁ ⊆ (tsupport (α := ℝ) (⇑(f 1) : (a : X) → ℝ))ᶜ
⊢ Membership.mem (γ := Set X) (support (M := ℝ) (⇑(f 1) : (a : X) → ℝ))ᶜ x

Tactic:
mem_of_subset_of_mem (subset_trans this (compl_subset_compl_of_subset subset_closure))
        hx

Premises used: Set.compl_subset_compl_of_subset, subset_closure, subset_trans, Set.mem_of_subset_of_mem
-- 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
x : X
hx : x ∈ s₁
this : s₁ ⊆ (tsupport (α := ℝ) (⇑(f 1) : (a : X) → ℝ))ᶜ
⊢ Membership.mem (γ := Set X) (support (M := ℝ) (⇑(f 1) : (a : X) → ℝ))ᶜ x

Tactic:
exact mem_of_subset_of_mem (subset_trans this (compl_subset_compl_of_subset subset_closure))
        hx

Premises used: Set.compl_subset_compl_of_subset, subset_closure, subset_trans, Set.mem_of_subset_of_mem
-- 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
x : X
hx : x ∈ s₁
⊢ Eq (α := ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
have : (f 1) x = 0 := by
      rw [← notMem_support]
      have : s₁ ⊆ (tsupport (f 1))ᶜ := by
        apply subset_trans _ (compl_subset_compl.mpr (f_supp_in_so 1))
        rw [hso]
        simp only [Fin.isValue, one_ne_zero, ↓reduceIte, compl_compl, subset_refl]
      apply notMem_of_mem_compl
      exact mem_of_subset_of_mem (subset_trans this (compl_subset_compl_of_subset subset_closure))
        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
x : X
hx : x ∈ s₁
this : Eq (α := ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) (0 : ℝ)
h :
  ∀ (hst : s₀ ⊆ t ∧ 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))
      (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₁) (this : Eq (α := ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) (0 : ℝ)),
      Eq (α := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) (1 : ℝ)
⊢ Eq (α := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
rw [union_subset_iff] at hst

Premises used: Set.union_subset_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₀ ⊆ t ∧ 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₁
this : Eq (α := ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) (0 : ℝ)
h : (f 0 : (a : X) → ℝ) x = HAdd.hAdd (α := ℝ) (β := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) (1 : ℝ)

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

Premises used: Set.mem_of_subset_of_mem, And.right
-- 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₀ ⊆ t ∧ 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₁
this : Eq (α := ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ (f 0 : (a : X) → ℝ) x = HAdd.hAdd (α := ℝ) (β := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
Eq.symm (AddMonoid.add_zero ((f 0) x))

Premises used: AddMonoid.add_zero, OfNat.ofNat, Eq.symm, DFunLike.coe
-- 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₀ ⊆ t ∧ 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₁
this : Eq (α := ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ (f 0 : (a : X) → ℝ) x = HAdd.hAdd (α := ℝ) (β := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
exact Eq.symm (AddMonoid.add_zero ((f 0) x))

Premises used: AddMonoid.add_zero, OfNat.ofNat, Eq.symm, DFunLike.coe
-- 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
x : X
hx : x ∈ t
h : Real.toNNReal ((f 1 : (a : X) → ℝ) x) + Real.toNNReal ((f 0 : (a : X) → ℝ) x) = 1
⊢ HAdd.hAdd (α := (a : X) → ℝ≥0) (β := (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) x =
    1 x

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

Premises used: CompactlySupportedContinuousMap.coe_mk, Pi.one_apply, Pi.add_apply, Fin.isValue, CompactlySupportedContinuousMap.nnrealPart_apply
-- 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
x : X
hx : x ∈ t
h : (HAdd.hAdd (α := ℝ) (β := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) ((f 1 : (a : X) → ℝ) x : ℝ)).toNNReal = 1
⊢ Real.toNNReal ((f 1 : (a : X) → ℝ) x) + Real.toNNReal ((f 0 : (a : X) → ℝ) x) = 1

Tactic:
rw [Real.toNNReal_add_toNNReal (f_in_icc 1 x).1 (f_in_icc 0 x).1, add_comm]

Premises used: add_comm, And.left, Real.toNNReal_add_toNNReal, OfNat.ofNat
-- 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
x : X
hx : x ∈ t
h : HAdd.hAdd (α := ℝ) (β := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) = 1
⊢ (HAdd.hAdd (α := ℝ) (β := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) ((f 1 : (a : X) → ℝ) x : ℝ)).toNNReal = 1

Tactic:
simp only [Fin.isValue, Real.toNNReal_eq_one]

Premises used: Fin.isValue, Real.toNNReal_eq_one
-- 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
x : X
hx : x ∈ t
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) = 1

Tactic:
sum_one_x x 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
x : X
hx : x ∈ t
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) = 1

Tactic:
exact sum_one_x x hx
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint (↑K₁ : Set X) (↑K₂ : Set X)
⊢ rieszContentAux Λ (K₁ ⊔ K₂) = rieszContentAux Λ K₁ + rieszContentAux Λ K₂

Tactic:
le_antisymm (rieszContentAux_sup_le Λ K₁ K₂) ?_

Premises used: rieszContentAux_sup_le, le_antisymm
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint (↑K₁ : Set X) (↑K₂ : Set X)
refine : rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ rieszContentAux Λ (K₁ ⊔ K₂)
⊢ rieszContentAux Λ (K₁ ⊔ K₂) = rieszContentAux Λ K₁ + rieszContentAux Λ K₂

Tactic:
refine le_antisymm (rieszContentAux_sup_le Λ K₁ K₂) ?_

Premises used: rieszContentAux_sup_le, le_antisymm
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint (↑K₁ : Set X) (↑K₂ : Set X)
⊢ rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ rieszContentAux Λ (K₁ ⊔ K₂)

Tactic:
le_csInf (rieszContentAux_image_nonempty Λ (K₁ ⊔ K₂)) ?_

Premises used: rieszContentAux_image_nonempty, le_csInf, rieszContentAux, Max.max
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint (↑K₁ : Set X) (↑K₂ : Set X)
refine :
  ∀ (b : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0)
        (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
          {f : X →C_c ℝ≥0 | ∀ x ∈ K₁ ⊔ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)})
        b →
      rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ b
⊢ rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ rieszContentAux Λ (K₁ ⊔ K₂)

Tactic:
refine le_csInf (rieszContentAux_image_nonempty Λ (K₁ ⊔ K₂)) ?_

Premises used: rieszContentAux_image_nonempty, le_csInf, Max.max
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint (↑K₁ : Set X) (↑K₂ : Set X)
b : ℝ≥0
this :
  ∀ (f : X →C_c ℝ≥0)
    (hf :
      Membership.mem (γ := Set (X →C_c ℝ≥0))
        {f : X →C_c ℝ≥0 | ∀ x ∈ K₁ ⊔ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)} f)
    (Λf_eq_b : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f = b), rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ b
⊢ Membership.mem (γ := Set ℝ≥0)
      (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
        {f : X →C_c ℝ≥0 | ∀ x ∈ K₁ ⊔ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)})
      b →
    rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ b

Tactic:
⟨f, ⟨hf, Λf_eq_b⟩⟩
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint (↑K₁ : Set X) (↑K₂ : Set X)
b : ℝ≥0
f : X →C_c ℝ≥0
hf :
  Membership.mem (γ := Set (X →C_c ℝ≥0))
    {f : X →C_c ℝ≥0 | ∀ x ∈ K₁ ⊔ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)} f
Λf_eq_b : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f = b
x : X
hx : x ∈ K₁ ⊔ K₂
⊢ Ne (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)

Tactic:
ne_of_gt <| lt_of_lt_of_le (zero_lt_one' ℝ≥0) (hf x hx)

Premises used: ne_of_gt, NNReal, zero_lt_one', lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint (↑K₁ : Set X) (↑K₂ : Set X)
b : ℝ≥0
f : X →C_c ℝ≥0
hf :
  Membership.mem (γ := Set (X →C_c ℝ≥0))
    {f : X →C_c ℝ≥0 | ∀ x ∈ K₁ ⊔ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)} f
Λf_eq_b : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f = b
x : X
hx : x ∈ K₁ ⊔ K₂
⊢ Ne (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)

Tactic:
exact ne_of_gt <| lt_of_lt_of_le (zero_lt_one' ℝ≥0) (hf x hx)

Premises used: ne_of_gt, NNReal, zero_lt_one', lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint (↑K₁ : Set X) (↑K₂ : Set X)
b : ℝ≥0
f : X →C_c ℝ≥0
hf :
  Membership.mem (γ := Set (X →C_c ℝ≥0))
    {f : X →C_c ℝ≥0 | ∀ x ∈ K₁ ⊔ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)} f
Λf_eq_b : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f = b
⊢ ∀ x ∈ K₁ ⊔ K₂, Membership.mem (γ := Set X) (support (M := ℝ≥0) (⇑f : (a : X) → ℝ≥0)) x

Tactic:
have hsuppf : ∀ x ∈ K₁ ⊔ K₂, x ∈ support f := by
    intro x hx
    rw [mem_support]
    exact ne_of_gt <| lt_of_lt_of_le (zero_lt_one' ℝ≥0) (hf x hx)
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint (↑K₁ : Set X) (↑K₂ : Set X)
b : ℝ≥0
f : X →C_c ℝ≥0
hf :
  Membership.mem (γ := Set (X →C_c ℝ≥0))
    {f : X →C_c ℝ≥0 | ∀ x ∈ K₁ ⊔ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)} f
Λf_eq_b : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, Membership.mem (γ := Set X) (support (M := ℝ≥0) (⇑f : (a : X) → ℝ≥0)) x
⊢ (↑K₁ : Set X) ∪ (↑K₂ : Set X) ⊆ tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)

Tactic:
have hsubsuppf : (K₁ : Set X) ∪ (K₂ : Set X) ⊆ tsupport f := subset_trans hsuppf subset_closure