awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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) → ℝ)
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
⊢ 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)}

Tactic:
use nnrealPart ⟨f, hfHasCompactSupport⟩

Premises used: CompactlySupportedContinuousMap.nnrealPart, CompactlySupportedContinuousMap.mk
-- 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 : 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
h :
  Eq (α := ℝ≥0) (1 : ℝ≥0)
    (({ toContinuousMap := f, hasCompactSupport' := hfHasCompactSupport : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) x :
      ℝ≥0)
⊢ LE.le (α := ℝ≥0) (1 : ℝ≥0)
    (({ toContinuousMap := f, hasCompactSupport' := hfHasCompactSupport : X →C_c ℝ }.nnrealPart : (a : X) → ℝ≥0) x :
      ℝ≥0)

Tactic:
apply le_of_eq

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

Tactic:
simp only [nnrealPart_apply, CompactlySupportedContinuousMap.coe_mk]

Premises used: CompactlySupportedContinuousMap.coe_mk, CompactlySupportedContinuousMap.nnrealPart_apply
-- 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 : 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
h : Eq (α := ℝ) (1 : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ 1 = Real.toNNReal ((f : (a : X) → ℝ) x)

Tactic:
rw [← Real.toNNReal_one, Real.toNNReal_eq_toNNReal_iff (zero_le_one' ℝ) (hfinicc x).1]

Premises used: Real, zero_le_one', Real.toNNReal_one, And.left, Real.toNNReal_eq_toNNReal_iff
-- 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 : 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 (α := ℝ) (1 : ℝ) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
hfeq1onK.symm hx

Premises used: Set.EqOn.symm
-- 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 : 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 (α := ℝ) (1 : ℝ) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
exact hfeq1onK.symm hx

Premises used: Set.EqOn.symm
-- 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
h : K₁ ≤ K₂
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)})
⊢ 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)}))

Tactic:
gcongr
-- 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
h : K₁ ≤ K₂
⊢ 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:
apply rieszContentAux_image_nonempty

Premises used: rieszContentAux_image_nonempty
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
K : Compacts X
f : X →C_c ℝ≥0
h : ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ rieszContentAux Λ K ≤ (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f

Tactic:
csInf_le (OrderBot.bddBelow _) ⟨f, ⟨h, rfl⟩⟩

Premises used: rieszContentAux, And.intro, Exists.intro, OrderBot.bddBelow, csInf_le, rfl
-- 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 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
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 + ε
⊢ ∃ (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)

Premises used: lt_add_of_pos_right, rieszContentAux_image_nonempty, rieszContentAux, exists_lt_of_csInf_lt
-- 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 : 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 + ε

Tactic:
⟨f, f_hyp.left, ?_⟩

Premises used: And.left, And.intro, Exists.intro
-- 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 : 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 = α
refine : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f < rieszContentAux Λ K + ε
⊢ ∃ (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:
refine ⟨f, f_hyp.left, ?_⟩
-- 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 : 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 = α
rw : α < rieszContentAux Λ K + ε
⊢ (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f < rieszContentAux Λ K + ε

Tactic:
rw [f_hyp.right]

Premises used: And.right
-- 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 : 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 = α
⊢ α < rieszContentAux Λ K + ε

Tactic:
α_hyp
-- 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 : 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 = α
⊢ α < rieszContentAux Λ K + ε

Tactic:
exact α_hyp
-- 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
K1 K2 : Compacts X
h : ∀ (ε : ℝ≥0), 0 < ε → rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
⊢ rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2

Tactic:
apply _root_.le_of_forall_pos_le_add

Premises used: le_of_forall_pos_le_add
-- 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
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
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 + ε
⊢ rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε

Tactic:
obtain ⟨f1, f_test_function_K1⟩ := exists_lt_rieszContentAux_add_pos Λ K1 (half_pos εpos)

Premises used: half_pos, exists_lt_rieszContentAux_add_pos
-- 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
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
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 + ε
⊢ rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε

Tactic:
obtain ⟨f2, f_test_function_K2⟩ := exists_lt_rieszContentAux_add_pos Λ K2 (half_pos εpos)

Premises used: half_pos, exists_lt_rieszContentAux_add_pos
-- 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
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
x : X
x_in_K1 : x ∈ (↑K1 : Set X)
⊢ LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 + f2 : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
le_add_right (f_test_function_K1.left x x_in_K1)

Premises used: And.left, le_add_right
-- 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
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
x : X
x_in_K1 : x ∈ (↑K1 : Set X)
⊢ LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 + f2 : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
exact le_add_right (f_test_function_K1.left x x_in_K1)

Premises used: And.left, le_add_right
-- 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
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
x : X
x_in_K2 : x ∈ (↑K2 : Set X)
⊢ LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 + f2 : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
le_add_left (f_test_function_K2.left x x_in_K2)

Premises used: And.left, le_add_left
-- 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
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
x : X
x_in_K2 : x ∈ (↑K2 : Set X)
⊢ LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f1 + f2 : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
exact le_add_left (f_test_function_K2.left x x_in_K2)

Premises used: And.left, le_add_left
-- 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
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
⊢ ∀ 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)
-- 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
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)
apply : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (f1 + f2) < rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
⊢ rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε

Tactic:
apply (rieszContentAux_le Λ f_test_function_union).trans (le_of_lt _)

Premises used: le_of_lt, LE.le.trans, rieszContentAux_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
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 :
  HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f1 : ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f2 : ℝ≥0) <
    rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
⊢ (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (f1 + f2) < rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε

Tactic:
rw [map_add]

Premises used: map_add
-- 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
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)
apply : rieszContentAux Λ K1 + ε / 2 + (rieszContentAux Λ K2 + ε / 2) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
⊢ 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:
apply lt_of_lt_of_le (_root_.add_lt_add f_test_function_K1.right f_test_function_K2.right)
    (le_of_eq _)

Premises used: add_lt_add, And.right, le_of_eq, 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
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 + ε
rw₄ rw₅ : rieszContentAux Λ K1 + (rieszContentAux Λ K2 + ε) = rieszContentAux Λ K1 + (rieszContentAux Λ K2 + ε)
⊢ rieszContentAux Λ K1 + ε / 2 + (rieszContentAux Λ K2 + ε / 2) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε

Tactic:
rw [add_assoc, add_comm (ε / 2), add_assoc, add_halves ε, add_assoc]

Premises used: add_halves, add_assoc, HDiv.hDiv, add_comm, 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
⊢ 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

Premises used: Compl.compl, OfNat.ofNat, Eq, ite
-- 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₁ᶜ
j : Fin 2
0 : IsOpen (so ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))
1 : IsOpen (so ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))
⊢ IsOpen (so j)

Tactic:
fin_cases j
-- 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₁ᶜ
0 : IsClosed s₀
⊢ IsOpen (so ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))

Tactic:
simp only [hso, Fin.zero_eta, Fin.isValue, ↓reduceIte, isOpen_compl_iff]

Premises used: Fin.zero_eta, Fin.isValue, reduceIte, isOpen_compl_iff