-- Mathlib/MeasureTheory/Measure/Haar/Unique.lean
/-- In a locally compact regular space with an inner regular measure, the measure of a compact
set `k` is the infimum of the integrals of compactly supported functions equal to `1` on `k`. -/
lemma IsCompact.measure_eq_biInf_integral_hasCompactSupport
    {X : Type*} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X]
    {k : Set X} (hk : IsCompact k)
    (μ : Measure X) [IsFiniteMeasureOnCompacts μ] [InnerRegularCompactLTTop μ]
    [LocallyCompactSpace X] [RegularSpace X] :
    μ k = ⨅ (f : X → ℝ) (_ : Continuous f) (_ : HasCompactSupport f) (_ : EqOn f 1 k)
      (_ : 0 ≤ f), ENNReal.ofReal (∫ x, f x ∂μ)

Proof state:
case a.f_nonneg
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst✝³ : IsFiniteMeasureOnCompacts μ
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
f : X → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport f
fk : EqOn f 1 k
f_nonneg : 0 ≤ f
⊢ 0 ≤ᶠ[ae μ] f

Tactic:
exact Eventually.of_forall f_nonneg

Result:
no goals

Proof state:
case a
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst✝³ : IsFiniteMeasureOnCompacts μ
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
⊢ μ k ≤
    ⨅ f,
      ⨅ (_ : Continuous f),
        ⨅ (_ : HasCompactSupport f), ⨅ (_ : EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ)

Tactic:
simp only [le_iInf_iff]

Result:
case a
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst✝³ : IsFiniteMeasureOnCompacts μ
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
⊢ ∀ (i : X → ℝ), Continuous i → HasCompactSupport i → EqOn i 1 k → 0 ≤ i → μ k ≤ ENNReal.ofReal (∫ (x : X), i x ∂μ)

Proof state:
case a
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst✝³ : IsFiniteMeasureOnCompacts μ
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
⊢ ⨅ f,
      ⨅ (_ : Continuous f),
        ⨅ (_ : HasCompactSupport f), ⨅ (_ : EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤
    μ k

Tactic:
apply le_of_forall_lt' (fun r hr ↦ ?_)

Result:
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst✝³ : IsFiniteMeasureOnCompacts μ
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
r : ℝ≥0∞
hr : μ k < r
⊢ ⨅ f,
      ⨅ (_ : Continuous f),
        ⨅ (_ : HasCompactSupport f), ⨅ (_ : EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ) <
    r

Proof state:
case intro.intro.intro.intro.mk.intro.intro.intro
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst✝³ : IsFiniteMeasureOnCompacts μ
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
r : ℝ≥0∞
hr : μ k < r
U : Set X
kU : k ⊆ U
U_open : IsOpen U
mu_U : μ U < r
f : X → ℝ
f_cont : Continuous f
fk : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 k
fU : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 0 Uᶜ
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
f_range : ∀ (x : X), { toFun := f, continuous_toFun := f_cont } x ∈ Icc 0 1
⊢ ∃ i, Continuous i ∧ HasCompactSupport i ∧ EqOn i 1 k ∧ 0 ≤ i ∧ ENNReal.ofReal (∫ (x : X), i x ∂μ) < r

Tactic:
refine ⟨f, f_cont, f_comp, fk, fun x ↦ (f_range x).1, ?_⟩

Result:
case intro.intro.intro.intro.mk.intro.intro.intro
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst✝³ : IsFiniteMeasureOnCompacts μ
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
r : ℝ≥0∞
hr : μ k < r
U : Set X
kU : k ⊆ U
U_open : IsOpen U
mu_U : μ U < r
f : X → ℝ
f_cont : Continuous f
fk : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 k
fU : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 0 Uᶜ
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
f_range : ∀ (x : X), { toFun := f, continuous_toFun := f_cont } x ∈ Icc 0 1
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) < r

Proof state:
case intro.intro.intro
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst✝³ : IsFiniteMeasureOnCompacts μ
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
r : ℝ≥0∞
hr : μ k < r
U : Set X
kU : k ⊆ U
U_open : IsOpen U
mu_U : μ U < r
⊢ ∃ i, Continuous i ∧ HasCompactSupport i ∧ EqOn i 1 k ∧ 0 ≤ i ∧ ENNReal.ofReal (∫ (x : X), i x ∂μ) < r

Tactic:
obtain ⟨⟨f, f_cont⟩, fk, fU, f_comp, f_range⟩ : ∃ (f : C(X, ℝ)), EqOn f 1 k ∧ EqOn f 0 Uᶜ
    ∧ HasCompactSupport f ∧ ∀ (x : X), f x ∈ Icc 0 1 := exists_continuous_one_zero_of_isCompact
  hk U_open.isClosed_compl (disjoint_compl_right_iff_subset.mpr kU)

Result:
case intro.intro.intro.intro.mk.intro.intro.intro
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst✝³ : IsFiniteMeasureOnCompacts μ
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
r : ℝ≥0∞
hr : μ k < r
U : Set X
kU : k ⊆ U
U_open : IsOpen U
mu_U : μ U < r
f : X → ℝ
f_cont : Continuous f
fk : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 k
fU : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 0 Uᶜ
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
f_range : ∀ (x : X), { toFun := f, continuous_toFun := f_cont } x ∈ Icc 0 1
⊢ ∃ i, Continuous i ∧ HasCompactSupport i ∧ EqOn i 1 k ∧ 0 ≤ i ∧ ENNReal.ofReal (∫ (x : X), i x ∂μ) < r