mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.MeanValue

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, 1 ∂ν
hν0 : ∫ (x : α) in s, 1 ∂ν = 0
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ

Tactic:
rcases hs_conn.nonempty with ⟨c, hc⟩

Goal state after:
case pos
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, 1 ∂ν
hν0 : ∫ (x : α) in s, 1 ∂ν = 0
c : α
hc : c ∈ s
⊢ ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
f✝ : ℝ → E✝
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (uIoc a b)] B
⊢ ∀ᵐ (t : ℝ), t ∈ Ioc a b → ‖deriv f t‖ ≤ B t

Tactic:
← ae_restrict_iff' measurableSet_Ioc,

Goal state after:
E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
f✝ : ℝ → E✝
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
hfB' : (fun x ↦ ‖deriv f x‖) ≤ᵐ[volume.restrict (uIoc a b)] B
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (Ioc a b), ‖deriv f x‖ ≤ B x
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : s₀ ⊆ s₁ᶜ
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
⊢ ∃ i, x ∈ if i = 0 then s₀ᶜ else s₁ᶜ

Tactic:
← compl_compl s₀,

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : s₀ᶜᶜ ⊆ s₁ᶜ
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
⊢ ∃ i, x ∈ if i = 0 then s₀ᶜ else s₁ᶜ
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
V : Set X
h : tsupport ⇑f ⊆ V
⊢ ↑(Λ f) ≤ (rieszMeasure Λ) (tsupport ⇑f)

Tactic:
apply le_rieszMeasure_of_isCompact_tsupport_subset Λ hf f.hasCompactSupport

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ≥0
hf : ∀ (x : X), f x ≤ 1
V : Set X
h : tsupport ⇑f ⊆ V
⊢ tsupport ⇑f ⊆ tsupport ⇑f
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case h.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range ⇑f ⊆ Ioo a (a + ↑N * ε)
b : ℝ := ⋯
y : Fin N → ℝ := ⋯
hy : ∀ {n m : Fin N}, n < m → y n + ε ≤ y m
E : Fin N → Set X := ⋯
m : Fin N
a✝¹ : m ∈ univ
n : Fin N
a✝ : n ∈ univ
hmn : m ≠ n
⊢ Disjoint {a | a ∈ ⇑f ⁻¹' Ioc (y m - ε) (y m) ∧ a ∈ tsupport ⇑f} {a | a ∈ ⇑f ⁻¹' Ioc (y n - ε) (y n) ∧ a ∈ tsupport ⇑f}

Tactic:
mem_preimage,

Goal state after:
case h.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range ⇑f ⊆ Ioo a (a + ↑N * ε)
b : ℝ := a + ↑N * ε
y : Fin N → ℝ := fun n ↦ a + ε * (↑↑n + 1)
hy : ∀ {n m : Fin N}, n < m → y n + ε ≤ y m
E : Fin N → Set X := fun n ↦ ⇑f ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport ⇑f
m : Fin N
a✝¹ : m ∈ univ
n : Fin N
a✝ : n ∈ univ
hmn : m ≠ n
⊢ Disjoint {a | f a ∈ Ioc (y m - ε) (y m) ∧ a ∈ tsupport ⇑f} {a | f a ∈ Ioc (y n - ε) (y n) ∧ a ∈ tsupport ⇑f}
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : μ.outerMeasure E ≠ ∞
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, f x < c
hε' : ε.toNNReal ≠ 0
V₁ : Opens X
hV₁ : E ⊆ ↑V₁ ∧ μ.outerMeasure ↑V₁ ≤ μ.outerMeasure E + ↑ε.toNNReal
V₂ : Opens X := { carrier := ⇑f ⁻¹' Iio c, is_open' := ⋯ }
⊢ μ.outerMeasure E + ↑ε.toNNReal = μ.measure E + ENNReal.ofReal ε

Tactic:
rw [Content.measure_apply μ hμ', ENNReal.ofNNReal_toNNReal]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: case h2
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ max (#↑s) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
C : #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ≤ max (#↑s) 2 ^ ℵ₀
⊢ #↑(range fun f ↦ ⋃ n, ↑(f n)) ≤ max (#↑s) 2 ^ ℵ₀

Tactic:
apply mk_range_le.trans
    simp only [mk_pi, prod_const, Cardinal.lift_uzero, mk_denumerable, lift_aleph0]
    have := @power_le_power_right _ _ ℵ₀ C
    rwa [← power_mul, aleph0_mul_aleph0] at this

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
x : E
L : StrongDual ℝ E
⊢ charFunDual (Measure.dirac x) L = cexp (↑(L x) * I)

Tactic:
by
  rw [charFunDual_apply, integral_dirac]

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
x : X
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
f : X → ↑I
hf : Continuous[inst✝¹, _] f
efx : f x = 0
hfU : stoneCechUnit ⁻¹' stoneCechExtend hf ⁻¹' {1}ᶜ ⊆ U
⊢ stoneCechUnit x ∈ stoneCechExtend hf ⁻¹' {1}ᶜ

Tactic:
mem_preimage,

Goal state after:
case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
x : X
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
f : X → ↑I
hf : Continuous[inst✝¹, _] f
efx : f x = 0
hfU : stoneCechUnit ⁻¹' stoneCechExtend hf ⁻¹' {1}ᶜ ⊆ U
⊢ stoneCechExtend hf (stoneCechUnit x) ∈ {1}ᶜ
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T35Space X
a b : X
⊢ stoneCechUnit a = stoneCechUnit b → a = b

Tactic:
hab

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T35Space X
a b : X
hab : stoneCechUnit a = stoneCechUnit b
⊢ a = b
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: case refine_3
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a✝ b c d : E
γ₁ : Path a✝ b
γ₂ : Path c d
s : Set (↑I × ↑I)
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : (↑γ₁).Homotopy ↑γ₂
hs : s.Countable
hφt : ∀ a ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, φ (a, b_1) ∈ t
hω : ∀ a ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, (a, b_1) ∉ s → HasFDerivWithinAt ω (dω (φ (a, b_1))) t (φ (a, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ a ∈ Ioo 0 1,
    ∀ b_1 ∈ Ioo 0 1,
      (a, b_1) ∉ s →
        ∀ u ∈ tangentConeAt ℝ t (φ (a, b_1)),
          ∀ v ∈ tangentConeAt ℝ t (φ (a, b_1)), ((dω (φ (a, b_1))) u) v = ((dω (φ (a, b_1))) v) u
U : Set (ℝ × ℝ) := Ioo 0 1 ×ˢ Ioo 0 1
hU : U = Ioo 0 1 ×ˢ Ioo 0 1
hinterior : interior (Icc 0 1) = U
hunique : UniqueDiffOn ℝ (Icc 0 1)
hUopen : IsOpen U
hU_subset : U ⊆ Icc 0 1
hclosure : closure U = Icc 0 1
ψ : ℝ × ℝ → E := fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hcontdiff : ContDiffOn ℝ 2 ψ (Icc 0 1)
hψ : ψ = fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hψφ : ∀ (a b_1 : ↑I), ψ (↑a, ↑b_1) = φ (a, b_1)
hψ_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ψ
hψUt : MapsTo ψ U t
dψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fderivWithin ℝ ψ (Icc 0 1)
s' : Set (ℝ × ℝ) := Prod.map Subtype.val Subtype.val '' s
hs' : s' = Prod.map Subtype.val Subtype.val '' s
hmem_s' : ∀ (x y : ↑I), (↑x, ↑y) ∈ s' ↔ (x, y) ∈ s
hs'c : s'.Countable
hdψ : ∀ a ∈ U, HasFDerivAt ψ (dψ a) a
d2ψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] E := fderivWithin ℝ dψ (Icc 0 1)
hd2ψ : ∀ a ∈ U, HasFDerivAt dψ (d2ψ a) a
hd2ψ_symm : ∀ a ∈ Icc 0 1, ∀ (x y : ℝ × ℝ), ((d2ψ a) x) y = ((d2ψ a) y) x
η : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun a ↦ ω (ψ a) ∘SL dψ a
f : ℝ × ℝ → F := fun a ↦ (η a) (0, 1)
hf : ∀ a ∈ Icc 0 1, f a = (ω (ψ a)) (derivWithin (ψ ∘ fun x ↦ (a.1, x)) I a.2)
g : ℝ × ℝ → F := fun a ↦ -(η a) (1, 0)
hg : ∀ a ∈ Icc 0 1, g a = (ω (ψ a)) (-derivWithin (ψ ∘ fun x ↦ (x, a.2)) I a.1)
dη : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] F :=
  fun a ↦ (ContinuousLinearMap.compL ℝ (ℝ × ℝ) E F) (ω (ψ a)) ∘SL d2ψ a + (dω (ψ a)).bilinearComp (dψ a) (dψ a)
a : ℝ × ℝ
haU : a ∈ U
has : a ∉ s'
⊢ ∀ᶠ (x' : ℝ × ℝ) in 𝓝 a, ψ x' ∈ t

Tactic:
· filter_upwards [hUopen.mem_nhds haU] using hψUt

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PseudoEMetricSpace Ω
inst✝³ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure κ
dμν_finite : levyProkhorovEDist μ ν ≠ ∞
⊢ levyProkhorovDist μ κ ≤ levyProkhorovDist μ ν + levyProkhorovDist ν κ

Tactic:
have dνκ_finite := (levyProkhorovEDist_lt_top ν κ).ne

Goal state after:
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : PseudoEMetricSpace Ω
inst✝³ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure κ
dμν_finite : levyProkhorovEDist μ ν ≠ ∞
dνκ_finite : levyProkhorovEDist ν κ ≠ ∞
⊢ levyProkhorovDist μ κ ≤ levyProkhorovDist μ ν + levyProkhorovDist ν κ
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ∞
μ : ProbabilityMeasure Ω
⊢ Tendsto (fun ε ↦ ∫ (t : ℝ) in A, (↑μ).real (thickening ε {a | t ≤ f a})) (𝓝[>] 0)
    (𝓝 (∫ (t : ℝ) in A, (↑μ).real {a | t ≤ f a}))

Tactic:
by
  apply tendsto_integral_filter_of_dominated_convergence (G := ℝ) (μ := volume.restrict A)
        (F := fun ε t ↦ (μ (thickening ε {a | t ≤ f a}))) (f := fun t ↦ (μ {a | t ≤ f a})) 1
  · apply Eventually.of_forall fun n ↦ Measurable.aestronglyMeasurable ?_
    simp only [measurable_coe_nnreal_real_iff]
    apply measurable_toNNReal.comp <| Antitone.measurable (fun s t hst ↦ ?_)
    exact measure_mono <| thickening_subset_of_subset _ <| fun ω h ↦ hst.trans h
  · apply Eventually.of_forall (fun i ↦ ?_)
    apply Eventually.of_forall (fun t ↦ ?_)
    simp only [Real.norm_eq_abs, NNReal.abs_eq, Pi.one_apply]
    exact ENNReal.toReal_mono one_ne_top prob_le_one
  · have aux : IsFiniteMeasure (volume.restrict A) := ⟨by simp [lt_top_iff_ne_top, A_finmeas]⟩
    apply integrable_const
  · apply Eventually.of_forall (fun t ↦ ?_)
    simp only [NNReal.tendsto_coe]
    apply (ENNReal.tendsto_toNNReal _).comp
    · apply tendsto_measure_thickening_of_isClosed ?_ ?_
      · exact ⟨1, ⟨Real.zero_lt_one, measure_ne_top _ _⟩⟩
      · exact isClosed_le continuous_const f.continuous
    · finiteness

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

Goal state before:
pp: G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
φ : G ≃ₜ* G
smul : haar = haar.haarScalarFactor μ • μ
| (haar.haarScalarFactor μ • μ).haarScalarFactor (map (⇑φ) haar) = μ.haarScalarFactor (map (⇑φ) μ)

Tactic:
enter [1, 2, 2]
    rw [smul]

Goal state after:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
φ : G ≃ₜ* G
smul : haar = haar.haarScalarFactor μ • μ
| haar.haarScalarFactor μ • μ
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : ⋃ n, Es n = univ
Es_disjoint : Pairwise fun n m ↦ Disjoint (Es n) (Es m)
⊢ ∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist (ofMeasure x) (ofMeasure P) < ε

Tactic:
obtain ⟨N, hN⟩ : ∃ N, P.toMeasure (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3) := by
    have exhaust := @tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint Ω _ P.toMeasure _
                    Es (fun n ↦ (Es_mble n).nullMeasurableSet) Es_disjoint
    simp only [tendsto_atTop_nhds, Function.comp_apply] at exhaust
    obtain ⟨N, hN⟩ := exhaust (Iio (ENNReal.ofReal (ε / 3))) third_ε_pos' isOpen_Iio
    refine ⟨N, ?_⟩
    have rewr : ⋃ i, ⋃ (_ : N ≤ i), Es i = (⋃ i, ⋃ (_ : i < N), Es i)ᶜ := by
      simpa only [mem_Iio, compl_Iio, mem_Ici] using
        (biUnion_compl_eq_of_pairwise_disjoint_of_iUnion_eq_univ Es_cover Es_disjoint (Iio N)).symm
    simpa only [mem_Iio, ← rewr, gt_iff_lt] using hN N le_rfl

Goal state after:
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : ⋃ n, Es n = univ
Es_disjoint : Pairwise fun n m ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ↑P (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
⊢ ∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist (ofMeasure x) (ofMeasure P) < ε
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (fun x ↦ sinc (r * x)) μ
⊢ 2 * ∫ (x : ℝ) in {x | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ ≤ 2 * ∫ (x : ℝ) in {x | 2 < |2 * r⁻¹ * x|}, 1 - sinc (2 * r⁻¹ * x) ∂μ

Tactic:
by
    gcongr (2 : ℝ) * ?_
    refine setIntegral_mono_on ?_
      ((integrable_const _).sub (integrable_sinc_const_mul _)).integrableOn ?_ fun x hx ↦ ?_
    · exact Integrable.integrableOn <| by fun_prop
    · exact MeasurableSet.preimage measurableSet_Ioi (by fun_prop)
    · have hx_ne : 2 * r⁻¹ * x ≠ 0 := by
        intro hx0
        simp only [hx0, Set.mem_ofPred_eq, abs_zero] at hx
        linarith
      rw [le_sub_iff_add_le, ← le_sub_iff_add_le']
      norm_num
      rw [one_div]
      refine (sinc_le_inv_abs hx_ne).trans ?_
      exact (inv_le_inv₀ (by positivity) (by positivity)).mpr (le_of_lt hx)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: case e_a
μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (fun x ↦ sinc (r * x)) μ
⊢ 2 = 2⁻¹ * r * 2 * (2 * r⁻¹)

Tactic:
ring_nf
      rw [mul_inv_cancel₀ (by positivity), one_mul]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.TightNormed

Goal state before:
pp: E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝ : PseudoMetricSpace E
hS : IsTightMeasureSet S
x : E
⊢ Tendsto (fun r ↦ ⨆ μ ∈ S, μ (Metric.closedBall x r)ᶜ) atTop (𝓝 0)

Tactic:
suffices Tendsto ((⨆ μ ∈ S, μ) ∘ (fun r ↦ (Metric.closedBall x r)ᶜ)) atTop (𝓝 0) by
    convert! this with r
    simp
  refine hS.comp <| .mono_right ?_ <| monotone_smallSets Metric.cobounded_le_cocompact
  exact (Metric.hasAntitoneBasis_cobounded_compl_closedBall _).tendsto_smallSets

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
g : E →ᵇ ℝ
ε : ℝ
εpos : ε > 0
I1 : ∀ᶠ (n : ℕ) in atTop, dist (∫ (x : E), g x ∂∑ i ∈ Finset.range (n + 1), ↑(ν i)) (∫ (x : E), g x ∂↑μ) < ε / 3
I2 : ∀ᶠ (n : ℕ) in atTop, ‖g‖ * ↑(u n) < ε / 3
n : ℕ
hn : dist (∫ (x : E), g x ∂∑ i ∈ Finset.range (n + 1), ↑(ν i)) (∫ (x : E), g x ∂↑μ) < ε / 3
h'n : ‖g‖ * ↑(u n) < ε / 3
this :
  Tendsto (fun ρ ↦ ∫ (x : E), g x ∂↑(∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i))) (↑f)
    (𝓝 (∫ (x : E), g x ∂↑(∑ i ∈ Finset.range (n + 1), ν i)))
ρ : FiniteMeasure E
hρ :
  dist (∫ (x : E), g x ∂↑(∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i)))
      (∫ (x : E), g x ∂↑(∑ i ∈ Finset.range (n + 1), ν i)) <
    ε / 3
h'ρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), ρ (K n)ᶜ ≤ u n
⊢ dist (∫ (x : E), g x ∂↑ρ) (∫ (x : E), g x ∂∑ i ∈ Finset.range (n + 1), ↑(ρ.restrict (disjointed K i))) +
        dist (∫ (x : E), g x ∂∑ i ∈ Finset.range (n + 1), ↑(ρ.restrict (disjointed K i)))
          (∫ (x : E), g x ∂∑ i ∈ Finset.range (n + 1), ↑(ν i)) +
      dist (∫ (x : E), g x ∂∑ i ∈ Finset.range (n + 1), ↑(ν i)) (∫ (x : E), g x ∂↑μ) <
    ε / 3 + ε / 3 + ε / 3

Tactic:
by
      gcongr
      · have : ρ = ρ.restrict (partialSups K n)ᶜ +
            ∑ i ∈ Finset.range (n + 1), ρ.restrict (disjointed K i) := by
          rw [I, ← FiniteMeasure.restrict_union disjoint_compl_left (A n).measurableSet]
          simp
        nth_rewrite 1 [this]
        rw [toMeasure_add, integral_add_measure (g.integrable _) (g.integrable _)]
        simp only [toMeasure_sum, dist_add_self_left]
        calc ‖∫ x, g x ∂(ρ.restrict ((partialSups K) n)ᶜ)‖
        _ ≤ ∫ x, ‖g x‖ ∂(ρ.restrict ((partialSups K) n)ᶜ) := norm_integral_le_integral_norm _
        _ ≤ ∫ x, ‖g‖ ∂(ρ.restrict ((partialSups K) n)ᶜ : Measure E) := by
          apply integral_mono_of_nonneg
          · filter_upwards with x using by positivity
          · simp
          · filter_upwards with x using norm_coe_le_norm g x
        _ = ‖g‖ * ρ ((partialSups K) n)ᶜ := by simp [mul_comm]
        _ ≤ ‖g‖ * ρ (K n)ᶜ := by gcongr; apply le_partialSups
        _ ≤ ‖g‖ * u n := by gcongr; exact h'ρ.2 n
        _ < ε / 3 := h'n
      · simpa using hρ

Goal state after:
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
a : ℝ≥0∞
ha : a < preVariationFun f s
⊢ ∃ P, a < ∑ p ∈ P.parts, f ↑p

Tactic:
simp_all [preVariationFun, lt_iSup_iff]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition ⟨s i, ⋯⟩
n : ℕ
s' : ℕ → Subtype MeasurableSet := fun i ↦ ⟨s i, ⋯⟩
i : ℕ
x✝¹ : i ∈ ↑(Finset.range n)
j : ℕ
x✝ : j ∈ ↑(Finset.range n)
hij : i ≠ j
⊢ (Disjoint on s') i j

Tactic:
by
    simp only [Function.onFun, disjoint_iff, Subtype.ext_iff]
    exact Set.disjoint_iff_inter_eq_empty.mp (hs' hij)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Support

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : MeasurableSpace X
μ : Measure X
K : Set X
hK : IsCompact K
hKsub : K ⊆ μ.supportᶜ
⊢ μ K = 0

Tactic:
refine hK.induction_on measure_empty ?_ ?_ ?_

Goal state after:
case refine_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : MeasurableSpace X
μ : Measure X
K : Set X
hK : IsCompact K
hKsub : K ⊆ μ.supportᶜ
⊢ ∀ ⦃s t : Set X⦄, s ⊆ t → μ t = 0 → μ s = 0

case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : MeasurableSpace X
μ : Measure X
K : Set X
hK : IsCompact K
hKsub : K ⊆ μ.supportᶜ
⊢ ∀ ⦃s t : Set X⦄, μ s = 0 → μ t = 0 → μ (s ∪ t) = 0

case refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : MeasurableSpace X
μ : Measure X
K : Set X
hK : IsCompact K
hKsub : K ⊆ μ.supportᶜ
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, μ t = 0
Module: Mathlib.MeasureTheory.Measure.Support

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : OpensMeasurableSpace X
s : Set X
⊢ interior s ∩ μ.support ⊆ (μ.restrict s).support

Tactic:
rintro x ⟨hxs, hxμ⟩

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : OpensMeasurableSpace X
s : Set X
x : X
hxs : x ∈ interior s
hxμ : x ∈ μ.support
⊢ x ∈ (μ.restrict s).support
Module: Mathlib.MeasureTheory.Measure.ResolventTransform

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : MeasurableSpace 𝕜
a : A
inst✝⁵ : OpensMeasurableSpace 𝕜
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : CompleteSpace A
inst✝¹ : MeasurableSpace A
inst✝ : BorelSpace A
⊢ Measurable (resolvent a)

Tactic:
classical
  have h1 : ContinuousOn (resolvent (R := 𝕜) a) (resolventSet 𝕜 a) :=
    HasDerivAt.continuousOn (fun _ hx ↦ hasDerivAt_resolvent_const_left hx)
  have h2 : ContinuousOn (resolvent (R := 𝕜) a) (resolventSet 𝕜 a)ᶜ := by
    rw [continuousOn_iff_continuous_domRestrict]
    convert continuous_const (y := (0 : A)) with x
    simp
  have h3 : MeasurableSet (resolventSet 𝕜 a) := (isOpen_resolventSet a).measurableSet
  simpa using h1.measurable_piecewise h2 h3

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Support

Goal state before:
pp: case h₂
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : OpensMeasurableSpace X
s : Set X
x : X
hxs : x ∈ interior s
hxμ : ∀ (i : Set X), x ∈ i ∧ IsOpen[inst✝²] i → 0 < μ i
u : Set X
hxu : x ∈ u
hu : IsOpen[inst✝²] u
⊢ interior s ⊆ s

Tactic:
exact interior_subset

Goal state after: