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

Goal state before:
pp: case pos.inr
α : 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 : Tendsto (fun n ↦ eLpNorm (f n - g) p (μ.restrict E)) atTop (𝓝 0)
⊢ ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε

Tactic:
rw [ENNReal.tendsto_atTop_zero] at hInner

Goal state after:
case pos.inr
α : 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, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
Module: Mathlib.MeasureTheory.Integral.CircleTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
⊢ ∫ (θ : ℝ) in 0..2 * π, (2 * ↑π * I)⁻¹ • deriv (circleMap z R) θ • (circleMap z R θ - w)⁻¹ • f (circleMap z R θ) =
    (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(z, R), (z - w)⁻¹ • f z

Tactic:
circleIntegral,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
z w : ℂ
f : ℂ → E
⊢ ∫ (θ : ℝ) in 0..2 * π, (2 * ↑π * I)⁻¹ • deriv (circleMap z R) θ • (circleMap z R θ - w)⁻¹ • f (circleMap z R θ) =
    (2 * ↑π * I)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, deriv (circleMap z R) θ • (circleMap z R θ - w)⁻¹ • f (circleMap z R θ)
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
x : α
inst✝ : Zero β
⊢ HasCompactSupport ⇑0

Tactic:
by simp [HasCompactSupport, tsupport]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : TopologicalSpace α
δ : Type u_5
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : Zero δ
f : γ →C_c δ
g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ HasCompactSupport ((↑f).comp ↑g).toFun

Tactic:
by
    apply IsCompact.of_isClosed_subset (g.isCompact_preimage_of_isClosed f.2 (isClosed_tsupport _))
      (isClosed_tsupport (f ∘ g))
    intro x hx
    rw [tsupport, Set.mem_preimage, _root_.mem_closure_iff]
    intro o ho hgxo
    rw [tsupport, _root_.mem_closure_iff] at hx
    obtain ⟨y, hy⟩ := hx (g ⁻¹' o) (IsOpen.preimage g.1.2 ho) hgxo
    exact ⟨g y, hy⟩

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

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

Tactic:
by
      rw [_root_.integral_rpow_mul_exp_neg_rpow (by linarith) (by linarith), add_assoc,
        one_add_one_eq_two]
      ring

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t

Tactic:
wlog hE : CompleteSpace E generalizing E

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E},
    ContinuousOn f (Icc a b) →
      DifferentiableOn ℝ f (Ioo a b) →
        (∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) → CompleteSpace E → ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
hE : ¬CompleteSpace E
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t

E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
f✝ : ℝ → E✝
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hBi : IntervalIntegrable B volume a b
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hE : CompleteSpace E
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
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) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
⊢ ‖∫ᶜ (x : E) in Path.segment a b, (ω x - ω a)‖ ≤ ε * ‖b - a‖

Tactic:
refine norm_curveIntegral_segment_le fun z hz ↦ ?_

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) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
z : E
hz : z ∈ [a -[ℝ] b]
⊢ ‖ω z - ω a‖ ≤ ε
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a b c d : E
γ₁ : Path a b
γ₂ : Path c d
s : Set (↑I × ↑I)
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : (↑γ₁).Homotopy ↑γ₂
hs : s.Countable
hφt : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, φ (a_1, b_1) ∈ t
hω : ∀ a_1 ∈ Ioo 0 1, ∀ b_1 ∈ Ioo 0 1, (a_1, b_1) ∉ s → HasFDerivWithinAt ω (dω (φ (a_1, b_1))) t (φ (a_1, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ a_1 ∈ Ioo 0 1,
    ∀ b_1 ∈ Ioo 0 1,
      (a_1, b_1) ∉ s →
        ∀ u ∈ tangentConeAt ℝ t (φ (a_1, b_1)),
          ∀ v ∈ tangentConeAt ℝ t (φ (a_1, b_1)), ((dω (φ (a_1, b_1))) u) v = ((dω (φ (a_1, b_1))) v) u
U : Set (ℝ × ℝ) := Ioo 0 1 ×ˢ Ioo 0 1
hU : U = Ioo 0 1 ×ˢ Ioo 0 1
hinterior : interior (Icc 0 1) = U
hunique : UniqueDiffOn ℝ (Icc 0 1)
hUopen : IsOpen U
hU_subset : U ⊆ Icc 0 1
hclosure : closure U = Icc 0 1
ψ : ℝ × ℝ → E := fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hcontdiff : ContDiffOn ℝ 2 ψ (Icc 0 1)
hψ : ψ = fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hψφ : ∀ (a_1 b_1 : ↑I), ψ (↑a_1, ↑b_1) = φ (a_1, b_1)
hψ_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ψ
⊢ MapsTo ψ U t

Tactic:
rintro ⟨a, b⟩ ⟨ha, hb⟩

Goal state after:
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
a✝ b✝ c d : E
γ₁ : Path a✝ b✝
γ₂ : Path c d
s : Set (↑I × ↑I)
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : (↑γ₁).Homotopy ↑γ₂
hs : s.Countable
hφt : ∀ a ∈ Ioo 0 1, ∀ b ∈ Ioo 0 1, φ (a, b) ∈ t
hω : ∀ a ∈ Ioo 0 1, ∀ b ∈ Ioo 0 1, (a, b) ∉ s → HasFDerivWithinAt ω (dω (φ (a, b))) t (φ (a, b))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ a ∈ Ioo 0 1,
    ∀ b ∈ Ioo 0 1,
      (a, b) ∉ s →
        ∀ u ∈ tangentConeAt ℝ t (φ (a, b)),
          ∀ v ∈ tangentConeAt ℝ t (φ (a, b)), ((dω (φ (a, b))) u) v = ((dω (φ (a, b))) v) u
U : Set (ℝ × ℝ) := Ioo 0 1 ×ˢ Ioo 0 1
hU : U = Ioo 0 1 ×ˢ Ioo 0 1
hinterior : interior (Icc 0 1) = U
hunique : UniqueDiffOn ℝ (Icc 0 1)
hUopen : IsOpen U
hU_subset : U ⊆ Icc 0 1
hclosure : closure U = Icc 0 1
ψ : ℝ × ℝ → E := fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hcontdiff : ContDiffOn ℝ 2 ψ (Icc 0 1)
hψ : ψ = fun xy ↦ Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2
hψφ : ∀ (a b : ↑I), ψ (↑a, ↑b) = φ (a, b)
hψ_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ψ
a b : ℝ
ha : (a, b).1 ∈ Ioo 0 1
hb : (a, b).2 ∈ Ioo 0 1
⊢ ψ (a, b) ∈ t
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ trapezoidal_integral f N a (a + ↑N * h) + trapezoidal_integral f 1 (a + ↑N * h) (a + ↑(N + 1) * h) =
    trapezoidal_integral f (N + 1) a (a + ↑(N + 1) * h)

Tactic:
← sum_trapezoidal_integral_adjacent_intervals N_nonzero,

Goal state after:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ ∑ i ∈ Finset.range N, trapezoidal_integral f 1 (a + ↑i * h) (a + (↑i + 1) * h) +
      trapezoidal_integral f 1 (a + ↑N * h) (a + ↑(N + 1) * h) =
    trapezoidal_integral f (N + 1) a (a + ↑(N + 1) * h)
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint ↑K₁ ↑K₂
b : ℝ≥0
⊢ b ∈ ⇑Λ '' {f | ∀ x ∈ K₁ ⊔ K₂, 1 ≤ f x} → rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ b

Tactic:
⟨f, ⟨hf, Λf_eq_b⟩⟩

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint ↑K₁ ↑K₂
b : ℝ≥0
f : X →C_c ℝ≥0
hf : f ∈ {f | ∀ x ∈ K₁ ⊔ K₂, 1 ≤ f x}
Λf_eq_b : Λ f = b
⊢ rieszContentAux Λ K₁ + rieszContentAux Λ K₂ ≤ b
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint ↑K₁ ↑K₂
b : ℝ≥0
f : X →C_c ℝ≥0
hf : f ∈ {f | ∀ x ∈ K₁ ⊔ K₂, 1 ≤ f x}
Λf_eq_b : Λ f = b
hsuppf : ∀ x ∈ K₁ ⊔ K₂, x ∈ support ⇑f
hsubsuppf : ↑K₁ ∪ ↑K₂ ⊆ tsupport ⇑f
g₁ g₂ : X →C_c ℝ≥0
hg₁ : EqOn (⇑g₁) 1 K₁.carrier
hg₂ : EqOn (⇑g₂) 1 K₂.carrier
sum_g : EqOn (⇑(g₁ + g₂)) 1 (tsupport f.toFun)
f_eq_sum : f = g₁ * f + g₂ * f
aux₁ : ∀ x ∈ K₁, 1 ≤ (g₁ * f) x
x : X
x_in_K₂ : x ∈ K₂
⊢ 1 ≤ (g₂ * f) x

Tactic:
simp [hg₂ x_in_K₂, hf x (mem_union_right _ x_in_K₂)]

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 ℝ
hf : ∀ (x : X), 0 ≤ f x ∧ f x ≤ 1
V : Set X
hV : tsupport ⇑f ⊆ V
this :
  (rieszContent (toNNRealLinear Λ)).measure ↑{ carrier := tsupport ⇑f, isCompact' := ⋯ } =
    (rieszContent (toNNRealLinear Λ)) { carrier := tsupport ⇑f, isCompact' := ⋯ }
⊢ ENNReal.ofReal (Λ f) ≤ (rieszMeasure Λ) (tsupport ⇑f)

Tactic:
rw [← Compacts.coe_mk (tsupport f) f.hasCompactSupport, rieszMeasure, this, rieszContent,
    ENNReal.ofReal_eq_coe_nnreal (Λ.map_nonneg fun x ↦ (hf x).1), Content.mk_apply,
    ENNReal.coe_le_coe]

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 ℝ
hf : ∀ (x : X), 0 ≤ f x ∧ f x ≤ 1
V : Set X
hV : tsupport ⇑f ⊆ V
this :
  (rieszContent (toNNRealLinear Λ)).measure ↑{ carrier := tsupport ⇑f, isCompact' := ⋯ } =
    (rieszContent (toNNRealLinear Λ)) { carrier := tsupport ⇑f, isCompact' := ⋯ }
⊢ NNReal.mk (Λ f) ⋯ ≤ rieszContentAux (toNNRealLinear Λ) { carrier := tsupport ⇑f, isCompact' := ⋯ }
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
⊢ |trapezoidal_error f N a b| ≤ (b - a) ^ 3 * ζ / (12 * ↑N ^ 2)

Tactic:
by
  let h := (b - a) / N
  let ak (k : ℕ) := a + k * h
  have h0 : ∀ k : ℕ, ak (k + 1) - ak k = h := by simp [ak, ← sub_mul]
  have hab : 0 < b - a := sub_pos.mpr a_lt_b
  have hpos : 0 < h := by positivity
  have hb : b = a + N * h := by field
  rw [hb, ← sum_trapezoidal_error_adjacent_intervals N_nonzero
    (hb ▸ h_df.continuousOn.intervalIntegrable_of_Icc a_lt_b.le)]
  grw [abs_sum_le_sum_abs]
  suffices ∀ k ∈ range N, |trapezoidal_error f 1 (ak k) (ak (k + 1))| ≤ (ζ / 12) * h ^ 3 by
    norm_cast
    calc
      _ ≤ ∑ k ∈ range N, ζ / 12 * h ^ 3 := sum_le_sum this
      _ = N * (ζ / 12 * h ^ 3)          := by simp [sum_const]
      _ = _                             := by push_cast; field
  intro k hk
  rw [Finset.mem_range] at hk
  have h1 : a ≤ ak k := by simp only [ak, le_add_iff_nonneg_right]; positivity
  have h2 : ak (k + 1) ≤ b := by simp only [ak, hb]; grw [Nat.lt_iff_add_one_le.mp hk]
  have h3 : Icc (ak k) (ak (k + 1)) ⊆ Icc a b := Icc_subset_Icc h1 h2
  have h4 : ak k < ak (k + 1) := by rwa [← sub_pos, h0]
  have h5 : EqOn (derivWithin f (Icc a b))
      (derivWithin f (Icc (ak k) (ak (k + 1)))) (Icc (ak k) (ak (k + 1))) := by
    intro x hx
    rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_df x (h3 hx))]
  have h6 : EqOn (iteratedDerivWithin 2 f (Icc a b))
    (iteratedDerivWithin 2 f (Icc (ak k) (ak (k + 1)))) (Icc (ak k) (ak (k + 1))) := by
    intro x hx
    simp only [iteratedDerivWithin_succ', iteratedDerivWithin_zero]
    rw [← derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_ddf x (h3 hx))]
    exact derivWithin_congr h5 (h5 hx)
  have h7 (x : ℝ) : |iteratedDerivWithin 2 f (Set.Icc (ak k) (ak (k + 1))) x| ≤ ζ := by
    by_cases hx : x ∈ Icc (ak k) (ak (k + 1))
    · grw [← h6 hx, fpp_bound]
    · rw [iteratedDerivWithin_succ, derivWithin_zero_of_notMem_closure
        (by rwa [closure_Icc]), abs_zero]
      exact (abs_nonneg _).trans (fpp_bound 0)
  refine (trapezoidal_error_le_of_lt' (ζ := ζ) h4 (h_df.mono h3) ?_ h7).trans_eq ?_
  · refine h_ddf.congr_mono (fun x hx ↦ ?_) h3
    exact derivWithin_subset h3 (uniqueDiffOn_Icc h4 x hx) (h_df x (h3 hx))
  · rw [h0, mul_div_assoc, mul_comm]

Goal state after:
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
⊢ ∫ (x : X), ↑(f x) ∂rieszMeasure Λ = (toRealPositiveLinear Λ) f.toReal

Tactic:
← RealRMK.integral_rieszMeasure (toRealPositiveLinear Λ) f.toReal

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
⊢ ∫ (x : X), ↑(f x) ∂rieszMeasure Λ = ∫ (x : X), f.toReal x ∂RealRMK.rieszMeasure (toRealPositiveLinear Λ)
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; simp

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (⇑(MeasurableEquiv.funUnique (Fin 1) ℝ).symm ⁻¹' Icc 0 fun x ↦ 2 * π) = Icc 0 (2 * π)
H₂ : torusMap c R = fun θ x ↦ circleMap (c 0) (R 0) (θ 0)
⊢ ∫ (θ : Fin 1 → ℝ) in Icc 0 fun x ↦ 2 * π, (∏ i, ↑(R i) * cexp (↑(θ i) * I) * I) • f (torusMap c R θ) =
    ∮ (z : ℂ) in C(c 0, R 0), f fun x ↦ z

Tactic:
circleIntegral,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin 1 → ℂ) → E
c : Fin 1 → ℂ
R : Fin 1 → ℝ
H₁ : (⇑(MeasurableEquiv.funUnique (Fin 1) ℝ).symm ⁻¹' Icc 0 fun x ↦ 2 * π) = Icc 0 (2 * π)
H₂ : torusMap c R = fun θ x ↦ circleMap (c 0) (R 0) (θ 0)
⊢ ∫ (θ : Fin 1 → ℝ) in Icc 0 fun x ↦ 2 * π, (∏ i, ↑(R i) * cexp (↑(θ i) * I) * I) • f (torusMap c R θ) =
    ∫ (θ : ℝ) in 0..2 * π, deriv (circleMap (c 0) (R 0)) θ • f fun x ↦ circleMap (c 0) (R 0) θ
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: case refine_4
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
f : ℕ → Set α
⊢ (∀ (n : ℕ), (∃ i, ∃ (_ : i < ω_ 1), f n ∈ generateMeasurableRec s i) ∧ ∃ j < ω_ 1, f n ∈ generateMeasurableRec s j) →
    ∃ i, ∃ (_ : i < ω_ 1), ⋃ n, f n ∈ generateMeasurableRec s i

Tactic:
H

Goal state after:
case refine_4
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
f : ℕ → Set α
H : ∀ (n : ℕ), (∃ i, ∃ (_ : i < ω_ 1), f n ∈ generateMeasurableRec s i) ∧ ∃ j < ω_ 1, f n ∈ generateMeasurableRec s j
⊢ ∃ i, ∃ (_ : i < ω_ 1), ⋃ n, f n ∈ generateMeasurableRec s i
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst✝¹] s
f : X → ↑I
hf : Continuous[inst✝¹, _] f ∧ f x = 0 ∧ EqOn f 1 sᶜ
⊢ ∃ v ∈ {s | IsClopen s}, x ∈ v ∧ v ⊆ s

Tactic:
obtain ⟨hfc, hf₀, hf₁⟩ := hf

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst✝¹] s
f : X → ↑I
hfc : Continuous[inst✝¹, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
⊢ ∃ v ∈ {s | IsClopen s}, x ∈ v ∧ v ⊆ s
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
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
⊢ ν (thickening r.toReal B) + r ≤ κ (thickening s.toReal (thickening r.toReal B)) + s + r

Tactic:
grw [left_measure_le_of_levyProkhorovEDist_lt lt_s isOpen_thickening.measurableSet]

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
⊢ Tendsto (toMeasure ∘ μs) atTop (𝓝 P)

Tactic:
set Ps := LevyProkhorov.toMeasure ∘ μs

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
⊢ Tendsto Ps atTop (𝓝 P)
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: 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

Tactic:
have norm_f_pos : 0 < ‖f‖ := lt_of_le_of_ne (norm_nonneg _) (fun a => f_zero a.symm)

Goal state after:
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
norm_f_pos : 0 < ‖f‖
⊢ limsup (fun i ↦ ∫ (x : Ω), f x ∂↑(Ps i)) atTop ≤ ∫ (x : Ω), f x ∂↑P
Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

Goal state before:
pp: G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
φ : G ≃ₜ* G
smul : haar = haar.haarScalarFactor μ • μ
⊢ haar.haarScalarFactor (map (⇑φ) haar) = μ.haarScalarFactor (map (⇑φ) μ)

Tactic:
conv =>
    enter [1, 1]
    rw [smul]

Goal state after:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
φ : G ≃ₜ* G
smul : haar = haar.haarScalarFactor μ • μ
⊢ (haar.haarScalarFactor μ • μ).haarScalarFactor (map (⇑φ) haar) = μ.haarScalarFactor (map (⇑φ) μ)
Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

Goal state before:
pp: G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
φ : G ≃ₜ* G
⊢ mulEquivHaarChar φ • μ = comap (⇑φ) μ

Tactic:
let e := φ.toHomeomorph.toMeasurableEquiv

Goal state after:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
⊢ mulEquivHaarChar φ • μ = comap (⇑φ) μ
Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

Goal state before:
pp: G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
f : G → ℝ
φ : G ≃ₜ* G
⊢ ∫ (a : G), f a ∂comap (⇑φ) μ = mulEquivHaarChar φ • ∫ (a : G), f a ∂μ

Tactic:
let e := φ.toHomeomorph.toMeasurableEquiv

Goal state after:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
f : G → ℝ
φ : G ≃ₜ* G
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
⊢ ∫ (a : G), f a ∂comap (⇑φ) μ = mulEquivHaarChar φ • ∫ (a : G), f a ∂μ