awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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)
⊢ (Λ' : (a : E →C_c ℝ) → ℝ) o ≤ (↑C : ℝ)
have h : ∀ᶠ (c : FiniteMeasure E) in (↑f : Filter (FiniteMeasure E)), ∫ (x : E), (o : (a : E) → ℝ) x ∂(↑c : Measure E) ≤ (↑C : ℝ)
Tactic: apply le_of_tendsto (hΛ o)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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)
⊢ ∀ᶠ (c : FiniteMeasure E) in (↑f : Filter (FiniteMeasure E)),
    ∫ (x : E), (o : (a : E) → ℝ) x ∂(↑c : Measure E) ≤ (↑C : ℝ)
have 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
Tactic: filter_upwards [hf] with μ hμ using by simpa [o] using hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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
⊢ ∀ᶠ (c : FiniteMeasure E) in (↑f : Filter (FiniteMeasure E)),
    ∫ (x : E), (o : (a : E) → ℝ) x ∂(↑c : Measure E) ≤ (↑C : ℝ)
have h₁ : ∀ (a : FiniteMeasure E), a.mass ≤ C → ∫ (x : E), (o : (a : E) → ℝ) x ∂(↑a : Measure E) ≤ (↑C : ℝ)
Tactic: filter_upwards [hf] with μ hμ using by simpa [o] using hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (hypothesis)
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 Λ'
⊢ ∃ (x : FiniteMeasure E),
    Membership.mem (γ := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass ≤ C} x ∧
      (↑f : Filter (FiniteMeasure E)) ≤ 𝓝 x
have μlim_le : (μ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μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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
have refine_1 : Membership.mem (γ := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass ≤ C} μlim'
Tactic: refine ⟨μlim', ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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'
⊢ ∃ (x : FiniteMeasure E),
    Membership.mem (γ := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass ≤ C} x ∧
      (↑f : Filter (FiniteMeasure E)) ≤ 𝓝 x
have refine_2 : (↑f : Filter (FiniteMeasure E)) ≤ 𝓝 μlim'
Tactic: refine ⟨μlim', ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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 ⋯
⊢ Membership.mem (γ := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass ≤ C} μlim'
have refine_1 : ENNReal.toNNReal ((μlim : (a : Set E) → ℝ≥0∞) univ) ≤ C
Tactic: simp only [mem_setOf_eq, FiniteMeasure.mk_apply, μlim', FiniteMeasure.mass]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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) ≤ C
have refine_1 : ENNReal.toNNReal ((μlim : (a : Set E) → ℝ≥0∞) univ) ≤ (ENNReal.ofReal (↑C : ℝ)).toNNReal
Tactic: rw [show C = (ENNReal.ofReal ↑C).toNNReal by simp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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 ⋯
⊢ (↑f : Filter (FiniteMeasure E)) ≤ 𝓝 μlim'
have refine_2 : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μlim')
Tactic: change Tendsto id f (𝓝 μlim')
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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 ⋯
⊢ Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μlim')
have apply : ∀ (g : E →ᵇ ℝ),
  Tendsto (β := ℝ) (fun (i : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑(id i) : Measure E))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μlim' : Measure E)))
Tactic: apply FiniteMeasure.tendsto_of_forall_integral_tendsto (fun g ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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 ⋯
g : E →ᵇ ℝ
g' : E →C_c ℝ := { toFun := (⇑g : (a : E) → ℝ), continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
⊢ Tendsto (β := ℝ) (fun (i : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑(id i) : Measure E))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μlim' : Measure E)))
have h : ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μlim' : Measure E) = Λ g'
Tactic: convert! hΛ g'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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 ⋯
g : E →ᵇ ℝ
g' : E →C_c ℝ := { toFun := (⇑g : (a : E) → ℝ), continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
⊢ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μlim' : Measure E) = Λ g'
have h : ∫ (x : E), (g' : (a : E) → ℝ) x ∂(↑μlim' : Measure E) = Λ g'
Tactic: change ∫ (x : E), g' x ∂μlim' = Λ g'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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 ⋯
g : E →ᵇ ℝ
g' : E →C_c ℝ := { toFun := (⇑g : (a : E) → ℝ), continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
⊢ ∫ (x : E), (g' : (a : E) → ℝ) x ∂(↑μlim' : Measure E) = Λ g'
have h : (Λ' : (a : E →C_c ℝ) → ℝ) g' = Λ g'
Tactic: simp only [FiniteMeasure.toMeasure_mk, RealRMK.integral_rieszMeasure, μlim', μlim]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (hypothesis)
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
⊢ IsCompact.{u_1} (X := FiniteMeasure E) {μ : FiniteMeasure E | μ.mass = C}
have this : Eq.{u_1 + 1} (α := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass = C}
  ({μ : FiniteMeasure E | μ.mass ≤ C} ∩ {μ : FiniteMeasure E | μ.mass = C})
Tactic: have : {μ : FiniteMeasure E | μ.mass = C} = {μ | μ.mass ≤ C} ∩ {μ | μ.mass = C} := by grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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
this :
  Eq.{u_1 + 1} (α := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass = C}
    ({μ : FiniteMeasure E | μ.mass ≤ C} ∩ {μ : FiniteMeasure E | μ.mass = C})
⊢ IsCompact.{u_1} (X := FiniteMeasure E) {μ : FiniteMeasure E | μ.mass = C}
have rw : IsCompact.{u_1} (X := FiniteMeasure E) ({μ : FiniteMeasure E | μ.mass ≤ C} ∩ {μ : FiniteMeasure E | μ.mass = C})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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
this :
  Eq.{u_1 + 1} (α := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass = C}
    ({μ : FiniteMeasure E | μ.mass ≤ C} ∩ {μ : FiniteMeasure E | μ.mass = C})
⊢ IsCompact.{u_1} (X := FiniteMeasure E) ({μ : FiniteMeasure E | μ.mass ≤ C} ∩ {μ : FiniteMeasure E | μ.mass = C})
have apply : IsClosed[instTopologicalSpace] {μ : FiniteMeasure E | μ.mass = C}
Tactic: apply IsCompact.inter_right (isCompact_setOf_finiteMeasure_le_of_compactSpace E C)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
⊢ CompactSpace.{u_1} (ProbabilityMeasure E)
have isCompact_univ : IsCompact.{u_1} (X := ProbabilityMeasure E) univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
⊢ IsCompact.{u_1} (X := ProbabilityMeasure E) univ
have isCompact_univ : IsCompact.{u_1} (X := FiniteMeasure E) (ProbabilityMeasure.toFiniteMeasure '' univ)
Tactic: apply (ProbabilityMeasure.toFiniteMeasure_isEmbedding E).isCompact_iff.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (hypothesis)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
⊢ IsCompact.{u_1} (X := FiniteMeasure E)
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)}
have hf : IsClosedEmbedding f
Tactic: have hf : IsClosedEmbedding f := IsClosedEmbedding.subtypeVal hK.isClosed
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (hypothesis)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
⊢ IsCompact.{u_1} (X := FiniteMeasure E)
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)}
have rf : range f = K
Tactic: have rf : range f = K := Subtype.range_val
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
⊢ {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} = F '' T
have h₁ : {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} ⊆ F '' T
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
h₁ : {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} ⊆ F '' T
⊢ {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} = F '' T
have h₂ : F '' T ⊆ {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)}
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure E
hμ :
  Membership.mem (γ := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} μ
⊢ ∃ x ∈ T, F x = μ
have h₁ : F (FiniteMeasure.comap f μ) = μ
Tactic: refine ⟨μ.comap f, (FiniteMeasure.mass_comap_le _ _).trans hμ.1, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure E
hμ :
  Membership.mem (γ := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} μ
⊢ F (FiniteMeasure.comap f μ) = μ
have h₁ : ∀ (s : Set E) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((↑(F (FiniteMeasure.comap f μ)) : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs