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
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
f : C(X, ℝ)
hsuppfsubV : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ interior V
hfeq1onK : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K.carrier
hfinicc : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfHasCompactSupport : HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ)
⊢ Set.Nonempty.{u_1} (α := X →C_c ℝ≥0)
    {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)}
have h : Membership.mem (γ := Set (X →C_c ℝ≥0))
  {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)}
  { toContinuousMap := f, hasCompactSupport' := hfHasCompactSupport : X →C_c ℝ }.nnrealPart
Tactic: use nnrealPart ⟨f, hfHasCompactSupport⟩
-- 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 : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
f : C(X, ℝ)
hsuppfsubV : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ interior V
hfeq1onK : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K.carrier
hfinicc : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfHasCompactSupport : HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ)
x : X
hx : x ∈ K
⊢ LE.le (α := ℝ≥0) (1 : ℝ≥0)
    (({ toContinuousMap := f, hasCompactSupport' := hfHasCompactSupport : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) x :
      ℝ≥0)
have h : Eq (α := ℝ≥0) (1 : ℝ≥0)
  (({ toContinuousMap := f, hasCompactSupport' := hfHasCompactSupport : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) x : ℝ≥0)
Tactic: apply le_of_eq
-- 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 : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
f : C(X, ℝ)
hsuppfsubV : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ interior V
hfeq1onK : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K.carrier
hfinicc : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfHasCompactSupport : HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ)
x : X
hx : x ∈ K
⊢ Eq (α := ℝ≥0) (1 : ℝ≥0)
    (({ toContinuousMap := f, hasCompactSupport' := hfHasCompactSupport : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) x :
      ℝ≥0)
have h : 1 = Real.toNNReal ((f : (a : X) → ℝ) x)
Tactic: simp only [nnrealPart_apply, CompactlySupportedContinuousMap.coe_mk]
-- 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 : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
f : C(X, ℝ)
hsuppfsubV : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ interior V
hfeq1onK : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K.carrier
hfinicc : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfHasCompactSupport : HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ)
x : X
hx : x ∈ K
⊢ 1 = Real.toNNReal ((f : (a : X) → ℝ) x)
have h : Eq (α := ℝ) (1 : ℝ) ((f : (a : X) → ℝ) x : ℝ)
Tactic: rw [← Real.toNNReal_one, Real.toNNReal_eq_toNNReal_iff (zero_le_one' ℝ) (hfinicc x).1]
-- 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
h : K₁ ≤ K₂
⊢ LE.le (α := ℝ≥0)
    (sInf
      (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
        {f : X →C_c ℝ≥0 | ∀ x ∈ K₁, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)}))
    (sInf
      (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
        {f : X →C_c ℝ≥0 | ∀ x ∈ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)}))
have h₁ : Set.Nonempty (α := ℝ≥0)
  (image (α := X →C_c ℝ≥0) (⇑Λ : (a : X →C_c ℝ≥0) → ℝ≥0)
    {f : X →C_c ℝ≥0 | ∀ x ∈ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)})
Tactic: gcongr
-- 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 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
⊢ ∃ (f : X →C_c ℝ≥0),
    (∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
      (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f < rieszContentAux Λ K + ε
have obtain : ∀ (α : ℝ≥0) (α_hyp : α < rieszContentAux Λ K + ε) (f : X →C_c ℝ≥0)
  (f_hyp :
    Membership.mem (γ := Set (X →C_c ℝ≥0))
        {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)} f ∧
      (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f = α),
  ∃ (f : X →C_c ℝ≥0),
    (∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
      (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f < rieszContentAux Λ K + ε
Tactic: obtain ⟨α, ⟨⟨f, f_hyp⟩, α_hyp⟩⟩ :=
    exists_lt_of_csInf_lt (rieszContentAux_image_nonempty Λ K)
      (lt_add_of_pos_right (rieszContentAux Λ K) εpos)
-- 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 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
α : ℝ≥0
α_hyp : α < rieszContentAux Λ K + ε
f : X →C_c ℝ≥0
f_hyp :
  Membership.mem (γ := Set (X →C_c ℝ≥0))
      {f : X →C_c ℝ≥0 | ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)} f ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f = α
⊢ ∃ (f : X →C_c ℝ≥0),
    (∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
      (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f < rieszContentAux Λ K + ε
have refine : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f < rieszContentAux Λ K + ε
Tactic: refine ⟨f, f_hyp.left, ?_⟩
-- 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
K1 K2 : Compacts X
⊢ rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2
have h : ∀ (ε : ℝ≥0), 0 < ε → rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
Tactic: apply _root_.le_of_forall_pos_le_add
-- 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
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
⊢ rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
have h : ∀ (f1 : X →C_c ℝ≥0)
  (f_test_function_K1 :
    (∀ x ∈ K1, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
      (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f1 < rieszContentAux Λ K1 + ε / 2),
  rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
Tactic: obtain ⟨f1, f_test_function_K1⟩ := exists_lt_rieszContentAux_add_pos Λ K1 (half_pos εpos)
-- 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
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →C_c ℝ≥0
f_test_function_K1 :
  (∀ x ∈ K1, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f1 < rieszContentAux Λ K1 + ε / 2
⊢ rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
have h : ∀ (f2 : X →C_c ℝ≥0)
  (f_test_function_K2 :
    (∀ x ∈ K2, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f2 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
      (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f2 < rieszContentAux Λ K2 + ε / 2),
  rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
Tactic: obtain ⟨f2, f_test_function_K2⟩ := exists_lt_rieszContentAux_add_pos Λ K2 (half_pos εpos)
-- 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
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →C_c ℝ≥0
f_test_function_K1 :
  (∀ x ∈ K1, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →C_c ℝ≥0
f_test_function_K2 :
  (∀ x ∈ K2, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f2 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f2 < rieszContentAux Λ K2 + ε / 2
⊢ rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
have f_test_function_union : ∀ x ∈ K1 ⊔ K2, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 + f2 : (a : X) → ℝ≥0) x : ℝ≥0)
Tactic: have f_test_function_union : ∀ x ∈ K1 ⊔ K2, (1 : ℝ≥0) ≤ (f1 + f2) x := by
    rintro x (x_in_K1 | x_in_K2)
    · exact le_add_right (f_test_function_K1.left x x_in_K1)
    · exact le_add_left (f_test_function_K2.left x x_in_K2)
-- 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
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →C_c ℝ≥0
f_test_function_K1 :
  (∀ x ∈ K1, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →C_c ℝ≥0
f_test_function_K2 :
  (∀ x ∈ K2, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f2 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f2 < rieszContentAux Λ K2 + ε / 2
f_test_function_union : ∀ x ∈ K1 ⊔ K2, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 + f2 : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
have apply : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (f1 + f2) < rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
Tactic: apply (rieszContentAux_le Λ f_test_function_union).trans (le_of_lt _)
-- 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
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →C_c ℝ≥0
f_test_function_K1 :
  (∀ x ∈ K1, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →C_c ℝ≥0
f_test_function_K2 :
  (∀ x ∈ K2, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f2 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f2 < rieszContentAux Λ K2 + ε / 2
f_test_function_union : ∀ x ∈ K1 ⊔ K2, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 + f2 : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (f1 + f2) < rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
have rw : HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f1 : ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f2 : ℝ≥0) <
  rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
Tactic: rw [map_add]
-- 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
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →C_c ℝ≥0
f_test_function_K1 :
  (∀ x ∈ K1, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →C_c ℝ≥0
f_test_function_K2 :
  (∀ x ∈ K2, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f2 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f2 < rieszContentAux Λ K2 + ε / 2
f_test_function_union : ∀ x ∈ K1 ⊔ K2, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 + f2 : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f1 : ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f2 : ℝ≥0) <
    rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
have apply : rieszContentAux Λ K1 + ε / 2 + (rieszContentAux Λ K2 + ε / 2) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
Tactic: apply lt_of_lt_of_le (_root_.add_lt_add f_test_function_K1.right f_test_function_K2.right)
    (le_of_eq _)
-- 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
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →C_c ℝ≥0
f_test_function_K1 :
  (∀ x ∈ K1, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →C_c ℝ≥0
f_test_function_K2 :
  (∀ x ∈ K2, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f2 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f2 < rieszContentAux Λ K2 + ε / 2
f_test_function_union : ∀ x ∈ K1 ⊔ K2, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 + f2 : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ rieszContentAux Λ K1 + ε / 2 + (rieszContentAux Λ K2 + ε / 2) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
have rw : rieszContentAux Λ K1 + (ε / 2 + (rieszContentAux Λ K2 + ε / 2)) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
Tactic: rw [add_assoc, add_comm (ε / 2), add_assoc, add_halves ε, add_assoc]
-- 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
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →C_c ℝ≥0
f_test_function_K1 :
  (∀ x ∈ K1, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →C_c ℝ≥0
f_test_function_K2 :
  (∀ x ∈ K2, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f2 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f2 < rieszContentAux Λ K2 + ε / 2
f_test_function_union : ∀ x ∈ K1 ⊔ K2, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 + f2 : (a : X) → ℝ≥0) x : ℝ≥0)
rw : rieszContentAux Λ K1 + (ε / 2 + (rieszContentAux Λ K2 + ε / 2)) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
⊢ rieszContentAux Λ K1 + ε / 2 + (rieszContentAux Λ K2 + ε / 2) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
have rw₁ : rieszContentAux Λ K1 + (rieszContentAux Λ K2 + ε / 2 + ε / 2) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
Tactic: rw [add_assoc, add_comm (ε / 2), add_assoc, add_halves ε, add_assoc]
-- 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
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →C_c ℝ≥0
f_test_function_K1 :
  (∀ x ∈ K1, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →C_c ℝ≥0
f_test_function_K2 :
  (∀ x ∈ K2, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f2 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f2 < rieszContentAux Λ K2 + ε / 2
f_test_function_union : ∀ x ∈ K1 ⊔ K2, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 + f2 : (a : X) → ℝ≥0) x : ℝ≥0)
rw : rieszContentAux Λ K1 + (ε / 2 + (rieszContentAux Λ K2 + ε / 2)) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
rw₁ : rieszContentAux Λ K1 + (rieszContentAux Λ K2 + ε / 2 + ε / 2) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
⊢ rieszContentAux Λ K1 + ε / 2 + (rieszContentAux Λ K2 + ε / 2) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
have rw₂ : rieszContentAux Λ K1 + (rieszContentAux Λ K2 + (ε / 2 + ε / 2)) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
Tactic: rw [add_assoc, add_comm (ε / 2), add_assoc, add_halves ε, add_assoc]
-- 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
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →C_c ℝ≥0
f_test_function_K1 :
  (∀ x ∈ K1, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →C_c ℝ≥0
f_test_function_K2 :
  (∀ x ∈ K2, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f2 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f2 < rieszContentAux Λ K2 + ε / 2
f_test_function_union : ∀ x ∈ K1 ⊔ K2, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 + f2 : (a : X) → ℝ≥0) x : ℝ≥0)
rw : rieszContentAux Λ K1 + (ε / 2 + (rieszContentAux Λ K2 + ε / 2)) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
rw₁ : rieszContentAux Λ K1 + (rieszContentAux Λ K2 + ε / 2 + ε / 2) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
rw₂ : rieszContentAux Λ K1 + (rieszContentAux Λ K2 + (ε / 2 + ε / 2)) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
⊢ rieszContentAux Λ K1 + ε / 2 + (rieszContentAux Λ K2 + ε / 2) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
have rw₃ : rieszContentAux Λ K1 + (rieszContentAux Λ K2 + ε) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
Tactic: rw [add_assoc, add_comm (ε / 2), add_assoc, add_halves ε, add_assoc]
-- 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
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →C_c ℝ≥0
f_test_function_K1 :
  (∀ x ∈ K1, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →C_c ℝ≥0
f_test_function_K2 :
  (∀ x ∈ K2, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f2 : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
    (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f2 < rieszContentAux Λ K2 + ε / 2
f_test_function_union : ∀ x ∈ K1 ⊔ K2, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 + f2 : (a : X) → ℝ≥0) x : ℝ≥0)
rw : rieszContentAux Λ K1 + (ε / 2 + (rieszContentAux Λ K2 + ε / 2)) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
rw₁ : rieszContentAux Λ K1 + (rieszContentAux Λ K2 + ε / 2 + ε / 2) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
rw₂ : rieszContentAux Λ K1 + (rieszContentAux Λ K2 + (ε / 2 + ε / 2)) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
rw₃ : rieszContentAux Λ K1 + (rieszContentAux Λ K2 + ε) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
⊢ rieszContentAux Λ K1 + ε / 2 + (rieszContentAux Λ K2 + ε / 2) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
have rw₄ : rieszContentAux Λ K1 + (rieszContentAux Λ K2 + ε) = rieszContentAux Λ K1 + (rieszContentAux Λ K2 + ε)
Tactic: rw [add_assoc, add_comm (ε / 2), add_assoc, add_halves ε, add_assoc]
-- 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
⊢ ∃ (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 hso : let so : Fin 2 → Set X := fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ;
so = fun (j : Fin 2) ↦ if j = 0 then s₀ᶜ else s₁ᶜ
Tactic: set so : Fin 2 → Set X := fun j => if j = 0 then s₀ᶜ else s₁ᶜ with hso
-- 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₁ᶜ
j : Fin 2
⊢ IsOpen (so j)
have 0 : IsOpen (so ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)))
Tactic: fin_cases j
Cleared hypotheses: j
-- 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₁ᶜ
j : Fin 2
0 : IsOpen (so ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))
⊢ IsOpen (so j)
have 1 : IsOpen (so ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)))
Tactic: fin_cases j
Cleared hypotheses: j
-- 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₁ᶜ
⊢ IsOpen (so ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))
have 0 : IsClosed s₀
Tactic: simp only [hso, Fin.zero_eta, Fin.isValue, ↓reduceIte, isOpen_compl_iff]
-- 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₁ᶜ
⊢ IsOpen (so ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))
have 1 : IsClosed s₁
Tactic: simp only [hso, Fin.isValue, Fin.mk_one, one_ne_zero, ↓reduceIte, isOpen_compl_iff]
-- 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₁ᶜ
⊢ ∃ (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 soopen : ∀ (j : Fin 2), IsOpen (so j)
Tactic: have soopen (j : Fin 2) : IsOpen (so j) := by
    fin_cases j
    · simp only [hso, Fin.zero_eta, Fin.isValue, ↓reduceIte, isOpen_compl_iff]
      exact IsCompact.isClosed <| s₀_compact
    · simp only [hso, Fin.isValue, Fin.mk_one, one_ne_zero, ↓reduceIte, isOpen_compl_iff]
      exact IsCompact.isClosed <| s₁_compact
-- 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
⊢ Membership.mem (γ := Set X) (⋃ (j : Fin 2), if j = 0 then s₀ᶜ else s₁ᶜ) x
have rw : ∃ (i : Fin 2), x ∈ if i = 0 then s₀ᶜ else s₁ᶜ
Tactic: rw [mem_iUnion]