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

Goal state before:
pp: Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
⊢ ∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist (ofMeasure x) (ofMeasure P) < ε

Tactic:
obtain ⟨Es, Es_mble, Es_bdd, Es_diam, Es_cover, Es_disjoint⟩ :=
    SeparableSpace.exists_measurable_partition_diam_le Ω third_ε_pos

Goal state after:
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : ⋃ n, Es n = univ
Es_disjoint : Pairwise fun n m ↦ Disjoint (Es n) (Es m)
⊢ ∀ᶠ (x : ProbabilityMeasure Ω) in 𝓝 P, dist (ofMeasure x) (ofMeasure P) < ε
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

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

Tactic:
intervalIntegral_integral_swap h_int

Goal state after:
μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
⊢ ∫ (y : ℝ), ∫ (x : ℝ) in -r..r, cexp (↑x * ↑y * I) ∂μ = ∫ (y : ℝ), ∫ (x : ℝ) in -r..r, cexp (↑x * ↑y * I) ∂μ
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: case neg.refine_2
μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
y : ℝ
hy : ¬y = 0
h : ↑y * ∫ (x : ℝ) in -r..r, cexp (↑y * ↑x * I) = ∫ (x : ℝ) in -(y * r)..y * r, cexp (↑x * I)
⊢ ∫ (x : ℝ) in -r..r, cexp (↑x * ↑y * I) = (↑y)⁻¹ * ∫ (x : ℝ) in -(y * r)..y * r, cexp (↑x * I)

Tactic:
← h,

Goal state after:
case neg.refine_2
μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
y : ℝ
hy : ¬y = 0
h : ↑y * ∫ (x : ℝ) in -r..r, cexp (↑y * ↑x * I) = ∫ (x : ℝ) in -(y * r)..y * r, cexp (↑x * I)
⊢ ∫ (x : ℝ) in -r..r, cexp (↑x * ↑y * I) = (↑y)⁻¹ * (↑y * ∫ (x : ℝ) in -r..r, cexp (↑y * ↑x * I))
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:
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]

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 + toLp (ENNReal.ofReal p) 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_add,

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 : ι → ℝ), ‖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))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: case inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i, |x i| ^ p) ^ (1 / p)
hr : 0 < r
⊢ volume {x | (∑ i, |x i| ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))

Tactic:
rw [← volume_sum_rpow_lt_one _ hp, ← ofReal_pow (le_of_lt hr), ← finrank_pi ℝ]

Goal state after:
case inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i, |x i| ^ p) ^ (1 / p)
hr : 0 < r
⊢ volume {x | (∑ i, |x i| ^ p) ^ (1 / p) < r} = ENNReal.ofReal (r ^ finrank ℝ (ι → ℝ)) * volume {x | ∑ i, |x i| ^ 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 + toLp (ENNReal.ofReal p) 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_add,

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 : ι → ℝ), ‖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))
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 + toLp (ENNReal.ofReal p) 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_add,

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 : ι → ℂ), ‖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))
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 + toLp (ENNReal.ofReal p) 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_add,

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 : ι → ℂ), ‖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))
Module: Mathlib.MeasureTheory.Measure.TightNormed

Goal state before:
pp: E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
h : Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖}) atTop (𝓝 0)
⊢ IsTightMeasureSet S

Tactic:
refine isTightMeasureSet_of_tendsto_measure_compl_closedBall (x := 0) ?_

Goal state after:
E : Type u_1
mE : MeasurableSpace E
S : Set (Measure E)
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
h : Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖}) atTop (𝓝 0)
⊢ Tendsto (fun r ↦ ⨆ μ ∈ S, μ (Metric.closedBall 0 r)ᶜ) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Measure.TightNormed

Goal state before:
pp: 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 : ℝ
⊢ ⨆ μ ∈ S, ∑ i, μ {x | r / √↑(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖} ≤
    ∑ i, ⨆ μ ∈ S, μ {x | r / √↑(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖}

Tactic:
refine iSup_le fun μ ↦ (iSup_le fun hμS ↦ ?_)

Goal state after:
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
⊢ ∑ i, μ {x | r / √↑(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖} ≤ ∑ i, ⨆ μ ∈ S, μ {x | r / √↑(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖}
Module: Mathlib.MeasureTheory.Measure.MeasuredSets

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε✝ : ℝ≥0∞
hε : 0 < ε✝
f : ℕ → Set α
f_disj : Pairwise (Function.onFun Disjoint f)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ) (ε : ℝ≥0∞), 0 < ε → ∃ t ∈ C, μ (t ∆ f i) < ε
ε : ℝ≥0∞
εpos : 0 < ε
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε / 2
t : ℕ → Set α
tC : ∀ (i : ℕ), t i ∈ C
ht : ∀ (i : ℕ), μ (t i ∆ f i) < δ i
this : Tendsto (fun n ↦ μ (⋃ i ∈ Ici n, f i)) atTop (𝓝 0)
n : ℕ
hn : μ (⋃ i ∈ Ici n, f i) < ε / 2
⊢ ∑ i ∈ Finset.range n, μ (t i ∆ f i) + μ (⋃ i ∈ Ici n, f i) ≤ ∑ i ∈ Finset.range n, δ i + μ (⋃ i ∈ Ici n, f i)

Tactic:
by
      gcongr with i; exact (ht i).le

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 : ↑(∑ i ∈ Finset.Ioc n m, ν i) univ ≤ ↑(u n)
⊢ ∑ i ∈ Finset.Ioc n m, ↑(ν i) (K n)ᶜ ≤ ↑(u n)

Tactic:
apply le_trans _ this

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 := ⋯
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 : ↑(∑ i ∈ Finset.Ioc n m, ν i) univ ≤ ↑(u n)
⊢ ∑ i ∈ Finset.Ioc n m, ↑(ν i) (K n)ᶜ ≤ ↑(∑ i ∈ Finset.Ioc n m, ν i) univ
Module: Mathlib.MeasureTheory.Measure.ResolventTransform

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : MeasurableSpace 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : RCLike A
inst✝¹ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
ha : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
s : Set A := ball a (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ (⇑(algebraMap 𝕜 A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
resolvent'_bound : ∀ᵐ (x : 𝕜) ∂μ, ∀ w ∈ s, ‖resolvent w x ^ 2‖ ≤ (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)⁻¹ ^ 2
h_deriv : ∀ᵐ (x : 𝕜) ∂μ, ∀ w ∈ s, HasDerivAt (fun w ↦ resolvent w x) (resolvent w x ^ 2) w
⊢ a ∉ ⇑(algebraMap 𝕜 A) '' μ.support

Tactic:
by simp [ha]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
⊢ ∀ (s : Set α), μ s = 0 ∨ μ s = 1

Tactic:
intro s
  by_cases hs : MeasurableSet s
  · exact IsZeroOneMeasure.zero_one₀ hs
  · obtain ⟨t, _, mt, ht⟩ := exists_measurable_superset μ s
    rw [← ht]
    exact IsZeroOneMeasure.zero_one₀ mt

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
s : Set X
hs : MeasurableSet s
a : ℝ≥0∞
ha : a < preVariationFun (fun x ↦ ‖μ x‖ₑ) s
⊢ ∃ P, (∀ t ∈ P, t ⊆ s) ∧ (↑P).PairwiseDisjoint id ∧ (∀ t ∈ P, MeasurableSet t) ∧ a < ∑ p ∈ P, ‖μ p‖ₑ

Tactic:
obtain ⟨P, hP⟩ : ∃ P : Finpartition (⟨s, hs⟩ : Subtype MeasurableSet),
      a < ∑ p ∈ P.parts, (fun x ↦ ‖μ x‖ₑ) p :=
    preVariation.exists_Finpartition_sum_gt (‖μ ·‖ₑ) _ ha

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
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
⊢ ∃ P, (∀ t ∈ P, t ⊆ s) ∧ (↑P).PairwiseDisjoint id ∧ (∀ t ∈ P, MeasurableSet t) ∧ a < ∑ p ∈ P, ‖μ p‖ₑ
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
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
hμ : preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≠ ∞
⊢ ∃ P,
    (∀ t ∈ P, t ⊆ s) ∧
      (↑P).PairwiseDisjoint id ∧ (∀ t ∈ P, MeasurableSet t) ∧ preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≤ ∑ x ∈ P, ‖μ x‖ₑ + ε

Tactic:
obtain ⟨P, hP⟩ : ∃ P : Finpartition (⟨s, hs⟩ : Subtype MeasurableSet),
      preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≤ ∑ p ∈ P.parts, (fun x ↦ ‖μ x‖ₑ) ↑p + ε :=
    preVariation.exists_Finpartition_sum_ge' (‖μ ·‖ₑ) hs hε hμ

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
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 + ε
⊢ ∃ P,
    (∀ t ∈ P, t ⊆ s) ∧
      (↑P).PairwiseDisjoint id ∧ (∀ t ∈ P, MeasurableSet t) ∧ preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≤ ∑ x ∈ P, ‖μ x‖ₑ + ε
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: case neg
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
⊢ μ s = 0

Tactic:
· exact μ.not_measurable hsm

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

Goal state before:
pp: case inl.refine_3
X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
s : Set X
hs : MeasurableSet s
a : ℝ≥0∞
ha : a < (variation μ) s
P : Finset (Set X)
Ps : ∀ t ∈ P, t ⊆ s
P_disj : (↑P).PairwiseDisjoint id
P_meas : ∀ t ∈ P, MeasurableSet t
hP : a < ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ + ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ
I : ∑ p ∈ P with 0 ≤ μ p, ‖μ p‖ₑ = ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ
J : ∑ p ∈ P with ¬0 ≤ μ p, ‖μ p‖ₑ = ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ
h : ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ ≤ ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ
⊢ a < ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ + ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ

Tactic:
· exact hP.trans_le (by gcongr)

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

Goal state before:
pp: case inr.refine_3
X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
s : Set X
hs : MeasurableSet s
a : ℝ≥0∞
ha : a < (variation μ) s
P : Finset (Set X)
Ps : ∀ t ∈ P, t ⊆ s
P_disj : (↑P).PairwiseDisjoint id
P_meas : ∀ t ∈ P, MeasurableSet t
hP : a < ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ + ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ
I : ∑ p ∈ P with 0 ≤ μ p, ‖μ p‖ₑ = ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ
J : ∑ p ∈ P with ¬0 ≤ μ p, ‖μ p‖ₑ = ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ
h : ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ ≤ ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ
⊢ a < ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ + ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ

Tactic:
· exact hP.trans_le (by gcongr)

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

Goal state before:
pp: case insert
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
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
s : ι → Set X
a✝ : ι
s✝ : Finset ι
hat : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, MeasurableSet (s i)) →
    (↑s✝).Pairwise (Disjoint on s) →
      (∀ i ∈ s✝, μ.IntegrableOn f (s i)) →
        ∫ᵛ (x : X) in ⋃ i ∈ s✝, s i, f x ∂[B; μ] = ∑ i ∈ s✝, ∫ᵛ (x : X) in s i, f x ∂[B; μ]
hs : ∀ i ∈ insert a✝ s✝, MeasurableSet (s i)
h's : (↑(insert a✝ s✝)).Pairwise (Disjoint on s)
hf : ∀ i ∈ insert a✝ s✝, μ.IntegrableOn f (s i)
⊢ ∫ᵛ (x : X) in ⋃ i ∈ insert a✝ s✝, s i, f x ∂[B; μ] = ∑ i ∈ insert a✝ s✝, ∫ᵛ (x : X) in s i, f x ∂[B; μ]

Tactic:
simp only [Finset.coe_insert, Finset.forall_mem_insert, Set.pairwise_insert,
      Finset.set_biUnion_insert] at hs hf h's ⊢
    rw [setIntegral_union]
    · rw [Finset.sum_insert hat, IH hs.2 h's.1 hf.2]
    · simp only [disjoint_iUnion_right]
      exact fun i hi => (h's.2 i hi (ne_of_mem_of_not_mem hi hat).symm).1
    · exact hs.1
    · exact Finset.measurableSet_biUnion _ hs.2
    · exact hf.1
    · apply IntegrableOn.biUnion_finset hs.2 hf.2

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

Goal state before:
pp: 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
f g : X → E
s : Set X
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : μ.IntegrableOn f s
hg : μ.IntegrableOn g sᶜ
⊢ ∫ᵛ (x : X), s.piecewise f g x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ] + ∫ᵛ (x : X) in sᶜ, g x ∂[B; μ]

Tactic:
rw [← Set.indicator_add_compl_eq_piecewise,
    integral_add (hf.integrable_indicator hs) (hg.integrable_indicator hs.compl),
    integral_indicator hs, integral_indicator hs.compl]

Goal state after: