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₀
h : Eq (α := ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) (1 : ℝ)
⊢ Eq (α := ℝ≥0) (({ toContinuousMap := f 1, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) x : ℝ≥0)
    (1 x : ℝ≥0)

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

Premises used: CompactlySupportedContinuousMap.coe_mk, Pi.one_apply, Fin.isValue, CompactlySupportedContinuousMap.nnrealPart_apply, 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 ∈ s₀
rw : x ∉ support (M := ℝ) (⇑(f 0) : (a : X) → ℝ)
⊢ Eq (α := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
rw [← notMem_support]

Premises used: Function.notMem_support
-- 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₀
apply : s₀ ⊆ (so 0)ᶜ
⊢ s₀ ⊆ (tsupport (α := ℝ) (⇑(f 0) : (a : X) → ℝ))ᶜ

Tactic:
apply subset_trans _ (compl_subset_compl.mpr (f_supp_in_so 0))

Premises used: Iff.mpr, subset_trans, Set.compl_subset_compl, 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 ∈ s₀
rw : s₀ ⊆ ((fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ) 0)ᶜ
⊢ s₀ ⊆ (so 0)ᶜ

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)
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₀ ⊆ ((fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ) 0)ᶜ

Tactic:
simp only [Fin.isValue, ↓reduceIte, compl_compl, subset_refl]

Premises used: compl_compl, subset_refl, Fin.isValue, reduceIte
-- 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 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]
-- 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 0) : (a : X) → ℝ))ᶜ
⊢ Membership.mem (γ := Set X) (support (M := ℝ) (⇑(f 0) : (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 0) : (a : X) → ℝ))ᶜ
⊢ Membership.mem (γ := Set X) (support (M := ℝ) (⇑(f 0) : (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 0 : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
have : (f 0) x = 0 := by
      rw [← notMem_support]
      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]
      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 0 : (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 0 : (a : X) → ℝ) x : ℝ) (0 : ℝ)),
      Eq (α := ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) (1 : ℝ)
⊢ Eq (α := ℝ) ((f 1 : (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 0 : (a : X) → ℝ) x : ℝ) (0 : ℝ)
h : (f 1 : (a : X) → ℝ) x = HAdd.hAdd (α := ℝ) (β := ℝ) (0 : ℝ) ((f 1 : (a : X) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) (1 : ℝ)

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

Premises used: Set.mem_of_subset_of_mem, And.left
-- 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 0 : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ (f 1 : (a : X) → ℝ) x = HAdd.hAdd (α := ℝ) (β := ℝ) (0 : ℝ) ((f 1 : (a : X) → ℝ) x : ℝ)

Tactic:
Eq.symm (AddZeroClass.zero_add ((f 1) x))

Premises used: AddZeroClass.zero_add, 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 0 : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ (f 1 : (a : X) → ℝ) x = HAdd.hAdd (α := ℝ) (β := ℝ) (0 : ℝ) ((f 1 : (a : X) → ℝ) x : ℝ)

Tactic:
exact Eq.symm (AddZeroClass.zero_add ((f 1) x))

Premises used: AddZeroClass.zero_add, 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 ∈ s₁
h : Eq (α := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) (1 : ℝ)
⊢ Eq (α := ℝ≥0) (({ toContinuousMap := f 0, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) x : ℝ≥0)
    (1 x : ℝ≥0)

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

Premises used: CompactlySupportedContinuousMap.coe_mk, Pi.one_apply, Fin.isValue, CompactlySupportedContinuousMap.nnrealPart_apply, 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 ∈ s₁
rw : x ∉ support (M := ℝ) (⇑(f 1) : (a : X) → ℝ)
⊢ Eq (α := ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
rw [← notMem_support]

Premises used: Function.notMem_support
-- 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₁
apply : s₁ ⊆ (so 1)ᶜ
⊢ s₁ ⊆ (tsupport (α := ℝ) (⇑(f 1) : (a : X) → ℝ))ᶜ

Tactic:
apply subset_trans _ (compl_subset_compl.mpr (f_supp_in_so 1))

Premises used: Iff.mpr, subset_trans, Set.compl_subset_compl, 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 ∈ s₁
rw : s₁ ⊆ ((fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ) 1)ᶜ
⊢ s₁ ⊆ (so 1)ᶜ

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)
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₁ ⊆ ((fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ) 1)ᶜ

Tactic:
simp only [Fin.isValue, one_ne_zero, ↓reduceIte, compl_compl, subset_refl]

Premises used: compl_compl, subset_refl, Fin.isValue, reduceIte, one_ne_zero