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₁ 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)
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
⊢ 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

Premises used: TopologicalSpace.Compacts.isCompact', HasCompactSupport.isCompact, CompactlySupportedContinuousMap.hasCompactSupport', exists_continuous_add_one_of_isCompact_nnreal
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint (↑K₁ : Set X) (↑K₂ : Set X)
b : ℝ≥0
f : X →C_c ℝ≥0
hf :
  Membership.mem (γ := Set (X →C_c ℝ≥0))
    {f : X →C_c ℝ≥0 | ∀ x ∈ K₁ ⊔ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)} f
Λf_eq_b : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, Membership.mem (γ := Set X) (support (M := ℝ≥0) (⇑f : (a : X) → ℝ≥0)) x
hsubsuppf : (↑K₁ : Set X) ∪ (↑K₂ : Set X) ⊆ tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)
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)
h : ∀ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ) = (↑((g₁ * f + g₂ * f : (a : X) → ℝ≥0) x) : ℝ)
⊢ f = g₁ * f + g₂ * f

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint (↑K₁ : Set X) (↑K₂ : Set X)
b : ℝ≥0
f : X →C_c ℝ≥0
hf :
  Membership.mem (γ := Set (X →C_c ℝ≥0))
    {f : X →C_c ℝ≥0 | ∀ x ∈ K₁ ⊔ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)} f
Λf_eq_b : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, Membership.mem (γ := Set X) (support (M := ℝ≥0) (⇑f : (a : X) → ℝ≥0)) x
hsubsuppf : (↑K₁ : Set X) ∪ (↑K₂ : Set X) ⊆ tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)
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)
x : X
h :
  (↑((f : (a : X) → ℝ≥0) x) : ℝ) =
    (↑(HAdd.hAdd (α := (a : X) → ℝ≥0) (β := (a : X) → ℝ≥0) (⇑g₁ : (a : X) → ℝ≥0) (⇑g₂ : (a : X) → ℝ≥0) x) : ℝ) *
      (↑((f : (a : X) → ℝ≥0) x) : ℝ)
⊢ (↑((f : (a : X) → ℝ≥0) x) : ℝ) = (↑((g₁ * f + g₂ * f : (a : X) → ℝ≥0) x) : ℝ)

Tactic:
simp only [CompactlySupportedContinuousMap.coe_add, CompactlySupportedContinuousMap.coe_mul,
      Pi.mul_apply, NNReal.coe_mul,
      Eq.symm (RightDistribClass.right_distrib _ _ _)]

Premises used: CompactlySupportedContinuousMap.coe_mul, Pi.mul_apply, NNReal.coe_mul, CompactlySupportedContinuousMap.coe_add, RightDistribClass.right_distrib, Eq.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
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)
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)
x : X
pos :
  ∀ (h : Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)),
    (↑((f : (a : X) → ℝ≥0) x) : ℝ) =
      (↑(HAdd.hAdd (α := (a : X) → ℝ≥0) (β := (a : X) → ℝ≥0) (⇑g₁ : (a : X) → ℝ≥0) (⇑g₂ : (a : X) → ℝ≥0) x) : ℝ) *
        (↑((f : (a : X) → ℝ≥0) x) : ℝ)
neg :
  ∀ (h : ¬Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)),
    (↑((f : (a : X) → ℝ≥0) x) : ℝ) =
      (↑(HAdd.hAdd (α := (a : X) → ℝ≥0) (β := (a : X) → ℝ≥0) (⇑g₁ : (a : X) → ℝ≥0) (⇑g₂ : (a : X) → ℝ≥0) x) : ℝ) *
        (↑((f : (a : X) → ℝ≥0) x) : ℝ)
⊢ (↑((f : (a : X) → ℝ≥0) x) : ℝ) =
    (↑(HAdd.hAdd (α := (a : X) → ℝ≥0) (β := (a : X) → ℝ≥0) (⇑g₁ : (a : X) → ℝ≥0) (⇑g₂ : (a : X) → ℝ≥0) x) : ℝ) *
      (↑((f : (a : X) → ℝ≥0) x) : ℝ)

Tactic:
by_cases h : f x = 0

Premises used: DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint (↑K₁ : Set X) (↑K₂ : Set X)
b : ℝ≥0
f : X →C_c ℝ≥0
hf :
  Membership.mem (γ := Set (X →C_c ℝ≥0))
    {f : X →C_c ℝ≥0 | ∀ x ∈ K₁ ⊔ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)} f
Λf_eq_b : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, Membership.mem (γ := Set X) (support (M := ℝ≥0) (⇑f : (a : X) → ℝ≥0)) x
hsubsuppf : (↑K₁ : Set X) ∪ (↑K₂ : Set X) ⊆ tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)
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)
x : X
h : Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
pos :
  (↑0 : ℝ) =
    (↑(HAdd.hAdd (α := (a : X) → ℝ≥0) (β := (a : X) → ℝ≥0) (⇑g₁ : (a : X) → ℝ≥0) (⇑g₂ : (a : X) → ℝ≥0) x) : ℝ) *
      (↑0 : ℝ)
⊢ (↑((f : (a : X) → ℝ≥0) x) : ℝ) =
    (↑(HAdd.hAdd (α := (a : X) → ℝ≥0) (β := (a : X) → ℝ≥0) (⇑g₁ : (a : X) → ℝ≥0) (⇑g₂ : (a : X) → ℝ≥0) x) : ℝ) *
      (↑((f : (a : X) → ℝ≥0) x) : ℝ)

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint (↑K₁ : Set X) (↑K₂ : Set X)
b : ℝ≥0
f : X →C_c ℝ≥0
hf :
  Membership.mem (γ := Set (X →C_c ℝ≥0))
    {f : X →C_c ℝ≥0 | ∀ x ∈ K₁ ⊔ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)} f
Λf_eq_b : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, Membership.mem (γ := Set X) (support (M := ℝ≥0) (⇑f : (a : X) → ℝ≥0)) x
hsubsuppf : (↑K₁ : Set X) ∪ (↑K₂ : Set X) ⊆ tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)
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)
x : X
h : Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
⊢ (↑0 : ℝ) =
    (↑(HAdd.hAdd (α := (a : X) → ℝ≥0) (β := (a : X) → ℝ≥0) (⇑g₁ : (a : X) → ℝ≥0) (⇑g₂ : (a : X) → ℝ≥0) x) : ℝ) *
      (↑0 : ℝ)

Tactic:
simp only [NNReal.coe_zero, mul_zero]

Premises used: NNReal.coe_zero, MulZeroClass.mul_zero
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint (↑K₁ : Set X) (↑K₂ : Set X)
b : ℝ≥0
f : X →C_c ℝ≥0
hf :
  Membership.mem (γ := Set (X →C_c ℝ≥0))
    {f : X →C_c ℝ≥0 | ∀ x ∈ K₁ ⊔ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)} f
Λf_eq_b : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, Membership.mem (γ := Set X) (support (M := ℝ≥0) (⇑f : (a : X) → ℝ≥0)) x
hsubsuppf : (↑K₁ : Set X) ∪ (↑K₂ : Set X) ⊆ tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)
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 (HAdd.hAdd (α := (a : X) → ℝ≥0) (⇑g₁ : (a : X) → ℝ≥0) (⇑g₂ : (a : X) → ℝ≥0)) 1
    (tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0))
x : X
h : ¬Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
neg : (↑((f : (a : X) → ℝ≥0) x) : ℝ) = (↑(1 x) : ℝ) * (↑((f : (a : X) → ℝ≥0) x) : ℝ)
⊢ (↑((f : (a : X) → ℝ≥0) x) : ℝ) =
    (↑(HAdd.hAdd (α := (a : X) → ℝ≥0) (β := (a : X) → ℝ≥0) (⇑g₁ : (a : X) → ℝ≥0) (⇑g₂ : (a : X) → ℝ≥0) x) : ℝ) *
      (↑((f : (a : X) → ℝ≥0) x) : ℝ)

Tactic:
rw [sum_g (mem_of_subset_of_mem subset_closure (mem_support.mpr h))]

Premises used: Iff.mpr, subset_closure, Set.mem_of_subset_of_mem, Function.mem_support
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint (↑K₁ : Set X) (↑K₂ : Set X)
b : ℝ≥0
f : X →C_c ℝ≥0
hf :
  Membership.mem (γ := Set (X →C_c ℝ≥0))
    {f : X →C_c ℝ≥0 | ∀ x ∈ K₁ ⊔ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)} f
Λf_eq_b : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, Membership.mem (γ := Set X) (support (M := ℝ≥0) (⇑f : (a : X) → ℝ≥0)) x
hsubsuppf : (↑K₁ : Set X) ∪ (↑K₂ : Set X) ⊆ tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)
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 (HAdd.hAdd (α := (a : X) → ℝ≥0) (⇑g₁ : (a : X) → ℝ≥0) (⇑g₂ : (a : X) → ℝ≥0)) 1
    (tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0))
x : X
h : ¬Eq (α := ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
⊢ (↑((f : (a : X) → ℝ≥0) x) : ℝ) = (↑(1 x) : ℝ) * (↑((f : (a : X) → ℝ≥0) x) : ℝ)

Tactic:
simp only [Pi.one_apply, NNReal.coe_one, one_mul]

Premises used: Pi.one_apply, NNReal.coe_one, one_mul
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint (↑K₁ : Set X) (↑K₂ : Set X)
b : ℝ≥0
f : X →C_c ℝ≥0
hf :
  Membership.mem (γ := Set (X →C_c ℝ≥0))
    {f : X →C_c ℝ≥0 | ∀ x ∈ K₁ ⊔ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)} f
Λf_eq_b : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, Membership.mem (γ := Set X) (support (M := ℝ≥0) (⇑f : (a : X) → ℝ≥0)) x
hsubsuppf : (↑K₁ : Set X) ∪ (↑K₂ : Set X) ⊆ tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)
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)
⊢ f = g₁ * f + g₂ * f

Tactic:
have f_eq_sum : f = g₁ * f + g₂ * f := by
    ext x
    simp only [CompactlySupportedContinuousMap.coe_add, CompactlySupportedContinuousMap.coe_mul,
      Pi.mul_apply, NNReal.coe_mul,
      Eq.symm (RightDistribClass.right_distrib _ _ _)]
    by_cases h : f x = 0
    · rw [h]
      simp only [NNReal.coe_zero, mul_zero]
    · simp only [CompactlySupportedContinuousMap.coe_add, ContinuousMap.toFun_eq_coe,
        CompactlySupportedContinuousMap.coe_toContinuousMap] at sum_g
      rw [sum_g (mem_of_subset_of_mem subset_closure (mem_support.mpr h))]
      simp only [Pi.one_apply, NNReal.coe_one, one_mul]
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint (↑K₁ : Set X) (↑K₂ : Set X)
b : ℝ≥0
f : X →C_c ℝ≥0
hf :
  Membership.mem (γ := Set (X →C_c ℝ≥0))
    {f : X →C_c ℝ≥0 | ∀ x ∈ K₁ ⊔ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)} f
Λf_eq_b : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, Membership.mem (γ := Set X) (support (M := ℝ≥0) (⇑f : (a : X) → ℝ≥0)) x
hsubsuppf : (↑K₁ : Set X) ∪ (↑K₂ : Set X) ⊆ tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)
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)
f_eq_sum : f = g₁ * f + g₂ * f
rw :
  rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤
    HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (g₁ * f) : ℝ≥0)
      ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (g₂ * f) : ℝ≥0)
⊢ rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ b

Tactic:
rw [← Λf_eq_b, f_eq_sum, 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
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)
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)
f_eq_sum : f = g₁ * f + g₂ * f
x : X
x_in_K₁ : x ∈ K₁
⊢ LE.le (α := ℝ≥0) (1 : ℝ≥0) ((g₁ * f : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
simp [hg₁ x_in_K₁, hf x (mem_union_left _ x_in_K₁)]

Premises used: Set.mem_union_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₁ 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)
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)
f_eq_sum : f = g₁ * f + g₂ * f
⊢ ∀ x ∈ K₁, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((g₁ * f : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
have aux₁ : ∀ x ∈ K₁, 1 ≤ (g₁ * f) x := by
    intro x x_in_K₁
    simp [hg₁ x_in_K₁, hf x (mem_union_left _ x_in_K₁)]
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint (↑K₁ : Set X) (↑K₂ : Set X)
b : ℝ≥0
f : X →C_c ℝ≥0
hf :
  Membership.mem (γ := Set (X →C_c ℝ≥0))
    {f : X →C_c ℝ≥0 | ∀ x ∈ K₁ ⊔ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)} f
Λf_eq_b : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, Membership.mem (γ := Set X) (support (M := ℝ≥0) (⇑f : (a : X) → ℝ≥0)) x
hsubsuppf : (↑K₁ : Set X) ∪ (↑K₂ : Set X) ⊆ tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)
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)
f_eq_sum : f = g₁ * f + g₂ * f
aux₁ : ∀ x ∈ K₁, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((g₁ * f : (a : X) → ℝ≥0) x : ℝ≥0)
x : X
x_in_K₂ : x ∈ K₂
⊢ LE.le (α := ℝ≥0) (1 : ℝ≥0) ((g₂ * f : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
simp [hg₂ x_in_K₂, hf x (mem_union_right _ x_in_K₂)]

Premises used: Set.mem_union_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₁ 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)
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)
f_eq_sum : f = g₁ * f + g₂ * f
aux₁ : ∀ x ∈ K₁, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((g₁ * f : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ ∀ x ∈ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((g₂ * f : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
have aux₂ : ∀ x ∈ K₂, 1 ≤ (g₂ * f) x := by
    intro x x_in_K₂
    simp [hg₂ x_in_K₂, hf x (mem_union_right _ x_in_K₂)]
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint (↑K₁ : Set X) (↑K₂ : Set X)
b : ℝ≥0
f : X →C_c ℝ≥0
hf :
  Membership.mem (γ := Set (X →C_c ℝ≥0))
    {f : X →C_c ℝ≥0 | ∀ x ∈ K₁ ⊔ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)} f
Λf_eq_b : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, Membership.mem (γ := Set X) (support (M := ℝ≥0) (⇑f : (a : X) → ℝ≥0)) x
hsubsuppf : (↑K₁ : Set X) ∪ (↑K₂ : Set X) ⊆ tsupport (α := ℝ≥0) (⇑f : (a : X) → ℝ≥0)
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)
f_eq_sum : f = g₁ * f + g₂ * f
aux₁ : ∀ x ∈ K₁, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((g₁ * f : (a : X) → ℝ≥0) x : ℝ≥0)
aux₂ : ∀ x ∈ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((g₂ * f : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤
    HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (g₁ * f) : ℝ≥0)
      ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (g₂ * f) : ℝ≥0)

Tactic:
add_le_add (rieszContentAux_le Λ aux₁) (rieszContentAux_le Λ aux₂)

Premises used: add_le_add, 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
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)
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)
f_eq_sum : f = g₁ * f + g₂ * f
aux₁ : ∀ x ∈ K₁, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((g₁ * f : (a : X) → ℝ≥0) x : ℝ≥0)
aux₂ : ∀ x ∈ K₂, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((g₂ * f : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤
    HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (g₁ * f) : ℝ≥0)
      ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) (g₂ * f) : ℝ≥0)

Tactic:
exact add_le_add (rieszContentAux_le Λ aux₁) (rieszContentAux_le Λ aux₂)

Premises used: add_le_add, 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
K : Compacts X
⊢ Ne (α := ℝ≥0∞) ((rieszContent Λ : (a : Compacts X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [rieszContent, ne_eq, ENNReal.coe_ne_top, not_false_eq_true]

Premises used: ne_eq, rieszContent, not_false_eq_true, ENNReal.coe_ne_top
-- 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
simp :
  (∀ (i : Compacts X) (i_1 : (↑K : Set X) ⊆ interior (↑i : Set X)), rieszContentAux Λ K ≤ rieszContentAux Λ i) ∧
    ⨅ (K' : Compacts X), ⨅ (_ : (↑K : Set X) ⊆ interior (↑K' : Set X)), (↑(rieszContentAux Λ K') : ℝ≥0∞) ≤
      (↑(rieszContentAux Λ K) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((rieszContent Λ : (a : Compacts X) → ℝ≥0∞) K : ℝ≥0∞)
    (⨅ (K' : Compacts X), ⨅ (_ : (↑K : Set X) ⊆ interior (↑K' : Set X)), (rieszContent Λ : (a : Compacts X) → ℝ≥0∞) K' :
      ℝ≥0∞)

Tactic:
simp only [rieszContent, le_antisymm_iff, le_iInf_iff, ENNReal.coe_le_coe, Content.mk_apply]

Premises used: le_iInf_iff, ENNReal.coe_le_coe, rieszContent, MeasureTheory.Content.mk_apply, le_antisymm_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
⊢ (∀ (i : Compacts X) (i_1 : (↑K : Set X) ⊆ interior (↑i : Set X)), rieszContentAux Λ K ≤ rieszContentAux Λ i) ∧
    ⨅ (K' : Compacts X), ⨅ (_ : (↑K : Set X) ⊆ interior (↑K' : Set X)), (↑(rieszContentAux Λ K') : ℝ≥0∞) ≤
      (↑(rieszContentAux Λ K) : ℝ≥0∞)

Tactic:
⟨fun K' hK' ↦ rieszContentAux_mono Λ (hK'.trans interior_subset), ?_⟩

Premises used: interior_subset, HasSubset.Subset.trans, rieszContentAux_mono, And.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
refine :
  ⨅ (K' : Compacts X), ⨅ (_ : (↑K : Set X) ⊆ interior (↑K' : Set X)), (↑(rieszContentAux Λ K') : ℝ≥0∞) ≤
    (↑(rieszContentAux Λ K) : ℝ≥0∞)
⊢ (∀ (i : Compacts X) (i_1 : (↑K : Set X) ⊆ interior (↑i : Set X)), rieszContentAux Λ K ≤ rieszContentAux Λ i) ∧
    ⨅ (K' : Compacts X), ⨅ (_ : (↑K : Set X) ⊆ interior (↑K' : Set X)), (↑(rieszContentAux Λ K') : ℝ≥0∞) ≤
      (↑(rieszContentAux Λ K) : ℝ≥0∞)

Tactic:
refine ⟨fun K' hK' ↦ rieszContentAux_mono Λ (hK'.trans interior_subset), ?_⟩
-- 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
rw :
  ∀ (b : ℝ≥0∞),
    (∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)) →
      b ≤ (↑(rieszContentAux Λ K) : ℝ≥0∞)
⊢ ⨅ (K' : Compacts X), ⨅ (_ : (↑K : Set X) ⊆ interior (↑K' : Set X)), (↑(rieszContentAux Λ K') : ℝ≥0∞) ≤
    (↑(rieszContentAux Λ K) : ℝ≥0∞)

Tactic:
rw [iInf_le_iff]

Premises used: iInf_le_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
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
rw :
  ∃ (p : ℝ≥0),
    b = (↑p : ℝ≥0∞) ∧
      p ≤
        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)})
⊢ b ≤ (↑(rieszContentAux Λ K) : ℝ≥0∞)

Tactic:
rw [rieszContentAux, ENNReal.le_coe_iff]

Premises used: ENNReal.le_coe_iff, rieszContentAux