mathlib-initiative/mathlib-tactics huggingface dataset:
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 ν κ + ε
⊢ s.toReal + r.toReal = (s + r).toReal

Tactic:
← ENNReal.toReal_add

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
⊢ (s + r).toReal = (s + r).toReal

case ha
Ω : 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 ν κ + ε
⊢ s ≠ ∞

case hb
Ω : 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 ν κ + ε
⊢ r ≠ ∞
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
g✝ : G
this✝ : MeasurableSpace A := borel A
this : BorelSpace A
g g' : G
⊢ (DomMulAct.mk (g * g') • addHaar).addHaarScalarFactor addHaar =
    (DomMulAct.mk g • addHaar).addHaarScalarFactor addHaar * (DomMulAct.mk g' • addHaar).addHaarScalarFactor addHaar

Tactic:
DomMulAct.mk_mul

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
g✝ : G
this✝ : MeasurableSpace A := borel A
this : BorelSpace A
g g' : G
⊢ ((DomMulAct.mk g' * DomMulAct.mk g) • addHaar).addHaarScalarFactor addHaar =
    (DomMulAct.mk g • addHaar).addHaarScalarFactor addHaar * (DomMulAct.mk g' • addHaar).addHaarScalarFactor addHaar
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: 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
inst✝⁴ : MeasurableSpace C
inst✝³ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝² : T2Space B
inst✝¹ : MeasurableSpace B
inst✝ : BorelSpace B
b : B
this : (map (fun x ↦ b * x) (H.inducedMeasure μA μC)).Regular
f : CompactlySupportedContinuousMap B ℝ
⊢ ∫ (x : B), f (b * x) ∂H.inducedMeasure μA μC = ∫ (x : B), f x ∂H.inducedMeasure μA μC

Tactic:
have h (x : B) : f (b * x) = f.comp (Homeomorph.mulLeft b).toCocompactMap x := rfl

Goal state after:
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
inst✝⁴ : MeasurableSpace C
inst✝³ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝² : T2Space B
inst✝¹ : MeasurableSpace B
inst✝ : BorelSpace B
b : B
this : (map (fun x ↦ b * x) (H.inducedMeasure μA μC)).Regular
f : CompactlySupportedContinuousMap B ℝ
h : ∀ (x : B), f (b * x) = (f.comp (Homeomorph.mulLeft b).toCocompactMap) x
⊢ ∫ (x : B), f (b * x) ∂H.inducedMeasure μA μC = ∫ (x : B), f x ∂H.inducedMeasure μA μC
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

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

Tactic:
mul_assoc,

Goal state after:
case e_s
μ : Measure ℝ
r : ℝ
inst✝ : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (fun x ↦ sinc (r * x)) μ
x : ℝ
⊢ r < |x| ↔ 2 < 2 * (r⁻¹ * |x|)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case inr
E : Type u_1
p : ℝ
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this✝ : 0 < ↑(finrank ℝ E)
this :
  (∫ (y : ℝ) in Set.Ioi 0, y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) / Real.Gamma (↑(finrank ℝ E) / p + 1) *
      ↑(finrank ℝ E) =
    1
⊢ μ (Metric.ball 0 1) =
    ENNReal.ofReal
      (μ.real (Metric.ball 0 1) *
          ((∫ (y : ℝ) in Set.Ioi 0, y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) / Real.Gamma (↑(finrank ℝ E) / p + 1)) *
        ↑(finrank ℝ E))

Tactic:
mul_assoc,

Goal state after:
case inr
E : Type u_1
p : ℝ
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hp : 0 < p
hE : Nontrivial E
this✝ : 0 < ↑(finrank ℝ E)
this :
  (∫ (y : ℝ) in Set.Ioi 0, y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) / Real.Gamma (↑(finrank ℝ E) / p + 1) *
      ↑(finrank ℝ E) =
    1
⊢ μ (Metric.ball 0 1) =
    ENNReal.ofReal
      (μ.real (Metric.ball 0 1) *
        ((∫ (y : ℝ) in Set.Ioi 0, y ^ (finrank ℝ E - 1) • Real.exp (-y ^ p)) / Real.Gamma (↑(finrank ℝ E) / p + 1) *
          ↑(finrank ℝ E)))
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

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

Tactic:
congr 1 with x
    simp only [Set.mem_ofPred_eq, abs_mul, Nat.abs_ofNat]
    rw [abs_of_nonneg (a := r⁻¹) (by positivity), mul_assoc, ← inv_mul_lt_iff₀ (by positivity),
      inv_mul_cancel₀ (by positivity), lt_inv_mul_iff₀ (by positivity), mul_one]

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

Goal state before:
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 MeasurableSet.preimage measurableSet_Ioi (by fun_prop)

Goal state after:
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.Measure.IntegralCharFun

Goal state before:
pp: case e'_3
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
L : StrongDual ℝ E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (Measure.map (⇑L) μ)
⊢ MeasurableSet {x | r < |x|}

Tactic:
· exact MeasurableSet.preimage measurableSet_Ioi (by fun_prop)

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

Goal state before:
pp: case e'_3
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
mE : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
a : E
r : ℝ
hr : 0 < r
this : IsProbabilityMeasure (Measure.map (fun x ↦ ⟪a, x⟫) μ)
⊢ MeasurableSet {x | r < |x|}

Tactic:
· exact MeasurableSet.preimage measurableSet_Ioi (by fun_prop)

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

Goal state before:
pp: case inr
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : 0 ≤ r
⊢ volume (Metric.ball x r) = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))

Tactic:
· suffices volume (Metric.ball (0 : EuclideanSpace ℝ ι) 1) =
        .ofReal (√π ^ card ι / Gamma (card ι / 2 + 1)) by
      rw [Measure.addHaar_ball _ _ hr, this, ofReal_pow hr, finrank_euclideanSpace]
    rw [← (PiLp.volume_preserving_toLp ι).measure_preimage
      measurableSet_ball.nullMeasurableSet]
    simp only [Set.preimage, ball_zero_eq _ zero_le_one, one_pow, Set.mem_ofPred_eq]
    convert! volume_sum_rpow_lt_one ι one_le_two using 4
    · simp [sq_abs]
    · rw [Gamma_add_one (by simp), Gamma_one_half_eq, ← mul_assoc, mul_div_cancel₀ _
        two_ne_zero, one_mul]

Goal state after:
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), Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
z : E
n : ℕ
h_tight : Tendsto (fun r ↦ ⨆ μ_1 ∈ {Measure.map (fun x ↦ ⟪z, x⟫_𝕜) (μ n)}, μ_1 {x | r < ‖x‖}) atTop (𝓝 0)
r : ℝ
⊢ MeasurableSet {x | r < ‖x‖}

Tactic:
· exact MeasurableSet.preimage measurableSet_Ioi (by fun_prop)

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

Goal state before:
pp: case refine_2.inl
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
L : Tendsto id (↑f) (𝓝 μ)
n : ℕ
h : NormalSpace E
this : (↑μ).InnerRegular
⊢ ⨆ f,
      ⨆ (_ : Continuous[inst✝², _] f),
        ⨆ (_ : EqOn f 0 (K n)ᶜᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : E), f x ∂↑μ) ≤
    ↑(u n)

Tactic:
simp only [compl_compl, iSup_le_iff, ENNReal.ofReal_le_coe]

Goal state after:
case refine_2.inl
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
L : Tendsto id (↑f) (𝓝 μ)
n : ℕ
h : NormalSpace E
this : (↑μ).InnerRegular
⊢ ∀ (i : E → ℝ), Continuous[inst✝², _] i → EqOn i 0 (K n) → 0 ≤ i → i ≤ 1 → ∫ (x : E), i x ∂↑μ ≤ ↑(u n)
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
⊢ ∑' (i : ℕ), preVariationFun f (s i) ≤ preVariationFun f (⋃ i, s i)

Tactic:
by
  refine ENNReal.tsum_le_of_sum_range_le fun n ↦ ?_
  by_cases hn : n = 0
  · simp [hn]
  refine ENNReal.le_of_forall_pos_le_add fun ε' hε' hsnetop ↦ ?_
  let ε := ε' / n
  have hε : 0 < ε := by positivity
  have hs'' i : preVariationFun f (s i) ≠ ⊤ := lt_top_iff_ne_top.mp <|
    (mono f (MeasurableSet.iUnion hs) (Set.subset_iUnion s i)).trans_lt hsnetop
  -- For each set `s i` we choose a Finpartition `P i` such that, for each `i`,
  -- `preVariationFun f (s i) ≤ ∑ p ∈ (P i), f p + ε`.
  choose P hP using fun i ↦ exists_Finpartition_sum_ge f (hs i) (hε) (hs'' i)
  calc ∑ i ∈ Finset.range n, preVariationFun f (s i)
    _ ≤ ∑ i ∈ Finset.range n, (∑ p ∈ (P i).parts, f p + ε) := Finset.sum_le_sum fun i _ => hP i
    _ = ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f p + ε' := by
      rw [Finset.sum_add_distrib]; norm_cast
      simp [show n * ε = ε' by field]
    _ ≤ preVariationFun f (⋃ i, s i) + ε' := by
      gcongr; exact sum_le_preVariationFun_iUnion' f hs hs' P n

Goal state after:
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
x : X
⊢ (∀ (i : Set X), x ∈ i ∧ IsOpen[inst✝²] i → 0 < (μ.restrict s) i) ↔ ∃ᶠ (u : Set X) in (𝓝[s] x).smallSets, 0 < μ u

Tactic:
(nhdsWithin_basis_open x s).frequently_smallSets pos_mono

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : OpensMeasurableSpace X
s : Set X
x : X
⊢ (∀ (i : Set X), x ∈ i ∧ IsOpen[inst✝²] i → 0 < (μ.restrict s) i) ↔
    ∀ (i : Set X), x ∈ i ∧ IsOpen[inst✝²] i → 0 < μ (i ∩ s)
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
x : X
hxs : x ∈ interior s
hxμ : x ∈ μ.support
⊢ ∃ᶠ (u : Set X) in (𝓝[s] x).smallSets, 0 < μ u

Tactic:
(nhdsWithin_basis_open x s).frequently_smallSets pos_mono

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : OpensMeasurableSpace X
s : Set X
x : X
hxs : x ∈ interior s
hxμ : x ∈ μ.support
⊢ ∀ (i : Set X), x ∈ i ∧ IsOpen[inst✝²] i → 0 < μ (i ∩ s)
Module: Mathlib.MeasureTheory.Measure.ResolventTransform

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : MeasurableSpace 𝕜
inst✝² : CompleteSpace 𝕜
inst✝¹ : NormedDivisionRing A
inst✝ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
this : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
⊢ ‖resolvent a x‖ ≤ (infDist a (⇑(algebraMap 𝕜 A) '' μ.support))⁻¹

Tactic:
have : infDist a (algebraMap 𝕜 A '' μ.support) ≤ ‖(algebraMap 𝕜 A) x - a‖ := by
    grw [infDist_le_dist_of_mem (y := (algebraMap 𝕜 A) x), ← dist_eq_norm, dist_comm]
    simp [hx]

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : MeasurableSpace 𝕜
inst✝² : CompleteSpace 𝕜
inst✝¹ : NormedDivisionRing A
inst✝ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
this✝ : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
this : infDist a (⇑(algebraMap 𝕜 A) '' μ.support) ≤ ‖(algebraMap 𝕜 A) x - a‖
⊢ ‖resolvent a x‖ ≤ (infDist a (⇑(algebraMap 𝕜 A) '' μ.support))⁻¹
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: case inr
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
⊢ {x | ∃ s, ∃ (hs : MeasurableSet s) (hμs : μ s ≠ ∞), indicatorConstLp p hs hμs c = x} ⊆
    closure {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ∞), indicatorConstLp p ⋯ hμs c = x}

Tactic:
have p_pos : 0 < p := lt_of_lt_of_le (by simp) one_le_p.elim

Goal state after:
case inr
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
⊢ {x | ∃ s, ∃ (hs : MeasurableSet s) (hμs : μ s ≠ ∞), indicatorConstLp p hs hμs c = x} ⊆
    closure {x | ∃ s, ∃ (hs : s ∈ 𝒜) (hμs : μ s ≠ ∞), indicatorConstLp p ⋯ hμs c = x}
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: case mp.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s : Set α
h : μ s = 1
h₀ : μ univ = 0
⊢ μ univ = 1

Tactic:
have := measure_mono (μ := μ) <| subset_univ s

Goal state after:
case mp.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s : Set α
h : μ s = 1
h₀ : μ univ = 0
this : μ s ≤ μ univ
⊢ μ univ = 1
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: case ac
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ∞
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n ↦ T n ∩ s
this✝ : Filter.Tendsto (fun n ↦ ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal (μ (⋃ n, T n ∩ s)).toReal < ε / 2
this : Fact (μ (T N) < ∞)
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N)) (s ∆ t) < ENNReal.ofReal (ε / 2)
⊢ dist (μ (T N ∩ s)).toReal (μ ((⋃ n, T n) ∩ s)).toReal < ε / 2

Tactic:
iUnion_inter _ T

Goal state after:
case ac
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ∞
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n ↦ T n ∩ s
this✝ : Filter.Tendsto (fun n ↦ ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal (μ (⋃ n, T n ∩ s)).toReal < ε / 2
this : Fact (μ (T N) < ∞)
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N)) (s ∆ t) < ENNReal.ofReal (ε / 2)
⊢ dist (μ (T N ∩ s)).toReal (μ (⋃ i, T i ∩ s)).toReal < ε / 2
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
mα : MeasurableSpace α
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
hC_gen : mα = MeasurableSpace.generateFrom C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ (m.measureCaratheodory hC m_sigma_subadd) s = m s

Tactic:
exact m.measureCaratheodory_eq hC m_sigma_subadd hs

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p q : ℝ≥0∞
inst✝² : Fact (1 ≤ q)
ι : Type u_2
inst✝¹ : Fintype ι
E : ι → Type u_3
inst✝ : (i : ι) → NormedAddCommGroup (E i)
f : X → PiLp q E
⊢ MemLp f p μ ↔ ∀ (i : ι), MemLp (fun x ↦ (f x).ofLp i) p μ

Tactic:
simp_rw [← memLp_pi_iff, ← Function.comp_apply (f := WithLp.ofLp)]

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p q : ℝ≥0∞
inst✝² : Fact (1 ≤ q)
ι : Type u_2
inst✝¹ : Fintype ι
E : ι → Type u_3
inst✝ : (i : ι) → NormedAddCommGroup (E i)
f : X → PiLp q E
⊢ MemLp f p μ ↔ MemLp (fun x ↦ (WithLp.ofLp ∘ f) x) p μ
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
D : Set ↥(Lp E p μ) := {s | ∃ n d t, s = key n d t}
a : E
s : Set X
ms : MeasurableSet s
hμs✝ : μ s < ∞
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : μ t ≠ ∞
hst : ‖indicatorConstLp p ms hμs b - indicatorConstLp p ⋯ hμt b‖ < ε / 3
mt : MeasurableSet t
⊢ ε / 3 * (1 / (1 + μ.real s ^ (1 / p.toReal))) * μ.real s ^ (1 / p.toReal) ≤ ε / 3 * 1

Tactic:
mul_assoc,

Goal state after:
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
D : Set ↥(Lp E p μ) := {s | ∃ n d t, s = key n d t}
a : E
s : Set X
ms : MeasurableSet s
hμs✝ : μ s < ∞
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : μ t ≠ ∞
hst : ‖indicatorConstLp p ms hμs b - indicatorConstLp p ⋯ hμt b‖ < ε / 3
mt : MeasurableSet t
⊢ ε / 3 * (1 / (1 + μ.real s ^ (1 / p.toReal)) * μ.real s ^ (1 / p.toReal)) ≤ ε / 3 * 1
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
s : Set X
⊢ (μ.restrict s).variation ≤ μ.variation.restrict s

Tactic:
by
  by_cases hs : MeasurableSet s
  · simp [variation_restrict hs]
  · simp [restrict_not_measurable _ hs, Measure.zero_le]

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

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup V
μ : VectorMeasure X V
𝕜 : Type u_3
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 V
c : 𝕜
⊢ (c • μ).variation ≤ ‖c‖₊ • μ.variation

Tactic:
apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)
  simp only [smul_apply, enorm_smul, Measure.smul_apply, Measure.nnreal_smul_coe_apply]
  grw [enorm_measure_le_variation, enorm_eq_nnnorm]

Goal state after: