mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
ν : FiniteMeasure Ω
f : Ω → Ω'
f_aemble : AEMeasurable f ↑ν
A : Set Ω'
A_mble : MeasurableSet A
⊢ (ν.map f) A = ν (f ⁻¹' A)

Tactic:
have key := ν.map_apply' f_aemble A_mble
  exact (ENNReal.toNNReal_eq_toNNReal_iff' (measure_ne_top _ _) (measure_ne_top _ _)).mpr key

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → μ G ≤ liminf (fun i ↦ (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
⊢ liminf (fun i ↦ ∫ (x : Ω), f x ∂μs i) atTop = (liminf (fun i ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop).toReal

Tactic:
simp only [fun i ↦ @integral_eq_lintegral_of_nonneg_ae Ω _ (μs i) f (Eventually.of_forall f_nn)
                        f.continuous.measurable.aestronglyMeasurable]
    let g := BoundedContinuousFunction.comp _ Real.lipschitzWith_toNNReal f
    have bound : ∀ i, ∫⁻ x, ENNReal.ofReal (f x) ∂(μs i) ≤ nndist 0 g := fun i ↦ by
      simpa only [coe_nnreal_ennreal_nndist, measure_univ, mul_one, ge_iff_le] using!
            BoundedContinuousFunction.lintegral_le_edist_mul (μ := μs i) g
    apply ENNReal.liminf_toReal_eq ENNReal.coe_ne_top (Eventually.of_forall bound)

Goal state after:
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
⊢ (Y i ⁻¹' t i ∩ if i ∈ s then f i else univ) = g i

Tactic:
by by_cases hi : i ∈ s <;> simp [hi, g]

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X Y : Ω → E
hXY : X =ᵐ[ℙ] Y
⊢ (map X ℙ).rnDeriv μ = (map Y ℙ).rnDeriv μ

Tactic:
map_congr hXY

Goal state after:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X Y : Ω → E
hXY : X =ᵐ[ℙ] Y
⊢ (map Y ℙ).rnDeriv μ = (map Y ℙ).rnDeriv μ
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁷ : Group G
mG : MeasurableSpace G
inst✝⁶ : MeasurableMul₂ G
inst✝⁵ : MeasurableInv G
μ : Measure G
inst✝⁴ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝³ : SFinite μ
inst✝² : HasPDF X ℙ μ
inst✝¹ : HasPDF Y ℙ μ
inst✝ : IsFiniteMeasure ℙ
hXY : X ⟂ᵢ[ℙ] Y
⊢ pdf (X * Y) ℙ μ =ᵐ[μ] pdf X ℙ μ ⋆ₘₗ[μ] pdf Y ℙ μ

Tactic:
rw [pdf, hXY.map_mul_eq_map_mconv_map₀ (HasPDF.aemeasurable' μ) (HasPDF.aemeasurable' μ)]
  apply rnDeriv_mconv <;> exact HasPDF.absolutelyContinuous

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
f : ι → Set Ω := fun n ↦ if n = a then t2 else if n ∈ s then ft1 n else univ
h_f_mem : ∀ n ∈ insert a s, f n ∈ π n
h_f_mem_pi : ∀ n ∈ s, f n ∈ π n
h_t1 : t1 = ⋂ n ∈ s, f n
h_μ_t1 : ∀ᵐ (a' : α) ∂μ, (κ a') t1 = ∏ n ∈ s, (κ a') (f n)
h_t2 : t2 = f a
h_μ_inter : ∀ᵐ (a' : α) ∂μ, (κ a') (t1 ∩ t2) = ∏ n ∈ insert a s, (κ a') (f n)
has : a ∉ s
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
filter_upwards [h_μ_t1, h_μ_inter] with a' ha1 ha2

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
f : ι → Set Ω := fun n ↦ if n = a then t2 else if n ∈ s then ft1 n else univ
h_f_mem : ∀ n ∈ insert a s, f n ∈ π n
h_f_mem_pi : ∀ n ∈ s, f n ∈ π n
h_t1 : t1 = ⋂ n ∈ s, f n
h_μ_t1 : ∀ᵐ (a' : α) ∂μ, (κ a') t1 = ∏ n ∈ s, (κ a') (f n)
h_t2 : t2 = f a
h_μ_inter : ∀ᵐ (a' : α) ∂μ, (κ a') (t1 ∩ t2) = ∏ n ∈ insert a s, (κ a') (f n)
has : a ∉ s
a' : α
ha1 : (κ a') t1 = ∏ n ∈ s, (κ a') (f n)
ha2 : (κ a') (t1 ∩ t2) = ∏ n ∈ insert a s, (κ a') (f n)
⊢ (κ a') (t1 ∩ t2) = (κ a') t1 * (κ a') t2
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case iSup
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ ⨆ n, ∫⁻ (a : Ω), f a * f' n a ∂μ = ⨆ i, (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (a : Ω), f' i a ∂μ

Tactic:
← h_ind_f'

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᵐ[μ] 0
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]

Tactic:
rw [variance_congr (Y := 0), variance_zero]
    · symm
      refine Finset.sum_eq_zero fun i hi ↦ ?_
      simp [variance_congr (h'' i hi)]
    · have := fun (i : s) ↦ h'' i.1 i.2
      filter_upwards [ae_all_iff.2 this] with ω hω
      simp only [Finset.sum_apply, Pi.zero_apply]
      exact Finset.sum_eq_zero fun i hi ↦ hω ⟨i, hi⟩

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: case e'_3.e'_3
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝³ : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝² : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst✝¹ : TopologicalSpace E
inst✝ : OpensMeasurableSpace E
i : ι
hX : ∀ (j : ι), IdentDistrib (X i) (X j) (μ i) (μ j)
hZ : IdentDistrib (X i) Z (μ i) μ'
j : ι
⊢ Measure.map (X j) (μ j) = Measure.map Z μ'

Tactic:
exact (hX j).map_eq.symm.trans hZ.map_eq

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁴ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst✝³ : PseudoEMetricSpace E
inst✝² : BorelSpace E
inst✝¹ : l.IsCountablyGenerated
inst✝ : l.NeBot
X : ι → Ω' → E
h : TendstoInMeasure μ' X l Z
hX : ∀ (i : ι), AEMeasurable (X i) μ'
hZ : AEMeasurable Z μ'
⊢ Tendsto (fun n ↦ ⟨Measure.map (X n) μ', ⋯⟩) l (𝓝 ⟨Measure.map Z μ', ⋯⟩)

Tactic:
refine Filter.tendsto_of_subseq_tendsto (fun ns hns ↦ ?_)

Goal state after:
ι : Type u_1
E : Type u_2
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁴ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
Z : Ω' → E
l : Filter ι
inst✝³ : PseudoEMetricSpace E
inst✝² : BorelSpace E
inst✝¹ : l.IsCountablyGenerated
inst✝ : l.NeBot
X : ι → Ω' → E
h : TendstoInMeasure μ' X l Z
hX : ∀ (i : ι), AEMeasurable (X i) μ'
hZ : AEMeasurable Z μ'
ns : ℕ → ι
hns : Tendsto ns atTop l
⊢ ∃ ms, Tendsto (fun n ↦ ⟨Measure.map (X (ns (ms n))) μ', ⋯⟩) atTop (𝓝 ⟨Measure.map Z μ', ⋯⟩)
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
⊢ sSup ((fun f ↦ ↑f i) '' s) ≤ m

Tactic:
by
        refine sSup_le fun m' hm' => ?_
        rw [Set.mem_image] at hm'
        obtain ⟨f, _, hfm'⟩ := hm'
        rw [← hfm']
        exact f.le i

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy✝ : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt✝ : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg✝ : ∀ (i : ι), MeasurableSet (g i)
a : α
hy : ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
a✝ : IsProbabilityMeasure (κ a)
hYt : (κ a) (⋂ i, Y i ⁻¹' t i) = ∏ i, (κ a) (Y i ⁻¹' t i)
hg : (κ a) (⋂ i, g i) = ∏ i, (κ a) (g i)
i : ι
⊢ (Y i ⁻¹' t i ∩ if i ∈ s then f i else univ) = g i

Tactic:
by by_cases hi : i ∈ s <;> simp [hi, g]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving

Goal state before:
pp: case indicatorConst
X : Type u_1
Y : Type u_2
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : BorelSpace X
inst✝⁸ : R1Space X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
inst✝⁴ : R1Space Y
μ : Measure X
ν : Measure Y
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure ν
E : Type u_3
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
hp₀ : p ≠ 0
c : E
s : Set Y
hs : MeasurableSet s
hνs : ν s < ∞
⊢ Continuous[_, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] fun y ↦
    (compMeasurePreserving ⇑↑(↑(simpleFunc.indicatorConst p hs ⋯ c), y).2 ⋯)
      (↑(simpleFunc.indicatorConst p hs ⋯ c), y).1

Tactic:
| @indicatorConst c s hs hνs =>

Goal state after:
Module: Mathlib.MeasureTheory.Group.ModularCharacter

Goal state before:
pp: G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : LocallyCompactSpace G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
μ : Measure G
inst✝ : μ.IsHaarMeasure
g : G
ν : Measure G := haar
f : G → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
f_nonneg : 0 ≤ { toFun := f, continuous_toFun := f_cont }
f_one : { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∀ (μ₀ : Measure G) [μ₀.IsHaarMeasure], ∫ (x : G), f x ∂μ₀ ≠ 0
t : ∫ (x : G), f (x * g) ∂ν = ∫ (x : G), f (x * g) ∂ν.haarScalarFactor μ • μ
r : ↑(ν.haarScalarFactor μ) / ↑(ν.haarScalarFactor μ) = 1
⊢ ↑(ν.haarScalarFactor μ) / ↑(ν.haarScalarFactor μ) * ((∫ (x : G), f (x * g) ∂μ) / ∫ (x : G), f x ∂μ) =
    1 * ((∫ (x : G), f (x * g) ∂μ) / ∫ (x : G), f x ∂μ)

Tactic:
rw [r]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleTransform

Goal state before:
pp: R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)

Tactic:
apply_rules [ContinuousOn.fun_smul, continuousOn_const]

Goal state after:
case hg.hf
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun i ↦ deriv (circleMap z R) i.2) (closedBall z r ×ˢ univ)

case hg.hg.hf
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun i ↦ ((circleMap z R i.2 - i.1) ^ 2)⁻¹) (closedBall z r ×ˢ univ)
Module: Mathlib.MeasureTheory.Integral.Regular

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst✝³ : IsFiniteMeasureOnCompacts μ
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
r : ENNReal
hr : μ k < r
U : Set X
kU : k ⊆ U
U_open : IsOpen U
mu_U : μ U < r
f : X → ℝ
f_cont : Continuous f
fk : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 k
fU : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 0 Uᶜ
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
f_range : ∀ (x : X), { toFun := f, continuous_toFun := f_cont } x ∈ Icc 0 1
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) < r

Tactic:
exact (integral_le_measure (fun x _hx ↦ (f_range x).2) (fun x hx ↦ (fU hx).le)).trans_lt mu_U

Goal state after:
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
K : Compacts X
b : ℝ≥0∞
hb : ∀ (i : Compacts X), b ≤ ⨅ (_ : ↑K ⊆ interior ↑i), ↑(rieszContentAux Λ i)
this : b < ∞
ε : ℝ≥0
hε : 0 < ↑ε
f : X →C_c ℝ≥0
hfleoneonK : ∀ x ∈ K, 1 ≤ f x
hfle : ↑(Λ f) < ↑(sInf (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x}) + NNReal.mk ↑ε ⋯)
α : ℝ≥0
hα : 1 < α
K' : Set X := ⇑f ⁻¹' Ici α⁻¹
hKK' : ↑K ⊆ interior K'
hK'cp : IsCompact K'
hb' : ↑K ⊆ interior K' → b ≤ ↑(rieszContentAux Λ { carrier := K', isCompact' := hK'cp })
⊢ b.toNNReal ≤ Λ (α • f)

Tactic:
exact (ENNReal.toNNReal_mono (by simp) <| hb' hKK').trans <| csInf_le'
    ⟨α • f, fun x ↦ (inv_le_iff_one_le_mul₀' (zero_lt_one.trans hα)).mp, by simp⟩

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

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ : ℝ≥0∞
h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ∞ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε
ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
⊢ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ ≤ μ (thickening ε.toReal B) + ε

Tactic:
prob_compl_eq_one_sub isOpen_thickening.measurableSet

Goal state after:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ : ℝ≥0∞
h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ∞ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε
ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
⊢ 1 - ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤ μ (thickening ε.toReal B) + ε
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ ε : ℝ≥0∞
B : Set Ω
h : μ (thickening ε.toReal B)ᶜ ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + ε
ε_gt : δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ
⊢ 1 - ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤ μ (thickening ε.toReal B) + ε

Tactic:
prob_compl_eq_one_sub isOpen_thickening.measurableSet

Goal state after:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ ε : ℝ≥0∞
B : Set Ω
h : 1 - μ (thickening ε.toReal B) ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + ε
ε_gt : δ < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ
⊢ 1 - ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤ μ (thickening ε.toReal B) + ε
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
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
hνK : ν K ≠ ∞
hμK : μ K ≠ ∞
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst✝⁷] V
pV3 : ν V ≤ ν K + ↑ε
VltTop : ν V < ∞
f : X →C_c ℝ
pf1 : EqOn (⇑f) 1 K
pf2 : tsupport ⇑f ⊆ V
pf3 : ∀ (x : X), f x ∈ Icc 0 1
hfV : ∀ (x : X), f x ≤ V.indicator 1 x
hfK : ∀ (x : X), K.indicator 1 x ≤ f x
⊢ (ν V).toReal ≤ (ν K).toReal + (↑ε).toReal

Tactic:
← ENNReal.toReal_add,

Goal state after:
X : Type u_1
inst✝⁷ : TopologicalSpace X
inst✝⁶ : T2Space X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
hνK : ν K ≠ ∞
hμK : μ K ≠ ∞
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst✝⁷] V
pV3 : ν V ≤ ν K + ↑ε
VltTop : ν V < ∞
f : X →C_c ℝ
pf1 : EqOn (⇑f) 1 K
pf2 : tsupport ⇑f ⊆ V
pf3 : ∀ (x : X), f x ∈ Icc 0 1
hfV : ∀ (x : X), f x ≤ V.indicator 1 x
hfK : ∀ (x : X), K.indicator 1 x ≤ f x
⊢ (ν V).toReal ≤ (ν K + ↑ε).toReal

case ha
X : Type u_1
inst✝⁷ : TopologicalSpace X
inst✝⁶ : T2Space X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
hνK : ν K ≠ ∞
hμK : μ K ≠ ∞
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst✝⁷] V
pV3 : ν V ≤ ν K + ↑ε
VltTop : ν V < ∞
f : X →C_c ℝ
pf1 : EqOn (⇑f) 1 K
pf2 : tsupport ⇑f ⊆ V
pf3 : ∀ (x : X), f x ∈ Icc 0 1
hfV : ∀ (x : X), f x ≤ V.indicator 1 x
hfK : ∀ (x : X), K.indicator 1 x ≤ f x
⊢ ν K ≠ ∞

case hb
X : Type u_1
inst✝⁷ : TopologicalSpace X
inst✝⁶ : T2Space X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
μ ν : Measure X
inst✝³ : LocallyCompactSpace X
inst✝² : ν.OuterRegular
inst✝¹ : IsFiniteMeasureOnCompacts ν
inst✝ : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ ≤ ∫ (x : X), f x ∂ν
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : ν K < ∞
hνK : ν K ≠ ∞
hμK : μ K ≠ ∞
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst✝⁷] V
pV3 : ν V ≤ ν K + ↑ε
VltTop : ν V < ∞
f : X →C_c ℝ
pf1 : EqOn (⇑f) 1 K
pf2 : tsupport ⇑f ⊆ V
pf3 : ∀ (x : X), f x ∈ Icc 0 1
hfV : ∀ (x : X), f x ≤ V.indicator 1 x
hfK : ∀ (x : X), K.indicator 1 x ≤ f x
⊢ ↑ε ≠ ∞
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case refine_4
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (fun x ↦ ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs x) ν + εs x) {a | t ≤ f a})) atTop
    (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
εs_pos : 0 < εs n
hn :
  ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs n) ν + εs n) {a | t ≤ f a}) <
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}) + δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
bound :
  ∫ (ω : Ω), f ω ∂↑(Ps n) ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs n) ν + εs n) {a | t ≤ f a})) + (dist (μs n) ν + εs n) * ‖f‖
⊢ ∫ (x : Ω), f x ∂↑(Ps n) ≤ ∫ (x : Ω), f x ∂↑P + δ

Tactic:
grw [bound, hn, BoundedContinuousFunction.integral_eq_integral_meas_le _ _ <| .of_forall f_nn,
        add_assoc, mul_comm]
      gcongr
      calc
        δ / 2 + ‖f‖ * (dist (μs n) ν + εs n)
        _ ≤ δ / 2 + ‖f‖ * (‖f‖⁻¹ * δ / 2) := by gcongr
        _ = δ := by field

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s t : MeasuredSets μ
⊢ μ.real ↑s - μ.real ↑t ≤ dist s t

Tactic:
by
  grw [dist_edist, ← sub_le_edist]
  exacts [ENNReal.le_toReal_sub (measure_ne_top _ _), edist_ne_top _ _]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
f : ℕ → Set α
f_disj : Pairwise (Function.onFun Disjoint f)
⊢ (∀ (i : ℕ), MeasurableSet (f i)) →
    (∀ (i : ℕ) (ε : ℝ≥0∞), 0 < ε → ∃ t ∈ C, μ (t ∆ f i) < ε) → ∀ (ε : ℝ≥0∞), 0 < ε → ∃ t ∈ C, μ (t ∆ ⋃ i, f i) < ε

Tactic:
f_meas

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
f : ℕ → Set α
f_disj : Pairwise (Function.onFun Disjoint f)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
⊢ (∀ (i : ℕ) (ε : ℝ≥0∞), 0 < ε → ∃ t ∈ C, μ (t ∆ f i) < ε) → ∀ (ε : ℝ≥0∞), 0 < ε → ∃ t ∈ C, μ (t ∆ ⋃ i, f i) < ε
Module: Mathlib.MeasureTheory.Measure.Support

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : MeasurableSpace X
μ : Measure X
h : IsLindelof μ.supportᶜ
s : X
hs : s ∈ μ.supportᶜ
⊢ ∃ t ∈ 𝓝[μ.supportᶜ] s, tᶜ ∈ ae μ

Tactic:
simpa [compl_mem_ae_iff, isOpen_compl_support.nhdsWithin_eq hs]
    using notMem_support_iff_exists.mp hs

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (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 : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (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 ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ‖1 - f (x • z)‖ ≤ ε / 4
⊢ 2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (t • z)‖ ≤ 2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ε / 4

Tactic:
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

Goal state after: