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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
x : E
h :
  LE.le (α := (fun (a : E) ↦ ℝ) x) (|(g : (a : E) → ℝ) x| : (fun (a : E) ↦ ℝ) x)
    ((fun (x : E) ↦ ‖g.toBoundedContinuousFunction‖) x : ℝ)
⊢ LE.le (α := (fun (a : E) ↦ ℝ) x) ((g : (a : E) → ℝ) x : ℝ) ((fun (x : E) ↦ ‖g.toBoundedContinuousFunction‖) x : ℝ)

Tactic:
apply le_of_abs_le

Premises used: le_of_abs_le
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
x : E
⊢ LE.le (α := (fun (a : E) ↦ ℝ) x) (|(g : (a : E) → ℝ) x| : (fun (a : E) ↦ ℝ) x)
    ((fun (x : E) ↦ ‖g.toBoundedContinuousFunction‖) x : ℝ)

Tactic:
g.toBoundedContinuousFunction.norm_coe_le_norm x

Premises used: CompactlySupportedContinuousMap.toBoundedContinuousFunction, BoundedContinuousFunction.norm_coe_le_norm
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
x : E
⊢ LE.le (α := (fun (a : E) ↦ ℝ) x) (|(g : (a : E) → ℝ) x| : (fun (a : E) ↦ ℝ) x)
    ((fun (x : E) ↦ ‖g.toBoundedContinuousFunction‖) x : ℝ)

Tactic:
exact g.toBoundedContinuousFunction.norm_coe_le_norm x

Premises used: CompactlySupportedContinuousMap.toBoundedContinuousFunction, BoundedContinuousFunction.norm_coe_le_norm
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
simp : (↑μ : Measure E).real univ * ‖g.toBoundedContinuousFunction‖ ≤ (↑C : ℝ) * ‖g.toBoundedContinuousFunction‖
⊢ ∫ (x : E), ‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E) ≤ (↑C : ℝ) * ‖g.toBoundedContinuousFunction‖

Tactic:
simp only [integral_const, smul_eq_mul]

Premises used: MeasureTheory.integral_const, smul_eq_mul
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
calc :
  LE.le (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
    (∫ (x : E), ‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E))
calc₁ : ∫ (x : E), ‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E) ≤ (↑C : ℝ) * ‖g.toBoundedContinuousFunction‖
⊢ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : 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μ

Premises used: CompactlySupportedContinuousMap.toBoundedContinuousFunction
-- 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 ℝ),
    ∃ 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μ
-- 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
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)
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
⊢ ∃ (x : FiniteMeasure E),
    Membership.mem (γ := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass ≤ C} x ∧
      (↑f : Filter (FiniteMeasure E)) ≤ 𝓝 x

Tactic:
choose Λ h₀Λ hΛ using L
-- 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 ℝ
⊢ Tendsto
    (fun (x : FiniteMeasure E) ↦
      HAdd.hAdd (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑x : Measure E))
        (∫ (x : E), (g' : (a : E) → ℝ) x ∂(↑x : Measure E)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g + Λ g'))

Tactic:
(hΛ g).add (hΛ g')

Premises used: Filter.Tendsto.add
-- 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 ℝ
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))
⊢ 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:
convert! (hΛ g).add (hΛ g')

Premises used: Filter.Tendsto.add
-- 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 ℝ
x : FiniteMeasure E
h : Integrable (ε := ℝ) (⇑g : (a : E) → ℝ) (↑x : Measure 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))

Tactic:
rw [integral_add]

Premises used: MeasureTheory.integral_add
-- 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 ℝ
x : FiniteMeasure E
⊢ Integrable (ε := ℝ) (⇑g : (a : E) → ℝ) (↑x : 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 ℝ
x : FiniteMeasure E
⊢ Integrable (ε := ℝ) (⇑g : (a : E) → ℝ) (↑x : 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 ℝ
x : FiniteMeasure E
⊢ Integrable (ε := ℝ) (⇑g' : (a : E) → ℝ) (↑x : 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 ℝ
x : FiniteMeasure E
⊢ Integrable (ε := ℝ) (⇑g' : (a : E) → ℝ) (↑x : 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 ℝ
⊢ 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
-- 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 ℝ
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'))
⊢ Λ (g + g') = Λ g + Λ g'

Tactic:
tendsto_nhds_unique (hΛ (g + g')) this

Premises used: HAdd.hAdd, tendsto_nhds_unique
-- 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 ℝ
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'))
⊢ Λ (g + g') = Λ g + Λ g'

Tactic:
exact tendsto_nhds_unique (hΛ (g + g')) this

Premises used: HAdd.hAdd, tendsto_nhds_unique
-- 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))
c : ℝ
g : E →C_c ℝ
⊢ Tendsto (fun (x : FiniteMeasure E) ↦ HSMul.hSMul (β := ℝ) c (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑x : Measure E)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (c • Λ g))

Tactic:
(hΛ g).const_smul c

Premises used: Filter.Tendsto.const_smul
-- 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))
c : ℝ
g : E →C_c ℝ
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))
⊢ Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), HSMul.hSMul (β := ℝ) c ((g : (a : E) → ℝ) x : ℝ) ∂(↑μ : Measure E))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (c • Λ g))

Tactic:
convert! (hΛ g).const_smul c

Premises used: Filter.Tendsto.const_smul
-- 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))
c : ℝ
g : E →C_c ℝ
x : FiniteMeasure E
h 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))
⊢ ∫ (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:
rw [integral_smul]

Premises used: MeasureTheory.integral_smul
-- 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))
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))

Tactic:
have : Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ x, c • g x ∂μ) f (𝓝 (c • Λ g)) := by
        convert! (hΛ g).const_smul c
        rw [integral_smul]
-- 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))
c : ℝ
g : E →C_c ℝ
this :
  Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), HSMul.hSMul (β := ℝ) c ((g : (a : E) → ℝ) x : ℝ) ∂(↑μ : Measure E))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (c • Λ g))
⊢ Λ (c • g) = HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ) (Λ g)

Tactic:
tendsto_nhds_unique (hΛ (c • g)) this

Premises used: HSMul.hSMul, tendsto_nhds_unique
-- 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))
c : ℝ
g : E →C_c ℝ
this :
  Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), HSMul.hSMul (β := ℝ) c ((g : (a : E) → ℝ) x : ℝ) ∂(↑μ : Measure E))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (c • Λ g))
⊢ Λ (c • g) = HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ) (Λ g)

Tactic:
exact tendsto_nhds_unique (hΛ (c • g)) this

Premises used: HSMul.hSMul, tendsto_nhds_unique
-- 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'
apply :
  ∀ (μ : FiniteMeasure E),
    LE.le (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (∫ (x : E), (g' : (a : E) → ℝ) x ∂(↑μ : Measure E))
⊢ Λ g ≤ Λ g'

Tactic:
apply le_of_tendsto_of_tendsto' (hΛ g) (hΛ g') (fun μ ↦ ?_)

Premises used: le_of_tendsto_of_tendsto'