mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.Piecewise

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
⊢ StronglyMeasurable (hs.piecewise f)

Tactic:
by_cases Fi : Finite ι

Goal state after:
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Finite ι
⊢ StronglyMeasurable (hs.piecewise f)

case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : ¬Finite ι
⊢ StronglyMeasurable (hs.piecewise f)
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp_ne_top : p ≠ ∞
hg : MemLp g p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ↑ε = ∞
⊢ ∃ s, μ s ≠ ∞ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((fun x ↦ g) i)) p μ ≤ ↑ε

Tactic:
exact ⟨∅, (by simp), fun _ => hε_top.symm ▸ le_top⟩

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifTight f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ↑ε = ∞
⊢ ∃ s, μ s ≠ ∞ ∧ ∀ (i : Fin (n + 1)), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
exact ⟨∅, (by simp), fun _ => hε_top.symm ▸ le_top⟩

Goal state after:
Module: Mathlib.Topology.Homotopy.Affine

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
f g : C(X, E)
⊢ Continuous fun x ↦ (Path.segment (f x.2) (g x.2)) x.1

Tactic:
dsimp [AffineMap.lineMap_apply]

Goal state after:
X : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
f g : C(X, E)
⊢ Continuous fun x ↦ ↑x.1 • (g x.2 - f x.2) + f x.2
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ ∫ (x : ℝ) in Ioi 0, (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-(x ^ (1 / p)) ^ p)) =
    ∫ (x : ℝ) in Ioi 0, (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)

Goal state after:
p q : ℝ
hp : 0 < p
hq : -1 < q
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ (1 / p * x✝ ^ (1 / p - 1)) • ((x✝ ^ (1 / p)) ^ q * rexp (-(x✝ ^ (1 / p)) ^ p)) =
    (1 / p * x✝ ^ (1 / p - 1)) • ((x✝ ^ (1 / p)) ^ q * rexp (-x✝))
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ ∫ (x : ℝ) in Ioi 0, 1 / p * (x ^ (1 / p - 1) * ((x ^ (1 / p)) ^ q * rexp (-x))) =
    ∫ (x : ℝ) in Ioi 0, 1 / p * (rexp (-x) * x ^ (1 / p - 1 + q / p))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)

Goal state after:
p q : ℝ
hp : 0 < p
hq : -1 < q
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ 1 / p * (x✝ ^ (1 / p - 1) * ((x✝ ^ (1 / p)) ^ q * rexp (-x✝))) = 1 / p * (rexp (-x✝) * x✝ ^ (1 / p - 1 + q / p))
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ ∫ (x : ℝ) in Ioi 0, x ^ q * rexp (-b * x ^ p) =
    ∫ (x : ℝ) in Ioi 0, b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)

Goal state after:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ x✝ ^ q * rexp (-b * x✝ ^ p) = b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x✝) ^ q * rexp (-(b ^ p⁻¹ * x✝) ^ p))
Module: Mathlib.MeasureTheory.Integral.MeanValue

Goal state before:
pp: α : 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
hν0' : (ν s).toReal ≠ 0
hνfin : ν s ≠ ⊤
hν0'' : ν s ≠ 0
hmul_ae : (fun x ↦ (ρ x).toReal * f x) =ᵐ[μ.restrict s] fun x ↦ f x * g x
h_IntOn : IntegrableOn (fun x ↦ (ρ x).toReal * f x) s μ
h_Int : Integrable f ((μ.restrict s).withDensity ρ)
t : Set α
ht : MeasurableSet t
⊢ (ν.restrict s) t = ((μ.restrict s).withDensity ρ) t

Tactic:
simp [ht, ν, hs_meas]

Goal state after:
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 : Disjoint 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)
hsot : t ⊆ ⋃ j, so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport ⇑(f i) ⊆ so i
sum_f_one_on_t : EqOn (∑ i, ⇑(f i)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), (f i) x ∈ Icc 0 1
f_hcs : ∀ (i : Fin 2), HasCompactSupport ⇑(f i)
sum_one_x : ∀ x ∈ t, (f 0) x + (f 1) x = 1
x : X
hx : x ∈ s₀
⊢ s₀ ⊆ ((fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ) 0)ᶜ

Tactic:
simp only [Fin.isValue, ↓reduceIte, compl_compl, subset_refl]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: 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
⊢ |trapezoidal_error f N a (a + ↑N * h)| ≤ (a + ↑N * h - a) ^ 3 * ζ / (12 * ↑N ^ 2)

Tactic:
← sum_trapezoidal_error_adjacent_intervals N_nonzero
    (hb ▸ h_df.continuousOn.intervalIntegrable_of_Icc a_lt_b.le)

Goal state after:
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
⊢ |∑ i ∈ Finset.range N, trapezoidal_error f 1 (a + ↑i * h) (a + (↑i + 1) * h)| ≤
    (a + ↑N * h - a) ^ 3 * ζ / (12 * ↑N ^ 2)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: 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
this : ∀ k ∈ Finset.range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * h ^ 3
⊢ ↑N * (ζ / 12 * h ^ 3) = (a + ↑N * h - a) ^ 3 * ζ / ↑(12 * N ^ 2)

Tactic:
push_cast

Goal state after:
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
this : ∀ k ∈ Finset.range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ ζ / 12 * h ^ 3
⊢ ↑N * (ζ / 12 * h ^ 3) = (a + ↑N * h - a) ^ 3 * ζ / (12 * ↑N ^ 2)
Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA : (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) (Subalgebra.restrictScalars ℝ A.toSubalgebra)
⊢ P = P'

Tactic:
have hA_toReal : (A_toReal.map (toContinuousMapₐ ℝ)).SeparatesPoints := by
    rw [RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict]
    exact Subalgebra.SeparatesPoints.rclike_to_real hA

Goal state after:
E : Type u_1
𝕜 : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA : (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm ⋯) (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
⊢ P = P'
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

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

pp: case h1.h1.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 ^ ℵ₀
⊢ #↑{∅} ≤ max (#↑s) 2 ^ ℵ₀

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:
· exact (self_le_power _ one_le_aleph0).trans (power_le_power_right (le_max_left _ _))

Goal state after:
case h1.h1.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 ^ ℵ₀
⊢ #↑{∅} ≤ max (#↑s) 2 ^ ℵ₀

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 ^ ℵ₀
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 !)⁻¹ * t ^ k) * iteratedDerivWithin k (charFun μ) univ 0 = (↑k !)⁻¹ * (↑t * I) ^ k * ↑(∫ (x : ℝ), x ^ k ∂μ)

Tactic:
push_cast

Goal state after:
μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n) μ
t : ℝ
k : ℕ
hkn : k ∈ Finset.range (n + 1)
⊢ (↑k !)⁻¹ * ↑t ^ k * iteratedDerivWithin k (charFun μ) univ 0 = (↑k !)⁻¹ * (↑t * I) ^ k * ↑(∫ (x : ℝ), x ^ k ∂μ)
Module: Mathlib.MeasureTheory.Measure.DiracProba

Goal state before:
pp: X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhds : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhds : interior U ∈ 𝓝 x
f : X →ᵇ ℝ≥0
fx_eq_one : f x = 1
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0
⊢ ¬Tendsto diracProba L (𝓝 (diracProba x))

Tactic:
ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto,

Goal state after:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhds : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhds : interior U ∈ 𝓝 x
f : X →ᵇ ℝ≥0
fx_eq_one : f x = 1
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0
⊢ ¬∀ (f : X →ᵇ ℝ≥0), Tendsto (fun i ↦ ∫⁻ (ω : X), ↑(f ω) ∂↑(diracProba i)) L (𝓝 (∫⁻ (ω : X), ↑(f ω) ∂↑(diracProba x)))
Module: Mathlib.MeasureTheory.Measure.DiracProba

Goal state before:
pp: case mpr
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : Tendsto id L (𝓝 x)
aux : ContinuousAt (fun x ↦ diracProba x) x
⊢ Tendsto diracProba L (𝓝 (diracProba x))

Tactic:
simp only [ContinuousAt] at aux

Goal state after:
case mpr
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : Tendsto id L (𝓝 x)
aux : Tendsto (fun x ↦ diracProba x) (𝓝 x) (𝓝 (diracProba x))
⊢ Tendsto diracProba L (𝓝 (diracProba x))
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
⊢ 0 < ε →
    ε < ∞ →
      MeasurableSet B →
        μ B ≤
            κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
                (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
              ε ∧
          κ B ≤
            μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
                (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
              ε

Tactic:
ε_pos

Goal state after:
case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
⊢ ε < ∞ →
    MeasurableSet B →
      μ B ≤
          κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
              (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
            ε ∧
        κ B ≤
          μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
              (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
            ε
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ∞
key :
  Tendsto (fun ε ↦ ν (thickening ε.toReal s)) (𝓝[>] 0)
    (𝓝 (ν (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)))
obs :
  Tendsto (fun x ↦ ν (thickening x.toReal s) + x) (𝓝[>] 0)
    (𝓝 (ν (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)))
ε : ℝ≥0∞
⊢ ε ∈ Ioi 0 → μ s ≤ ν (thickening ε.toReal s) + ε

Tactic:
ε_pos

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ∞
key :
  Tendsto (fun ε ↦ ν (thickening ε.toReal s)) (𝓝[>] 0)
    (𝓝 (ν (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)))
obs :
  Tendsto (fun x ↦ ν (thickening x.toReal s) + x) (𝓝[>] 0)
    (𝓝 (ν (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)))
ε : ℝ≥0∞
ε_pos : ε ∈ Ioi 0
⊢ μ s ≤ ν (thickening ε.toReal s) + ε
Module: Mathlib.MeasureTheory.Measure.FiniteMeasureProd

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ (μ.prod ν).map Prod.swap = ν.prod μ

Tactic:
by
  apply Subtype.ext
  simp [Measure.prod_swap]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
⊢ (μ.prod ν).map ⋯ = ν.prod μ

Tactic:
by
  apply Subtype.ext
  simp [Measure.prod_swap]

Goal state after:
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
⊢ μ K ≤ ν K

Tactic:
refine ENNReal.le_of_forall_pos_le_add fun ε hε hν ↦ ?_
  have hνK : ν K ≠ ⊤ := hν.ne
  have hμK : μ K ≠ ⊤ := hK.measure_lt_top.ne
  obtain ⟨V, pV1, pV2, pV3⟩ : ∃ V ⊇ K, IsOpen V ∧ ν V ≤ ν K + ε :=
    exists_isOpen_le_add K ν (ne_of_gt (ENNReal.coe_lt_coe.mpr hε))
  suffices μ.real K ≤ ν.real K + ε by
    rwa [← ENNReal.toReal_le_toReal, ENNReal.toReal_add, ENNReal.coe_toReal]
    all_goals finiteness
  have VltTop : ν V < ⊤ := pV3.trans_lt <| by finiteness
  obtain ⟨f, pf1, pf2, pf3⟩ :
      ∃ f : C_c(X, ℝ), Set.EqOn (⇑f) 1 K ∧ tsupport ⇑f ⊆ V ∧ ∀ (x : X), f x ∈ Set.Icc 0 1 := by
    obtain ⟨f, hf1, hf2, hf3⟩ := exists_continuousMap_one_of_isCompact_subset_isOpen hK pV2 pV1
    exact ⟨⟨f, hasCompactSupport_def.mpr hf2⟩, hf1, hf3⟩
  have hfV (x : X) : f x ≤ V.indicator 1 x := by
    by_cases hx : x ∈ tsupport f
    · simp [(pf2 hx), (pf3 x).2]
    · simp [image_eq_zero_of_notMem_tsupport hx, Set.indicator_nonneg]
  have hfK (x : X) : K.indicator 1 x ≤ f x := by
    by_cases hx : x ∈ K
    · simp [hx, pf1 hx]
    · simp [hx, (pf3 x).1]
  calc
    μ.real K = ∫ x, K.indicator 1 x ∂μ := integral_indicator_one hK.measurableSet |>.symm
    _ ≤ ∫ x, f x ∂μ := by
      refine integral_mono ?_ f.integrable hfK
      exact (continuousOn_const.integrableOn_compact hK).integrable_indicator hK.measurableSet
    _ ≤ ∫ x, f x ∂ν := hμν f
    _ ≤ ∫ x, V.indicator 1 x ∂ν := by
      refine integral_mono f.integrable ?_ hfV
      exact IntegrableOn.integrable_indicator integrableOn_const pV2.measurableSet
    _ ≤ (ν K).toReal + ↑ε := by
      rwa [integral_indicator_one pV2.measurableSet, measureReal_def,
        ← ENNReal.coe_toReal, ← ENNReal.toReal_add, ENNReal.toReal_le_toReal]
      all_goals finiteness

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
⊢ ε > 0 → ∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist (ofMeasure x) (ofMeasure P) < ε

Tactic:
ε_pos

Goal state after:
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
⊢ ∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist (ofMeasure x) (ofMeasure P) < ε
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: case inr
A : Type u_1
B : Type u_2
C : Type u_3
inst✝¹⁷ : Group A
inst✝¹⁶ : Group B
inst✝¹⁵ : Group C
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝¹¹ : IsTopologicalGroup A
inst✝¹⁰ : IsTopologicalGroup B
inst✝⁹ : MeasurableSpace A
inst✝⁸ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁷ : IsTopologicalGroup C
inst✝⁶ : LocallyCompactSpace B
inst✝⁵ : MeasurableSpace C
inst✝⁴ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝³ : T2Space B
inst✝² : MeasurableSpace B
inst✝¹ : BorelSpace B
U : Set B
hU : IsOpen U
inst✝ : DiscreteTopology A
h✝ : μC Set.univ * μA {1} < (H.inducedMeasure μA μC) U
ho : 0 < μA {1}
ht : μA {1} < ⊤
K : Set B
hKU : K ⊆ U
hK : IsCompact K
f : C(B, ℝ)
hf1 : Set.EqOn (⇑f) 1 K
hf2 : IsCompact (tsupport ⇑f)
hf3 : tsupport ⇑f ⊆ U
hf4 : ∀ (x : B), f x ∈ Set.Icc 0 1
h : ∀ (c : C), ((H.pushforward μA) { toContinuousMap := f, hasCompactSupport' := hf2 }) c ≤ (μA {1}).toReal
hC : μC Set.univ < ⊤
this : IsFiniteMeasure μC
⊢ ENNReal.ofReal (∫ (c : C), ((H.pushforward μA) { toContinuousMap := f, hasCompactSupport' := hf2 }) c ∂μC) ≤
    μC Set.univ * μA {1}

Tactic:
ENNReal.ofReal_le_iff_le_toReal (ENNReal.mul_lt_top hC ht).ne,

Goal state after:
case inr
A : Type u_1
B : Type u_2
C : Type u_3
inst✝¹⁷ : Group A
inst✝¹⁶ : Group B
inst✝¹⁵ : Group C
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝¹¹ : IsTopologicalGroup A
inst✝¹⁰ : IsTopologicalGroup B
inst✝⁹ : MeasurableSpace A
inst✝⁸ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁷ : IsTopologicalGroup C
inst✝⁶ : LocallyCompactSpace B
inst✝⁵ : MeasurableSpace C
inst✝⁴ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝³ : T2Space B
inst✝² : MeasurableSpace B
inst✝¹ : BorelSpace B
U : Set B
hU : IsOpen U
inst✝ : DiscreteTopology A
h✝ : μC Set.univ * μA {1} < (H.inducedMeasure μA μC) U
ho : 0 < μA {1}
ht : μA {1} < ⊤
K : Set B
hKU : K ⊆ U
hK : IsCompact K
f : C(B, ℝ)
hf1 : Set.EqOn (⇑f) 1 K
hf2 : IsCompact (tsupport ⇑f)
hf3 : tsupport ⇑f ⊆ U
hf4 : ∀ (x : B), f x ∈ Set.Icc 0 1
h : ∀ (c : C), ((H.pushforward μA) { toContinuousMap := f, hasCompactSupport' := hf2 }) c ≤ (μA {1}).toReal
hC : μC Set.univ < ⊤
this : IsFiniteMeasure μC
⊢ ∫ (c : C), ((H.pushforward μA) { toContinuousMap := f, hasCompactSupport' := hf2 }) c ∂μC ≤
    (μC Set.univ * μA {1}).toReal
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: μ : 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 : ℝ), if r * y = 0 then 2 * ↑r else ↑y⁻¹ * ∫ (x : ℝ) in -(y * r)..y * r, cexp (↑x * I) ∂μ =
    ∫ (x : ℝ), 2 * ↑r * ↑(sinc (r * x)) ∂μ

Tactic:
by
    congr with y
    rw [integral_exp_mul_I_eq_sinc]
    split_ifs with hry
    · simp [hry]
    have hy : y ≠ 0 := fun hy ↦ hry (by simp [hy])
    norm_cast
    field_simp

Goal state after: