mathlib-initiative/mathlib-tactics huggingface dataset:
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)
this : tsupport ⇑f ⊆ ⋃ n, (V n).carrier
g' : Fin N → C(X, ℝ)
hg :
  (∀ (i : Fin N), tsupport ⇑(g' i) ⊆ (V i).carrier) ∧
    EqOn (∑ i, ⇑(g' i)) 1 (tsupport f.toFun) ∧
      (∀ (i : Fin N) (x : X), (g' i) x ∈ Icc 0 1) ∧ ∀ (i : Fin N), HasCompactSupport ⇑(g' i)
⊢ ∃ g,
    (∀ (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)

Tactic:
exact ⟨fun n ↦ ⟨g' n, hg.2.2.2 n⟩, hg⟩

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyRegularSpace Y
f : X → Y
hf : IsInducing f
x : X
K : Set X
hK : IsClosed[inst✝²] K
hxK : x ∉ K
⊢ ∃ f, Continuous[inst✝², _] f ∧ f x = 0 ∧ EqOn f 1 K

Tactic:
rw [hf.isClosed_iff] at hK

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : CompletelyRegularSpace Y
f : X → Y
hf : IsInducing f
x : X
K : Set X
hK : ∃ t, IsClosed[inst✝¹] t ∧ f ⁻¹' t = K
hxK : x ∉ K
⊢ ∃ f, Continuous[inst✝², _] f ∧ f x = 0 ∧ EqOn f 1 K
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : 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) + ε

Tactic:
refine le_add_right <| measure_mono <| self_subset_thickening ?_ _

Goal state after:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ : Measure Ω
ε : ℝ≥0∞
x✝¹ : ε ∈ Ioo 0 ∞
B : Set Ω
x✝ : MeasurableSet B
hε₀ : 0 < ε
hε_top : ε < ∞
⊢ 0 < ε.toReal
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
⊢ levyProkhorovEDist μ ν = levyProkhorovEDist ν μ

Tactic:
by
  simp only [levyProkhorovEDist, and_comm]

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

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
⊢ ∫ (ω : Ω), f ω ∂μ ≤ (∫ (t : ℝ) in Ioc 0 ‖f‖, ν.real (thickening ε {a | t ≤ f a})) + ε * ‖f‖

Tactic:
rw [BoundedContinuousFunction.integral_eq_integral_meas_le f μ f_nn]

Goal state after:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᵐ[μ] ⇑f
⊢ ∫ (t : ℝ) in Ioc 0 ‖f‖, μ.real {a | t ≤ f a} ≤ (∫ (t : ℝ) in Ioc 0 ‖f‖, ν.real (thickening ε {a | t ≤ f a})) + ε * ‖f‖
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case refine_2
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (fun x ↦ ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs x) ν + εs x) {a | t ≤ f a})) atTop
    (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
εs_pos : 0 < εs n
hn :
  ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs n) ν + εs n) {a | t ≤ f a}) <
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}) + δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
⊢ levyProkhorovEDist ↑(Ps n) ↑P < ENNReal.ofReal (dist (μs n) ν + εs n)

Tactic:
rw [ENNReal.ofReal_add (by positivity) (by positivity), ← add_zero (levyProkhorovEDist _ _)]

Goal state after:
case refine_2
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (fun x ↦ ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs x) ν + εs x) {a | t ≤ f a})) atTop
    (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
εs_pos : 0 < εs n
hn :
  ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real (thickening (dist (μs n) ν + εs n) {a | t ≤ f a}) <
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P).real {a | t ≤ f a}) + δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
⊢ levyProkhorovEDist ↑(Ps n) ↑P + 0 < ENNReal.ofReal (dist (μs n) ν) + ENNReal.ofReal (εs n)
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
f : CompactlySupportedContinuousMap B E
⊢ Continuous fun c ↦ ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) c)) a ∂μA

Tactic:
let := IsTopologicalGroup.rightUniformSpace B
      simp_rw [← H.isOpenQuotientMap.continuous_comp_iff, Function.comp_def,
        integral_pullback_invFun_apply, Metric.continuous_iff']
      intro b ε hε
      obtain ⟨U₀, hU₀, hb⟩ := exists_compact_mem_nhds b
      obtain ⟨K, hK, hf₀⟩ := exists_compact_iff_hasCompactSupport.mpr f.hasCompactSupport
      let S : Set A := φ ⁻¹' (U₀⁻¹ * K)
      have hSc : IsCompact S := H.isClosedEmbedding.isCompact_preimage (hU₀.inv.mul hK)
      obtain ⟨δ, hδ0, hδ⟩ : ∃ δ > 0, ENNReal.ofReal δ * μA S < ENNReal.ofReal ε := by
        rw [← ENNReal.ofReal_toReal hSc.measure_ne_top, ← measureReal_def]
        by_cases hS' : μA.real S = 0
        · simp [hS', hε, exists_gt]
        · refine ⟨ε / 2 / μA.real S, by positivity, ?_⟩
          rwa [← ENNReal.ofReal_mul' measureReal_nonneg, ENNReal.ofReal_lt_ofReal_iff hε,
            div_mul_cancel₀ _ hS', half_lt_self_iff]
      have hS {x} (hx : x ∈ U₀) {y} (hy : y ∉ S) : H.pullback f x y = 0 := by
        contrapose! hy
        exact Set.mem_mul.mpr ⟨x⁻¹, Set.inv_mem_inv.mpr hx, x * φ y,
          not_imp_comm.mp (hf₀ (x * φ y)) hy, inv_mul_cancel_left x (φ y)⟩
      have ha := f.hasCompactSupport.uniformContinuous_of_continuous f.continuous
      rw [uniformContinuous_iff_eventually] at ha
      obtain ⟨U, hU, hf⟩ := ha _ (Metric.dist_mem_uniformity hδ0)
      refine Filter.mem_of_superset (Filter.inter_mem
        (mul_singleton_mem_nhds_of_nhds_one b (inv_mem_nhds_one B hU)) hb) ?_
      rintro - ⟨⟨t, ht, b, rfl, -, rfl⟩, htb⟩
      have h (a) (ha : a ∈ S) : edist (H.pullback f (t * b) a) (H.pullback f b a) ≤ .ofReal δ := by
        rw [edist_dist]
        exact ENNReal.ofReal_le_ofReal (@hf ⟨t * b * φ a, b * φ a⟩ (by simpa)).le
      grw [Set.mem_ofPred_eq, dist_integral_le_lintegral_edist (H.pullback f (t * b)).integrable
        (H.pullback f b).integrable, ← setLIntegral_eq_of_support_subset]
      · refine ENNReal.toReal_lt_of_lt_ofReal ((setLIntegral_mono measurable_const h).trans_lt ?_)
        rwa [lintegral_const, restrict_apply_univ]
      · intro y hy
        contrapose hy
        rw [Function.notMem_support, hS htb hy, hS (mem_of_mem_nhds hb) hy, edist_self]

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

Goal state before:
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 := ⋯
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure ↑K → FiniteMeasure E := ⋯
T : Set (FiniteMeasure ↑K) := ⋯
μ : FiniteMeasure E
hμ : μ ∈ {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
s : Set E
hs : MeasurableSet s
⊢ μ (range f)ᶜ = 0

Tactic:
rw [rf]

Goal state after:
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
⊢ μ Kᶜ = 0
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

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

Tactic:
Metric.ball_eq_empty.mpr hr,

Goal state after:
case inl
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Fintype ι
x : EuclideanSpace ℝ ι
r : ℝ
hr : r ≤ 0
⊢ volume ∅ = ENNReal.ofReal r ^ card ι * ENNReal.ofReal (√π ^ card ι / Gamma (↑(card ι) / 2 + 1))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ ENNReal.ofReal r ^ (2 * k + 1) * ENNReal.ofReal (√π ^ (2 * k + 1) / Gamma (↑(2 * k + 1) / 2 + 1)) =
    ENNReal.ofReal r ^ (2 * k + 1) * ENNReal.ofReal (π ^ k * 2 ^ (k + 1) / ↑(2 * k + 1)‼)

Tactic:
pow_succ (√π),

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ ENNReal.ofReal r ^ (2 * k + 1) * ENNReal.ofReal (√π ^ (2 * k) * √π / Gamma (↑(2 * k + 1) / 2 + 1)) =
    ENNReal.ofReal r ^ (2 * k + 1) * ENNReal.ofReal (π ^ k * 2 ^ (k + 1) / ↑(2 * k + 1)‼)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: x : EuclideanSpace ℝ (Fin 2)
r : ℝ
⊢ volume (ball x r) = ENNReal.ofReal r ^ 2 * ENNReal.ofReal π

Tactic:
norm_num [InnerProductSpace.volume_ball_of_dim_even (k := 1) (by simp) x]

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

Goal state before:
pp: case h
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h : ∀ (i : ι), Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖⟪b i, x⟫_𝕜‖}) atTop (𝓝 0)
hE : Nontrivial E
h_rank : 0 < ↑(Fintype.card ι)
this✝ : Nonempty ι
this : ProperSpace E
r : ℝ
μ : Measure E
hμS : μ ∈ S
x : E
hx : x ∈ {x | r < ‖x‖}
⊢ x ∈ ⋃ i, {x | r / √↑(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖}

Tactic:
simp only [Set.mem_ofPred_eq, Set.mem_iUnion] at hx ⊢

Goal state after:
case h
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι 𝕜 E
h : ∀ (i : ι), Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖⟪b i, x⟫_𝕜‖}) atTop (𝓝 0)
hE : Nontrivial E
h_rank : 0 < ↑(Fintype.card ι)
this✝ : Nonempty ι
this : ProperSpace E
r : ℝ
μ : Measure E
hμS : μ ∈ S
x : E
hx : r < ‖x‖
⊢ ∃ i, r / √↑(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: 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
⊢ Tendsto (fun r ↦ limsup (fun n ↦ (μ n).real {x | r < ‖⟪z, x⟫‖}) atTop) atTop (𝓝 0)

Tactic:
have h_le_4 n r (hr : 0 < r) :
      2⁻¹ * r * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4 := by
    have hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹ := by rw [neg_le_self_iff]; positivity
    calc 2⁻¹ * r * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
    _ ≤ 2⁻¹ * r * ∫ t in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - charFun (μ n) (t • z)‖ := by
      grw [neg_mul, intervalIntegral.norm_integral_le_integral_norm hr']
    _ ≤ 2⁻¹ * r * ∫ t in -(2 * r⁻¹)..2 * r⁻¹, 2 := by
      gcongr
      rw [intervalIntegral.integral_of_le hr', intervalIntegral.integral_of_le hr']
      refine integral_mono_of_nonneg ?_ (by fun_prop) ?_
      · exact ae_of_all _ fun _ ↦ by positivity
      · exact ae_of_all _ fun _ ↦ norm_one_sub_charFun_le_two
    _ ≤ 4 := by
      simp only [intervalIntegral.integral_const, sub_neg_eq_add, smul_eq_mul]
      field_simp
      norm_num

Goal state after:
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
⊢ Tendsto (fun r ↦ limsup (fun n ↦ (μ n).real {x | r < ‖⟪z, x⟫‖}) atTop) atTop (𝓝 0)
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)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ∞
hμst : μ (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal) = ε

Tactic:
by
        rw [toReal_ofReal (by positivity),
          one_div, Real.rpow_rpow_inv (by positivity) (toReal_pos p_pos.ne.symm p_ne_top.elim).ne',
          mul_div_cancel₀ _ (norm_ne_zero_iff.2 hc)]

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
m_top : ∀ s ∉ C, m s = ∞
hs : s ∈ C
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hs_subset : s ⊆ ⋃ i, f i
⊢ m s ≤ ∑' (i : ℕ), m (f i)

Tactic:
calc m s = m (s ∩ ⋃ i, f i) := by rw [inter_eq_self_of_subset_left hs_subset]
    _ = m (⋃ i, s ∩ f i) := by rw [inter_iUnion]
    _ ≤ ∑' i, m (s ∩ f i) := by
      refine m_sigma_subadd (fun i ↦ hC.inter_mem _ hs _ (hf i)) ?_
      rwa [← inter_iUnion, inter_eq_self_of_subset_left hs_subset]
    _ ≤ ∑' i, m (f i) := by
      refine ENNReal.summable.tsum_le_tsum (fun i ↦ ?_) ENNReal.summable
      exact addContent_mono hC (hC.inter_mem _ hs _ (hf i)) (hf i) Set.inter_subset_right

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

Goal state before:
pp: case refine_4
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 : MeasurableSet s
a : ℝ≥0∞
ha : a < preVariationFun (fun x ↦ ‖μ x‖ₑ) s
P : Finpartition ⟨s, hs⟩
hP : a < ∑ p ∈ P.parts, (fun x ↦ ‖μ x‖ₑ) ↑p
⊢ a < ∑ p ∈ Finset.map (Function.Embedding.subtype MeasurableSet) P.parts, ‖μ p‖ₑ

Tactic:
· rwa [Finset.sum_map]

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

Goal state before:
pp: case refine_4
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 : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
hμ : preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≠ ∞
P : Finpartition ⟨s, hs⟩
hP : preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≤ ∑ p ∈ P.parts, (fun x ↦ ‖μ x‖ₑ) ↑p + ε
⊢ preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≤ ∑ x ∈ Finset.map (Function.Embedding.subtype MeasurableSet) P.parts, ‖μ x‖ₑ + ε

Tactic:
· rwa [Finset.sum_map]

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✝³ : TopologicalSpace V
inst✝² : ENormedAddCommMonoid V
inst✝¹ : T2Space V
μ : VectorMeasure X V
Y : Type u_3
inst✝ : MeasurableSpace Y
φ : X → Y
hφ : MeasurableEmbedding φ
s : Set Y
hs : MeasurableSet s
this : (μ.map φ).variation s = (μ.map φ).variation (s ∩ Set.range φ)
t : Set X
ht : MeasurableSet t
⊢ ‖μ t‖ₑ ≤ ‖(μ.map φ) (φ '' t)‖ₑ

Tactic:
map_apply _ hφ.measurable (hφ.measurableSet_image.2 ht),

Goal state after:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝³ : TopologicalSpace V
inst✝² : ENormedAddCommMonoid V
inst✝¹ : T2Space V
μ : VectorMeasure X V
Y : Type u_3
inst✝ : MeasurableSpace Y
φ : X → Y
hφ : MeasurableEmbedding φ
s : Set Y
hs : MeasurableSet s
this : (μ.map φ).variation s = (μ.map φ).variation (s ∩ Set.range φ)
t : Set X
ht : MeasurableSet t
⊢ ‖μ t‖ₑ ≤ ‖μ (φ ⁻¹' φ '' t)‖ₑ
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ μ s
inst✝ : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
n : ℕ
⊢ m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)

Tactic:
induction n with

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ μ s
inst✝ : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
B : ∀ (n : ℕ), m (⋃ i, f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
n : ℕ
⊢ m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i)

Tactic:
A

Goal state after:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ μ s
inst✝ : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
B : ∀ (n : ℕ), m (⋃ i, f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i)
n : ℕ
⊢ ∑ i ∈ Finset.range n, m (f i) + m (⋃ i ∈ Set.Ici n, f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i)
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : {a} = ⋂ n, Ioc (u n) a
⊢ Tendsto (fun n ↦ hf.vectorMeasure (Ioc (u n) a)) atTop (𝓝 (hf.vectorMeasure {a}))

Tactic:
A

Goal state after:
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a : α
hf : BoundedVariationOn f univ
ha : ¬IsBot a
b : α
hb : b < a
u : ℕ → α
u_mono : StrictMono u
u_lim : Tendsto u atTop (𝓝 a)
u_lt_a : ∀ (n : ℕ), u n < a
A : {a} = ⋂ n, Ioc (u n) a
⊢ Tendsto (fun n ↦ hf.vectorMeasure (Ioc (u n) a)) atTop (𝓝 (hf.vectorMeasure (⋂ n, Ioc (u n) a)))
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
a : α
this✝ : Nonempty α
hlim : Tendsto f atBot (𝓝 (atBot.limUnder f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
this : Iic a = ⋃ n, Icc (u n) a
i j : ℕ
hij : i ≤ j
x : α
hx : x ∈ (fun n ↦ Icc (u n) a) i
⊢ x ∈ (fun n ↦ Icc (u n) a) j

Tactic:
by grind [Antitone]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case pos
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
f : X → E
s : Set X
hs : μ.variation s = 0
h's : MeasurableSet s
⊢ ∫ᵛ (x : X) in s, f x ∂[B; μ] = 0

Tactic:
have : (μ.restrict s).variation = 0 := by
    rw [variation_restrict h's]
    apply Measure.restrict_eq_zero.2 hs

Goal state after:
case pos
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
f : X → E
s : Set X
hs : μ.variation s = 0
h's : MeasurableSet s
this : (μ.restrict s).variation = 0
⊢ ∫ᵛ (x : X) in s, f x ∂[B; μ] = 0