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

Goal state before:
pp: α : 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)
n : ℕ
⊢ f n ≤ 1

Tactic:
rintro a

Goal state after:
α : 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)
n : ℕ
a : α
⊢ f n a ≤ 1 a
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁸ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁷ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : BorelSpace E
E' : Type u_6
mE' : MeasurableSpace E'
inst✝³ : SeminormedAddCommGroup E'
inst✝² : SecondCountableTopology E'
inst✝¹ : BorelSpace E'
inst✝ : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun x ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
this : TendstoInMeasure μ'' (fun n ω ↦ (0, Y n ω - c)) l 0
⊢ TendstoInMeasure μ'' ((fun n ω ↦ (X n ω, Y n ω)) - fun n ω ↦ (X n ω, c)) l 0

Tactic:
convert! this with n ω

Goal state after:
case e'_3
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁸ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁷ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : BorelSpace E
E' : Type u_6
mE' : MeasurableSpace E'
inst✝³ : SeminormedAddCommGroup E'
inst✝² : SecondCountableTopology E'
inst✝¹ : BorelSpace E'
inst✝ : l.IsCountablyGenerated
X : ι → Ω'' → E
Y : ι → Ω'' → E'
Z : Ω' → E
c : E'
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hY : TendstoInMeasure μ'' Y l fun x ↦ c
hY_meas : ∀ (i : ι), AEMeasurable (Y i) μ''
hX : ∀ (i : ι), AEMeasurable (X i) μ''
this : TendstoInMeasure μ'' (fun n ω ↦ (0, Y n ω - c)) l 0
n : ι
ω : Ω''
⊢ (((fun n ω ↦ (X n ω, Y n ω)) - fun n ω ↦ (X n ω, c)) n ω).1 = 0
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 < ∞
f : { f // MeasurePreserving (⇑f) μ ν }
⊢ Tendsto (fun y ↦ μ ((⇑↑y ⁻¹' s) ∆ (⇑↑f ⁻¹' s))) (𝓝 f) (𝓝 0)

Tactic:
apply tendsto_measure_symmDiff_preimage_nhds_zero continuousAt_subtype_val _ f.2
      hs.nullMeasurableSet hνs.ne

Goal state after:
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 < ∞
f : { f // MeasurePreserving (⇑f) μ ν }
⊢ ∀ᶠ (a : { f // MeasurePreserving (⇑f) μ ν }) in 𝓝 f, MeasurePreserving (⇑↑a) μ ν
Module: Mathlib.MeasureTheory.Function.Intersectivity

Goal state before:
pp: case refine_1
α : 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
⊢ ∀ᶠ (a : ℕ) in atTop, (fun x1 x2 ↦ x1 ≤ x2) (⨍⁻ (x : α), f a x ∂μ) 1

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:
· refine Eventually.of_forall fun n ↦ ?_
    obtain rfl | _ := eq_zero_or_neZero μ
    · simp
    · rw [← laverage_const μ 1]
      exact lintegral_mono (hf₁ _)

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
⊢ r / μ univ ≤ b
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
⊢ ∀ {f : Fin 0 → α → β}, (∀ (i : Fin 0), MemLp (f i) p μ) → UnifTight f p μ

Tactic:
| zero =>

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

Goal state before:
pp: R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn ((fun x ↦ ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑x‖

Tactic:
have none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty :=
    (nonempty_closedBall.2 hr').prod nonempty_uIcc

Goal state after:
R r : ℝ
hr : r < R
hr' : 0 ≤ r
z : ℂ
cts : ContinuousOn ((fun x ↦ ‖x‖) ∘ circleTransformBoundingFunction R z) (closedBall z r ×ˢ univ)
comp : IsCompact (closedBall z r ×ˢ [[0, 2 * π]])
none : (closedBall z r ×ˢ [[0, 2 * π]]).Nonempty
⊢ ∃ x,
    ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])),
      ‖circleTransformBoundingFunction R z ↑y‖ ≤ ‖circleTransformBoundingFunction R z ↑x‖
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✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
𝕝 : Type u_4
inst✝² : RCLike 𝕝
inst✝¹ : NormedSpace 𝕝 F
inst✝ : SMulCommClass 𝕜 𝕝 F
c : 𝕝
⊢ CurveIntegrable (c • ω) γ ↔ c = 0 ∨ CurveIntegrable ω γ

Tactic:
by
  rcases eq_or_ne c 0 with rfl | hc
  · simp [CurveIntegrable.zero]
  · simp only [hc, false_or]
    refine ⟨fun h ↦ ?_, .smul⟩
    simpa [hc] using h.smul (c := c⁻¹)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ (a : α), (↑(f a) ≠ 0 → g a = g' a) → f a ≠ 0 → ↑(f a) • g a = ↑(f a) • g' a

Tactic:
intro a

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
a : α
⊢ (↑(f a) ≠ 0 → g a = g' a) → f a ≠ 0 → ↑(f a) • g a = ↑(f a) • g' a
Module: Mathlib.Order.Interval.Set.Union

Goal state before:
pp: case zero
X : Type u_1
inst✝ : LinearOrder X
a : ℕ → X
⊢ Ioc (a 0) (a 0) ⊆ ⋃ i ∈ Finset.range 0, Ioc (a i) (a (i + 1))

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Order.Interval.Set.Union

Goal state before:
pp: case zero
X : Type u_1
inst✝ : LinearOrder X
a : ℕ → X
⊢ Ico (a 0) (a 0) ⊆ ⋃ i ∈ Finset.range 0, Ico (a i) (a (i + 1))

Tactic:
| zero =>

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| ≤ ζ
g : ℝ → ℝ := fun t ↦ trapezoidal_error f 1 a t
dg : ℝ → ℝ := fun t ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : ℝ → ℝ := fun t ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ y ∈ Set.Icc a b, HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ y ∈ Set.Icc a b, HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
x : ℝ
hx : x ∈ Set.Icc a b
⊢ |x - a| / |2| * |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ / 2 * (x - a)

Tactic:
abs_two

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| ≤ ζ
g : ℝ → ℝ := fun t ↦ trapezoidal_error f 1 a t
dg : ℝ → ℝ := fun t ↦ 1 / 2 * (f a + f t) + (t - a) / 2 * _root_.derivWithin f (Set.Icc a b) t - f t
ddg : ℝ → ℝ := fun t ↦ (t - a) / 2 * iteratedDerivWithin 2 f (Set.Icc a b) t
h_dg : ∀ y ∈ Set.Icc a b, HasDerivWithinAt g (dg y) (Set.Icc a b) y
h_ddg : ∀ y ∈ Set.Icc a b, HasDerivWithinAt dg (ddg y) (Set.Icc a b) y
x : ℝ
hx : x ∈ Set.Icc a b
⊢ |x - a| / 2 * |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ / 2 * (x - a)
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : X →C_c ℝ≥0
⊢ 0 ≤ fun a ↦ ↑(f a)

Tactic:
intro a

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : LocallyCompactSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
f : X →C_c ℝ≥0
a : X
⊢ 0 a ≤ (fun a ↦ ↑(f a)) a
Module: Mathlib.MeasureTheory.Integral.TorusIntegral

Goal state before:
pp: n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
hf : TorusIntegrable f c R
hg : TorusIntegrable g c R
⊢ (∯ (x : Fin n → ℂ) in T(c, R), f x + g x) = (∯ (x : Fin n → ℂ) in T(c, R), f x) + ∯ (x : Fin n → ℂ) in T(c, R), g x

Tactic:
by
  simpa only [torusIntegral, smul_add, Pi.add_apply] using
    integral_add hf.function_integrable hg.function_integrable

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
⊢ invariants f ≤ invariants f^[0]

Tactic:
| zero =>

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 ℝ)
hint' : ∀ (k : ℕ), ↑k ≤ ↑n → Integrable (fun x ↦ ‖x‖ ^ k * ‖1 x‖) μ
⊢ Integrable (fun v ↦ ‖v‖ ^ n * ‖1 v‖) μ

Tactic:
by simpa using hint.integrable_norm_pow'

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

Goal state before:
pp: E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
t : E
⊢ ‖charFun μ t‖ ≤ μ.real Set.univ

Tactic:
charFun_eq_fourierIntegral

Goal state after:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
t : E
⊢ ‖VectorFourier.fourierIntegral probChar μ (innerₗ E) 1 (-t)‖ ≤ μ.real Set.univ
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
inst✝ : R0Space X
x : X
K : Set X
hK : IsClosed[inst✝²] K
hx : x ∉ K
cx : IsClosed[inst✝²] (closure[inst✝²] {x})
⊢ closure[inst✝²] {x} ∩ K ⊆ ∅

Tactic:
intro a

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
inst✝ : R0Space X
x : X
K : Set X
hK : IsClosed[inst✝²] K
hx : x ∉ K
cx : IsClosed[inst✝²] (closure[inst✝²] {x})
a : X
⊢ a ∈ closure[inst✝²] {x} ∩ K → a ∈ ∅
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
p : ℝ≥0∞
inst✝² : Fact (1 ≤ p)
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : StrongDual ℝ (WithLp p (E × F))
⊢ charFunDual (Measure.map (toLp p) (μ.prod ν)) L =
    charFunDual μ (L ∘SL ↑(prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inl ℝ E F) *
      charFunDual ν (L ∘SL ↑(prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inr ℝ E F)

Tactic:
simp_rw [charFunDual_apply, ← integral_prod_mul, ← Complex.exp_add, ← add_mul, ← ofReal_add,
    L.comp_apply, ← map_add, ContinuousLinearMap.comp_inl_add_comp_inr]

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
p : ℝ≥0∞
inst✝² : Fact (1 ≤ p)
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : StrongDual ℝ (WithLp p (E × F))
⊢ ∫ (v : WithLp p (E × F)), cexp (↑(L v) * I) ∂Measure.map (toLp p) (μ.prod ν) =
    ∫ (z : E × F), cexp (↑(L (↑(prodContinuousLinearEquiv p ℝ E F).symm z)) * I) ∂μ.prod ν
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T35Space X
⊢ Function.Injective stoneCechUnit

Tactic:
intro a

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T35Space X
a : X
⊢ ∀ ⦃a₂ : X⦄, stoneCechUnit a = stoneCechUnit a₂ → a = a₂
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 : 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)ᶜ
almost : 1 ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + (ε + μ (thickening ε.toReal B))
⊢ 1 - ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤ μ (thickening ε.toReal B) + ε

Tactic:
apply (tsub_le_tsub_right almost _).trans

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)ᶜ
almost : 1 ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + (ε + μ (thickening ε.toReal B))
⊢ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + (ε + μ (thickening ε.toReal B)) -
      ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤
    μ (thickening ε.toReal B) + ε
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case f_mble
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
key : (fun t ↦ μ.real {a | t ≤ f a}) ≤ fun t ↦ ν.real (thickening ε {a | t ≤ f a}) + ε
intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume
⊢ AEStronglyMeasurable (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) volume

Tactic:
apply (Measurable.ennreal_toReal (Antitone.measurable ?_)).aestronglyMeasurable
      exact fun _ _ hst ↦ measure_mono <| thickening_subset_of_subset ε (fun _ h ↦ hst.trans h)

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
Λ : (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)
h : ∑ n, y n ≤ ↑N * b
⊢ ↑N ≠ 0

Tactic:
simp [hN.ne.symm]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case a
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 ℝ
⊢ Λ f ≤ ∫ (x : X), f x ∂rieszMeasure Λ

Tactic:
· exact integral_riesz_aux Λ f

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case e'_3
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : μ Kᶜ = 0
μ' : Measure ↑K := Measure.comap Subtype.val μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
g : X →ᵇ ℝ
⊢ ∫ (x : X), g x ∂Measure.map Subtype.val ν' =
    ∫ (x : ↑K), (g.compContinuous { toFun := Subtype.val, continuous_toFun := ⋯ }) x ∂ν'

Tactic:
rw [integral_map (φ := Subtype.val) (by fun_prop) (by fun_prop)]

Goal state after:
case e'_3
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : μ Kᶜ = 0
μ' : Measure ↑K := Measure.comap Subtype.val μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
g : X →ᵇ ℝ
⊢ ∫ (x : { x // x ∈ K }), g ↑x ∂ν' =
    ∫ (x : ↑K), (g.compContinuous { toFun := Subtype.val, continuous_toFun := ⋯ }) x ∂ν'