mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
⊢ -trapezoidal_integral f N b a - -∫ (x : ℝ) in b..a, f x = -(trapezoidal_integral f N b a - ∫ (x : ℝ) in b..a, f x)

Tactic:
neg_sub_neg,

Goal state after:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
⊢ (∫ (x : ℝ) in b..a, f x) - trapezoidal_integral f N b a = -(trapezoidal_integral f N b a - ∫ (x : ℝ) in b..a, f x)
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) + ∑ x ∈ Finset.range (N - 1), f (a + (↑x + 1) * h) +
        (f (a + ↑0 * 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))

Tactic:
← sum_add_distrib,

Goal state after:
f : ℝ → ℝ
N : ℕ
a h : ℝ
N_nonzero : 0 < N
⊢ h / 2 *
      (∑ x ∈ Finset.range (N - 1), (f (a + ↑(x + 1) * h) + f (a + (↑x + 1) * h)) +
        (f (a + ↑0 * 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.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)
n : Fin N
⊢ E n ⊆ tsupport ⇑f

Tactic:
rw [hE.1]

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)
n : Fin N
⊢ E n ⊆ ⋃ j, E j
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
hint : MemLp id 2 (Measure.map X P)
t : ℝ
⊢ taylorWithinEval (charFun (Measure.map X P)) 2 univ 0 t =
    1 + ↑(∫ (x : Ω), X x ∂P) * ↑t * I - ↑(∫ (x : Ω), (X ^ 2) x ∂P) * ↑t ^ 2 / 2

Tactic:
have : IsProbabilityMeasure (P.map X) := Measure.isProbabilityMeasure_map hX

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
hint : MemLp id 2 (Measure.map X P)
t : ℝ
this : IsProbabilityMeasure (Measure.map X P)
⊢ taylorWithinEval (charFun (Measure.map X P)) 2 univ 0 t =
    1 + ↑(∫ (x : Ω), X x ∂P) * ↑t * I - ↑(∫ (x : Ω), (X ^ 2) x ∂P) * ↑t ^ 2 / 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)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
⊢ μ (tsupport ⇑f) = ∑ i, μ (E i)

Tactic:
rw [hE.1]

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)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
⊢ μ (⋃ j, E j) = ∑ i, μ (E i)
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ : Measure Ω
⊢ levyProkhorovEDist μ μ ≤ sInf (Ioo 0 ∞)

Tactic:
refine sInf_le_sInf fun ε ⟨hε₀, hε_top⟩ B _ ↦ and_self_iff.2 ?_

Goal state after:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ : Measure Ω
ε : ℝ≥0∞
x✝¹ : ε ∈ Ioo 0 ∞
B : Set Ω
x✝ : MeasurableSet B
hε₀ : 0 < ε
hε_top : ε < ∞
⊢ μ B ≤ μ (thickening ε.toReal B) + ε
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 s.toReal B) + s ≤ μ (thickening r.toReal (thickening s.toReal B)) + r + s

Tactic:
by
      grw [right_measure_le_of_levyProkhorovEDist_lt lt_r isOpen_thickening.measurableSet]

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
inst✝¹ : CompactSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := fun g ↦ ∫ (x : X), g x ∂μ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
g : X →ᵇ ℝ
g' : X →C_c ℝ := { toFun := ⇑g, continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
⊢ ∫ (x : X), g x ∂μ = ∫ (x : X), g x ∂rieszMeasure Λ

Tactic:
exact (integral_rieszMeasure Λ g').symm

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

Goal state before:
pp: α : Type u_1
inst✝⁹ : MeasurableSpace α
β : Type u_2
inst✝⁸ : MeasurableSpace β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : SecondCountableTopology β
inst✝³ : PseudoMetrizableSpace α
inst✝² : PseudoMetrizableSpace β
inst✝¹ : OpensMeasurableSpace α
inst✝ : OpensMeasurableSpace β
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace] fun μ ↦ μ.1.prod μ.2

Tactic:
by
  refine continuous_iff_continuousAt.2 (fun μ ↦ ?_)
  /- It suffices to check the convergence along elements of a π-system containing arbitrarily
  small neighborhoods of any point, by `tendsto_probabilityMeasure_of_tendsto_of_mem`.
  We take as a π-system the sets of the form `a ×ˢ b` where `a` and `b` have null frontier. -/
  let S : Set (Set (α × β)) := {t | ∃ (a : Set α) (b : Set β),
    MeasurableSet a ∧ μ.1 (frontier a) = 0 ∧ MeasurableSet b ∧ μ.2 (frontier b) = 0
    ∧ t = a ×ˢ b}
  have : IsPiSystem S := by
    rintro - ⟨a, b, ameas, ha, bmeas, hb, rfl⟩ - ⟨a', b', a'meas, ha', b'meas, hb', rfl⟩ -
    refine ⟨a ∩ a', b ∩ b', ameas.inter a'meas, ?_, bmeas.inter b'meas, ?_, prod_inter_prod⟩
    · rw [null_iff_toMeasure_null] at ha ha' ⊢
      exact null_frontier_inter ha ha'
    · rw [null_iff_toMeasure_null] at hb hb' ⊢
      exact null_frontier_inter hb hb'
  apply this.tendsto_probabilityMeasure_of_tendsto_of_mem
  · rintro s ⟨a, b, ameas, -, bmeas, -, rfl⟩
    exact ameas.prod bmeas
  · let : PseudoMetricSpace α := TopologicalSpace.pseudoMetrizableSpacePseudoMetric α
    let : PseudoMetricSpace β := TopologicalSpace.pseudoMetrizableSpacePseudoMetric β
    intro u u_open x xu
    obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, ball x ε ⊆ u := Metric.isOpen_iff.1 u_open x xu
    rcases exists_null_frontier_thickening (μ.1 : Measure α) {x.1} εpos with ⟨r, hr, μr⟩
    rcases exists_null_frontier_thickening (μ.2 : Measure β) {x.2} εpos with ⟨r', hr', μr'⟩
    simp only [thickening_singleton] at μr μr'
    refine ⟨ball x.1 r ×ˢ ball x.2 r', ⟨ball x.1 r, ball x.2 r', measurableSet_ball,
      by simp [coeFn_def, μr], measurableSet_ball, by simp [coeFn_def, μr'], rfl⟩, ?_, ?_⟩
    · exact (isOpen_ball.prod isOpen_ball).mem_nhds (by simp [hr.1, hr'.1])
    · calc ball x.1 r ×ˢ ball x.2 r'
      _ ⊆ ball x.1 ε ×ˢ ball x.2 ε := by gcongr; exacts [hr.2.le, hr'.2.le]
      _ ⊆ _ := by rwa [ball_prod_same]
  · rintro s ⟨a, b, ameas, ha, bmeas, hb, rfl⟩
    simp only [prod_prod]
    apply Filter.Tendsto.mul
    · exact tendsto_measure_of_null_frontier_of_tendsto tendsto_id.fst_nhds ha
    · exact tendsto_measure_of_null_frontier_of_tendsto tendsto_id.snd_nhds hb

Goal state after:
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
φ : G ≃ₜ* G
⊢ (mulEquivHaarChar φ)⁻¹ = mulEquivHaarChar φ.symm

Tactic:
apply inv_eq_of_mul_eq_one_right

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
φ : G ≃ₜ* G
⊢ mulEquivHaarChar φ * mulEquivHaarChar φ.symm = 1
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
⊢ ∀ (x : ProbabilityMeasure Ω), ContinuousAt ofMeasure x

Tactic:
intro P

Goal state after:
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
P : ProbabilityMeasure Ω
⊢ ContinuousAt ofMeasure P
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

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

Tactic:
rw [ENNReal.ofReal_le_iff_le_toReal (ENNReal.mul_lt_top hC ht).ne, ENNReal.toReal_mul,
        ← Measure.real_def, ← smul_eq_mul, ← integral_const]

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

Goal state before:
pp: μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
⊢ ∫ (x : ℝ), 2 * ↑r * ↑(sinc (r * x)) ∂μ = 2 * ↑r * ↑(∫ (x : ℝ), sinc (r * x) ∂μ)

Tactic:
norm_cast
    rw [← integral_const_mul]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: E : Type u_1
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : BorelSpace E
inst✝² : T2Space E
inst✝¹ : ContinuousSMul ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p✝ : ℝ
hp : 0 < p✝
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this✝³ : NormedAddCommGroup F := p.toNormedAddCommGroup
this✝² : NormedSpace ℝ F := { toModule := inst✝⁶, norm_smul_le := ⋯ }
this✝¹ : TopologicalSpace F := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
this✝ : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv
⊢ μ {x | g x < 1} = ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p✝) ∂μ) / Real.Gamma (↑(finrank ℝ E) / p✝ + 1))

Tactic:
let ν : Measure F := @Measure.map E F mE _ φ μ

Goal state after:
E : Type u_1
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : BorelSpace E
inst✝² : T2Space E
inst✝¹ : ContinuousSMul ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p✝ : ℝ
hp : 0 < p✝
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this✝³ : NormedAddCommGroup F := p.toNormedAddCommGroup
this✝² : NormedSpace ℝ F := { toModule := inst✝⁶, norm_smul_le := ⋯ }
this✝¹ : TopologicalSpace F := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
this✝ : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv
ν : Measure F := map (⇑φ) μ
⊢ μ {x | g x < 1} = ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p✝) ∂μ) / Real.Gamma (↑(finrank ℝ E) / p✝ + 1))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: E : Type u_1
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
inst✝⁶ : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : BorelSpace E
inst✝³ : T2Space E
inst✝² : ContinuousSMul ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
inst✝ : Nontrivial E
r : ℝ
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this✝³ : NormedAddCommGroup F := p.toNormedAddCommGroup
this✝² : NormedSpace ℝ F := { toModule := inst✝⁷, norm_smul_le := ⋯ }
this✝¹ : TopologicalSpace F := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
this✝ : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv
⊢ μ {x | g x ≤ r} = μ {x | g x < r}

Tactic:
let ν : Measure F := @Measure.map E F mE _ φ μ

Goal state after:
E : Type u_1
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
inst✝⁶ : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst✝⁵ : IsTopologicalAddGroup E
inst✝⁴ : BorelSpace E
inst✝³ : T2Space E
inst✝² : ContinuousSMul ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
inst✝ : Nontrivial E
r : ℝ
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this✝³ : NormedAddCommGroup F := p.toNormedAddCommGroup
this✝² : NormedSpace ℝ F := { toModule := inst✝⁷, norm_smul_le := ⋯ }
this✝¹ : TopologicalSpace F := PseudoMetricSpace.toUniformSpace.toTopologicalSpace
this✝ : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv
ν : Measure F := map (⇑φ) μ
⊢ μ {x | g x ≤ r} = μ {x | g x < r}
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
g : E →C_c ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ μ ∈
    (fun μ ↦ ∫ (x : E), g x ∂↑μ) ⁻¹'
      Icc (-(↑C * ‖g.toBoundedContinuousFunction‖)) (↑C * ‖g.toBoundedContinuousFunction‖)

Tactic:
simp only [mem_preimage, mem_Icc]

Goal state after:
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
g : E →C_c ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ -(↑C * ‖g.toBoundedContinuousFunction‖) ≤ ∫ (x : E), g x ∂↑μ ∧
    ∫ (x : E), g x ∂↑μ ≤ ↑C * ‖g.toBoundedContinuousFunction‖
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case h₁
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ ↑μ (Subtype.val '' Subtype.val ⁻¹' s) = ↑μ s

pp: case h₁.hf
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ ∀ (s : Set { x // x ∈ K }), MeasurableSet s → MeasurableSet (Subtype.val '' s)

pp: case h₁.hs
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ MeasurableSet (Subtype.val ⁻¹' s)

Tactic:
image_preimage_eq_inter_range

Goal state after:
case h₁
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ ↑μ (s ∩ range Subtype.val) = ↑μ s

case h₁.hf
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ ∀ (s : Set { x // x ∈ K }), MeasurableSet s → MeasurableSet (Subtype.val '' s)

case h₁.hs
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : ↑K → E := Subtype.val
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := fun μ ↦ μ.map f
T : Set (FiniteMeasure ↑K) := {μ | μ.mass ≤ C}
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ MeasurableSet (Subtype.val ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 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))

Tactic:
have h₁ : 0 < p := by linarith
  have : (ENNReal.ofReal p).toReal = p := toReal_ofReal (le_of_lt h₁)
  -- We collect facts about `Lp` norms that will be used in `measure_le_one_eq_lt_one`
  have eq_norm (x : ι → ℝ) : ‖toLp (.ofReal p) x‖ = (∑ i, |x i| ^ p) ^ (1 / p) := by
    simp [PiLp.norm_eq_sum (f := toLp (.ofReal p) x) (this.symm ▸ h₁), this]
  have : Fact (1 ≤ ENNReal.ofReal p) := fact_iff.mpr (ofReal_one ▸ (ofReal_le_ofReal hp))
  have nm_zero : ‖toLp (.ofReal p) (0 : ι → ℝ)‖ = 0 := norm_zero
  have eq_zero (x : ι → ℝ) : ‖toLp (.ofReal p) x‖ = 0 ↔ x = 0 :=
    norm_eq_zero.trans (toLp_eq_zero _)
  have nm_neg := fun x : ι → ℝ => norm_neg (toLp (.ofReal p) x)
  have nm_add := fun x y : ι → ℝ => norm_add_le (toLp (.ofReal p) x) (toLp (.ofReal p) y)
  have nm_smul := fun (r : ℝ) (x : ι → ℝ) =>
    norm_smul_le (β := PiLp (.ofReal p) (fun _ : ι => ℝ)) r (toLp (.ofReal p) x)
  simp_rw [← toLp_neg, ← toLp_add, ← toLp_smul, eq_norm,
    norm_eq_abs] at eq_zero nm_zero nm_neg nm_add nm_smul
  rw [measure_le_eq_lt _ nm_zero (fun x ↦ nm_neg x) (fun x y ↦ nm_add x y) (eq_zero _).mp
    (fun r x => nm_smul r x), volume_sum_rpow_lt _ hp]

Goal state after: