awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
g g' : E →C_c ℝ
hgg' : g ≤ g'
μ : FiniteMeasure E
apply : Integrable (ε := ℝ) (⇑g : (a : E) → ℝ) (↑μ : Measure E)
apply₁ : Integrable (ε := ℝ) (⇑g' : (a : E) → ℝ) (↑μ : Measure E)
⊢ LE.le (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) (∫ (x : E), (g' : (a : E) → ℝ) x ∂(↑μ : Measure E))

Tactic:
apply integral_mono _ _ hgg'

Premises used: MeasureTheory.integral_mono
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
g g' : E →C_c ℝ
hgg' : g ≤ g'
μ : FiniteMeasure E
⊢ Integrable (ε := ℝ) (⇑g : (a : E) → ℝ) (↑μ : Measure E)

Tactic:
g.continuous.integrable_of_hasCompactSupport g.hasCompactSupport

Premises used: ContinuousMap.continuous, CompactlySupportedContinuousMap.hasCompactSupport, Continuous.integrable_of_hasCompactSupport, CompactlySupportedContinuousMap.toContinuousMap
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
g g' : E →C_c ℝ
hgg' : g ≤ g'
μ : FiniteMeasure E
⊢ Integrable (ε := ℝ) (⇑g : (a : E) → ℝ) (↑μ : Measure E)

Tactic:
exact g.continuous.integrable_of_hasCompactSupport g.hasCompactSupport

Premises used: ContinuousMap.continuous, CompactlySupportedContinuousMap.hasCompactSupport, Continuous.integrable_of_hasCompactSupport, CompactlySupportedContinuousMap.toContinuousMap
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
g g' : E →C_c ℝ
hgg' : g ≤ g'
μ : FiniteMeasure E
⊢ Integrable (ε := ℝ) (⇑g' : (a : E) → ℝ) (↑μ : Measure E)

Tactic:
g'.continuous.integrable_of_hasCompactSupport g'.hasCompactSupport

Premises used: ContinuousMap.continuous, CompactlySupportedContinuousMap.hasCompactSupport, Continuous.integrable_of_hasCompactSupport, CompactlySupportedContinuousMap.toContinuousMap
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
g g' : E →C_c ℝ
hgg' : g ≤ g'
μ : FiniteMeasure E
⊢ Integrable (ε := ℝ) (⇑g' : (a : E) → ℝ) (↑μ : Measure E)

Tactic:
exact g'.continuous.integrable_of_hasCompactSupport g'.hasCompactSupport

Premises used: ContinuousMap.continuous, CompactlySupportedContinuousMap.hasCompactSupport, Continuous.integrable_of_hasCompactSupport, CompactlySupportedContinuousMap.toContinuousMap
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
o : E →C_c ℝ := { toFun := 1, continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((o : (a : E) → ℝ) x : ℝ)

Tactic:
simp [o]
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
o : E →C_c ℝ := { toFun := 1, continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
x : E
⊢ Membership.mem (γ := Set E) univ x → Eq (α := ℝ) ((o : (a : E) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
simp [o]
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
o : E →C_c ℝ := { toFun := 1, continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
⊢ (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal ((Λ' : (a : E →C_c ℝ) → ℝ) o)

Tactic:
have : μlim univ ≤ ENNReal.ofReal (Λ' o) := RealRMK.rieszMeasure_le_of_eq_one Λ'
      (fun x ↦ by simp [o]) isCompact_univ (fun x ↦ by simp [o])
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
o : E →C_c ℝ := { toFun := 1, continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
this : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal ((Λ' : (a : E →C_c ℝ) → ℝ) o)
apply : ENNReal.ofReal ((Λ' : (a : E →C_c ℝ) → ℝ) o) ≤ ENNReal.ofReal (↑C : ℝ)
⊢ (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal (↑C : ℝ)

Tactic:
apply this.trans

Premises used: LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
o : E →C_c ℝ := { toFun := 1, continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
this : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal ((Λ' : (a : E →C_c ℝ) → ℝ) o)
h : (Λ' : (a : E →C_c ℝ) → ℝ) o ≤ (↑C : ℝ)
⊢ ENNReal.ofReal ((Λ' : (a : E →C_c ℝ) → ℝ) o) ≤ ENNReal.ofReal (↑C : ℝ)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
o : E →C_c ℝ := { toFun := 1, continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
this : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal ((Λ' : (a : E →C_c ℝ) → ℝ) o)
h :
  ∀ᶠ (c : FiniteMeasure E) in (↑f : Filter (FiniteMeasure E)),
    ∫ (x : E), (o : (a : E) → ℝ) x ∂(↑c : Measure E) ≤ (↑C : ℝ)
⊢ (Λ' : (a : E →C_c ℝ) → ℝ) o ≤ (↑C : ℝ)

Tactic:
apply le_of_tendsto (hΛ o)

Premises used: le_of_tendsto
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
o : E →C_c ℝ := { toFun := 1, continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
this : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal ((Λ' : (a : E →C_c ℝ) → ℝ) o)
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ ∫ (x : E), (o : (a : E) → ℝ) x ∂(↑μ : Measure E) ≤ (↑C : ℝ)

Tactic:
simpa [o] using hμ
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
o : E →C_c ℝ := { toFun := 1, continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
this : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal ((Λ' : (a : E →C_c ℝ) → ℝ) o)
h :
  ∀ (a : FiniteMeasure E),
    Membership.mem (γ := Set (FiniteMeasure E))
      {x : FiniteMeasure E |
        Membership.mem (γ := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass ≤ C} x →
          Membership.mem (γ := Set (FiniteMeasure E))
            {x : FiniteMeasure E |
              (fun (c : FiniteMeasure E) ↦ ∫ (x : E), (o : (a : E) → ℝ) x ∂(↑c : Measure E) ≤ (↑C : ℝ)) x}
            x}
      a
h₁ h₂ : ∀ (μ : FiniteMeasure E) (hμ : μ.mass ≤ C), ∫ (x : E), (o : (a : E) → ℝ) x ∂(↑μ : Measure E) ≤ (↑C : ℝ)
⊢ ∀ᶠ (c : FiniteMeasure E) in (↑f : Filter (FiniteMeasure E)),
    ∫ (x : E), (o : (a : E) → ℝ) x ∂(↑c : Measure E) ≤ (↑C : ℝ)

Tactic:
filter_upwards [hf] with μ hμ using by simpa [o] using hμ
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
⊢ (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal (↑C : ℝ)

Tactic:
have μlim_le : μlim univ ≤ ENNReal.ofReal C := by
    let o : C_c(E, ℝ) :=
    { toFun := 1
      hasCompactSupport' := HasCompactSupport.of_compactSpace 1 }
    have : μlim univ ≤ ENNReal.ofReal (Λ' o) := RealRMK.rieszMeasure_le_of_eq_one Λ'
      (fun x ↦ by simp [o]) isCompact_univ (fun x ↦ by simp [o])
    apply this.trans
    gcongr
    apply le_of_tendsto (hΛ o)
    filter_upwards [hf] with μ hμ using by simpa [o] using hμ
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal (↑C : ℝ)
⊢ ENNReal.ofReal (↑C : ℝ) < ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal (↑C : ℝ)
μlim' : FiniteMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) μlim ⋯
⊢ ∃ (x : FiniteMeasure E),
    Membership.mem (γ := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass ≤ C} x ∧
      (↑f : Filter (FiniteMeasure E)) ≤ 𝓝 x

Tactic:
⟨μlim', ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal (↑C : ℝ)
μlim' : FiniteMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) μlim ⋯
refine_1 : Membership.mem (γ := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass ≤ C} μlim'
refine_2 : (↑f : Filter (FiniteMeasure E)) ≤ 𝓝 μlim'
⊢ ∃ (x : FiniteMeasure E),
    Membership.mem (γ := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass ≤ C} x ∧
      (↑f : Filter (FiniteMeasure E)) ≤ 𝓝 x

Tactic:
refine ⟨μlim', ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal (↑C : ℝ)
μlim' : FiniteMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) μlim ⋯
refine_1 : ENNReal.toNNReal ((μlim : (a : Set E) → ℝ≥0∞) univ) ≤ C
⊢ Membership.mem (γ := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass ≤ C} μlim'

Tactic:
simp only [mem_setOf_eq, FiniteMeasure.mk_apply, μlim', FiniteMeasure.mass]

Premises used: MeasureTheory.FiniteMeasure.mass, Set.mem_setOf_eq, MeasureTheory.FiniteMeasure.mk_apply
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal (↑C : ℝ)
μlim' : FiniteMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) μlim ⋯
⊢ C = (ENNReal.ofReal (↑C : ℝ)).toNNReal

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal (↑C : ℝ)
μlim' : FiniteMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) μlim ⋯
refine_1 : ENNReal.toNNReal ((μlim : (a : Set E) → ℝ≥0∞) univ) ≤ (ENNReal.ofReal (↑C : ℝ)).toNNReal
⊢ ENNReal.toNNReal ((μlim : (a : Set E) → ℝ≥0∞) univ) ≤ C

Tactic:
rw [show C = (ENNReal.ofReal ↑C).toNNReal by simp]
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal (↑C : ℝ)
μlim' : FiniteMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) μlim ⋯
⊢ ENNReal.ofReal (↑C : ℝ) ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal (↑C : ℝ)
μlim' : FiniteMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) μlim ⋯
⊢ ENNReal.toNNReal ((μlim : (a : Set E) → ℝ≥0∞) univ) ≤ (ENNReal.ofReal (↑C : ℝ)).toNNReal

Tactic:
exact ENNReal.toNNReal_mono (by simp) μlim_le

Premises used: ENNReal.toNNReal_mono
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal (↑C : ℝ)
μlim' : FiniteMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) μlim ⋯
refine_2 : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μlim')
⊢ (↑f : Filter (FiniteMeasure E)) ≤ 𝓝 μlim'

Tactic:
change Tendsto id f (𝓝 μlim')

Premises used: nhds, id, Filter.Tendsto