awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
h_limsup_le :
  ∀ (r : ℝ) (hr : 0 < r),
    limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < |⟪z, x⟫|}) atTop ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z))
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ (x : ℝ) (hx : x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)), ‖1 - f (x • z)‖ ≤ ε / 4
hf_meas : Measurable f
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))).EventuallyLE (β := ℝ)
    (fun (x : ℝ) ↦ ‖1 - f (x • z)‖) fun (x : ℝ) ↦ ε / 4

Tactic:
exact ae_restrict_of_forall_mem measurableSet_Ioc h_le_Ioc

Premises used: MeasureTheory.ae_restrict_of_forall_mem, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
h_limsup_le :
  ∀ (r : ℝ) (hr : 0 < r),
    limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < |⟪z, x⟫|}) atTop ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z))
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ (x : ℝ) (hx : x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)), ‖1 - f (x • z)‖ ≤ ε / 4
simp : 2⁻¹ * r * ((2 * r⁻¹ + 2 * r⁻¹) * ε / 4) = ε / 2
⊢ 2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ε / 4 = ε / 2

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
h_limsup_le :
  ∀ (r : ℝ) (hr : 0 < r),
    limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < |⟪z, x⟫|}) atTop ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z))
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ (x : ℝ) (hx : x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)), ‖1 - f (x • z)‖ ≤ ε / 4
⊢ 2⁻¹ * r * ((2 * r⁻¹ + 2 * r⁻¹) * ε / 4) = ε / 2

Tactic:
field
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
h_limsup_le :
  ∀ (r : ℝ) (hr : 0 < r),
    limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < |⟪z, x⟫|}) atTop ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z))
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ (x : ℝ) (hx : x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)), ‖1 - f (x • z)‖ ≤ ε / 4
⊢ ε / 2 < ε

Tactic:
simp [hε]
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
h_limsup_le :
  ∀ (r : ℝ) (hr : 0 < r),
    limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < |⟪z, x⟫|}) atTop ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z))
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ (x : ℝ) (hx : x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)), ‖1 - f (x • z)‖ ≤ ε / 4
calc :
  2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)) ≤
    2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (t • z)‖
calc₁ : 2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (t • z)‖ ≤ 2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ε / 4
calc₂ : 2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ε / 4 = ε / 2
calc₃ : ε / 2 < ε
⊢ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)) < ε

Tactic:
calc 2⁻¹ * r * ‖∫ t in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)‖
  _ ≤ 2⁻¹ * r * ∫ t in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (t • z)‖ := by
    grw [intervalIntegral.norm_integral_le_integral_norm hr']
  _ ≤ 2⁻¹ * r * ∫ t in -(2 * r⁻¹)..2 * r⁻¹, ε / 4 := by
    gcongr
    rw [intervalIntegral.integral_of_le hr', intervalIntegral.integral_of_le hr']
    have hf_meas : Measurable f := by
      refine measurable_of_tendsto_metrizable (f := fun n t ↦ charFun (μ n) t) (by fun_prop) ?_
      rwa [tendsto_pi_nhds]
    refine integral_mono_ae ?_ (by fun_prop) ?_
    · refine Integrable.mono' (integrable_const (ε / 4)) ?_ ?_
      · exact Measurable.aestronglyMeasurable <| by fun_prop
      · simpa using ae_restrict_of_forall_mem measurableSet_Ioc h_le_Ioc
    · exact ae_restrict_of_forall_mem measurableSet_Ioc h_le_Ioc
  _ = ε / 2 := by simp; field
  _ < ε := by simp [hε]

Premises used: HMul.hMul, Inv.inv, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1) {x : Measure E | ∃ (n : ι), (↑(μ n) : Measure E) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_3, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
hμ :
  ∀ g ∈ A,
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) 𝓕
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
inl :
  ∀
    (hμ :
      ∀ g ∈ A,
        Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) ⊥
          (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))),
    Tendsto μ ⊥ (𝓝 μ₀)
inr : 𝓕.NeBot → Tendsto μ 𝓕 (𝓝 μ₀)
⊢ Tendsto μ 𝓕 (𝓝 μ₀)

Tactic:
obtain rfl | _ := 𝓕.eq_or_neBot

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
ι : Type u_4
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1) {x : Measure E | ∃ (n : ι), (↑(μ n) : Measure E) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_3, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
hμ :
  ∀ g ∈ A,
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) ⊥
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))
⊢ Tendsto μ ⊥ (𝓝 μ₀)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1) {x : Measure E | ∃ (n : ι), (↑(μ n) : Measure E) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_3, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
hμ :
  ∀ g ∈ A,
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) 𝓕
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h : 𝓕.NeBot
⊢ Tendsto μ 𝓕 (𝓝 μ₀)

Tactic:
(Filter.tendsto_iff_ultrafilter _ _ _).2 fun U hU ↦ ?_

Premises used: Iff.mpr, Filter.tendsto_iff_ultrafilter
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1) {x : Measure E | ∃ (n : ι), (↑(μ n) : Measure E) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_3, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
hμ :
  ∀ g ∈ A,
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) 𝓕
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h : 𝓕.NeBot
inr : ∀ (U : Ultrafilter ι) (hU : (↑U : Filter ι) ≤ 𝓕), Tendsto μ (↑U : Filter ι) (𝓝 μ₀)
⊢ Tendsto μ 𝓕 (𝓝 μ₀)

Tactic:
refine (Filter.tendsto_iff_ultrafilter _ _ _).2 fun U hU ↦ ?_

Premises used: Iff.mpr, Filter.tendsto_iff_ultrafilter
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1) {x : Measure E | ∃ (n : ι), (↑(μ n) : Measure E) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_3, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
hμ :
  ∀ g ∈ A,
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) 𝓕
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h : 𝓕.NeBot
U : Ultrafilter ι
hU : (↑U : Filter ι) ≤ 𝓕
⊢ IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1)
    {x : Measure E |
      ∃ (μ_1 : ProbabilityMeasure E),
        Membership.mem (γ := Set (ProbabilityMeasure E)) {x : ProbabilityMeasure E | ∃ (n : ι), μ n = x} μ_1 ∧
          (↑μ_1 : Measure E) = x}

Tactic:
simpa using h_tight
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1) {x : Measure E | ∃ (n : ι), (↑(μ n) : Measure E) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_3, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
hμ :
  ∀ g ∈ A,
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) 𝓕
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h : 𝓕.NeBot
U : Ultrafilter ι
hU : (↑U : Filter ι) ≤ 𝓕
⊢ IsCompact.{u_3} (X := ProbabilityMeasure E)
    (closure[instTopologicalSpace] {x : ProbabilityMeasure E | ∃ (n : ι), μ n = x})

Tactic:
have h_compact : IsCompact (closure {μ n | n}) :=
    isCompact_closure_of_isTightMeasureSet (by simpa using h_tight)
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1) {x : Measure E | ∃ (n : ι), (↑(μ n) : Measure E) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_3, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
hμ :
  ∀ g ∈ A,
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) 𝓕
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h : 𝓕.NeBot
U : Ultrafilter ι
hU : (↑U : Filter ι) ≤ 𝓕
h_compact :
  IsCompact.{u_3} (X := ProbabilityMeasure E)
    (closure[instTopologicalSpace] {x : ProbabilityMeasure E | ∃ (n : ι), μ n = x})
⊢ (↑(Ultrafilter.map μ U) : Filter (ProbabilityMeasure E)) ≤ 𝓟 {x : ProbabilityMeasure E | ∃ (n : ι), μ n = x}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1) {x : Measure E | ∃ (n : ι), (↑(μ n) : Measure E) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_3, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
hμ :
  ∀ g ∈ A,
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) 𝓕
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h : 𝓕.NeBot
U : Ultrafilter ι
hU : (↑U : Filter ι) ≤ 𝓕
h_compact :
  IsCompact.{u_3} (X := ProbabilityMeasure E)
    (closure[instTopologicalSpace] {x : ProbabilityMeasure E | ∃ (n : ι), μ n = x})
inr : ∀ (μ' : ProbabilityMeasure E) (hμ' : Tendsto μ (↑U : Filter ι) (𝓝 μ')), Tendsto μ (↑U : Filter ι) (𝓝 μ₀)
⊢ Tendsto μ (↑U : Filter ι) (𝓝 μ₀)

Tactic:
obtain ⟨μ', -, hμ' : Tendsto _ _ _⟩ := h_compact.ultrafilter_le_nhds (U.map μ)
    (.trans (by simp) (monotone_principal subset_closure))

Premises used: subset_closure, Filter.Tendsto, LE.le.trans, IsCompact.ultrafilter_le_nhds, Ultrafilter.map, Filter.monotone_principal
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1) {x : Measure E | ∃ (n : ι), (↑(μ n) : Measure E) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_3, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
hμ :
  ∀ g ∈ A,
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) 𝓕
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))
this_1 : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h : 𝓕.NeBot
U : Ultrafilter ι
hU : (↑U : Filter ι) ≤ 𝓕
h_compact :
  IsCompact.{u_3} (X := ProbabilityMeasure E)
    (closure[instTopologicalSpace] {x : ProbabilityMeasure E | ∃ (n : ι), μ n = x})
μ' : ProbabilityMeasure E
hμ' : Tendsto μ (↑U : Filter ι) (𝓝 μ')
this : (↑μ' : Measure E) = (↑μ₀ : Measure E)
⊢ Tendsto μ (↑U : Filter ι) (𝓝 μ')

Tactic:
hμ'
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1) {x : Measure E | ∃ (n : ι), (↑(μ n) : Measure E) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_3, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
hμ :
  ∀ g ∈ A,
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) 𝓕
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))
this_1 : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h_1 : 𝓕.NeBot
U : Ultrafilter ι
hU : (↑U : Filter ι) ≤ 𝓕
h_compact :
  IsCompact.{u_3} (X := ProbabilityMeasure E)
    (closure[instTopologicalSpace] {x : ProbabilityMeasure E | ∃ (n : ι), μ n = x})
μ' : ProbabilityMeasure E
hμ' : Tendsto μ (↑U : Filter ι) (𝓝 μ')
this : (↑μ' : Measure E) = (↑μ₀ : Measure E)
h : μ₀ = μ'
⊢ Tendsto μ (↑U : Filter ι) (𝓝 μ₀)

Tactic:
convert! hμ'
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1) {x : Measure E | ∃ (n : ι), (↑(μ n) : Measure E) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_3, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
hμ :
  ∀ g ∈ A,
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) 𝓕
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))
this_1 : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h_1 : 𝓕.NeBot
U : Ultrafilter ι
hU : (↑U : Filter ι) ≤ 𝓕
h_compact :
  IsCompact.{u_3} (X := ProbabilityMeasure E)
    (closure[instTopologicalSpace] {x : ProbabilityMeasure E | ∃ (n : ι), μ n = x})
μ' : ProbabilityMeasure E
hμ' : Tendsto μ (↑U : Filter ι) (𝓝 μ')
this : (↑μ' : Measure E) = (↑μ₀ : Measure E)
h :
  ∀ (s : Set E),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((↑μ₀ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
        (((↑μ' : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ₀ = μ'

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1) {x : Measure E | ∃ (n : ι), (↑(μ n) : Measure E) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_3, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
hμ :
  ∀ g ∈ A,
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) 𝓕
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))
this_1 : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h_1 : 𝓕.NeBot
U : Ultrafilter ι
hU : (↑U : Filter ι) ≤ 𝓕
h_compact :
  IsCompact.{u_3} (X := ProbabilityMeasure E)
    (closure[instTopologicalSpace] {x : ProbabilityMeasure E | ∃ (n : ι), μ n = x})
μ' : ProbabilityMeasure E
hμ' : Tendsto μ (↑U : Filter ι) (𝓝 μ')
this : (↑μ' : Measure E) = (↑μ₀ : Measure E)
s : Set E
h_2 : MeasurableSet s
h h₁ :
  Eq (α := ℝ≥0∞) (((↑μ₀ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (((↑μ₀ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((↑μ₀ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (((↑μ' : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1) {x : Measure E | ∃ (n : ι), (↑(μ n) : Measure E) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_3, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
hμ :
  ∀ g ∈ A,
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) 𝓕
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h : 𝓕.NeBot
U : Ultrafilter ι
hU : (↑U : Filter ι) ≤ 𝓕
h_compact :
  IsCompact.{u_3} (X := ProbabilityMeasure E)
    (closure[instTopologicalSpace] {x : ProbabilityMeasure E | ∃ (n : ι), μ n = x})
μ' : ProbabilityMeasure E
hμ' : Tendsto μ (↑U : Filter ι) (𝓝 μ')
inr : (↑μ' : Measure E) = (↑μ₀ : Measure E)
⊢ Tendsto μ (↑U : Filter ι) (𝓝 μ₀)

Tactic:
suffices (μ' : Measure E) = μ₀ by convert! hμ'; ext; rw [this]