awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₀
⊢ Eq (α := ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) (1 : ℝ)
have this : 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
-- 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₀
this : Eq (α := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) (1 : ℝ)
have 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 : ℝ)
Tactic: rw [union_subset_iff] at hst
Cleared hypotheses: hst, so, hso, soopen, hsot, f, f_supp_in_so, sum_f_one_on_t, f_in_icc, f_hcs, sum_one_x, x, hx, this
-- 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₀ ⊆ 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 : ℝ)
⊢ Eq (α := ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) (1 : ℝ)
have h : (f 1 : (a : X) → ℝ) x = HAdd.hAdd (α := ℝ) (β := ℝ) (0 : ℝ) ((f 1 : (a : X) → ℝ) x : ℝ)
Tactic: rw [← sum_one_x x (mem_of_subset_of_mem hst.1 hx), this]
-- 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 0, hasCompactSupport' := ⋯ : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) x : ℝ≥0)
    (1 x : ℝ≥0)
have h : Eq (α := ℝ) ((f 0 : (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 1 : (a : X) → ℝ) x : ℝ) (0 : ℝ)
have rw : x ∉ support (M := ℝ) (⇑(f 1) : (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 1) : (a : X) → ℝ))ᶜ
have apply : s₁ ⊆ (so 1)ᶜ
Tactic: apply subset_trans _ (compl_subset_compl.mpr (f_supp_in_so 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)
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 1) : (a : X) → ℝ)
have this : 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]
-- 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₁
⊢ Eq (α := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) (1 : ℝ)
have this : 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
-- 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₁
this : Eq (α := ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) (1 : ℝ)
have 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 : ℝ)
Tactic: rw [union_subset_iff] at hst
Cleared hypotheses: hst, so, hso, soopen, hsot, f, f_supp_in_so, sum_f_one_on_t, f_in_icc, f_hcs, sum_one_x, x, hx, this
-- 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₀ ⊆ 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 : ℝ)
⊢ Eq (α := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) (1 : ℝ)
have h : (f 0 : (a : X) → ℝ) x = HAdd.hAdd (α := ℝ) (β := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) (0 : ℝ)
Tactic: rw [← sum_one_x x (mem_of_subset_of_mem hst.2 hx), this]
-- 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 ∈ t
⊢ 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
have h : Real.toNNReal ((f 1 : (a : X) → ℝ) x) + Real.toNNReal ((f 0 : (a : X) → ℝ) x) = 1
Tactic: simp only [Fin.isValue, Pi.add_apply, nnrealPart_apply,
      CompactlySupportedContinuousMap.coe_mk, Pi.one_apply]
-- 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 ∈ t
⊢ Real.toNNReal ((f 1 : (a : X) → ℝ) x) + Real.toNNReal ((f 0 : (a : X) → ℝ) x) = 1
have h : (HAdd.hAdd (α := ℝ) (β := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) ((f 1 : (a : X) → ℝ) x : ℝ)).toNNReal = 1
Tactic: rw [Real.toNNReal_add_toNNReal (f_in_icc 1 x).1 (f_in_icc 0 x).1, add_comm]
-- 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 ∈ t
⊢ (HAdd.hAdd (α := ℝ) (β := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) ((f 1 : (a : X) → ℝ) x : ℝ)).toNNReal = 1
have h : HAdd.hAdd (α := ℝ) (β := ℝ) ((f 0 : (a : X) → ℝ) x : ℝ) ((f 1 : (a : X) → ℝ) x : ℝ) = 1
Tactic: simp only [Fin.isValue, Real.toNNReal_eq_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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₂
have refine : rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ rieszContentAux Λ (K₁ ⊔ K₂)
Tactic: refine le_antisymm (rieszContentAux_sup_le Λ K₁ K₂) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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₂)
have 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
Tactic: refine le_csInf (rieszContentAux_image_nonempty Λ (K₁ ⊔ K₂)) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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
⊢ 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
have 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
Tactic: ⟨f, ⟨hf, Λf_eq_b⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (hypothesis)
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
⊢ rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ b
have hsuppf : ∀ 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (hypothesis)
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
⊢ rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ b
have hsubsuppf : (↑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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic (goal)
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
hsubsuppf : (↑K₁ : Set X) ∪ (↑K₂ : Set X) ⊆ tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)
⊢ rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ b
have obtain : ∀ (g₁ g₂ : X →C_c ℝ≥0) (hg₁ : EqOn (β := ℝ≥0) (⇑g₁ : (a : X) → ℝ≥0) 1 K₁.carrier)
  (hg₂ : EqOn (β := ℝ≥0) (⇑g₂ : (a : X) → ℝ≥0) 1 K₂.carrier)
  (sum_g : EqOn (β := ℝ≥0) (⇑(g₁ + g₂) : (a : X) → ℝ≥0) 1 (tsupport f.toFun)),
  rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ b
Tactic: obtain ⟨g₁, g₂, hg₁, hg₂, sum_g⟩ := exists_continuous_add_one_of_isCompact_nnreal K₁.isCompact'
    K₂.isCompact' f.hasCompactSupport'.isCompact disj hsubsuppf