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)
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)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this_2 :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
this : mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i) ≤ u n
⊢ (((↑(∑ i ∈ Finset.Ioc n m, ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑(u n) : ℝ≥0∞)
have h₁ : (((↑(∑ i ∈ Finset.Ioc n m, ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ =
  (↑(mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i)) : ℝ≥0∞)
Tactic: convert! ENNReal.coe_le_coe.2 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
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
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)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
⊢ (((↑(∑ i ∈ Finset.Ioc n m, ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑(u n) : ℝ≥0∞)
have h₁ : mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i) ≤ u n
Tactic: suffices (∑ i ∈ Finset.Ioc n m, ν i).mass ≤ u n by
      convert! ENNReal.coe_le_coe.2 this
      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)
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)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
⊢ Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i)))
have h₁ : Tendsto (β := FiniteMeasure E) (fun (i : FiniteMeasure E) ↦ ∑ i_1 ∈ Finset.Ioc n m, i.restrict (disjointed K i_1))
  (↑f : Filter (FiniteMeasure E)) (𝓝 (∑ i ∈ Finset.Ioc n m, ν i))
Tactic: apply Tendsto.mass
-- 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)
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)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
⊢ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i) ≤ u n
have this₁ : Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)))
  (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i)))
Tactic: have : Tendsto (fun (μ : FiniteMeasure E) ↦
        (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)).mass) f
        (𝓝 ((∑ i ∈ Finset.Ioc n m, ν i).mass)) := by
      apply Tendsto.mass
      exact 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)
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)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this_2 :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
this :
  Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i)))
⊢ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i) ≤ u n
have h₁ : ∀ᶠ (c : FiniteMeasure E) in (↑f : Filter (FiniteMeasure E)),
  mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, c.restrict (disjointed K i)) ≤ u n
Tactic: apply le_of_tendsto 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
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
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)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this_2 :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
this :
  Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i)))
⊢ ∀ᶠ (c : FiniteMeasure E) in (↑f : Filter (FiniteMeasure E)),
    mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, c.restrict (disjointed K i)) ≤ u n
have h₁ : ∀ (μ : FiniteMeasure E) (hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n),
  mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)) ≤ u n
Tactic: filter_upwards [hf] with μ 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)
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∞)
μ_1 : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ_1)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this_2 :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
this :
  Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i)))
μ : FiniteMeasure E
hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ ∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i) = μ.restrict (K m \ K n)
have hd : (↑(Finset.Ioc n m) : Set ℕ).Pairwise (Disjoint on disjointed K)
Tactic: rw [← biUnion_Ioc_disjointed_of_monotone h hm, FiniteMeasure.restrict_biUnion_finset]
-- 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)
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∞)
μ_1 : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ_1)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this_2 :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
this :
  Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i)))
μ : FiniteMeasure E
hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
hd : (↑(Finset.Ioc n m) : Set ℕ).Pairwise (Disjoint on disjointed K)
⊢ ∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i) = μ.restrict (K m \ K n)
have hm₁ : ∀ (i : ℕ), MeasurableSet (disjointed K i)
Tactic: rw [← biUnion_Ioc_disjointed_of_monotone h hm, FiniteMeasure.restrict_biUnion_finset]
-- 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)
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∞)
μ_1 : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ_1)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this_2 :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
this :
  Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i)))
μ : FiniteMeasure E
hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)) ≤ u n
have this₁ : ∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i) = μ.restrict (K m \ K n)
Tactic: have : ∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i) = μ.restrict (K m \ K n) := by
      rw [← biUnion_Ioc_disjointed_of_monotone h hm, FiniteMeasure.restrict_biUnion_finset]
      · exact (disjoint_disjointed K).set_pairwise _
      · exact MeasurableSet.disjointed (fun i ↦ (hK i).measurableSet)
-- 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)
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∞)
μ_1 : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ_1)
n : ℕ
h : Monotone K
this_1 :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this_2 :
  Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
this_3 :
  Tendsto (fun (μ : FiniteMeasure E) ↦ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i)))
μ : FiniteMeasure E
hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
this : ∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i) = μ.restrict (K m \ K n)
⊢ mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)) ≤ u n
have h₁ : (μ : (a : Set E) → ℝ≥0) (K m \ K n) ≤ u n
Tactic: rw [this, restrict_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
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
⊢ Eq.{u_1 + 1} (α := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass = C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}
    ({μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∩
      {μ : FiniteMeasure E | μ.mass = C})
have h₁ : ∀ (x : FiniteMeasure E),
  Membership.mem (γ := Set (FiniteMeasure E))
      {μ : FiniteMeasure E | μ.mass = C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} x ↔
    Membership.mem (γ := Set (FiniteMeasure E))
      ({μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∩
        {μ : FiniteMeasure E | μ.mass = C})
      x
Tactic: ext
-- 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
⊢ IsCompact.{u_1} (X := FiniteMeasure E)
    {μ : FiniteMeasure E | μ.mass = C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}
have this : Eq.{u_1 + 1} (α := Set (FiniteMeasure E))
  {μ : FiniteMeasure E | μ.mass = C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n}
  ({μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∩
    {μ : FiniteMeasure E | μ.mass = C})
Tactic: have : {μ : FiniteMeasure E | μ.mass = C ∧ ∀ n, μ (K n)ᶜ ≤ u n} =
    {μ | μ.mass ≤ C ∧ ∀ n, μ (K n)ᶜ ≤ u n} ∩ {μ | μ.mass = C} := by ext; grind