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
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 :
  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
i : ℕ
hi : i ≤ m
h'i : i ≤ n
⊢ (K n)ᶜ ⊆ (K i)ᶜ

Tactic:
compl_subset_compl.2 (h h'i)

Premises used: Iff.mpr, Set.compl_subset_compl
-- 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
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 :
  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
i : ℕ
hi : i ≤ m
h'i : i ≤ n
⊢ (K n)ᶜ ⊆ (K i)ᶜ

Tactic:
exact compl_subset_compl.2 (h h'i)

Premises used: Iff.mpr, Set.compl_subset_compl
-- 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
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 :
  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
⊢ 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)ᶜ)

Tactic:
have : ∑ i ∈ Finset.range (m + 1), (ν i : Measure E) (K n)ᶜ
        = ∑ i ∈ Finset.Ioc n m, (ν i : Measure E) (K n)ᶜ := by
      apply (Finset.sum_subset (by grind) _).symm
      simp +contextual only [Finset.mem_range_succ_iff, Finset.mem_Ioc, not_and,
        not_true_eq_false, imp_false, not_lt, ← null_iff_toMeasure_null]
      intro i hi h'i
      apply (ν i).mono_null _ (νK i)
      rw [Monotone.partialSups_eq h]
      exact compl_subset_compl.2 (h h'i)
-- 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
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)ᶜ)
h₁ : ∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ ≤ (↑(u n) : ℝ≥0∞)
⊢ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ ≤ (↑(u n) : ℝ≥0∞)

Tactic:
rw [this]
-- 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
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 : (((↑(∑ i ∈ Finset.Ioc n m, ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑(u n) : ℝ≥0∞)
apply :
  LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ : ℝ≥0∞)
    ((((↑(∑ i ∈ Finset.Ioc n m, ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ ≤ (↑(u n) : ℝ≥0∞)

Tactic:
apply le_trans _ this

Premises used: le_trans
-- 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
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 : (((↑(∑ i ∈ Finset.Ioc n m, ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑(u n) : ℝ≥0∞)
simp :
  LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ c ∈ Finset.Ioc n m, ((↑(ν c) : Measure E) : (a : Set E) → ℝ≥0∞) univ)
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ : ℝ≥0∞)
    ((((↑(∑ i ∈ Finset.Ioc n m, ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
simp only [toMeasure_sum, Measure.coe_finsetSum, Finset.sum_apply]

Premises used: MeasureTheory.Measure.coe_finsetSum, Finset.sum_apply, MeasureTheory.FiniteMeasure.toMeasure_sum
-- 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
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 : (((↑(∑ i ∈ Finset.Ioc n m, ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑(u n) : ℝ≥0∞)
h₁ : ∀ i ∈ Finset.Ioc n m, (K n)ᶜ ⊆ univ
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    (∑ c ∈ Finset.Ioc n m, ((↑(ν c) : Measure E) : (a : Set E) → ℝ≥0∞) univ)

Tactic:
gcongr
-- 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
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 : (((↑(∑ i ∈ Finset.Ioc n m, ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑(u n) : ℝ≥0∞)
i : ℕ
h_1 : i ∈ Finset.Ioc n m
⊢ (K n)ᶜ ⊆ univ

Tactic:
simp
-- 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
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)ᶜ)
h₁ : (((↑(∑ i ∈ Finset.Ioc n m, ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑(u n) : ℝ≥0∞)
⊢ ∑ i ∈ Finset.Ioc n m, ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ ≤ (↑(u n) : ℝ≥0∞)

Tactic:
suffices (∑ i ∈ Finset.Ioc n m, ν i).toMeasure univ ≤ u n by
      apply le_trans _ this
      simp only [toMeasure_sum, Measure.coe_finsetSum, Finset.sum_apply]
      gcongr
      simp
-- 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
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
⊢ (↑(mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i)) : ℝ≥0∞) ≤ (↑(u n) : ℝ≥0∞)

Tactic:
ENNReal.coe_le_coe.2 this

Premises used: Iff.mpr, ENNReal.coe_le_coe
-- 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
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
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∞)
⊢ (((↑(∑ i ∈ Finset.Ioc n m, ν i) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑(u n) : ℝ≥0∞)

Tactic:
convert! ENNReal.coe_le_coe.2 this

Premises used: Iff.mpr, ENNReal.coe_le_coe
-- 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
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 =
    (↑(mass.{u_1} (Ω := E) (∑ i ∈ Finset.Ioc n m, ν i)) : ℝ≥0∞)

Tactic:
simp