awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
ι : Type u_2
𝓕 : Filter ι
μ₀ : ProbabilityMeasure E
μ : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ι) ↦ charFun (↑(μ n) : Measure E) t) 𝓕 (𝓝 (charFun (↑μ₀ : Measure E) t))
g : E →ᵇ ℂ
w : AddMonoidAlgebra ℂ E
hw :
  Eq (α := (a : E) → ℂ) (⇑g : (a : E) → ℂ) fun (x : E) ↦
    ∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
        ((↑((probChar : (a : ℝ) → Circle)
                (((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
            ℂ) :
          ℂ)
h_eq :
  ∀ (μ : Measure E) (hμ : IsProbabilityMeasure μ),
    Eq (α := ℂ) (∫ (x : E), (g : (a : E) → ℂ) x ∂μ)
      (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
          (∫ (x : E),
              (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
                ℂ) ∂μ :
            ℂ))
⊢ Tendsto (β := ℂ) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → ℂ) x ∂(↑(μ n) : Measure E)) 𝓕
    (𝓝 (∫ (x : E), (g : (a : E) → ℂ) x ∂(↑μ₀ : Measure E)))
have simp_rw : Tendsto (β := ℂ)
  (fun (n : ι) ↦
    ∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
        (∫ (x : E),
            (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
              ℂ) ∂(↑(μ n) : Measure E) :
          ℂ))
  𝓕
  (𝓝
    (∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
        (∫ (x : E),
            (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
              ℂ) ∂(↑μ₀ : Measure E) :
          ℂ)))
Tactic: simp_rw [h_eq (μ _), h_eq μ₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
ι : Type u_2
𝓕 : Filter ι
μ₀ : ProbabilityMeasure E
μ : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ι) ↦ charFun (↑(μ n) : Measure E) t) 𝓕 (𝓝 (charFun (↑μ₀ : Measure E) t))
g : E →ᵇ ℂ
w : AddMonoidAlgebra ℂ E
hw :
  Eq (α := (a : E) → ℂ) (⇑g : (a : E) → ℂ) fun (x : E) ↦
    ∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
        ((↑((probChar : (a : ℝ) → Circle)
                (((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
            ℂ) :
          ℂ)
h_eq :
  ∀ (μ : Measure E) (hμ : IsProbabilityMeasure μ),
    Eq (α := ℂ) (∫ (x : E), (g : (a : E) → ℂ) x ∂μ)
      (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
          (∫ (x : E),
              (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
                ℂ) ∂μ :
            ℂ))
⊢ Tendsto (β := ℂ)
    (fun (n : ι) ↦
      ∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
          (∫ (x : E),
              (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
                ℂ) ∂(↑(μ n) : Measure E) :
            ℂ))
    𝓕
    (𝓝
      (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
          (∫ (x : E),
              (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
                ℂ) ∂(↑μ₀ : Measure E) :
            ℂ)))
have refine : ∀ (y : E) (hy : y ∈ w.support),
  Tendsto (β := ℂ)
    (fun (n : ι) ↦
      ∫ (x : E),
        (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y)) :
          ℂ) ∂(↑(μ n) : Measure E))
    𝓕
    (𝓝
      (∫ (x : E),
        (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y)) :
          ℂ) ∂(↑μ₀ : Measure E)))
Tactic: refine tendsto_finsetSum _ fun y hy ↦ Tendsto.const_mul _ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
⊢ Tendsto μ atTop (𝓝 μ₀)
have h_tight : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst_3) {x : Measure E | ∃ (n : ℕ), (↑(μ n) : Measure E) = x}
Tactic: have h_tight : IsTightMeasureSet (𝓧 := E) {μ n | n} :=
    isTightMeasureSet_of_tendsto_charFun (by fun_prop) h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
h_tight : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst_3) {x : Measure E | ∃ (n : ℕ), (↑(μ n) : Measure E) = x}
⊢ Tendsto μ atTop (𝓝 μ₀)
have refine_1 : Subalgebra.SeparatesPoints.{u_1, 0, 0} (α := E) (A := ℂ)
  (StarSubalgebra.toSubalgebra
    (StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly (W := E) (L := innerₗ E) continuous_probChar sorry)))
Tactic: refine tendsto_of_tight_of_separatesPoints h_tight (𝕜 := ℂ)
    (A := charPoly continuous_probChar (L := innerₗ E) continuous_inner) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
h_tight : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst_3) {x : Measure E | ∃ (n : ℕ), (↑(μ n) : Measure E) = x}
refine_1 :
  Subalgebra.SeparatesPoints.{u_1, 0, 0} (α := E) (A := ℂ)
    (StarSubalgebra.toSubalgebra
      (StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly (W := E) (L := innerₗ E) continuous_probChar ⋯)))
⊢ Tendsto μ atTop (𝓝 μ₀)
have refine_2 : ∀ (g : E →ᵇ ℂ),
  Membership.mem (γ := StarSubalgebra ℂ (E →ᵇ ℂ)) (charPoly (W := E) (L := innerₗ E) continuous_probChar sorry) g →
    Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∫ (x : E), (g : (a : E) → ℂ) x ∂(↑(μ n) : Measure E)) atTop
      (𝓝 (∫ (x : E), (g : (a : E) → ℂ) x ∂(↑μ₀ : Measure E)))
Tactic: refine tendsto_of_tight_of_separatesPoints h_tight (𝕜 := ℂ)
    (A := charPoly continuous_probChar (L := innerₗ E) continuous_inner) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
h_tight : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst_3) {x : Measure E | ∃ (n : ℕ), (↑(μ n) : Measure E) = x}
⊢ Subalgebra.SeparatesPoints.{u_1, 0, 0} (α := E) (A := ℂ)
    (StarSubalgebra.toSubalgebra
      (StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly (W := E) (L := innerₗ E) continuous_probChar ⋯)))
have refine_1 : ∀ (v : E),
  v ≠ 0 → Ne (α := E →ₗ[ℝ] ℝ) (((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) v : E →ₗ[ℝ] ℝ) (0 : E →ₗ[ℝ] ℝ)
Tactic: refine separatesPoints_charPoly continuous_probChar probChar_ne_one _ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
⊢ Tendsto μ atTop (𝓝 μ₀) ↔
    ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
have refine : ∀ (h : Tendsto μ atTop (𝓝 μ₀)) (t : E),
  Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
Tactic: refine ⟨fun h t ↦ ?_, tendsto_of_tendsto_charFun⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h : Tendsto μ atTop (𝓝 μ₀)
t : E
⊢ Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
have rw : ∀
  (h :
    ∀ (f : E →ᵇ ℂ),
      Tendsto (β := ℂ) (fun (i : ℕ) ↦ ∫ (ω : E), (f : (a : E) → ℂ) ω ∂(↑(μ i) : Measure E)) atTop
        (𝓝 (∫ (ω : E), (f : (a : E) → ℂ) ω ∂(↑μ₀ : Measure E))))
  (t : E), Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
Tactic: rw [ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto ℂ] at h
Cleared hypotheses: h, t
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h :
  ∀ (f : E →ᵇ ℂ),
    Tendsto (β := ℂ) (fun (i : ℕ) ↦ ∫ (ω : E), (f : (a : E) → ℂ) ω ∂(↑(μ i) : Measure E)) atTop
      (𝓝 (∫ (ω : E), (f : (a : E) → ℂ) ω ∂(↑μ₀ : Measure E)))
t : E
⊢ Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
have simp_rw : Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∫ (v : E), (innerProbChar t : (a : E) → ℂ) v ∂(↑(μ n) : Measure E)) atTop
  (𝓝 (∫ (v : E), (innerProbChar t : (a : E) → ℂ) v ∂(↑μ₀ : Measure E)))
Tactic: simp_rw [charFun_eq_integral_innerProbChar]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
ε₁ ε₂ : ℝ≥0∞
μ ν : Measure Ω
h_le : ε₁ ≤ ε₂
B : Set Ω
hε₁ : (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₁.toReal B) : ℝ≥0∞) ε₁
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₂.toReal B) : ℝ≥0∞) ε₂
have pos : ∀ (ε_top : ε₂ = ∞),
  (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₂.toReal B) : ℝ≥0∞) ε₂
Tactic: by_cases ε_top : ε₂ = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
ε₁ ε₂ : ℝ≥0∞
μ ν : Measure Ω
h_le : ε₁ ≤ ε₂
B : Set Ω
hε₁ : (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₁.toReal B) : ℝ≥0∞) ε₁
pos :
  ∀ (ε_top : ε₂ = ∞),
    (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₂.toReal B) : ℝ≥0∞) ε₂
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₂.toReal B) : ℝ≥0∞) ε₂
have neg : ∀ (ε_top : ¬ε₂ = ∞),
  (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₂.toReal B) : ℝ≥0∞) ε₂
Tactic: by_cases ε_top : ε₂ = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
ε₁ ε₂ : ℝ≥0∞
μ ν : Measure Ω
h_le : ε₁ ≤ ε₂
B : Set Ω
hε₁ : (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₁.toReal B) : ℝ≥0∞) ε₁
ε_top : ¬ε₂ = ∞
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₂.toReal B) : ℝ≥0∞) ε₂
have apply : LE.le (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₁.toReal B) : ℝ≥0∞)
  ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₂.toReal B) : ℝ≥0∞)
Tactic: apply hε₁.trans (add_le_add ?_ h_le)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
c : ℝ≥0∞
h : levyProkhorovEDist μ ν < c
B : Set Ω
B_mble : MeasurableSet B
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening c.toReal B) : ℝ≥0∞) c
have obtain : ∀ (c' : ℝ≥0∞)
  (hc' :
    Membership.mem (γ := Set ℝ≥0∞)
      {ε : ℝ≥0∞ |
        ∀ (B : Set Ω),
          MeasurableSet B →
            (μ : (a : Set Ω) → ℝ≥0∞) B ≤
                HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε ∧
              (ν : (a : Set Ω) → ℝ≥0∞) B ≤
                HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε}
      c')
  (lt_c : c' < c),
  (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening c.toReal B) : ℝ≥0∞) c
Tactic: obtain ⟨c', ⟨hc', lt_c⟩⟩ := sInf_lt_iff.mp h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
c : ℝ≥0∞
h : levyProkhorovEDist μ ν < c
B : Set Ω
B_mble : MeasurableSet B
⊢ (ν : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening c.toReal B) : ℝ≥0∞) c
have obtain : ∀ (c' : ℝ≥0∞)
  (hc' :
    Membership.mem (γ := Set ℝ≥0∞)
      {ε : ℝ≥0∞ |
        ∀ (B : Set Ω),
          MeasurableSet B →
            (μ : (a : Set Ω) → ℝ≥0∞) B ≤
                HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε ∧
              (ν : (a : Set Ω) → ℝ≥0∞) B ≤
                HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε}
      c')
  (lt_c : c' < c),
  (ν : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening c.toReal B) : ℝ≥0∞) c
Tactic: obtain ⟨c', ⟨hc', lt_c⟩⟩ := sInf_lt_iff.mp h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    0 < ε →
      ε < ∞ →
        MeasurableSet B →
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening (δ + ε).toReal B) : ℝ≥0∞) δ + ε ∧
            (ν : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (δ + ε).toReal B) : ℝ≥0∞) δ + ε
⊢ levyProkhorovEDist μ ν ≤ δ
have h₁ : ∀ (ε : ℝ≥0), 0 < ε → δ < ∞ → levyProkhorovEDist μ ν ≤ δ + (↑ε : ℝ≥0∞)
Tactic: apply ENNReal.le_of_forall_pos_le_add
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    0 < ε →
      ε < ∞ →
        MeasurableSet B →
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening (δ + ε).toReal B) : ℝ≥0∞) δ + ε ∧
            (ν : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (δ + ε).toReal B) : ℝ≥0∞) δ + ε
ε : ℝ≥0
hε : 0 < ε
h_1 : δ < ∞
⊢ levyProkhorovEDist μ ν ≤ δ + (↑ε : ℝ≥0∞)
have pos : ∀ (ε_top : (↑ε : ℝ≥0∞) = ∞), levyProkhorovEDist μ ν ≤ δ + (↑ε : ℝ≥0∞)
Tactic: by_cases ε_top : ε = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    0 < ε →
      ε < ∞ →
        MeasurableSet B →
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening (δ + ε).toReal B) : ℝ≥0∞) δ + ε ∧
            (ν : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (δ + ε).toReal B) : ℝ≥0∞) δ + ε
ε : ℝ≥0
hε : 0 < ε
h_1 : δ < ∞
pos : ∀ (ε_top : (↑ε : ℝ≥0∞) = ∞), levyProkhorovEDist μ ν ≤ δ + (↑ε : ℝ≥0∞)
⊢ levyProkhorovEDist μ ν ≤ δ + (↑ε : ℝ≥0∞)
have neg : ∀ (ε_top : ¬(↑ε : ℝ≥0∞) = ∞), levyProkhorovEDist μ ν ≤ δ + (↑ε : ℝ≥0∞)
Tactic: by_cases ε_top : ε = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    0 < ε →
      ε < ∞ →
        MeasurableSet B →
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening (δ + ε).toReal B) : ℝ≥0∞) δ + ε ∧
            (ν : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (δ + ε).toReal B) : ℝ≥0∞) δ + ε
ε : ℝ≥0
hε : 0 < ε
h_1 : δ < ∞
ε_top : ¬(↑ε : ℝ≥0∞) = ∞
⊢ levyProkhorovEDist μ ν ≤ δ + (↑ε : ℝ≥0∞)
have neg : Membership.mem (γ := Set ℝ≥0∞)
  {ε : ℝ≥0∞ |
    ∀ (B : Set Ω),
      MeasurableSet B →
        (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε ∧
          (ν : (a : Set Ω) → ℝ≥0∞) B ≤
            HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε}
  (δ + (↑ε : ℝ≥0∞))
Tactic: apply sInf_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    δ < ε →
      ε < ∞ →
        MeasurableSet B →
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε ∧
            (ν : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
⊢ levyProkhorovEDist μ ν ≤ δ
have pos : ∀ (δ_top : δ = ∞), levyProkhorovEDist μ ν ≤ δ
Tactic: by_cases δ_top : δ = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    δ < ε →
      ε < ∞ →
        MeasurableSet B →
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε ∧
            (ν : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
pos : ∀ (δ_top : δ = ∞), levyProkhorovEDist μ ν ≤ δ
⊢ levyProkhorovEDist μ ν ≤ δ
have neg : ∀ (δ_top : ¬δ = ∞), levyProkhorovEDist μ ν ≤ δ
Tactic: by_cases δ_top : δ = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
δ : ℝ≥0∞
h :
  ∀ (ε : ℝ≥0∞) (B : Set Ω),
    δ < ε →
      ε < ∞ →
        MeasurableSet B →
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε ∧
            (ν : (a : Set Ω) → ℝ≥0∞) B ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
δ_top : ¬δ = ∞
⊢ levyProkhorovEDist μ ν ≤ δ
have neg : ∀ (ε : ℝ≥0∞) (B : Set Ω),
  0 < ε →
    ε < ∞ →
      MeasurableSet B →
        (μ : (a : Set Ω) → ℝ≥0∞) B ≤
            HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening (δ + ε).toReal B) : ℝ≥0∞) δ + ε ∧
          (ν : (a : Set Ω) → ℝ≥0∞) B ≤
            HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (δ + ε).toReal B) : ℝ≥0∞) δ + ε
Tactic: apply levyProkhorovEDist_le_of_forall_add_pos_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
⊢ levyProkhorovEDist μ ν ≤ max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ)
have refine_1 : ∀ (B : Set Ω),
  MeasurableSet B →
    (μ : (a : Set Ω) → ℝ≥0∞) B ≤
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((ν : (a : Set Ω) → ℝ≥0∞)
            (thickening (ENNReal.toReal (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ))) B) :
          ℝ≥0∞)
        (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ) : ℝ≥0∞)
Tactic: refine sInf_le fun B _ ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
refine_1 :
  ∀ (B : Set Ω),
    MeasurableSet B →
      (μ : (a : Set Ω) → ℝ≥0∞) B ≤
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((ν : (a : Set Ω) → ℝ≥0∞)
              (thickening (ENNReal.toReal (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ))) B) :
            ℝ≥0∞)
          (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ) : ℝ≥0∞)
⊢ levyProkhorovEDist μ ν ≤ max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ)
have refine_2 : ∀ (B : Set Ω),
  MeasurableSet B →
    (ν : (a : Set Ω) → ℝ≥0∞) B ≤
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞)
            (thickening (ENNReal.toReal (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ))) B) :
          ℝ≥0∞)
        (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ) : ℝ≥0∞)
Tactic: refine sInf_le fun B _ ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
B : Set Ω
h : MeasurableSet B
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((ν : (a : Set Ω) → ℝ≥0∞)
          (thickening (ENNReal.toReal (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ))) B) :
        ℝ≥0∞)
      (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ) : ℝ≥0∞)
have refine_1 : LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) B : ℝ≥0∞)
  (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ) : ℝ≥0∞)
Tactic: apply le_add_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
B : Set Ω
h : MeasurableSet B
⊢ (ν : (a : Set Ω) → ℝ≥0∞) B ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞)
          (thickening (ENNReal.toReal (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ))) B) :
        ℝ≥0∞)
      (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ) : ℝ≥0∞)
have refine_2 : LE.le (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) B : ℝ≥0∞)
  (max ((μ : (a : Set Ω) → ℝ≥0∞) univ) ((ν : (a : Set Ω) → ℝ≥0∞) univ) : ℝ≥0∞)
Tactic: apply le_add_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ : Measure Ω
⊢ levyProkhorovEDist μ μ = 0
have rw : levyProkhorovEDist μ μ ≤ sInf (Ioo 0 ∞)
Tactic: rw [← nonpos_iff_eq_zero, ← csInf_Ioo zero_lt_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ : Measure Ω
⊢ levyProkhorovEDist μ μ ≤ sInf (Ioo 0 ∞)
have refine : ∀ (ε : ℝ≥0∞),
  Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) ε →
    ∀ (B : Set Ω),
      MeasurableSet B →
        ∀ (hε₀ : 0 < ε) (hε_top : ε < ∞),
          (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
Tactic: refine sInf_le_sInf fun ε ⟨hε₀, hε_top⟩ B _ ↦ and_self_iff.2 ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ : Measure Ω
ε : ℝ≥0∞
h : Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 ∞) ε
B : Set Ω
h_1 : MeasurableSet B
hε₀ : 0 < ε
hε_top : ε < ∞
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal B) : ℝ≥0∞) ε
have refine : 0 < ε.toReal
Tactic: refine le_add_right <| measure_mono <| self_subset_thickening ?_ _