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
hmE : MeasurableSet (Ef ∪ Eg)
hfmE : μ (Ef ∪ Eg) < ∞
⊢ ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε

Tactic:
set E : Set α := Ef ∪ Eg

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 < ∞
⊢ ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
have hf := fun n => (haef n).stronglyMeasurable_mk

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
⊢ Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
G : Type u_5
inst✝² : FunLike G α β
inst✝¹ : ContinuousMapClass G α β
inst✝ : CompactSpace α
⊢ ∀ (f : G), HasCompactSupport ⇑f

Tactic:
intro f

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Zero β
inst✝³ : TopologicalSpace β
G : Type u_5
inst✝² : FunLike G α β
inst✝¹ : ContinuousMapClass G α β
inst✝ : CompactSpace α
f : G
⊢ HasCompactSupport ⇑f
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ HasCompactSupport (f₂.toContinuousMap - f₁.toContinuousMap).toFun

Tactic:
apply (f₁.hasCompactSupport'.union f₂.hasCompactSupport').of_isClosed_subset isClosed_closure

Goal state after:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ closure (Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun) ⊆ tsupport f₁.toFun ∪ tsupport f₂.toFun
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
ω : E → E →L[𝕜] F
hω : ∀ᶠ (z : E) in 𝓝 a, ContinuousAt ω z
⊢ ∀ᶠ (x : E) in 𝓝[univ] a, ContinuousWithinAt ω univ x

Tactic:
by simpa only [nhdsWithin_univ, continuousWithinAt_univ]

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

Goal state before:
pp: case a
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst✝³ : IsFiniteMeasureOnCompacts μ
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
⊢ ∀ (i : X → ℝ), Continuous i → HasCompactSupport i → EqOn i 1 k → 0 ≤ i → μ k ≤ ENNReal.ofReal (∫ (x : X), i x ∂μ)

Tactic:
intro f

Goal state after:
case a
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst✝³ : IsFiniteMeasureOnCompacts μ
inst✝² : μ.InnerRegularCompactLTTop
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
f : X → ℝ
⊢ Continuous f → HasCompactSupport f → EqOn f 1 k → 0 ≤ f → μ k ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)
Module: Mathlib.MeasureTheory.Integral.Regular

Goal state before:
pp: case a
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : NormalSpace X
⊢ ∀ (i : X → ℝ), Continuous i → EqOn i 0 Uᶜ → 0 ≤ i → i ≤ 1 → ENNReal.ofReal (∫ (x : X), i x ∂μ) ≤ μ U

Tactic:
intro f

Goal state after:
case a
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : NormalSpace X
f : X → ℝ
⊢ Continuous f → EqOn f 0 Uᶜ → 0 ≤ f → f ≤ 1 → ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ μ U
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

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

Tactic:
sum_range_succ,

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

Goal state before:
pp: 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) =
    ∑ i ∈ Finset.range (N + 1), trapezoidal_integral f 1 (a + ↑i * h) (a + (↑i + 1) * h)

Tactic:
sum_range_succ,

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) =
    ∑ x ∈ Finset.range N, trapezoidal_integral f 1 (a + ↑x * h) (a + (↑x + 1) * h) +
      trapezoidal_integral f 1 (a + ↑N * h) (a + (↑N + 1) * h)
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)
⊢ ∑ i ∈ Finset.range N, trapezoidal_error f 1 (a + ↑i * h) (a + (↑i + 1) * h) = trapezoidal_error f N a (a + ↑N * h)

Tactic:
by
  unfold trapezoidal_error
  rw [sum_sub_distrib, sum_trapezoidal_integral_adjacent_intervals N_nonzero]
  norm_cast
  rw [sum_integral_adjacent_intervals]
  · simp
  · intro k hk
    suffices ∀ {k : ℕ}, k ≤ N → a + k * h ∈ [[a, a + N * h]] from
      IntervalIntegrable.mono h_f_int (Set.uIcc_subset_uIcc (this hk.le) (this hk)) le_rfl
    rcases le_total h 0 with h_neg | h_pos <;> intro k hk <;> rw [← Nat.cast_le (α := ℝ)] at hk
    · simpa [Set.mem_uIcc] using .inr
        ⟨mul_le_mul_of_nonpos_right hk h_neg, mul_nonpos_of_nonneg_of_nonpos k.cast_nonneg h_neg⟩
    · exact Set.mem_uIcc_of_le (le_add_of_nonneg_right (by positivity)) (by 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| ≤ ζ
⊢ |trapezoidal_error f 1 a b| ≤ (b - a) ^ 3 * ζ / 12

Tactic:
rw [mul_div_assoc, mul_comm]

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| ≤ ζ
⊢ |trapezoidal_error f 1 a b| ≤ ζ / 12 * (b - a) ^ 3
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
μ ν : Measure X
inst✝¹ : μ.Regular
inst✝ : ν.Regular
hμν : ∀ (f : X →C_c ℝ≥0), ∫ (x : X), ↑(f x) ∂μ = ∫ (x : X), ↑(f x) ∂ν
⊢ ∀ (f : X →C_c ℝ), ∫ (x : X), f x ∂μ = ∫ (x : X), f x ∂ν

Tactic:
intro f

Goal state after:
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : T2Space X
inst✝⁴ : LocallyCompactSpace X
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
μ ν : Measure X
inst✝¹ : μ.Regular
inst✝ : ν.Regular
hμν : ∀ (f : X →C_c ℝ≥0), ∫ (x : X), ↑(f x) ∂μ = ∫ (x : X), ↑(f x) ∂ν
f : X →C_c ℝ
⊢ ∫ (x : X), f x ∂μ = ∫ (x : X), f x ∂ν
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∃ i, ∃ (_ : i < ω_ 1), t ∈ generateMeasurableRec s i

Tactic:
refine generateMeasurableRec_induction ?_ ?_ ?_ ?_ ht

Goal state after:
case refine_1
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∀ t ∈ s, ∃ i, ∃ (_ : i < ω_ 1), t ∈ generateMeasurableRec s i

case refine_2
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∃ i, ∃ (_ : i < ω_ 1), ∅ ∈ generateMeasurableRec s i

case refine_3
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ generateMeasurableRec s (ω_ 1)
⊢ ∀ (u : Set α),
    (∃ i, ∃ (_ : i < ω_ 1), u ∈ generateMeasurableRec s i) →
      (∃ j < ω_ 1, u ∈ generateMeasurableRec s j) → ∃ i, ∃ (_ : i < ω_ 1), uᶜ ∈ generateMeasurableRec s i

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
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:
intro f

Goal state after:
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
Module: Mathlib.MeasureTheory.MeasurableSpace.Card

Goal state before:
pp: α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ max (#↑s) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
⊢ Cardinal.lift.{u, v} i.card ≤ Cardinal.lift.{v, u} (max (#↑s) 2 ^ ℵ₀)

Tactic:
· rw [lift_power, lift_aleph0]
      rw [← Ordinal.lift_le.{u}, lift_omega, Ordinal.lift_one, ← ord_aleph] at hi
      have H := card_le_of_le_ord hi
      rw [← Ordinal.lift_card] at H
      apply H.trans <| aleph_one_le_continuum.trans <| power_le_power_right _
      rw [lift_max, Cardinal.lift_ofNat]
      exact le_max_right _ _

Goal state after:
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 →ᵇ ℝ) := ⋯
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
heq' : ∀ g ∈ A_toReal, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
⊢ ∀ (f : E →ᵇ ℝ), ∫ (x : E), f x ∂P = ∫ (x : E), f x ∂P'

Tactic:
intro f

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
heq' : ∀ g ∈ A_toReal, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
f : E →ᵇ ℝ
⊢ ∫ (x : E), f x ∂P = ∫ (x : E), f x ∂P'
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: W : Type u_1
inst✝¹¹ : AddCommGroup W
inst✝¹⁰ : Module ℝ W
inst✝⁹ : TopologicalSpace W
e : AddChar ℝ Circle
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module ℝ V
inst✝⁶ : PseudoEMetricSpace V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : CompleteSpace V
inst✝² : SecondCountableTopology V
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
he' : e ≠ 1
hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0
hL : Continuous fun p ↦ (L p.1) p.2
P P' : Measure V
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
h : ∀ (w : W), ∫ (v : V), (char he hL w) v ∂P = ∫ (v : V), (char he hL w) v ∂P'
⊢ P = P'

Tactic:
by
  apply ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable
      (separatesPoints_charPoly he he' hL hL')
  intro _ hg
  simp only [mem_charPoly] at hg
  obtain ⟨w, hw⟩ := hg
  rw [hw]
  have hsum (P : Measure V) [IsFiniteMeasure P] :
      ∫ v, w.coeff.sum (fun a z ↦ z * e (L v a)) ∂P =
        w.coeff.sum (fun a z ↦ ∫ v, z * e (L v a) ∂P) :=
    integral_finsetSum _ fun a ha ↦ ((char he hL a).integrable P).const_mul  _
  rw [hsum P, hsum P']
  apply Finset.sum_congr rfl fun i _ => ?_
  simp only [MeasureTheory.integral_const_mul, mul_eq_mul_left_iff]
  exact Or.inl (h i)

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

Goal state before:
pp: E : Type u_3
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : BorelSpace E
r t : E
⊢ charFun (Measure.map (fun x ↦ r + x) μ) t = charFun μ t * cexp (↑⟪r, t⟫ * I)

Tactic:
simp_rw [add_comm r]

Goal state after:
E : Type u_3
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : BorelSpace E
r t : E
⊢ charFun (Measure.map (fun x ↦ x + r) μ) t = charFun μ t * cexp (↑⟪r, t⟫ * I)
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
r : E
L : StrongDual ℝ E
⊢ charFunDual (Measure.map (fun x ↦ r + x) μ) L = charFunDual μ L * cexp (↑(L r) * I)

Tactic:
simp_rw [add_comm r]

Goal state after:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
r : E
L : StrongDual ℝ E
⊢ charFunDual (Measure.map (fun x ↦ x + r) μ) L = charFunDual μ L * cexp (↑(L r) * I)
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case calc_4
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, (|a| + y n + ε') * (μ.real (E n) + ε' / ↑N) - |a| * ∑ n, Λ (g n) ≤
    ∑ n, (|a| + y n + ε') * (μ.real (E n) + ε' / ↑N) - |a| * μ.real K

Tactic:
gcongr
    rw [← map_sum Λ g _]
    have h x : 0 ≤ (∑ n, g n) x := by simpa using Fintype.sum_nonneg fun n ↦ (hg.2.2.1 n x).1
    apply ENNReal.toReal_le_of_le_ofReal
    · exact Λ.map_nonneg (fun x ↦ h x)
    · have h' x (hx : x ∈ K) : (∑ n, g n) x = 1 := by simp [hg.2.1 hx]
      refine rieszMeasure_le_of_eq_one Λ h f.2 h'

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

Goal state before:
pp: ι : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
E : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
L : StrongDual ℝ ((i : ι) → E i)
⊢ ∫ (v : (i : ι) → E i), cexp ((∑ i, ↑((L ∘SL ContinuousLinearMap.single ℝ E i) (v i))) * I) ∂Measure.pi μ =
    ∏ i, ∫ (v : E i), cexp (↑((L ∘SL ContinuousLinearMap.single ℝ E i) v) * I) ∂μ i

Tactic:
Finset.sum_mul,

Goal state after:
ι : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
E : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
L : StrongDual ℝ ((i : ι) → E i)
⊢ ∫ (v : (i : ι) → E i), cexp (∑ i, ↑((L ∘SL ContinuousLinearMap.single ℝ E i) (v i)) * I) ∂Measure.pi μ =
    ∏ i, ∫ (v : E i), cexp (↑((L ∘SL ContinuousLinearMap.single ℝ E i) v) * I) ∂μ i
Module: Mathlib.MeasureTheory.Measure.DiracProba

Goal state before:
pp: X : Type u_2
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace.SeparatesPoints X
x y : X
x_eq_y : (fun x ↦ diracProba x) x = (fun x ↦ diracProba x) y
⊢ x = y

Tactic:
simpa [diracProba, dirac_eq_dirac_iff] using congr(ProbabilityMeasure.toMeasure $x_eq_y)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ (((↑μ).prod ↑ν) (univ ×ˢ univ)).toNNReal = (↑μ univ).toNNReal * (↑ν univ).toNNReal

Tactic:
← ENNReal.toNNReal_mul

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ (((↑μ).prod ↑ν) (univ ×ˢ univ)).toNNReal = (↑μ univ * ↑ν univ).toNNReal
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 : Ω →ᵇ ℝ), 0 ≤ f → limsup (fun i ↦ ∫ (x : Ω), f x ∂↑(Ps i)) atTop ≤ ∫ (x : Ω), f x ∂↑P

Tactic:
intro f

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
⊢ 0 ≤ f → limsup (fun i ↦ ∫ (x : Ω), f x ∂↑(Ps i)) atTop ≤ ∫ (x : Ω), f x ∂↑P
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
Λ : (E →C_c ℝ) → ℝ
h₀Λ : ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-↑C * ‖g.toBoundedContinuousFunction‖) (↑C * ‖g.toBoundedContinuousFunction‖)
hΛ : ∀ (g : E →C_c ℝ), Tendsto (fun μ ↦ ∫ (x : E), g x ∂↑μ) (↑f) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : μlim univ ≤ ENNReal.ofReal ↑C
μlim' : FiniteMeasure E := ⟨μlim, ⋯⟩
g : E →ᵇ ℝ
g' : E →C_c ℝ := { toFun := ⇑g, continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
⊢ Tendsto (fun i ↦ ∫ (x : E), g x ∂↑(id i)) (↑f) (𝓝 (∫ (x : E), g x ∂↑μlim'))

Tactic:
convert! hΛ g'

Goal state after:
case e'_5
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
Λ : (E →C_c ℝ) → ℝ
h₀Λ : ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-↑C * ‖g.toBoundedContinuousFunction‖) (↑C * ‖g.toBoundedContinuousFunction‖)
hΛ : ∀ (g : E →C_c ℝ), Tendsto (fun μ ↦ ∫ (x : E), g x ∂↑μ) (↑f) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : μlim univ ≤ ENNReal.ofReal ↑C
μlim' : FiniteMeasure E := ⟨μlim, ⋯⟩
g : E →ᵇ ℝ
g' : E →C_c ℝ := { toFun := ⇑g, continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
⊢ ∫ (x : E), g x ∂↑μlim' = Λ g'
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i, |x i| ^ p) ^ (1 / p)
hr : r ≤ 0
⊢ volume {x | (∑ i, |x i| ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Tactic:
have : {x : ι → ℝ | (∑ i, |x i| ^ p) ^ (1 / p) < r} = ∅ := by
      ext x
      refine ⟨fun hx => ?_, fun hx => hx.elim⟩
      exact not_le.mpr (lt_of_lt_of_le (Set.mem_ofPred.mp hx) hr) (h₂ x)

Goal state after:
case inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i, |x i| ^ p) ^ (1 / p)
hr : r ≤ 0
this : {x | (∑ i, |x i| ^ p) ^ (1 / p) < r} = ∅
⊢ volume {x | (∑ i, |x i| ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this✝ : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℂ), 0 ≤ ∑ i, ‖x i‖ ^ p
eq_norm : ∀ (x : ι → ℂ), ‖toLp (ENNReal.ofReal p) x‖ = (∑ i, ‖x i‖ ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
eq_zero : ∀ (x : ι → ℂ), (∑ i, ‖x i‖ ^ p) ^ (1 / p) = 0 ↔ x = 0
nm_zero : (∑ i, ‖0 i‖ ^ p) ^ (1 / p) = 0
nm_neg : ∀ (x : ι → ℂ), (∑ i, ‖(-x) i‖ ^ p) ^ (1 / p) = (∑ i, ‖x i‖ ^ p) ^ (1 / p)
nm_add : ∀ (x y : ι → ℂ), (∑ i, ‖(x + y) i‖ ^ p) ^ (1 / p) ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p) + (∑ i, ‖y i‖ ^ p) ^ (1 / p)
nm_smul : ∀ (r : ℝ) (x : ι → ℂ), (∑ i, ‖(r • x) i‖ ^ p) ^ (1 / p) ≤ ‖r‖ * (∑ i, ‖x i‖ ^ p) ^ (1 / p)
x✝ : ι → ℂ
⊢ 0 ≤ ∑ i, ‖x✝ i‖ ^ p

Tactic:
exact Finset.sum_nonneg' (fun _ => rpow_nonneg (norm_nonneg _) _)

Goal state after: