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

Goal state before:
pp: case mpr.inr.refine_2
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
F : Filter γ
inst✝ : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ C, ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ L, LipschitzWith L f) → Tendsto (fun i ↦ ∫ (ω : Ω), f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), f ω ∂↑μ))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := ⋯
key₁ : Tendsto (fun n ↦ ∫ (ω : Ω), fs n ω ∂↑μ) atTop (𝓝 ((↑μ).real s))
room₁ : (↑μ).real s < (↑μ).real s + ε / 2
M : ℕ
hM : ∀ (b : ℕ), M ≤ b → ∫ (ω : Ω), fs b ω ∂↑μ < (↑μ).real s + ε / 2
key₂ : Tendsto (fun i ↦ ∫ (ω : Ω), fs M ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), fs M ω ∂↑μ))
room₂ : ∫ (a : Ω), fs M a ∂↑μ < ∫ (a : Ω), fs M a ∂↑μ + ε / 2
ev_near : ∀ᶠ (x : γ) in F, (↑(μs x)).real s ≤ ∫ (a : Ω), fs M a ∂↑μ + ε / 2
⊢ ∫ (a : Ω), fs M a ∂↑μ + ε / 2 ≤ (↑μ).real s + ε

Tactic:
apply (add_le_add (hM M rfl.le).le (le_refl (ε / 2))).trans_eq
    ring

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ ¬MemLp X 2 μ → eVar[X; μ] = ∞

Tactic:
exact evariance_eq_top hX

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
inst✝ : MeasurableSingletonClass Ω
x : Ω
⊢ Var[X; Measure.dirac x] = 0

Tactic:
rw [variance_eq_integral]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
inst✝ : MeasurableSingletonClass Ω
x : Ω
⊢ ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂Measure.dirac x) ^ 2 ∂Measure.dirac x = 0

Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
inst✝ : MeasurableSingletonClass Ω
x : Ω
⊢ AEMeasurable X (Measure.dirac x)
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst✝ : IsFiniteMeasure μ
ι' : Type u_3
Y : ι' → Ω → ℝ
t : Finset ι'
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : ∀ i ∈ t, MemLp (Y i) 2 μ
⊢ ∑ i ∈ s, cov[X i, ∑ j ∈ t, Y j; μ] = ∑ i ∈ s, ∑ j ∈ t, cov[X i, Y j; μ]

Tactic:
exact Finset.sum_congr rfl fun i hi ↦ by rw [covariance_sum_right' hY (hX i hi)]

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

Goal state before:
pp: case e'_4.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x ↦ ∫ (x : Ω), X x ∂μ) μ
⊢ eVar[X; μ] = (∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ) ^ 1

Tactic:
ENNReal.rpow_one,

Goal state after:
case e'_4.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x ↦ ∫ (x : Ω), X x ∂μ) μ
⊢ eVar[X; μ] = ∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf_indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
⊢ IndepFun (fun a ↦ (f i a, f j a)) (fun a ↦ (f k a, f l a)) κ μ

Tactic:
let g (i j : ι) (v : Π x : ({i, j} : Finset ι), β x) : β i × β j :=
    ⟨v ⟨i, mem_insert_self _ _⟩, v ⟨j, mem_insert_of_mem <| mem_singleton_self _⟩⟩
  have hg (i j : ι) : Measurable (g i j) := by fun_prop
  exact (hf_indep.indepFun_finset {i, j} {k, l} (by aesop) hf_meas).comp (hg i j) (hg k l)

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

Goal state before:
pp: case lim
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g✝ : X → Z
inst✝² : Nonempty Z
inst✝¹ : TopologicalSpace Z
inst✝ : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g : ℕ → X → Z
i : X → Z
hg : ∀ (n : ℕ), StronglyMeasurable (g n)
hi : StronglyMeasurable i
h₂ : ∀ (x : X), Tendsto (fun x_1 ↦ g x_1 x) atTop (𝓝 (i x))
h : ℕ → Y → Z
mh : ∀ (n : ℕ), StronglyMeasurable (h n)
hh : ∀ (n : ℕ), g n = h n ∘ f
x : X
⊢ Tendsto (fun x_1 ↦ h x_1 (f x)) atTop (𝓝 (i x))

Tactic:
simp_all

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableConstSMul M α
c : M
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
b : E
⊢ μ ((fun x ↦ c • x) ⁻¹' s) ≠ ∞

Tactic:
by rwa [SMulInvariantMeasure.measure_preimage_smul c hs]

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun x_1 ↦ f x_1 x) atTop ∂μ ≤ μ univ
x : α
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun x ↦ f x a) atTop ∂μ ≤ limsup (fun x_1 ↦ f x_1 x) atTop
b : ℝ≥0∞
hb : ∀ᶠ (n : ℕ) in atTop, ⨍⁻ (x : α), f n x ∂μ ≤ b
⊢ r / μ univ ≤ b

Tactic:
obtain ⟨n, hn⟩ := hb.exists

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
hf₁ : ∀ (n : ℕ), f n ≤ 1
hrf : ∀ (n : ℕ), r ≤ ∫⁻ (a : α), f n a ∂μ
hμ : μ ≠ 0
this : ∫⁻ (x : α), limsup (fun x_1 ↦ f x_1 x) atTop ∂μ ≤ μ univ
x : α
hxN : x ∉ N
hx : ⨍⁻ (a : α), limsup (fun x ↦ f x a) atTop ∂μ ≤ limsup (fun x_1 ↦ f x_1 x) atTop
b : ℝ≥0∞
hb : ∀ᶠ (n : ℕ) in atTop, ⨍⁻ (x : α), f n x ∂μ ≤ b
n : ℕ
hn : ⨍⁻ (x : α), f n x ∂μ ≤ b
⊢ r / μ univ ≤ b
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε
F : Fin N → α → β := fun n ↦ f ↑n
hF : ∀ (n : Fin N), MemLp (F n) p μ
s : Set α
hμs : μ s ≠ ∞
hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ ↑ε
⊢ ∃ s, μ s ≠ ∞ ∧ ∀ (i : ℕ), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
refine ⟨s, hμs, fun n => ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ≥0
hε : 0 < ε
N : ℕ
hNε : ∀ n ≥ N, eLpNorm (f n) p μ ≤ ↑ε
F : Fin N → α → β := fun n ↦ f ↑n
hF : ∀ (n : Fin N), MemLp (F n) p μ
s : Set α
hμs : μ s ≠ ∞
hFε : ∀ (i : Fin N), eLpNorm (sᶜ.indicator (F i)) p μ ≤ ↑ε
n : ℕ
⊢ eLpNorm (sᶜ.indicator (f n)) p μ ≤ ↑ε
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
x : E
hx : x ∈ ↑K ∩ (↑L \ {0})
⊢ x ∈ L

Tactic:
simp_all

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

Goal state before:
pp: E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
this : μ F * 2 ^ finrank ℝ E < μ ↑(S n)
h_symm' : ∀ x ∈ S n, -x ∈ S n
x : ↥L
hx_nz : x ≠ 0
hx_mem : ↑x ∈ ↑(S n)
⊢ ↑x ∈ ↑L \ {0}

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
f f' : ℕ → α → β
g g' : α → β
hff' : ∀ (n : ℕ), f n =ᵐ[μ] f' n
hgg' : g =ᵐ[μ] g'
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f' n x) atTop (𝓝 (g' x))

Tactic:
have hff'' := eventually_countable_forall.mpr hff'
  filter_upwards [hff'', hgg', hfg] with x hff'x hgg'x hfgx
  apply Tendsto.congr hff'x
  rw [← hgg'x]; exact hfgx

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
⊢ ∀ᶠ (x : E) in 𝓝[s] a, ‖∫ᶜ (x : E) in Path.segment a x, ω x - (ω a) (x - a)‖ ≤ ε * ‖x - a‖

Tactic:
eventually_nhdsWithin_iff

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
⊢ ∀ᶠ (x : E) in 𝓝 a, x ∈ s → ‖∫ᶜ (x : E) in Path.segment a x, ω x - (ω a) (x - a)‖ ≤ ε * ‖x - a‖
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: case pos
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / ↑N
ak : ℕ → ℝ := fun k ↦ a + ↑k * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + ↑N * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
h5 :
  EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
h6 :
  EqOn (iteratedDerivWithin 2 f (Set.Icc a b)) (iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
x : ℝ
hx : x ∈ Set.Icc (ak k) (ak (k + 1))
⊢ |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ

Tactic:
fpp_bound

Goal state after:
case pos
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / ↑N
ak : ℕ → ℝ := fun k ↦ a + ↑k * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + ↑N * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
h5 :
  EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
h6 :
  EqOn (iteratedDerivWithin 2 f (Set.Icc a b)) (iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))
x : ℝ
hx : x ∈ Set.Icc (ak k) (ak (k + 1))
⊢ ζ ≤ ζ
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: α : 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 ^ ℵ₀
⊢ #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀

Tactic:
have C : #(⋃ j < i, generateMeasurableRec s j) ≤ max #s 2 ^ ℵ₀ := by
    apply mk_biUnion_le_of_le_lift _ B _
    · intro j hj
      exact IH j hj (hj.trans_le hi).le
    · rw [lift_power, lift_aleph0]
      rw [← Ordinal.lift_le.{u}, lift_omega, Ordinal.lift_one, ← ord_aleph] at hi
      have H := card_le_of_le_ord hi
      rw [← Ordinal.lift_card] at H
      apply H.trans <| aleph_one_le_continuum.trans <| power_le_power_right _
      rw [lift_max, Cardinal.lift_ofNat]
      exact le_max_right _ _

Goal state after:
α : 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 ^ ℵ₀
⊢ #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n) μ
k : ℕ
hk : ↑k ≤ ↑n
⊢ ↑k ≤ ↑n

Tactic:
simp_all

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ∞
hint : ∀ (k : ℕ), MemLp id (↑k) μ
k : ℕ
hk : ↑k ≤ n
⊢ ↑k ≤ ↑k

Tactic:
simp_all

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n) μ
x : Fin n → E
h : innerₗ E = ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)
k : ℕ
hk : ↑k ≤ ↑n
⊢ ↑k ≤ ↑n

Tactic:
simp_all

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

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n) μ
t : ℝ
k : ℕ
hkn : k ∈ Finset.range (n + 1)
⊢ ↑k ≤ ↑n

Tactic:
simp_all

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

Goal state before:
pp: case convert_7
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
⊢ ∫ (x : Ω), id (X x) ^ 2 ∂P ≠ 0

Tactic:
simp_all

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

Goal state before:
pp: ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⨅ i, t i
x : X
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : ↥I' → X → ↑I
hfs : ∀ (i : ↥I'), Continuous[t ↑i, _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
⊢ ∃ f, Continuous[⨅ i, t i, _] f ∧ f x = 0 ∧ EqOn f 1 (⋂ i, V i)ᶜ

Tactic:
use I'.attach.sup fs

Goal state after:
case h
ι : Type u_1
X : Type u_2
t : ι → TopologicalSpace X
ht : ∀ (i : ι), CompletelyRegularSpace X
this : TopologicalSpace X := ⋯
x : X
I' : Finset ι
V U : ↥I' → Set X
hUV : ∀ (i : ↥I'), U i ⊆ V i
fs : ↥I' → X → ↑I
hfs : ∀ (i : ↥I'), Continuous[t ↑i, _] (fs i)
hxfs : ∀ (i : ↥I'), fs i x = 0
hfsU : ∀ (i : ↥I'), EqOn (fs i) 1 (U i)ᶜ
⊢ Continuous[⨅ i, t i, _] (I'.attach.sup fs) ∧ I'.attach.sup fs x = 0 ∧ EqOn (I'.attach.sup fs) 1 (⋂ i, V i)ᶜ
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T35Space X
x y : X
x_ne_y : x ≠ y
f : X → ↑I
f_cont : Continuous[inst✝¹, _] f
f_zero : f x = 0
f_one : EqOn f 1 {y}
⊢ (fun x ↦ ↑(f x)) x ≠ (fun x ↦ ↑(f x)) y

Tactic:
simp_all

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T35Space X
x y : X
x_ne_y : x ≠ y
f : X → ↑I
f_cont : Continuous[inst✝¹, _] f
f_zero : f x = 0
f_one : EqOn f 1 {y}
⊢ f x ≠ f y

Tactic:
simp_all

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
⊢ s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε

Tactic:
s,

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
⊢ levyProkhorovEDist ν κ + ε / 2 + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case refine_1
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : BorelSpace Ω
μ ν : LevyProkhorov (ProbabilityMeasure Ω)
h : dist μ ν = 0
⊢ inst✝³ = MeasurableSpace.generateFrom {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}

Tactic:
BorelSpace.measurable_eq (α := Ω),

Goal state after:
case refine_1
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : BorelSpace Ω
μ ν : LevyProkhorov (ProbabilityMeasure Ω)
h : dist μ ν = 0
⊢ borel Ω = MeasurableSpace.generateFrom {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
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
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
this✝ : ∀ (n : Fin N), y n ≤ b
this : ∑ n, y n ≤ ∑ n, b
⊢ ∑ n, y n ≤ ↑N * b

Tactic:
simp_all

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

Goal state before:
pp: Ω : 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_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 (0 + 0))
⊢ Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)

Tactic:
rw [tendsto_nhdsWithin_iff]

Goal state after:
Ω : 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_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 (0 + 0))
⊢ Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝 0) ∧ ∀ᶠ (n : ℕ) in atTop, dist (μs n) ν + εs n ∈ Ioi 0
Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝¹⁰ : Group G
inst✝⁹ : AddCommGroup A
inst✝⁸ : DistribMulAction G A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : IsTopologicalAddGroup A
inst✝⁵ : LocallyCompactSpace A
inst✝⁴ : ContinuousConstSMul G A
g : G
inst✝³ : MeasurableSpace A
inst✝² : BorelSpace A
μ : Measure A
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : μ.Regular
s : Set A
hs₀ : μ s ≠ 0
hs : μ s ≠ ∞
r : ℝ≥0
hμgs : μ (g • s) = ↑r * μ s
⊢ (distribHaarChar A) g = r

Tactic:
refine ENNReal.coe_injective ?_
  rw [distribHaarChar_eq_div hs₀ hs, hμgs, ENNReal.mul_div_cancel_right] <;> simp [*]

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

Goal state before:
pp: case neg
μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
y : ℝ
hy : ¬y = 0
⊢ ∫ (x : ℝ) in -r..r, cexp (↑x * ↑y * I) =
    if r * y = 0 then 2 * ↑r else ↑y⁻¹ * ∫ (x : ℝ) in -(y * r)..y * r, cexp (↑x * I)

Tactic:
simp only [mul_eq_zero, hr.ne', hy, or_self, ↓reduceIte, ofReal_inv]

Goal state after:
case neg
μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
y : ℝ
hy : ¬y = 0
⊢ ∫ (x : ℝ) in -r..r, cexp (↑x * ↑y * I) = (↑y)⁻¹ * ∫ (x : ℝ) in -(y * r)..y * r, cexp (↑x * I)