mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case indicator
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ ∫⁻ (ω : Ω), s'.indicator (fun x ↦ c') ω * T.indicator (fun x ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), s'.indicator (fun x ↦ c') ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ

Tactic:
simp_rw [← inter_indicator_mul]

Goal state after:
case indicator
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s | MeasurableSet s} {T} μ
h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a ↦ g a * T.indicator (fun x ↦ c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
⊢ ∫⁻ (ω : Ω), (s' ∩ T).indicator (fun j ↦ c' * c) ω ∂μ =
    (∫⁻ (ω : Ω), s'.indicator (fun x ↦ c') ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x ↦ c) ω ∂μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Var[X; μ] + cov[Y, X; μ] + (cov[Y, X; μ] + Var[Y; μ]) = Var[X; μ] + 2 * cov[Y, X; μ] + Var[Y; μ]

pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable Y μ

pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable X μ

pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable (X + Y) μ

Tactic:
· ring

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable Y μ

Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable X μ

Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable (X + Y) μ
Module: Mathlib.Probability.Moments.Covariance

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

Tactic:
by
  classical
  induction s using Finset.induction with
  | empty => simp
  | insert i s hi h_ind =>
    rw [Finset.sum_insert hi, Finset.sum_insert hi, covariance_add_left, h_ind]
    · exact fun j hj ↦ hX j (by simp [hj])
    · exact hX i (by simp)
    · exact memLp_finsetSum' s (fun j hj ↦ hX j (by simp [hj]))
    · exact hY

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
⊢ c.toNNReal ≠ 0

Tactic:
by simp [hc]

Goal state after:
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:
by
  classical
  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.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
hm' : ∃ x ∈ s, ↑x i = m'
⊢ m' ≤ (fun i ↦ sSup ((fun f ↦ ↑f i) '' s)) j

Tactic:
obtain ⟨f, hf_mem, hfm'⟩ := hm'

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : ↑f i = m'
⊢ m' ≤ (fun i ↦ sSup ((fun f ↦ ↑f i) '' s)) j
Module: Mathlib.Probability.Process.Filtration

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

Tactic:
by
        refine sSup_le fun m' hm' => ?_
        rw [Set.mem_image] at hm'
        obtain ⟨f, hf_mem, hfm'⟩ := hm'
        rw [← hfm']
        refine (f.mono hij).trans ?_
        have hfj_mem : f j ∈ (fun g : Filtration ι m => g j) '' s := ⟨f, hf_mem, rfl⟩
        exact le_sSup hfj_mem

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
⊢ (∫ (x : G), f (x * g) ∂ν) / ∫ (x : G), f x ∂ν = (∫ (x : G), f (x * g) ∂ν.haarScalarFactor μ • μ) / ∫ (x : G), f x ∂ν

Tactic:
by rw [t]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : μ Eg < ∞
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : μ Ef < ∞
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : μ E < ∞
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (μ E < ∞)
hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
hfnEcε : eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3
hmfngEc : AEStronglyMeasurable (Eᶜ.indicator (f n - g)) μ
⊢ eLpNorm (Eᶜ.indicator (f n - g)) p μ = eLpNorm (Eᶜ.indicator (f n) - Eᶜ.indicator g) p μ

Tactic:
by
        rw [(Eᶜ.indicator_sub' _ _)]

Goal state after:
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, b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p)) =
    (b ^ p⁻¹)⁻¹ * ∫ (x : ℝ) in Ioi 0, b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p))

Tactic:
by
      rw [integral_comp_mul_left_Ioi (fun x => b ^ (-p⁻¹ * q) * (x ^ q * exp (-x ^ p))) 0,
        mul_zero, smul_eq_mul]
      all_goals positivity

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

Goal state before:
pp: p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ ∫ (x : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)) ∂volume.prod volume =
    ∫ (z : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, z.1 * |z.1| ^ q * rexp (-|z.1| ^ p) * 1 ∂volume.prod volume

Tactic:
simp_rw [mul_one]

Goal state after:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ ∫ (x : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)) ∂volume.prod volume =
    ∫ (z : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, z.1 * |z.1| ^ q * rexp (-|z.1| ^ p) ∂volume.prod volume
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ ∫ (x : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)) ∂volume.prod volume =
    ∫ (z : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, z.1 * |z.1| ^ q * rexp (-b * |z.1| ^ p) * 1 ∂volume.prod volume

Tactic:
simp_rw [mul_one]

Goal state after:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ ∫ (x : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)) ∂volume.prod volume =
    ∫ (z : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, z.1 * |z.1| ^ q * rexp (-b * |z.1| ^ p) ∂volume.prod volume
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
⊢ ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, (ρ x).toReal * f x ∂μ

Tactic:
apply MeasureTheory.integral_congr_ae

Goal state after:
α : 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 := ⋯
ν : Measure α := ⋯
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
⊢ (fun a ↦ f a * g a) =ᵐ[μ.restrict s] fun a ↦ (ρ a).toReal * f a
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: case h₁
𝕜 : 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) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
⊢ IntervalIntegrable (fun t ↦ (ω ((lineMap a b) t)) (b - a)) volume 0 1

Tactic:
refine ContinuousOn.intervalIntegrable_of_Icc zero_le_one fun t ht ↦ ?_

Goal state after:
case h₁
𝕜 : 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) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
t : ℝ
ht : t ∈ Icc 0 1
⊢ ContinuousWithinAt (fun t ↦ (ω ((lineMap a b) t)) (b - a)) (Icc 0 1) t
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
⊢ (b - a) / ↑N * ((f a + f b) / 2 + ∑ k ∈ Finset.range (N - 1), f (a + (↑k + 1) * (b - a) / ↑N)) =
    -((a - b) / ↑N) * ((f b + f a) / 2 + ∑ k ∈ Finset.range (N - 1), f (b + (↑k + 1) * (a - b) / ↑N))

Tactic:
neg_div',

Goal state after:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
⊢ (b - a) / ↑N * ((f a + f b) / 2 + ∑ k ∈ Finset.range (N - 1), f (a + (↑k + 1) * (b - a) / ↑N)) =
    -(a - b) / ↑N * ((f b + f a) / 2 + ∑ k ∈ Finset.range (N - 1), f (b + (↑k + 1) * (a - b) / ↑N))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
⊢ (b - a) / ↑N * ((f a + f b) / 2 + ∑ k ∈ Finset.range (N - 1), f (a + (↑k + 1) * (b - a) / ↑N)) =
    -(a - b) / ↑N * ((f b + f a) / 2 + ∑ k ∈ Finset.range (N - 1), f (b + (↑k + 1) * (a - b) / ↑N))

Tactic:
neg_sub,

Goal state after:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
⊢ (b - a) / ↑N * ((f a + f b) / 2 + ∑ k ∈ Finset.range (N - 1), f (a + (↑k + 1) * (b - a) / ↑N)) =
    (b - a) / ↑N * ((f b + f a) / 2 + ∑ k ∈ Finset.range (N - 1), f (b + (↑k + 1) * (a - b) / ↑N))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
h_f_int : IntervalIntegrable f volume a (a + ↑N * h)
k✝ : ℕ
hk✝ : k✝ < N
h_pos : 0 ≤ h
k : ℕ
hk : ↑k ≤ ↑N
⊢ a + ↑k * h ≤ a + ↑N * h

Tactic:
grw [hk]

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
⊢ |trapezoidal_error f 1 a b| ≤ ζ / 12 * (b - a) ^ 3

Tactic:
have h_ddg (y : ℝ) (hx : y ∈ Icc a b) : HasDerivWithinAt dg (ddg y) (Icc a b) y := by
    -- The eventual expression for g'' has several terms that cancel, which we have to undo here
    -- so that the various HasDerivWithinAt theorems will have everything they need.
    let dfaky := derivWithin f (Icc a b) y
    rw [(by ring : ddg y = (1 / 2) * dfaky + ((1 / 2) * dfaky + ddg y) - dfaky)]
    refine fun_sub (fun_add (const_mul _ (const_add _ (h_df y hx).hasDerivWithinAt))
      (fun_mul (div_const (sub_const _ (hasDerivWithinAt_id _ _)) _) ?_))
      (h_df y hx).hasDerivWithinAt
    rw [iteratedDerivWithin_eq_iterate]
    exact (h_ddf y hx).hasDerivWithinAt

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
⊢ |trapezoidal_error f 1 a b| ≤ ζ / 12 * (b - a) ^ 3
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: case inr.inr
f : ℝ → ℝ
a b : ℝ
h_df : DifferentiableOn ℝ f (Set.Icc b a)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc b a)) (Set.Icc b a)
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc b a) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_gt : b < a
⊢ |trapezoidal_error f N a b| ≤ (-(b - a)) ^ 3 * ζ / (12 * ↑N ^ 2)

Tactic:
neg_sub,

Goal state after:
case inr.inr
f : ℝ → ℝ
a b : ℝ
h_df : DifferentiableOn ℝ f (Set.Icc b a)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc b a)) (Set.Icc b a)
ζ : ℝ
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc b a) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h_gt : b < a
⊢ |trapezoidal_error f N a b| ≤ (a - b) ^ 3 * ζ / (12 * ↑N ^ 2)
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)
n : Fin N
hn : n ∈ Finset.univ
⊢ |a| + a + ε' * (↑↑n + 1) ≤ |a| + y n + ε'

Tactic:
← add_assoc,

Goal state after:
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)
n : Fin N
hn : n ∈ Finset.univ
⊢ |a| + a + ε' * (↑↑n + 1) ≤ |a| + a + ε' * (↑↑n + 1) + ε'
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ (∀ (x : X) (x_1 : Set X), IsClosed[inst✝] x_1ᶜ → x ∉ x_1ᶜ → ∃ f, Continuous[inst✝, _] f ∧ f x = 0 ∧ EqOn f 1 x_1ᶜ) =
    ?m.25

Tactic:
isClosed_compl_iff,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
⊢ (∀ (x : X) (x_1 : Set X), IsOpen[inst✝] x_1 → x ∉ x_1ᶜ → ∃ f, Continuous[inst✝, _] f ∧ f x = 0 ∧ EqOn f 1 x_1ᶜ) =
    ?m.25
Module: Mathlib.Topology.Separation.CompletelyRegular

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

Tactic:
← preimage_compl,

Goal state after:
case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
x : X
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
f : X → ↑I
hf : Continuous[inst✝¹, _] f
efx : f x = 0
hfU : f ⁻¹' {1}ᶜ ⊆ U
⊢ ∃ i, stoneCechUnit x ∈ i ∧ IsOpen i ∧ stoneCechUnit ⁻¹' i ⊆ U
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
⊢ levyProkhorovEDist μ ν = levyProkhorovEDist ν μ

Tactic:
simp only [levyProkhorovEDist, and_comm]

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
⊢ levyProkhorovEDist ν κ + (levyProkhorovEDist μ ν + ε) = levyProkhorovEDist μ ν + (levyProkhorovEDist ν κ + ε)

Tactic:
← add_assoc,

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 ν κ + levyProkhorovEDist μ ν + ε = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : 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}) + ε
⊢ IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) volume

Tactic:
apply Measure.integrableOn_of_bounded (M := μ.real univ) measure_Ioc_lt_top.ne

Goal state after:
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}) + ε
⊢ AEStronglyMeasurable (fun t ↦ μ.real {a | t ≤ f a}) volume

case f_bdd
Ω : 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}) + ε
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc 0 ‖f‖), ‖μ.real {a_1 | a ≤ f a_1}‖ ≤ μ.real univ
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
⊢ limsup (fun i ↦ ∫ (x : Ω), f x ∂↑(Ps i)) atTop ≤ ∫ (x : Ω), f x ∂↑P

Tactic:
by_cases f_zero : ‖f‖ = 0

Goal state after:
case pos
Ω : 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
⊢ limsup (fun i ↦ ∫ (x : Ω), f x ∂↑(Ps i)) atTop ≤ ∫ (x : Ω), f x ∂↑P

case neg
Ω : 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
⊢ limsup (fun i ↦ ∫ (x : Ω), f x ∂↑(Ps i)) atTop ≤ ∫ (x : Ω), f x ∂↑P