mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: p : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ p)
ι : 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 ℝ (PiLp p E)
⊢ ∫ (v : WithLp p ((i : ι) → E i)), cexp (↑(L v) * I) ∂Measure.map (toLp p) (Measure.pi μ) =
    ∫ (x : (i : ι) → E i),
      cexp
        ((∑ i, ↑((L ∘SL ↑(PiLp.continuousLinearEquiv p ℝ E).symm ∘SL ContinuousLinearMap.single ℝ E i) (x i))) *
          I) ∂Measure.pi μ

Tactic:
← ofReal_sum,

Goal state after:
p : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ p)
ι : 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 ℝ (PiLp p E)
⊢ ∫ (v : WithLp p ((i : ι) → E i)), cexp (↑(L v) * I) ∂Measure.map (toLp p) (Measure.pi μ) =
    ∫ (x : (i : ι) → E i),
      cexp
        (↑(∑ i, (L ∘SL ↑(PiLp.continuousLinearEquiv p ℝ E).symm ∘SL ContinuousLinearMap.single ℝ E i) (x i)) *
          I) ∂Measure.pi μ
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

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

Tactic:
simp_rw [mul_add, this]

Goal state after:
case calc_5
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)
⊢ ∑ x, ((|a| + 2 * ε') * μ.real (E x) + (y x - ε') * μ.real (E x) + (|a| + y x + ε') * (ε' / ↑N)) - |a| * μ.real K =
    ∑ n, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / ↑N * ∑ n, (|a| + y n + ε')
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ∞
μ : ProbabilityMeasure Ω
n s t : ℝ
hst : s ≤ t
⊢ ↑μ (thickening n {a | t ≤ f a}) ≤ ↑μ (thickening n {a | s ≤ f a})

Tactic:
exact measure_mono <| thickening_subset_of_subset _ <| fun ω h ↦ hst.trans h

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝⁹ : Group G
inst✝⁸ : AddCommGroup A
inst✝⁷ : DistribMulAction G A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalAddGroup A
inst✝⁴ : LocallyCompactSpace A
inst✝³ : ContinuousConstSMul G A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
g : G
⊢ (DomMulAct.mk g • μ).addHaarScalarFactor (DomMulAct.mk g • (DomMulAct.mk g)⁻¹ • μ) = (distribHaarChar A) g

Tactic:
simp_rw [← mul_smul, mul_inv_cancel, one_smul]

Goal state after:
G : Type u_1
A : Type u_2
inst✝⁹ : Group G
inst✝⁸ : AddCommGroup A
inst✝⁷ : DistribMulAction G A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalAddGroup A
inst✝⁴ : LocallyCompactSpace A
inst✝³ : ContinuousConstSMul G A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
g : G
⊢ (DomMulAct.mk g • μ).addHaarScalarFactor μ = (distribHaarChar A) g
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
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✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace A
inst✝³ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝² : NormedSpace ℝ E
inst✝¹ : IsTopologicalGroup C
inst✝ : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
b : B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
hb : U₀ ∈ nhds b
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, f x = 0
S : Set A := ⇑φ ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
hS' : ¬μA.real S = 0
⊢ ENNReal.ofReal (ε / 2 / μA.real S * μA.real S) < ENNReal.ofReal ε

Tactic:
ENNReal.ofReal_lt_ofReal_iff hε,

Goal state after:
case neg
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
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✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace A
inst✝³ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝² : NormedSpace ℝ E
inst✝¹ : IsTopologicalGroup C
inst✝ : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
b : B
ε : ℝ
hε : ε > 0
U₀ : Set B
hU₀ : IsCompact U₀
hb : U₀ ∈ nhds b
K : Set B
hK : IsCompact K
hf₀ : ∀ x ∉ K, f x = 0
S : Set A := ⇑φ ⁻¹' (U₀⁻¹ * K)
hSc : IsCompact S
hS' : ¬μA.real S = 0
⊢ ε / 2 / μA.real S * μA.real S < ε
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: case hbc.refine_1
μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (fun x ↦ sinc (r * x)) μ
⊢ IntegrableOn (fun x ↦ 2⁻¹) {x | 2 < |2 * r⁻¹ * x|} μ

pp: case hbc.refine_2
μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (fun x ↦ sinc (r * x)) μ
⊢ MeasurableSet {x | 2 < |2 * r⁻¹ * x|}

pp: case hbc.refine_3
μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (fun x ↦ sinc (r * x)) μ
x : ℝ
hx : x ∈ {x | 2 < |2 * r⁻¹ * x|}
⊢ 2⁻¹ ≤ 1 - sinc (2 * r⁻¹ * x)

Tactic:
· exact Integrable.integrableOn <| by fun_prop

Goal state after:
case hbc.refine_2
μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (fun x ↦ sinc (r * x)) μ
⊢ MeasurableSet {x | 2 < |2 * r⁻¹ * x|}

case hbc.refine_3
μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (fun x ↦ sinc (r * x)) μ
x : ℝ
hx : x ∈ {x | 2 < |2 * r⁻¹ * x|}
⊢ 2⁻¹ ≤ 1 - sinc (2 * r⁻¹ * x)
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Goal state before:
pp: case hs
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] ψ
hψUt : MapsTo ψ U t
dψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fderivWithin ℝ ψ (Icc 0 1)
s' : Set (ℝ × ℝ) := Prod.map Subtype.val Subtype.val '' s
hs' : s' = Prod.map Subtype.val Subtype.val '' s
hmem_s' : ∀ (x y : ↑I), (↑x, ↑y) ∈ s' ↔ (x, y) ∈ s
hs'c : s'.Countable
hdψ : ∀ a ∈ U, HasFDerivAt ψ (dψ a) a
d2ψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] E := fderivWithin ℝ dψ (Icc 0 1)
hd2ψ : ∀ a ∈ U, HasFDerivAt dψ (d2ψ a) a
hd2ψ_symm : ∀ a ∈ Icc 0 1, ∀ (x y : ℝ × ℝ), ((d2ψ a) x) y = ((d2ψ a) y) x
η : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun a ↦ ω (ψ a) ∘SL dψ a
f : ℝ × ℝ → F := fun a ↦ (η a) (0, 1)
hf : ∀ a ∈ Icc 0 1, f a = (ω (ψ a)) (derivWithin (ψ ∘ fun x ↦ (a.1, x)) I a.2)
g : ℝ × ℝ → F := fun a ↦ -(η a) (1, 0)
hg : ∀ a ∈ Icc 0 1, g a = (ω (ψ a)) (-derivWithin (ψ ∘ fun x ↦ (x, a.2)) I a.1)
dη : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] F :=
  fun a ↦ (ContinuousLinearMap.compL ℝ (ℝ × ℝ) E F) (ω (ψ a)) ∘SL d2ψ a + (dω (ψ a)).bilinearComp (dψ a) (dψ a)
hdη : ∀ a ∈ U \ s', HasFDerivAt η (dη a) a
hdη_symm : ∀ a ∈ U \ s', ∀ (u v : ℝ × ℝ), ((dη a) u) v = ((dη a) v) u
f' : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun a ↦ (ContinuousLinearMap.apply ℝ F) (0, 1) ∘SL dη a
hf' : ∀ a ∈ U \ s', HasFDerivAt f (f' a) a
g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun a ↦ -(ContinuousLinearMap.apply ℝ F) (1, 0) ∘SL dη a
hg' : ∀ a ∈ U \ s', HasFDerivAt g (g' a) a
hf'g' : (fun a ↦ (f' a) (1, 0) + (g' a) (0, 1)) =ᵐ[volume.restrict (Icc 0 1)] 0
this : ∫ (a : ℝ × ℝ) in Icc 0 1, (f' a) (1, 0) + (g' a) (0, 1) = 0
hηc : ContinuousOn η (Icc 0 1)
⊢ s'.Countable

Tactic:
exact hs'c

Goal state after:
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}
⊢ F (FiniteMeasure.comap f μ) = μ

Tactic:
ext s hs

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
⊢ ↑(F (FiniteMeasure.comap f μ)) s = ↑μ s
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case e'_3.e'_5
ι : 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)
⊢ (π * Real.Gamma (2 / p + 1)) ^ card ι = ∫ (x : ι → ℂ), rexp (-((∑ i, ‖x i‖ ^ p) ^ (1 / p)) ^ p)

Tactic:
simp_rw [← rpow_mul (h₂ _), div_mul_cancel₀ _ (ne_of_gt h₁), Real.rpow_one,
      ← Finset.sum_neg_distrib, Real.exp_sum]

Goal state after:
case e'_3.e'_5
ι : 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)
⊢ (π * Real.Gamma (2 / p + 1)) ^ card ι = ∫ (x : ι → ℂ), ∏ x_1, rexp (-‖x x_1‖ ^ p)
Module: Mathlib.MeasureTheory.Measure.TightNormed

Goal state before:
pp: E : Type u_1
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h : ∀ (y : E), ‖y‖ = 1 → Tendsto (fun r ↦ limsup (fun n ↦ (μ n).real {x | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
C : ℝ≥0
hμ : ∀ᶠ (n : ℕ) in atTop, (μ n) Set.univ ≤ ↑C
z : E
hz : ‖z‖ = 1
⊢ Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | r < ‖⟪z, x⟫_𝕜‖}) atTop) atTop (𝓝 0)

Tactic:
have h_ofReal (r : ℝ) : limsup (fun n ↦ μ n {x | r < ‖⟪z, x⟫_𝕜‖}) atTop
      = ENNReal.ofReal (limsup (fun n ↦ (μ n).real {x | r < ‖⟪z, x⟫_𝕜‖}) atTop) := by
    simp_rw [measureReal_def]
    rw [ENNReal.ofReal_limsup_toReal (C := C)]
    filter_upwards [hμ] with n hμn using (measure_mono (Set.subset_univ _)).trans hμn

Goal state after:
E : Type u_1
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h : ∀ (y : E), ‖y‖ = 1 → Tendsto (fun r ↦ limsup (fun n ↦ (μ n).real {x | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
C : ℝ≥0
hμ : ∀ᶠ (n : ℕ) in atTop, (μ n) Set.univ ≤ ↑C
z : E
hz : ‖z‖ = 1
h_ofReal :
  ∀ (r : ℝ),
    limsup (fun n ↦ (μ n) {x | r < ‖⟪z, x⟫_𝕜‖}) atTop =
      ENNReal.ofReal (limsup (fun n ↦ (μ n).real {x | r < ‖⟪z, x⟫_𝕜‖}) atTop)
⊢ Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | r < ‖⟪z, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: case refine_3
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
⊢ ∀ᶠ (b : ℝ) in atTop,
    limsup (fun n ↦ (μ n).real {x | b < ‖⟪z, x⟫‖}) atTop ≤ 2⁻¹ * b * ‖∫ (t : ℝ) in -2 * b⁻¹..2 * b⁻¹, 1 - f (t • z)‖

pp: case refine_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
⊢ Tendsto (fun r ↦ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖) atTop (𝓝 0)

Tactic:
· filter_upwards [eventually_gt_atTop 0] with r hr using h_limsup_le r hr

Goal state after:
case refine_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
⊢ Tendsto (fun r ↦ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Measure.Support

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : OpensMeasurableSpace X
s : Set X
⊢ (μ.restrict s).support ⊆ closure[inst✝²] s ∩ μ.support

Tactic:
by
  refine Set.subset_inter (support_subset_of_isClosed isClosed_closure ?_)
    (support_mono restrict_le_self)
  rw [mem_ae_iff, μ.restrict_apply isClosed_closure.isOpen_compl.measurableSet]
  convert! μ.empty
  exact subset_closure.disjoint_compl_left.eq_bot

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν ξ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ - ν ≤ ξ
s : Set α
hs : IsHahnDecomposition μ ν s
h_le_s : μ.restrict s ≤ ξ.restrict s + ν.restrict s
⊢ μ.restrict sᶜ - ν.restrict sᶜ ≤ ξ.restrict sᶜ

Tactic:
rw [← restrict_sub_eq_restrict_sub_restrict hs.measurableSet.compl]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν ξ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ - ν ≤ ξ
s : Set α
hs : IsHahnDecomposition μ ν s
h_le_s : μ.restrict s ≤ ξ.restrict s + ν.restrict s
⊢ (μ - ν).restrict sᶜ ≤ ξ.restrict sᶜ
Module: Mathlib.MeasureTheory.Measure.SubFinite

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hg : Measurable g
hgf : g ≤ᵐ[μ] f
⊢ μ.withDensity (f - g) = μ.withDensity f - μ.withDensity g

Tactic:
ext s hs

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
inst✝ : IsFiniteMeasure (μ.withDensity g)
hg : Measurable g
hgf : g ≤ᵐ[μ] f
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (f - g)) s = (μ.withDensity f - μ.withDensity g) s
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep : ∀ x ∈ univ, ∀ y ∈ univ, (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : ℕ → Set α := ⋯
mBn : MeasurableSet (⋂ n, B n)
hBn : μ (⋂ n, B n) = 1
x₀ : α
hx₀ : ⋂ n, B n = {x₀}
⊢ μ = Measure.dirac x₀

Tactic:
ext s hs

Goal state after:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep : ∀ x ∈ univ, ∀ y ∈ univ, (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : ℕ → Set α := fun n ↦ if h : μ (A n) = 1 then A n else (A n)ᶜ
mBn : MeasurableSet (⋂ n, B n)
hBn : μ (⋂ n, B n) = 1
x₀ : α
hx₀ : ⋂ n, B n = {x₀}
s : Set α
hs : MeasurableSet s
⊢ μ s = (Measure.dirac x₀) s
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: case refine_1
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
⊢ m ≤ MeasurableSpace.generateFrom (generateSetAlgebra 𝒜)

Tactic:
rw [← hgen]

Goal state after:
case refine_1
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
⊢ MeasurableSpace.generateFrom (countableGeneratingSet X) ≤ MeasurableSpace.generateFrom (generateSetAlgebra 𝒜)
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
E : Set X
⊢ ‖μ E‖ₑ ≤ μ.variation E

Tactic:
by
  by_cases hE : MeasurableSet E
  swap; · simp [hE]
  by_cases hE' : (⟨E, hE⟩ : Subtype MeasurableSet) = ⊥
  · simp_all
  simp only [variation_apply, preVariation, ennrealToMeasure_apply hE, ennrealPreVariation_apply]
  calc
    ‖μ E‖ₑ = ∑ p ∈ (Finpartition.indiscrete hE').parts, ‖μ p‖ₑ := by simp
    _ ≤ preVariationFun (‖μ ·‖ₑ) E := by apply preVariation.sum_le

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: case pos
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : μ.ennrealVariation s = 0
hsm : MeasurableSet s
⊢ μ.variation s ≤ 0

Tactic:
← ennrealVariation_apply _ hsm,

Goal state after:
case pos
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : μ.ennrealVariation s = 0
hsm : MeasurableSet s
⊢ μ.ennrealVariation s ≤ 0
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: case insert
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝³ : TopologicalSpace V
inst✝² : ENormedAddCommMonoid V
inst✝¹ : T2Space V
inst✝ : ContinuousAdd V
ι : Type u_3
μ : ι → VectorMeasure X V
i : ι
s : Finset ι
his : i ∉ s
ih : (∑ i ∈ s, μ i).variation ≤ ∑ i ∈ s, (μ i).variation
⊢ (∑ i ∈ insert i s, μ i).variation ≤ ∑ i ∈ insert i s, (μ i).variation

Tactic:
simpa [Finset.sum_insert his] using
      variation_add_le.trans (add_le_add_right ih ((μ i).variation))

Goal state after: