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₁ 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
have h : ∀ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ) = (↑((g₁ * f + g₂ * f : (a : X) → ℝ≥0) x) : ℝ)
Tactic: ext x
-- 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)
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
⊢ (↑((f : (a : X) → ℝ≥0) x) : ℝ) = (↑((g₁ * f + g₂ * f : (a : X) → ℝ≥0) x) : ℝ)
have 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) : ℝ)
Tactic: simp only [CompactlySupportedContinuousMap.coe_add, CompactlySupportedContinuousMap.coe_mul,
      Pi.mul_apply, NNReal.coe_mul,
      Eq.symm (RightDistribClass.right_distrib _ _ _)]
-- 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)
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
⊢ (↑((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) : ℝ)
have 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) : ℝ)
Tactic: by_cases h : f x = 0
-- 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)
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) : ℝ)
⊢ (↑((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) : ℝ)
have 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) : ℝ)
Tactic: by_cases h : f x = 0
-- 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)
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)
⊢ (↑((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) : ℝ)
have pos : (↑0 : ℝ) =
  (↑(HAdd.hAdd (α := (a : X) → ℝ≥0) (β := (a : X) → ℝ≥0) (⇑g₁ : (a : X) → ℝ≥0) (⇑g₂ : (a : X) → ℝ≥0) x) : ℝ) * (↑0 : ℝ)
Tactic: rw [h]
-- 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)
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) : ℝ) =
    (↑(HAdd.hAdd (α := (a : X) → ℝ≥0) (β := (a : X) → ℝ≥0) (⇑g₁ : (a : X) → ℝ≥0) (⇑g₂ : (a : X) → ℝ≥0) x) : ℝ) *
      (↑((f : (a : X) → ℝ≥0) x) : ℝ)
have neg : (↑((f : (a : X) → ℝ≥0) x) : ℝ) = (↑(1 x) : ℝ) * (↑((f : (a : X) → ℝ≥0) x) : ℝ)
Tactic: rw [sum_g (mem_of_subset_of_mem subset_closure (mem_support.mpr h))]
-- 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
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)
⊢ rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ b
have f_eq_sum : 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]
-- 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)
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
⊢ rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ b
have 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)
Tactic: rw [← Λf_eq_b, f_eq_sum, map_add]
-- 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
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
⊢ 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)
have aux₁ : ∀ 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₁)]
-- 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
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)
⊢ 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)
have aux₂ : ∀ 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₂)]
-- 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
⊢ 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∞)
have 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∞)
Tactic: simp only [rieszContent, le_antisymm_iff, le_iInf_iff, ENNReal.coe_le_coe, Content.mk_apply]
-- 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
⊢ (∀ (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∞)
have refine : ⨅ (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), ?_⟩
-- 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
⊢ ⨅ (K' : Compacts X), ⨅ (_ : (↑K : Set X) ⊆ interior (↑K' : Set X)), (↑(rieszContentAux Λ K') : ℝ≥0∞) ≤
    (↑(rieszContentAux Λ K) : ℝ≥0∞)
have rw : ∀ (b : ℝ≥0∞),
  (∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)) →
    b ≤ (↑(rieszContentAux Λ K) : ℝ≥0∞)
Tactic: rw [iInf_le_iff]
-- 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
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
⊢ b ≤ (↑(rieszContentAux Λ K) : ℝ≥0∞)
have 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)})
Tactic: rw [rieszContentAux, ENNReal.le_coe_iff]
-- 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
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
⊢ b < ∞
have obtain : ∀ (F : Set X) (hF : IsCompact F ∧ K.carrier ⊆ interior F), b < ∞
Tactic: obtain ⟨F, hF⟩ := exists_compact_superset K.2
-- 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 : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
⊢ ∃ (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)})
have this : b < ∞
Tactic: have : b < ⊤ := by
    obtain ⟨F, hF⟩ := exists_compact_superset K.2
    exact (le_iInf_iff.mp (hb ⟨F, hF.1⟩) hF.2).trans_lt ENNReal.coe_lt_top
-- 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
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
⊢ ∃ (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)})
have refine : (↑b.toNNReal : ℝ) ≤
  (↑(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: refine ⟨b.toNNReal, (ENNReal.coe_toNNReal this.ne).symm, NNReal.coe_le_coe.mp ?_⟩
-- 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
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
⊢ (↑b.toNNReal : ℝ) ≤
    (↑(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 apply : ∀ (ε : ℝ),
  0 < ε →
    (↑b.toNNReal : ℝ) ≤
      (↑(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: apply le_iff_forall_pos_le_add.mpr
-- 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
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
ε : ℝ
hε : 0 < ε
⊢ (↑b.toNNReal : ℝ) ≤
    (↑(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 lift : ∀ (ε : ℝ≥0) (hε : 0 < (↑ε : ℝ)),
  (↑b.toNNReal : ℝ) ≤
    (↑(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: lift ε to ℝ≥0 using hε.le
Cleared hypotheses: ε, hε
-- 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
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
⊢ (↑b.toNNReal : ℝ) ≤
    (↑(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 obtain : ∀ (f : X →C_c ℝ≥0) (hfleoneonK : ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0))
  (hfle : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f < rieszContentAux Λ K + (↑ε : ℝ).toNNReal),
  (↑b.toNNReal : ℝ) ≤
    (↑(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: obtain ⟨f, hfleoneonK, hfle⟩ := exists_lt_rieszContentAux_add_pos Λ K (Real.toNNReal_pos.mpr hε)
-- 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 : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)
hfle : (Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f < rieszContentAux Λ K + (↑ε : ℝ).toNNReal
⊢ (↑b.toNNReal : ℝ) ≤
    (↑(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 hfle₁ : (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ) <
  (↑(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)}) +
        NNReal.mk (↑ε : ℝ) sorry) :
    ℝ)
Tactic: rw [rieszContentAux, Real.toNNReal_of_nonneg hε.le, ← NNReal.coe_lt_coe] at hfle
Cleared hypotheses: hfle
-- 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
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : (↑K : Set X) ⊆ interior (↑i : Set X)), (↑(rieszContentAux Λ i) : ℝ≥0∞)
this : b < ∞
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((f : (a : X) → ℝ≥0) x : ℝ≥0)
hfle :
  (↑((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f) : ℝ) <
    (↑(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)}) +
          NNReal.mk (↑ε : ℝ) ⋯) :
      ℝ)
⊢ (↑b.toNNReal : ℝ) ≤
    (↑(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 refine : ∀ (α : ℝ≥0) (hα : 1 < α), b.toNNReal ≤ HMul.hMul (α := ℝ≥0) ((Λ : (a : X →C_c ℝ≥0) → ℝ≥0) f : ℝ≥0) α
Tactic: refine ((le_iff_forall_one_lt_le_mul₀ (zero_le (a := Λ f))).mpr fun α hα ↦ ?_).trans hfle.le