mathlib-initiative/mathlib-tactics huggingface dataset:
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 Set.univ * μA {1} <
    ENNReal.ofReal (∫ (c : C), ((H.pushforward μA) { toContinuousMap := f, hasCompactSupport' := hf2 }) c ∂μC)
hc : Set.InjOn (⇑ψ) U
b : B
key : (Function.support fun a ↦ f (b * φ a)).Subsingleton
a : A
ha : (Function.support fun a ↦ f (b * φ a)) = {a}
⊢ μA.real {a} • f (b * φ a) ≤ (μA {1}).toReal

Tactic:
real_def,

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 Set.univ * μA {1} <
    ENNReal.ofReal (∫ (c : C), ((H.pushforward μA) { toContinuousMap := f, hasCompactSupport' := hf2 }) c ∂μC)
hc : Set.InjOn (⇑ψ) U
b : B
key : (Function.support fun a ↦ f (b * φ a)).Subsingleton
a : A
ha : (Function.support fun a ↦ f (b * φ a)) = {a}
⊢ (μA {a}).toReal • f (b * φ a) ≤ (μA {1}).toReal
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: 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)
⊢ 1 / p * Real.Gamma (↑(finrank ℝ E) / p) / Real.Gamma (↑(finrank ℝ E) / p + 1) * ↑(finrank ℝ E) = 1

Tactic:
Real.Gamma_add_one (ne_of_gt (by positivity))

Goal state after:
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)
⊢ 1 / p * Real.Gamma (↑(finrank ℝ E) / p) / (↑(finrank ℝ E) / p * Real.Gamma (↑(finrank ℝ E) / p)) * ↑(finrank ℝ E) = 1
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:
← inv_mul_lt_iff₀ (by positivity),

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.IntegralCharFun

Goal state before:
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:
have hx_ne : 2 * r⁻¹ * x ≠ 0 := by
        intro hx0
        simp only [hx0, Set.mem_ofPred_eq, abs_zero] at hx
        linarith

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|}
hx_ne : 2 * r⁻¹ * x ≠ 0
⊢ 2⁻¹ ≤ 1 - sinc (2 * r⁻¹ * x)
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:

Tactic:
μ.real {x | r < |x|}
  _ = μ.real {x | 2 < |2 * r⁻¹ * x|} := by
    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]
  _ = ∫ x in {x | 2 < |2 * r⁻¹ * x|}, 1 ∂μ := by simp
  _ = 2 * ∫ x in {x | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ := by
    rw [← integral_const_mul]
    congr with _
    rw [mul_inv_cancel₀ (by positivity)]
  _ ≤ 2 * ∫ x in {x | 2 < |2 * r⁻¹ * x|}, 1 - sinc (2 * r⁻¹ * x) ∂μ := by
    gcongr (2 : ℝ) * ?_
    refine setIntegral_mono_on ?_
      ((integrable_const _).sub (integrable_sinc_const_mul _)).integrableOn ?_ fun x hx ↦ ?_
    · exact Integrable.integrableOn <| by fun_prop
    · exact MeasurableSet.preimage measurableSet_Ioi (by fun_prop)
    · have hx_ne : 2 * r⁻¹ * x ≠ 0 := by
        intro hx0
        simp only [hx0, Set.mem_ofPred_eq, abs_zero] at hx
        linarith
      rw [le_sub_iff_add_le, ← le_sub_iff_add_le']
      norm_num
      rw [one_div]
      refine (sinc_le_inv_abs hx_ne).trans ?_
      exact (inv_le_inv₀ (by positivity) (by positivity)).mpr (le_of_lt hx)
  _ ≤ 2 * ∫ x, 1 - sinc (2 * r⁻¹ * x) ∂μ := by
    grw [setIntegral_le_integral (by fun_prop) <| ae_of_all _ fun x ↦ ?_]
    simp only [Pi.zero_apply, sub_nonneg]
    exact sinc_le_one (2 * r⁻¹ * x)
  _ ≤ 2 * ‖∫ x, 1 - sinc (2 * r⁻¹ * x) ∂μ‖ := by
    gcongr
    exact Real.le_norm_self _
  _ = 2⁻¹ * r *
      ‖2 * (r : ℂ)⁻¹ + 2 * r⁻¹ - 2 * (2 * r⁻¹) * ∫ x, sinc (2 * r⁻¹ * x) ∂μ‖ := by
    norm_cast
    rw [← two_mul, mul_assoc 2, ← mul_sub, norm_mul, Real.norm_ofNat, ← mul_assoc,
      ← mul_one_sub, norm_mul, Real.norm_of_nonneg (r := 2 * r⁻¹) (by positivity), ← mul_assoc]
    congr
    · ring_nf
      rw [mul_inv_cancel₀ (by positivity), one_mul]
    · rw [integral_sub (integrable_const _) (integrable_sinc_const_mul _)]
      simp
  _ = 2⁻¹ * r * ‖∫ t in (-2 * r⁻¹)..(2 * r⁻¹), 1 - charFun μ t‖ := by
    rw [intervalIntegral.integral_sub intervalIntegrable_const intervalIntegrable_charFun, neg_mul,
      integral_charFun_Icc (by positivity)]
    simp

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

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

Tactic:
← toLp_smul,

Goal state after:
ι : 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)
nm_zero : ‖toLp (ENNReal.ofReal p) 0‖ = 0
eq_zero : ∀ (x : ι → ℝ), ‖toLp (ENNReal.ofReal p) x‖ = 0 ↔ x = 0
nm_neg : ∀ (x : ι → ℝ), ‖toLp (ENNReal.ofReal p) (-x)‖ = ‖toLp (ENNReal.ofReal p) x‖
nm_add : ∀ (x y : ι → ℝ), ‖toLp (ENNReal.ofReal p) (x + y)‖ ≤ ‖toLp (ENNReal.ofReal p) x‖ + ‖toLp (ENNReal.ofReal p) y‖
nm_smul : ∀ (r : ℝ) (x : ι → ℝ), ‖toLp (ENNReal.ofReal p) (r • x)‖ ≤ ‖r‖ * ‖toLp (ENNReal.ofReal p) x‖
⊢ volume {x | ∑ i, |x i| ^ p < 1} = ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

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

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
this✝ : (ENNReal.ofReal p).toReal = p
eq_norm : ∀ (x : ι → ℝ), ‖toLp (ENNReal.ofReal p) x‖ = (∑ i, |x i| ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : ‖toLp (ENNReal.ofReal p) 0‖ = 0
eq_zero : ∀ (x : ι → ℝ), ‖toLp (ENNReal.ofReal p) x‖ = 0 ↔ x = 0
nm_neg : ∀ (x : ι → ℝ), ‖toLp (ENNReal.ofReal p) (-x)‖ = ‖toLp (ENNReal.ofReal p) x‖
nm_add : ∀ (x y : ι → ℝ), ‖toLp (ENNReal.ofReal p) (x + y)‖ ≤ ‖toLp (ENNReal.ofReal p) x‖ + ‖toLp (ENNReal.ofReal p) y‖
nm_smul : ∀ (r : ℝ) (x : ι → ℝ), ‖toLp (ENNReal.ofReal p) (r • x)‖ ≤ ‖r‖ * ‖toLp (ENNReal.ofReal p) x‖
⊢ volume {x | (∑ i, |x i| ^ p) ^ (1 / p) ≤ r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

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

Tactic:
← toLp_smul,

Goal state after:
ι : 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)
nm_zero : ‖toLp (ENNReal.ofReal p) 0‖ = 0
eq_zero : ∀ (x : ι → ℂ), ‖toLp (ENNReal.ofReal p) x‖ = 0 ↔ x = 0
nm_neg : ∀ (x : ι → ℂ), ‖toLp (ENNReal.ofReal p) (-x)‖ = ‖toLp (ENNReal.ofReal p) x‖
nm_add : ∀ (x y : ι → ℂ), ‖toLp (ENNReal.ofReal p) (x + y)‖ ≤ ‖toLp (ENNReal.ofReal p) x‖ + ‖toLp (ENNReal.ofReal p) y‖
nm_smul : ∀ (r : ℝ) (x : ι → ℂ), ‖toLp (ENNReal.ofReal p) (r • x)‖ ≤ ‖r‖ * ‖toLp (ENNReal.ofReal p) x‖
⊢ volume {x | ∑ i, ‖x i‖ ^ p < 1} =
    ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
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
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
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
n : ℕ
⊢ ∃ ν ∈ {ρ | ρ.mass ≤ C ∧ ρ ((partialSups K) n)ᶜ = 0}, Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 ν)

Tactic:
by
      simp only [Tendsto]
      rw [← Ultrafilter.coe_map]
      apply IsCompact.ultrafilter_le_nhds'
        (isCompact_setOfPred_finiteMeasure_le_of_isCompact C (A n))
      simp only [null_iff_toMeasure_null, Ultrafilter.mem_map, preimage_ofPred_eq]
      filter_upwards [hf] with ρ hρ
      simp only [restrict_mass, restrict_measure_eq,
        Measure.restrict_apply (A n).measurableSet.compl]
      refine ⟨(apply_le_mass ρ _).trans hρ.1, ?_⟩
      convert! measure_empty (μ := (ρ : Measure E))
      apply disjoint_iff.1
      apply disjoint_compl_left.mono_right
      exact le_trans sdiff_le (le_partialSups _ _)

Goal state after:
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
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
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))
this✝¹ : Tendsto (fun n ↦ ∑ i ∈ Finset.range (n + 1), ↑(ν i) univ) atTop (𝓝 (∑' (i : ℕ), ↑(ν i) univ))
n : ℕ
this✝ : ∑ i ∈ Finset.range (n + 1), ↑(ν i) univ = ↑(∑ i ∈ Finset.range (n + 1), ν i) univ
this :
  Tendsto (fun μ ↦ (∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i)).mass) (↑f)
    (𝓝 (∑ i ∈ Finset.range (n + 1), ν i).mass)
μ : FiniteMeasure E
hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n
⊢ (μ.restrict ((partialSups K) n)).mass ≤ C

Tactic:
restrict_mass

Goal state after:
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)
h : NormalSpace E ∨ Monotone K
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))
this✝¹ : Tendsto (fun n ↦ ∑ i ∈ Finset.range (n + 1), ↑(ν i) univ) atTop (𝓝 (∑' (i : ℕ), ↑(ν i) univ))
n : ℕ
this✝ : ∑ i ∈ Finset.range (n + 1), ↑(ν i) univ = ↑(∑ i ∈ Finset.range (n + 1), ν i) univ
this :
  Tendsto (fun μ ↦ (∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i)).mass) (↑f)
    (𝓝 (∑ i ∈ Finset.range (n + 1), ν i).mass)
μ : FiniteMeasure E
hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n
⊢ μ ((partialSups K) n) ≤ C
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

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

Tactic:
← toLp_smul,

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : 0 < p
this✝ : (ENNReal.ofReal p).toReal = p
eq_norm : ∀ (x : ι → ℂ), ‖toLp (ENNReal.ofReal p) x‖ = (∑ i, ‖x i‖ ^ p) ^ (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : ‖toLp (ENNReal.ofReal p) 0‖ = 0
eq_zero : ∀ (x : ι → ℂ), ‖toLp (ENNReal.ofReal p) x‖ = 0 ↔ x = 0
nm_neg : ∀ (x : ι → ℂ), ‖toLp (ENNReal.ofReal p) (-x)‖ = ‖toLp (ENNReal.ofReal p) x‖
nm_add : ∀ (x y : ι → ℂ), ‖toLp (ENNReal.ofReal p) (x + y)‖ ≤ ‖toLp (ENNReal.ofReal p) x‖ + ‖toLp (ENNReal.ofReal p) y‖
nm_smul : ∀ (r : ℝ) (x : ι → ℂ), ‖toLp (ENNReal.ofReal p) (r • x)‖ ≤ ‖r‖ * ‖toLp (ENNReal.ofReal p) x‖
⊢ volume {x | (∑ i, ‖x i‖ ^ p) ^ (1 / p) ≤ r} =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: case refine_2
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)‖
r : ℝ
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
⊢ ∀ (n : ℕ), ∀ᵐ (a : ℝ) ∂volume.restrict (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)), ‖1 - charFun (μ n) (a • z)‖ ≤ 2

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)‖
r : ℝ
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)),
    Tendsto (fun n ↦ 1 - charFun (μ n) (a • z)) atTop (𝓝 (1 - f (a • z)))

Tactic:
· exact fun _ ↦ ae_of_all _ fun _ ↦ norm_one_sub_charFun_le_two

Goal state after:
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)‖
r : ℝ
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)),
    Tendsto (fun n ↦ 1 - charFun (μ n) (a • z)) atTop (𝓝 (1 - f (a • z)))
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition ⟨⋃ i, s i, ⋯⟩
hQ : b < ∑ p ∈ Q.parts, f ↑p
s' : ℕ → Subtype MeasurableSet := fun i ↦ ⟨s i, ⋯⟩
P : (i : ℕ) → Finpartition (s' i) := fun i ↦ Q.restrict ⋯
q : Subtype MeasurableSet
hq : q ∈ Q.parts
⊢ ↑q = ⋃ i, ↑q ∩ s i

Tactic:
rw [← Set.inter_iUnion]

Goal state after:
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition ⟨⋃ i, s i, ⋯⟩
hQ : b < ∑ p ∈ Q.parts, f ↑p
s' : ℕ → Subtype MeasurableSet := fun i ↦ ⟨s i, ⋯⟩
P : (i : ℕ) → Finpartition (s' i) := fun i ↦ Q.restrict ⋯
q : Subtype MeasurableSet
hq : q ∈ Q.parts
⊢ ↑q = ↑q ∩ ⋃ i, s i
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ t ∈ 𝒜, μ t ≠ ∞ ∧ μ (s ∆ t) < ENNReal.ofReal ε

Tactic:
by
  rcases h𝒜.approx s ms hμs ε ε_pos with ⟨t, t_mem, ht⟩
  exact ⟨t, t_mem, (measure_ne_top_iff_of_symmDiff <| ne_top_of_lt ht).1 hμs, ht⟩

Goal state after:
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
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 : Monotone K
this✝² : Tendsto (fun m ↦ ∑ i ∈ Finset.range (m + 1), ↑(ν i) (K n)ᶜ) atTop (𝓝 (∑' (i : ℕ), ↑(ν i) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this✝¹ : ∑ i ∈ Finset.range (m + 1), ↑(ν i) (K n)ᶜ = ∑ i ∈ Finset.Ioc n m, ↑(ν i) (K n)ᶜ
this✝ :
  Tendsto (fun μ ↦ (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)).mass) (↑f) (𝓝 (∑ i ∈ Finset.Ioc n m, ν i).mass)
μ : FiniteMeasure E
hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n
this : ∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i) = μ.restrict (K m \ K n)
⊢ (μ.restrict (K m \ K n)).mass ≤ u n

Tactic:
restrict_mass

Goal state after:
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 : Monotone K
this✝² : Tendsto (fun m ↦ ∑ i ∈ Finset.range (m + 1), ↑(ν i) (K n)ᶜ) atTop (𝓝 (∑' (i : ℕ), ↑(ν i) (K n)ᶜ))
m : ℕ
hm : n ≤ m
this✝¹ : ∑ i ∈ Finset.range (m + 1), ↑(ν i) (K n)ᶜ = ∑ i ∈ Finset.Ioc n m, ↑(ν i) (K n)ᶜ
this✝ :
  Tendsto (fun μ ↦ (∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i)).mass) (↑f) (𝓝 (∑ i ∈ Finset.Ioc n m, ν i).mass)
μ : FiniteMeasure E
hμ : μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n
this : ∑ i ∈ Finset.Ioc n m, μ.restrict (disjointed K i) = μ.restrict (K m \ K n)
⊢ μ (K m \ K n) ≤ u n