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
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
g : E →ᵇ ℝ
ε : ℝ
εpos : ε > 0
I1 :
  ∀ᶠ (n : ℕ) in atTop,
    dist (α := ℝ)
        (@integral _ _ _ _ inst (∑ i ∈ Finset.range (n + 1), (↑(ν i) : Measure E)) fun (x : E) ↦ (g : (a : E) → ℝ) x)
        (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) <
      ε / 3
I2 : ∀ᶠ (n : ℕ) in atTop, ‖g‖ * (↑(u n) : ℝ) < ε / 3
n : ℕ
hn :
  dist (α := ℝ)
      (@integral _ _ _ _ inst (∑ i ∈ Finset.range (n + 1), (↑(ν i) : Measure E)) fun (x : E) ↦ (g : (a : E) → ℝ) x)
      (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) <
    ε / 3
h'n : ‖g‖ * (↑(u n) : ℝ) < ε / 3
⊢ Tendsto (β := ℝ)
    (fun (ρ : FiniteMeasure E) ↦
      @integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)) : Measure E) fun (x : E) ↦
        (g : (a : E) → ℝ) x)
    (↑f : Filter (FiniteMeasure E))
    (𝓝 (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) fun (x : E) ↦ (g : (a : E) → ℝ) x))
have apply : Tendsto (β := FiniteMeasure E) (fun (i : FiniteMeasure E) ↦ ∑ i_1 ∈ Finset.range (n + 1), i.restrict (disjointed K i_1))
  (↑f : Filter (FiniteMeasure E)) (𝓝 (∑ i ∈ Finset.range (n + 1), ν i))
Tactic: apply tendsto_iff_forall_integral_tendsto.1 _ g
-- 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
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
g : E →ᵇ ℝ
ε : ℝ
εpos : ε > 0
I1 :
  ∀ᶠ (n : ℕ) in atTop,
    dist (α := ℝ)
        (@integral _ _ _ _ inst (∑ i ∈ Finset.range (n + 1), (↑(ν i) : Measure E)) fun (x : E) ↦ (g : (a : E) → ℝ) x)
        (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) <
      ε / 3
I2 : ∀ᶠ (n : ℕ) in atTop, ‖g‖ * (↑(u n) : ℝ) < ε / 3
n : ℕ
hn :
  dist (α := ℝ)
      (@integral _ _ _ _ inst (∑ i ∈ Finset.range (n + 1), (↑(ν i) : Measure E)) fun (x : E) ↦ (g : (a : E) → ℝ) x)
      (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) <
    ε / 3
h'n : ‖g‖ * (↑(u n) : ℝ) < ε / 3
⊢ ∀ᶠ (x : FiniteMeasure E) in (↑f : Filter (FiniteMeasure E)),
    dist (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑(id x) : Measure E))
        (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) <
      ε
have this : Tendsto (β := ℝ)
  (fun (ρ : FiniteMeasure E) ↦
    @integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)) : Measure E) fun (x : E) ↦
      (g : (a : E) → ℝ) x)
  (↑f : Filter (FiniteMeasure E))
  (𝓝 (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) fun (x : E) ↦ (g : (a : E) → ℝ) x))
Tactic: have : Tendsto (fun (ρ : FiniteMeasure E) ↦
        ∫ x, g x ∂(∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i) : FiniteMeasure E)) f
        (𝓝 (∫ x, g x ∂(∑ i ∈ Finset.range (n + 1), ν i : FiniteMeasure E))) := by
      apply tendsto_iff_forall_integral_tendsto.1 _ g
      apply tendsto_finsetSum _ (fun i hi ↦ hν i)
-- 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
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
g : E →ᵇ ℝ
ε : ℝ
εpos : ε > 0
I1 :
  ∀ᶠ (n : ℕ) in atTop,
    dist (α := ℝ)
        (@integral _ _ _ _ inst (∑ i ∈ Finset.range (n + 1), (↑(ν i) : Measure E)) fun (x : E) ↦ (g : (a : E) → ℝ) x)
        (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) <
      ε / 3
I2 : ∀ᶠ (n : ℕ) in atTop, ‖g‖ * (↑(u n) : ℝ) < ε / 3
n : ℕ
hn :
  dist (α := ℝ)
      (@integral _ _ _ _ inst (∑ i ∈ Finset.range (n + 1), (↑(ν i) : Measure E)) fun (x : E) ↦ (g : (a : E) → ℝ) x)
      (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) <
    ε / 3
h'n : ‖g‖ * (↑(u n) : ℝ) < ε / 3
this :
  Tendsto (β := ℝ)
    (fun (ρ : FiniteMeasure E) ↦
      @integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)) : Measure E) fun (x : E) ↦
        (g : (a : E) → ℝ) x)
    (↑f : Filter (FiniteMeasure E))
    (𝓝 (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) fun (x : E) ↦ (g : (a : E) → ℝ) x))
⊢ ∀ᶠ (x : FiniteMeasure E) in (↑f : Filter (FiniteMeasure E)),
    dist (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑(id x) : Measure E))
        (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) <
      ε
have h₁ : ∀ (ρ : FiniteMeasure E)
  (hρ :
    dist (α := ℝ)
        (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)) : Measure E) fun (x : E) ↦
          (g : (a : E) → ℝ) x)
        (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) fun (x : E) ↦ (g : (a : E) → ℝ) x) <
      ε / 3)
  (h'ρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n),
  dist (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑(id ρ) : Measure E))
      (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) <
    ε
Tactic: filter_upwards [Metric.tendsto_nhds.1 this (ε / 3) (by positivity), hf] with ρ hρ 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
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
g : E →ᵇ ℝ
ε : ℝ
εpos : ε > 0
I1 :
  ∀ᶠ (n : ℕ) in atTop,
    dist (α := ℝ)
        (@integral _ _ _ _ inst (∑ i ∈ Finset.range (n + 1), (↑(ν i) : Measure E)) fun (x : E) ↦ (g : (a : E) → ℝ) x)
        (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) <
      ε / 3
I2 : ∀ᶠ (n : ℕ) in atTop, ‖g‖ * (↑(u n) : ℝ) < ε / 3
n : ℕ
hn :
  dist (α := ℝ)
      (@integral _ _ _ _ inst (∑ i ∈ Finset.range (n + 1), (↑(ν i) : Measure E)) fun (x : E) ↦ (g : (a : E) → ℝ) x)
      (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) <
    ε / 3
h'n : ‖g‖ * (↑(u n) : ℝ) < ε / 3
this :
  Tendsto (β := ℝ)
    (fun (ρ : FiniteMeasure E) ↦
      @integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)) : Measure E) fun (x : E) ↦
        (g : (a : E) → ℝ) x)
    (↑f : Filter (FiniteMeasure E))
    (𝓝 (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) fun (x : E) ↦ (g : (a : E) → ℝ) x))
ρ : FiniteMeasure E
hρ :
  dist (α := ℝ)
      (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)) : Measure E) fun (x : E) ↦
        (g : (a : E) → ℝ) x)
      (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) fun (x : E) ↦ (g : (a : E) → ℝ) x) <
    ε / 3
h'ρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ ρ = ρ.restrict ((partialSups K : (a : ℕ) → Set E) n)ᶜ + ∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)
have rw : ρ = ρ.restrict (((partialSups K : (a : ℕ) → Set E) n)ᶜ ∪ (partialSups K : (a : ℕ) → Set E) n)
Tactic: rw [I, ← FiniteMeasure.restrict_union disjoint_compl_left (A n).measurableSet]
-- 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
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
g : E →ᵇ ℝ
ε : ℝ
εpos : ε > 0
I1 :
  ∀ᶠ (n : ℕ) in atTop,
    dist (α := ℝ)
        (@integral _ _ _ _ inst (∑ i ∈ Finset.range (n + 1), (↑(ν i) : Measure E)) fun (x : E) ↦ (g : (a : E) → ℝ) x)
        (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) <
      ε / 3
I2 : ∀ᶠ (n : ℕ) in atTop, ‖g‖ * (↑(u n) : ℝ) < ε / 3
n : ℕ
hn :
  dist (α := ℝ)
      (@integral _ _ _ _ inst (∑ i ∈ Finset.range (n + 1), (↑(ν i) : Measure E)) fun (x : E) ↦ (g : (a : E) → ℝ) x)
      (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) <
    ε / 3
h'n : ‖g‖ * (↑(u n) : ℝ) < ε / 3
this :
  Tendsto (β := ℝ)
    (fun (ρ : FiniteMeasure E) ↦
      @integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)) : Measure E) fun (x : E) ↦
        (g : (a : E) → ℝ) x)
    (↑f : Filter (FiniteMeasure E))
    (𝓝 (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) fun (x : E) ↦ (g : (a : E) → ℝ) x))
ρ : FiniteMeasure E
hρ :
  dist (α := ℝ)
      (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)) : Measure E) fun (x : E) ↦
        (g : (a : E) → ℝ) x)
      (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) fun (x : E) ↦ (g : (a : E) → ℝ) x) <
    ε / 3
h'ρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ dist (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑ρ : Measure E))
      (@integral _ _ _ _ inst (∑ i ∈ Finset.range (n + 1), (↑(ρ.restrict (disjointed K i)) : Measure E)) fun (x : E) ↦
        (g : (a : E) → ℝ) x) <
    ε / 3
have this₁ : ρ = ρ.restrict ((partialSups K : (a : ℕ) → Set E) n)ᶜ + ∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)
Tactic: have : ρ = ρ.restrict (partialSups K n)ᶜ +
            ∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i) := by
          rw [I, ← FiniteMeasure.restrict_union disjoint_compl_left (A n).measurableSet]
          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
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
g : E →ᵇ ℝ
ε : ℝ
εpos : ε > 0
I1 :
  ∀ᶠ (n : ℕ) in atTop,
    dist (α := ℝ)
        (@integral _ _ _ _ inst (∑ i ∈ Finset.range (n + 1), (↑(ν i) : Measure E)) fun (x : E) ↦ (g : (a : E) → ℝ) x)
        (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) <
      ε / 3
I2 : ∀ᶠ (n : ℕ) in atTop, ‖g‖ * (↑(u n) : ℝ) < ε / 3
n : ℕ
hn :
  dist (α := ℝ)
      (@integral _ _ _ _ inst (∑ i ∈ Finset.range (n + 1), (↑(ν i) : Measure E)) fun (x : E) ↦ (g : (a : E) → ℝ) x)
      (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) <
    ε / 3
h'n : ‖g‖ * (↑(u n) : ℝ) < ε / 3
this_1 :
  Tendsto (β := ℝ)
    (fun (ρ : FiniteMeasure E) ↦
      @integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)) : Measure E) fun (x : E) ↦
        (g : (a : E) → ℝ) x)
    (↑f : Filter (FiniteMeasure E))
    (𝓝 (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) fun (x : E) ↦ (g : (a : E) → ℝ) x))
ρ : FiniteMeasure E
hρ :
  dist (α := ℝ)
      (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)) : Measure E) fun (x : E) ↦
        (g : (a : E) → ℝ) x)
      (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) fun (x : E) ↦ (g : (a : E) → ℝ) x) <
    ε / 3
h'ρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
this : ρ = ρ.restrict ((partialSups K : (a : ℕ) → Set E) n)ᶜ + ∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)
⊢ LE.le (α := ℝ)
    (∫ (x : E),
      norm (E := ℝ) ((g : (a : E) → ℝ) x : ℝ) ∂(↑(ρ.restrict ((partialSups K : (a : ℕ) → Set E) n)ᶜ) : Measure E))
    (∫ (x : E), ‖g‖ ∂(↑(ρ.restrict ((partialSups K : (a : ℕ) → Set E) n)ᶜ) : Measure E))
have hf₁ : (ae (↑(ρ.restrict ((partialSups K : (a : ℕ) → Set E) n)ᶜ) : Measure E)).EventuallyLE (β := ℝ) 0 fun (a : E) ↦
  norm (E := ℝ) ((g : (a : E) → ℝ) a : ℝ)
Tactic: apply integral_mono_of_nonneg
-- 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
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
g : E →ᵇ ℝ
ε : ℝ
εpos : ε > 0
I1 :
  ∀ᶠ (n : ℕ) in atTop,
    dist (α := ℝ)
        (@integral _ _ _ _ inst (∑ i ∈ Finset.range (n + 1), (↑(ν i) : Measure E)) fun (x : E) ↦ (g : (a : E) → ℝ) x)
        (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) <
      ε / 3
I2 : ∀ᶠ (n : ℕ) in atTop, ‖g‖ * (↑(u n) : ℝ) < ε / 3
n : ℕ
hn :
  dist (α := ℝ)
      (@integral _ _ _ _ inst (∑ i ∈ Finset.range (n + 1), (↑(ν i) : Measure E)) fun (x : E) ↦ (g : (a : E) → ℝ) x)
      (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) <
    ε / 3
h'n : ‖g‖ * (↑(u n) : ℝ) < ε / 3
this_1 :
  Tendsto (β := ℝ)
    (fun (ρ : FiniteMeasure E) ↦
      @integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)) : Measure E) fun (x : E) ↦
        (g : (a : E) → ℝ) x)
    (↑f : Filter (FiniteMeasure E))
    (𝓝 (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) fun (x : E) ↦ (g : (a : E) → ℝ) x))
ρ : FiniteMeasure E
hρ :
  dist (α := ℝ)
      (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)) : Measure E) fun (x : E) ↦
        (g : (a : E) → ℝ) x)
      (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) fun (x : E) ↦ (g : (a : E) → ℝ) x) <
    ε / 3
h'ρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
this : ρ = ρ.restrict ((partialSups K : (a : ℕ) → Set E) n)ᶜ + ∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)
⊢ (ae (↑(ρ.restrict ((partialSups K : (a : ℕ) → Set E) n)ᶜ) : Measure E)).EventuallyLE (β := ℝ) 0 fun (a : E) ↦
    norm (E := ℝ) ((g : (a : E) → ℝ) a : ℝ)
have hf₁ : ∀ (a : E),
  Membership.mem (γ := Set E)
    {x : E | (fun (x : E) ↦ LE.le (α := ℝ) (0 x) ((fun (a : E) ↦ norm (E := ℝ) ((g : (a : E) → ℝ) a : ℝ)) x)) x} a
Tactic: filter_upwards with x using by positivity
-- 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
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
g : E →ᵇ ℝ
ε : ℝ
εpos : ε > 0
I1 :
  ∀ᶠ (n : ℕ) in atTop,
    dist (α := ℝ)
        (@integral _ _ _ _ inst (∑ i ∈ Finset.range (n + 1), (↑(ν i) : Measure E)) fun (x : E) ↦ (g : (a : E) → ℝ) x)
        (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) <
      ε / 3
I2 : ∀ᶠ (n : ℕ) in atTop, ‖g‖ * (↑(u n) : ℝ) < ε / 3
n : ℕ
hn :
  dist (α := ℝ)
      (@integral _ _ _ _ inst (∑ i ∈ Finset.range (n + 1), (↑(ν i) : Measure E)) fun (x : E) ↦ (g : (a : E) → ℝ) x)
      (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) <
    ε / 3
h'n : ‖g‖ * (↑(u n) : ℝ) < ε / 3
this_1 :
  Tendsto (β := ℝ)
    (fun (ρ : FiniteMeasure E) ↦
      @integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)) : Measure E) fun (x : E) ↦
        (g : (a : E) → ℝ) x)
    (↑f : Filter (FiniteMeasure E))
    (𝓝 (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) fun (x : E) ↦ (g : (a : E) → ℝ) x))
ρ : FiniteMeasure E
hρ :
  dist (α := ℝ)
      (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)) : Measure E) fun (x : E) ↦
        (g : (a : E) → ℝ) x)
      (@integral _ _ _ _ inst (↑(∑ i ∈ Finset.range (n + 1), ν i) : Measure E) fun (x : E) ↦ (g : (a : E) → ℝ) x) <
    ε / 3
h'ρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
this : ρ = ρ.restrict ((partialSups K : (a : ℕ) → Set E) n)ᶜ + ∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)
hf₁ :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E | (fun (x : E) ↦ LE.le (α := ℝ) (0 x) ((fun (a : E) ↦ norm (E := ℝ) ((g : (a : E) → ℝ) a : ℝ)) x)) x} a
⊢ (ae (↑(ρ.restrict ((partialSups K : (a : ℕ) → Set E) n)ᶜ) : Measure E)).EventuallyLE (β := ℝ) 0 fun (a : E) ↦
    norm (E := ℝ) ((g : (a : E) → ℝ) a : ℝ)
have hf₂ : ∀ (a : E), 0 a ≤ norm (E := ℝ) ((g : (a : E) → ℝ) a : ℝ)
Tactic: filter_upwards with x using by positivity