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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ -((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ≤ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)
have calc : -((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ≤ ∫ (x : E), -‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E)
Tactic: calc - (C * ‖g.toBoundedContinuousFunction‖)
      _ ≤ ∫ (x : E), - ‖g.toBoundedContinuousFunction‖ ∂μ := by
        simp only [integral_const, smul_eq_mul, mul_neg, neg_le_neg_iff]
        gcongr
        exact hμ
      _ ≤ ∫ x, g x ∂μ := by
        gcongr
        · simp
        · exact g.continuous.integrable_of_hasCompactSupport g.hasCompactSupport
        · intro x
          apply neg_le_of_abs_le
          exact g.toBoundedContinuousFunction.norm_coe_le_norm x
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
calc : -((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ≤ ∫ (x : E), -‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E)
⊢ -((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ≤ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)
have calc₁ : LE.le (α := ℝ) (∫ (x : E), -‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E))
  (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
Tactic: calc - (C * ‖g.toBoundedContinuousFunction‖)
      _ ≤ ∫ (x : E), - ‖g.toBoundedContinuousFunction‖ ∂μ := by
        simp only [integral_const, smul_eq_mul, mul_neg, neg_le_neg_iff]
        gcongr
        exact hμ
      _ ≤ ∫ x, g x ∂μ := by
        gcongr
        · simp
        · exact g.continuous.integrable_of_hasCompactSupport g.hasCompactSupport
        · intro x
          apply neg_le_of_abs_le
          exact g.toBoundedContinuousFunction.norm_coe_le_norm x
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ LE.le (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
    (∫ (x : E), ‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E))
have hf₁ : Integrable (ε := ℝ) (⇑g : (a : E) → ℝ) (↑μ : Measure E)
Tactic: gcongr
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
hf₁ : Integrable (ε := ℝ) (⇑g : (a : E) → ℝ) (↑μ : Measure E)
⊢ LE.le (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
    (∫ (x : E), ‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E))
have hg : Integrable (ε := ℝ) (fun (x : E) ↦ ‖g.toBoundedContinuousFunction‖) (↑μ : Measure E)
Tactic: gcongr
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
hf₁ : Integrable (ε := ℝ) (⇑g : (a : E) → ℝ) (↑μ : Measure E)
hg : Integrable (ε := ℝ) (fun (x : E) ↦ ‖g.toBoundedContinuousFunction‖) (↑μ : Measure E)
⊢ LE.le (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
    (∫ (x : E), ‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E))
have h : LE.le (α := E → ℝ) (⇑g : (a : E) → ℝ) fun (x : E) ↦ ‖g.toBoundedContinuousFunction‖
Tactic: gcongr
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
x : E
⊢ LE.le (α := (fun (a : E) ↦ ℝ) x) ((g : (a : E) → ℝ) x : ℝ) ((fun (x : E) ↦ ‖g.toBoundedContinuousFunction‖) x : ℝ)
have h : LE.le (α := (fun (a : E) ↦ ℝ) x) (|(g : (a : E) → ℝ) x| : (fun (a : E) ↦ ℝ) x)
  ((fun (x : E) ↦ ‖g.toBoundedContinuousFunction‖) x : ℝ)
Tactic: apply le_of_abs_le
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ ∫ (x : E), ‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E) ≤ (↑C : ℝ) * ‖g.toBoundedContinuousFunction‖
have simp : (↑μ : Measure E).real univ * ‖g.toBoundedContinuousFunction‖ ≤ (↑C : ℝ) * ‖g.toBoundedContinuousFunction‖
Tactic: simp only [integral_const, smul_eq_mul]
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E) ≤ (↑C : ℝ) * ‖g.toBoundedContinuousFunction‖
have calc : LE.le (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
  (∫ (x : E), ‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E))
Tactic: calc ∫ x, g x ∂μ
      _ ≤ ∫ (x : E), ‖g.toBoundedContinuousFunction‖ ∂μ := by
        gcongr
        · exact g.continuous.integrable_of_hasCompactSupport g.hasCompactSupport
        · simp
        · intro x
          apply le_of_abs_le
          exact g.toBoundedContinuousFunction.norm_coe_le_norm x
      _ ≤ C * ‖g.toBoundedContinuousFunction‖ := by
        simp only [integral_const, smul_eq_mul]
        gcongr
        exact 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
calc :
  LE.le (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
    (∫ (x : E), ‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E))
⊢ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E) ≤ (↑C : ℝ) * ‖g.toBoundedContinuousFunction‖
have calc₁ : ∫ (x : E), ‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E) ≤ (↑C : ℝ) * ‖g.toBoundedContinuousFunction‖
Tactic: calc ∫ x, g x ∂μ
      _ ≤ ∫ (x : E), ‖g.toBoundedContinuousFunction‖ ∂μ := by
        gcongr
        · exact g.continuous.integrable_of_hasCompactSupport g.hasCompactSupport
        · simp
        · intro x
          apply le_of_abs_le
          exact g.toBoundedContinuousFunction.norm_coe_le_norm x
      _ ≤ C * ‖g.toBoundedContinuousFunction‖ := by
        simp only [integral_const, smul_eq_mul]
        gcongr
        exact 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
⊢ ∃ (x : FiniteMeasure E),
    Membership.mem (γ := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass ≤ C} x ∧
      (↑f : Filter (FiniteMeasure E)) ≤ 𝓝 x
have L : ∀ (g : E →C_c ℝ),
  ∃ x ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 x)
Tactic: have L (g : C_c(E, ℝ)) :
      ∃ x ∈ Icc (-C * ‖g.toBoundedContinuousFunction‖) (C * ‖g.toBoundedContinuousFunction‖),
      Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ x, g x ∂μ) f (𝓝 x) := by
    simp only [Tendsto, ← Ultrafilter.coe_map]
    apply IsCompact.ultrafilter_le_nhds' isCompact_Icc
    simp only [neg_mul, Ultrafilter.mem_map]
    filter_upwards [hf] with μ hμ
    simp only [mem_preimage, mem_Icc]
    refine ⟨?_, ?_⟩
    · calc - (C * ‖g.toBoundedContinuousFunction‖)
      _ ≤ ∫ (x : E), - ‖g.toBoundedContinuousFunction‖ ∂μ := by
        simp only [integral_const, smul_eq_mul, mul_neg, neg_le_neg_iff]
        gcongr
        exact hμ
      _ ≤ ∫ x, g x ∂μ := by
        gcongr
        · simp
        · exact g.continuous.integrable_of_hasCompactSupport g.hasCompactSupport
        · intro x
          apply neg_le_of_abs_le
          exact g.toBoundedContinuousFunction.norm_coe_le_norm x
    · calc ∫ x, g x ∂μ
      _ ≤ ∫ (x : E), ‖g.toBoundedContinuousFunction‖ ∂μ := by
        gcongr
        · exact g.continuous.integrable_of_hasCompactSupport g.hasCompactSupport
        · simp
        · intro x
          apply le_of_abs_le
          exact g.toBoundedContinuousFunction.norm_coe_le_norm x
      _ ≤ C * ‖g.toBoundedContinuousFunction‖ := by
        simp only [integral_const, smul_eq_mul]
        gcongr
        exact 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
L :
  ∀ (g : E →C_c ℝ),
    ∃ x ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖),
      Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
        (↑f : Filter (FiniteMeasure E)) (𝓝 x)
⊢ ∃ (x : FiniteMeasure E),
    Membership.mem (γ := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass ≤ C} x ∧
      (↑f : Filter (FiniteMeasure E)) ≤ 𝓝 x
have choose : ∀ (Λ : (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))),
  ∃ (x : FiniteMeasure E),
    Membership.mem (γ := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass ≤ C} x ∧
      (↑f : Filter (FiniteMeasure E)) ≤ 𝓝 x
Tactic: choose Λ h₀Λ hΛ using L
Cleared hypotheses: L
-- 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))
g g' : E →C_c ℝ
⊢ Tendsto
    (fun (μ : FiniteMeasure E) ↦
      ∫ (x : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g' : (a : E) → ℝ) x : ℝ) ∂(↑μ : Measure E))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g + Λ g'))
have h : ∀ (x : FiniteMeasure E),
  ∫ (x : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g' : (a : E) → ℝ) x : ℝ) ∂(↑x : Measure E) =
    HAdd.hAdd (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑x : Measure E))
      (∫ (x : E), (g' : (a : E) → ℝ) x ∂(↑x : Measure E))
Tactic: convert! (hΛ g).add (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))
g g' : E →C_c ℝ
x : FiniteMeasure E
⊢ ∫ (x : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g' : (a : E) → ℝ) x : ℝ) ∂(↑x : Measure E) =
    HAdd.hAdd (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑x : Measure E))
      (∫ (x : E), (g' : (a : E) → ℝ) x ∂(↑x : Measure E))
have h : Integrable (ε := ℝ) (⇑g : (a : E) → ℝ) (↑x : Measure E)
Tactic: rw [integral_add]
-- 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))
g g' : E →C_c ℝ
x : FiniteMeasure E
h : Integrable (ε := ℝ) (⇑g : (a : E) → ℝ) (↑x : Measure E)
⊢ ∫ (x : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g' : (a : E) → ℝ) x : ℝ) ∂(↑x : Measure E) =
    HAdd.hAdd (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑x : Measure E))
      (∫ (x : E), (g' : (a : E) → ℝ) x ∂(↑x : Measure E))
have h₁ : Integrable (ε := ℝ) (⇑g' : (a : E) → ℝ) (↑x : Measure E)
Tactic: rw [integral_add]
-- 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))
g g' : E →C_c ℝ
⊢ Λ (g + g') = Λ g + Λ g'
have this : Tendsto
  (fun (μ : FiniteMeasure E) ↦
    ∫ (x : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((g' : (a : E) → ℝ) x : ℝ) ∂(↑μ : Measure E))
  (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g + Λ g'))
Tactic: have : Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ x, g x + g' x ∂μ) f (𝓝 (Λ g + Λ g')) := by
        convert! (hΛ g).add (hΛ g')
        rw [integral_add]
        · exact g.continuous.integrable_of_hasCompactSupport g.hasCompactSupport
        · exact g'.continuous.integrable_of_hasCompactSupport g'.hasCompactSupport
-- 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))
c : ℝ
g : E →C_c ℝ
⊢ Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), HSMul.hSMul (β := ℝ) c ((g : (a : E) → ℝ) x : ℝ) ∂(↑μ : Measure E))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (c • Λ g))
have h : ∀ (x : FiniteMeasure E),
  ∫ (x : E), HSMul.hSMul (β := ℝ) c ((g : (a : E) → ℝ) x : ℝ) ∂(↑x : Measure E) =
    HSMul.hSMul (β := ℝ) c (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑x : Measure E))
Tactic: convert! (hΛ g).const_smul 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
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))
c : ℝ
g : E →C_c ℝ
x : FiniteMeasure E
⊢ ∫ (x : E), HSMul.hSMul (β := ℝ) c ((g : (a : E) → ℝ) x : ℝ) ∂(↑x : Measure E) =
    HSMul.hSMul (β := ℝ) c (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑x : Measure E))
have h : HSMul.hSMul (β := ℝ) c (∫ (a : E), (g : (a : E) → ℝ) a ∂(↑x : Measure E)) =
  HSMul.hSMul (β := ℝ) c (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑x : Measure E))
Tactic: rw [integral_smul]
-- 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))
c : ℝ
g : E →C_c ℝ
⊢ Λ (c • g) = HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ) (Λ g)
have this : Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), HSMul.hSMul (β := ℝ) c ((g : (a : E) → ℝ) x : ℝ) ∂(↑μ : Measure E))
  (↑f : Filter (FiniteMeasure E)) (𝓝 (c • Λ g))
Tactic: have : Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ x, c • g x ∂μ) f (𝓝 (c • Λ g)) := by
        convert! (hΛ g).const_smul c
        rw [integral_smul]
-- 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))
g g' : E →C_c ℝ
hgg' : g ≤ g'
⊢ Λ g ≤ Λ g'
have apply : ∀ (μ : FiniteMeasure E),
  LE.le (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) (∫ (x : E), (g' : (a : E) → ℝ) x ∂(↑μ : Measure E))
Tactic: apply le_of_tendsto_of_tendsto' (hΛ g) (hΛ g') (fun μ ↦ ?_)
-- 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))
g g' : E →C_c ℝ
hgg' : g ≤ g'
μ : FiniteMeasure E
⊢ LE.le (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) (∫ (x : E), (g' : (a : E) → ℝ) x ∂(↑μ : Measure E))
have apply : Integrable (ε := ℝ) (⇑g : (a : E) → ℝ) (↑μ : Measure E)
Tactic: apply integral_mono _ _ hgg'
-- 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))
g g' : E →C_c ℝ
hgg' : g ≤ g'
μ : FiniteMeasure 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))
have apply₁ : Integrable (ε := ℝ) (⇑g' : (a : E) → ℝ) (↑μ : Measure E)
Tactic: apply integral_mono _ _ hgg'
-- 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 Λ'
o : E →C_c ℝ := { toFun := 1, continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
⊢ (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal (↑C : ℝ)
have this : (μ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])
-- 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)
⊢ (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal (↑C : ℝ)
have apply : ENNReal.ofReal ((Λ' : (a : E →C_c ℝ) → ℝ) o) ≤ ENNReal.ofReal (↑C : ℝ)
Tactic: apply this.trans
-- 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)
⊢ ENNReal.ofReal ((Λ' : (a : E →C_c ℝ) → ℝ) o) ≤ ENNReal.ofReal (↑C : ℝ)
have h : (Λ' : (a : E →C_c ℝ) → ℝ) o ≤ (↑C : ℝ)
Tactic: gcongr