mathlib-initiative/mathlib-tactics huggingface dataset:
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
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)

Tactic:
have h_le n r (hr : 0 < r) : (μ n).real {x | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ :=
    measureReal_abs_inner_gt_le_integral_charFun hr

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
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)‖
⊢ Tendsto (fun r ↦ limsup (fun n ↦ (μ n).real {x | r < ‖⟪z, x⟫‖}) atTop) atTop (𝓝 0)
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)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
r : ℝ
hr : 0 < r
u : ℝ
hu : ∀ᶠ (n : ℕ) in atTop, (μ n).real {x | r < ‖⟪z, x⟫‖} ≤ u
⊢ 0 ≤ u

Tactic:
· exact ENNReal.toReal_nonneg.trans hu.exists.choose_spec

Goal state after:
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:
refine ENNReal.tsum_le_of_sum_range_le fun n ↦ ?_

Goal state after:
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
⊢ ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ i, s i)
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
this : 1 ≤ μ univ
⊢ μ univ = 1

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s = 1
hμt : μ t = 1
h✝ : μ (s ∩ t) = 0
this : 1 - μ (s ∩ t) ≤ 0
⊢ False

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s = 1
hμt : μ t = 1
h✝ : μ (s ∩ t) = 0
⊢ μ univ - μ s + μ tᶜ ≤ 0

Tactic:
measure_univ hμs,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s = 1
hμt : μ t = 1
h✝ : μ (s ∩ t) = 0
⊢ 1 - μ s + μ tᶜ ≤ 0
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:

Tactic:
μ.real ((⋃ n, f n) ∆ (⋃ n ∈ (Finset.range (N + 1)), g n))
            ≤ (μ ((⋃ n, f n) \ ((⋃ n ∈ (Finset.range (N + 1)), f n)) ∪
              ((⋃ n ∈ (Finset.range (N + 1)), f n) ∆
              (⋃ n ∈ (Finset.range (N + 1)), g ↑n)))).toReal :=
                toReal_mono (measure_ne_top _ _)
                  (measure_mono <| symmDiff_of_ge (iUnion_subset <|
                  fun i ↦ iUnion_subset (fun _ ↦ subset_iUnion f i)) ▸ symmDiff_triangle ..)
          _ ≤ (μ ((⋃ n, f n) \
              ((⋃ n ∈ (Finset.range (N + 1)), f n)))).toReal +
              (μ ((⋃ n ∈ (Finset.range (N + 1)), f n) ∆
              (⋃ n ∈ (Finset.range (N + 1)), g ↑n))).toReal := by
                rw [← toReal_add (measure_ne_top _ _) (measure_ne_top _ _)]
                exact toReal_mono (add_ne_top.2 ⟨measure_ne_top _ _, measure_ne_top _ _⟩) <|
                  measure_union_le _ _
          _ < ε := by
                rw [← add_halves ε]
                apply _root_.add_lt_add
                · rw [measure_sdiff (h_fin := measure_ne_top _ _),
                    toReal_sub_of_le (ha := measure_ne_top _ _)]
                  · apply lt_of_le_of_lt (sub_le_dist ..)
                    simp only [Finset.mem_range, Nat.lt_add_one_iff]
                    exact (dist_comm (α := ℝ) .. ▸ hN N (le_refl N))
                  · exact measure_mono <| iUnion_subset <|
                      fun i ↦ iUnion_subset fun _ ↦ subset_iUnion f i
                  · exact iUnion_subset <| fun i ↦ iUnion_subset (fun _ ↦ subset_iUnion f i)
                  · exact MeasurableSet.biUnion (countable_coe_iff.1 inferInstance)
                      (fun n _ ↦ (hf n).1.nullMeasurableSet)
                · calc
                    (μ ((⋃ n ∈ (Finset.range (N + 1)), f n) ∆
                    (⋃ n ∈ (Finset.range (N + 1)), g ↑n))).toReal
                      ≤ μ.real (⋃ n ∈ (Finset.range (N + 1)), f n ∆ g n) :=
                          toReal_mono (measure_ne_top _ _) (measure_mono biSup_symmDiff_biSup_le)
                    _ ≤ ∑ n ∈ Finset.range (N + 1), μ.real (f n ∆ g n) := by
                          simp_rw [measureReal_def, ← toReal_sum (fun _ _ ↦ measure_ne_top _ _)]
                          exact toReal_mono (ne_of_lt <| sum_lt_top.2 fun _ _ ↦ measure_lt_top μ _)
                            (measure_biUnion_finset_le _ _)
                    _ < ∑ n ∈ Finset.range (N + 1), (ε / (2 * (N + 1))) :=
                          Finset.sum_lt_sum (fun i _ ↦ le_of_lt (hg i)) ⟨0, by simp, hg 0⟩
                    _ ≤ ε / 2 := by
                          simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul,
                            Nat.cast_add, Nat.cast_one]
                          rw [div_mul_eq_div_mul_one_div, ← mul_assoc, mul_comm ((N : ℝ) + 1),
                            mul_assoc]
                          exact mul_le_of_le_one_right (by linarith [ε_pos]) <|
                            le_of_eq <| mul_one_div_cancel <| Nat.cast_add_one_ne_zero _

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

Goal state before:
pp: case inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
h : μ univ = 0
⊢ IsProbabilityMeasure μ

Tactic:
simp_all

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

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep : ∀ x ∈ univ, ∀ y ∈ univ, (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : ℕ → Set α := fun n ↦ if h : μ (A n) = 1 then A n else (A n)ᶜ
mBn : MeasurableSet (⋂ n, B n)
n : ℕ
h : μ (A n) = 1
⊢ μ (A n)ᶜ = 0

Tactic:
simp_all

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

Goal state before:
pp: case neg.inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep : ∀ x ∈ univ, ∀ y ∈ univ, (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : ℕ → Set α := fun n ↦ if h : μ (A n) = 1 then A n else (A n)ᶜ
mBn : MeasurableSet (⋂ n, B n)
n : ℕ
h : ¬μ (A n) = 1
h₁ : μ (A n) = 1
⊢ μ (A n) = 0

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep : ∀ x ∈ univ, ∀ y ∈ univ, (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : ℕ → Set α := fun n ↦ if h : μ (A n) = 1 then A n else (A n)ᶜ
mBn : MeasurableSet (⋂ n, B n)
hBn : μ ∅ = 1
h : ⋂ n, B n = ∅
⊢ False

Tactic:
simp_all

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

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

Tactic:
simp_all

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

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

Tactic:
simp_all

Goal state after:
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior sᶜ
H : Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 1)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
this : 0 < ε n
⊢ 0 < ENNReal.ofReal ((2 * (ε n / 4)) ^ Fintype.card ι) →
    ENNReal.ofReal ((2 * (ε n / 4)) ^ Fintype.card ι) < ENNReal.ofReal ((2 * ε n) ^ Fintype.card ι) →
      ENNReal.ofReal ((2 * ε n) ^ Fintype.card ι) ≠ 0

Tactic:
simp_all

Goal state after:
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: case pos
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
x✝ : ℝ
⊢ x ∈ frontier sᶜ

Tactic:
rwa [frontier_compl]

Goal state after:
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: case pos
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∈ closure s
x✝ : ℝ
⊢ x ∈ frontier sᶜ

Tactic:
rwa [frontier_compl]

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

Goal state before:
pp: case h
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝² : PseudoMetricSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : ⋃ i, U i = univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : ℕ → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction : ∀ (k : ℕ), ↑((μ k) (⋃ i, ⋃ (_ : i ≤ k), U i)) ≤ 1 - ↑(NNReal.mk ε hε')
μlim : ProbabilityMeasure 𝓧
left✝ : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
b : ℝ
c : ℕ
h : ∀ (b_1 : ℕ), c ≤ b_1 → b ≤ ↑((μ (sub b_1)) (⋃ i, ⋃ (_ : i ≤ sub b_1), U i))
⊢ ↑((μ (sub c)) (⋃ i, ⋃ (_ : i ≤ sub c), U i)) ≤ ENNReal.ofReal (1 - ε)

Tactic:
apply le_trans (hcontradiction (sub c))

Goal state after:
case h
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝² : PseudoMetricSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : ⋃ i, U i = univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : ℕ → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction : ∀ (k : ℕ), ↑((μ k) (⋃ i, ⋃ (_ : i ≤ k), U i)) ≤ 1 - ↑(NNReal.mk ε hε')
μlim : ProbabilityMeasure 𝓧
left✝ : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
n : ℕ
b : ℝ
c : ℕ
h : ∀ (b_1 : ℕ), c ≤ b_1 → b ≤ ↑((μ (sub b_1)) (⋃ i, ⋃ (_ : i ≤ sub b_1), U i))
⊢ 1 - ↑(NNReal.mk ε hε') ≤ ENNReal.ofReal (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
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet Q.parts).sup id) := Q.ofSubset ⋯ ⋯
defQ' : Q' = Q.ofSubset ⋯ ⋯
hQ' : ∀ t ∈ Q'.parts, t ⊆ s
⊢ ∀ p ∈ Q.parts, p ∉ filter MeasurableSet Q.parts → ‖μ p‖ₑ = 0

Tactic:
simp_all

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

Goal state before:
pp: case inl
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
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet Q.parts).sup id) := Q.ofSubset ⋯ ⋯
defQ' : Q' = Q.ofSubset ⋯ ⋯
hQ' : ∀ t ∈ Q'.parts, t ⊆ s
p : Set X
hp : p ∈ (Q'.extendOfLE ⋯).parts
h : p ∈ Q'.parts
⊢ MeasurableSet p

Tactic:
simp_all

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

Goal state before:
pp: case pos
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
E : Set X
hE : MeasurableSet E
hE' : ⟨E, hE⟩ = ⊥
⊢ ‖μ E‖ₑ ≤ μ.variation E

Tactic:
simp_all

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 : μ.ennrealVariation s = 0
hsm : MeasurableSet s
this : ‖μ s‖ₑ ≤ 0
⊢ μ s = 0

Tactic:
simp_all

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 : 𝕜
hc : c ≠ 0
⊢ ‖c‖₊ • (c⁻¹ • c • μ).variation ≤ ‖c‖₊ • ‖c⁻¹‖₊ • (c • μ).variation

Tactic:
gcongr
    exact variation_smul_le

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
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
β : Type u_7
inst✝ : MeasurableSpace β
φ : X → β
f : β → E
hφ : MeasurableEmbedding φ
s : Set β
hs : MeasurableSet s
⊢ ∫ᵛ (y : β) in s, f y ∂[B; μ.map φ] = ∫ᵛ (x : X) in φ ⁻¹' s, f (φ x) ∂[B; μ]

Tactic:
rw [restrict_map μ hφ.measurable hs, hφ.integral_map_vectorMeasure]

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

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
h : μ.semivariation univ = ∞
t : Set X → Set X
t_meas : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → MeasurableSet (t s)
t_subs : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → t s ⊆ s
t_var : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → μ.semivariation (t s) = ∞
ht : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → 1 ≤ ‖μ (s \ t s)‖ₑ
s : ℕ → Set X := fun n ↦ t^[n] univ
hs : ∀ (n : ℕ), MeasurableSet (s n) ∧ μ.semivariation (s n) = ∞
⊢ False

Tactic:
let u n := s n \ s (n + 1)

Goal state after:
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
h : μ.semivariation univ = ∞
t : Set X → Set X
t_meas : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → MeasurableSet (t s)
t_subs : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → t s ⊆ s
t_var : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → μ.semivariation (t s) = ∞
ht : ∀ (s : Set X), MeasurableSet s → μ.semivariation s = ∞ → 1 ≤ ‖μ (s \ t s)‖ₑ
s : ℕ → Set X := fun n ↦ t^[n] univ
hs : ∀ (n : ℕ), MeasurableSet (s n) ∧ μ.semivariation (s n) = ∞
u : ℕ → Set X := fun n ↦ s n \ s (n + 1)
⊢ False
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case pos.h_ae
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
H : Type u_6
mX : MeasurableSpace X
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedAddCommGroup H
μ : VectorMeasure X F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace ℝ G
inst✝ : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
f✝ : X → H
C : H →L[ℝ] E
hf✝ : Integrable f✝ μ.variation
hG : CompleteSpace G
f g : X → H
hfg : f =ᵐ[μ.variation] g
a✝ : Integrable f μ.variation
hf : ∫ᵛ (y : X), C (f y) ∂[B; μ] = ∫ᵛ (y : X), f y ∂[B ∘SL C; μ]
⊢ ∫ᵛ (y : X), C (g y) ∂[B; μ] = ∫ᵛ (y : X), g y ∂[B ∘SL C; μ]

Tactic:
have : ∀ᵐ x ∂μ.variation, C (f x) = C (g x) := by
      filter_upwards [hfg] with x hx using by simp [hx]

Goal state after:
case pos.h_ae
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
H : Type u_6
mX : MeasurableSpace X
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedAddCommGroup H
μ : VectorMeasure X F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace ℝ G
inst✝ : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
f✝ : X → H
C : H →L[ℝ] E
hf✝ : Integrable f✝ μ.variation
hG : CompleteSpace G
f g : X → H
hfg : f =ᵐ[μ.variation] g
a✝ : Integrable f μ.variation
hf : ∫ᵛ (y : X), C (f y) ∂[B; μ] = ∫ᵛ (y : X), f y ∂[B ∘SL C; μ]
this : ∀ᵐ (x : X) ∂μ.variation, C (f x) = C (g x)
⊢ ∫ᵛ (y : X), C (g y) ∂[B; μ] = ∫ᵛ (y : X), g y ∂[B ∘SL C; μ]
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsCancelAdd M
a : M
t : Finset M
ih : ∀ m < t.card, ∀ (a : M) (t : Finset M), t.card = m → IsProperSemilinearSet (a +ᵥ ↑(closure ↑t))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : ∑ x ∈ t', f x • x = ∑ x ∈ t \ t', f x • x
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ),
      g i = m → a +ᵥ ∑ a ∈ t, g a • a ∈ ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ ↑(closure ↑(t.erase j))
hfg : ∀ j ∈ t', f j ≤ g j
⊢ ∑ a ∈ t', g a • a + ∑ a ∈ t \ t', g a • a = ∑ a ∈ t, (if a ∈ t' then g a - f a else g a + f a) • a

Tactic:
ite_smul,

Goal state after:
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsCancelAdd M
a : M
t : Finset M
ih : ∀ m < t.card, ∀ (a : M) (t : Finset M), t.card = m → IsProperSemilinearSet (a +ᵥ ↑(closure ↑t))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : ∑ x ∈ t', f x • x = ∑ x ∈ t \ t', f x • x
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ),
      g i = m → a +ᵥ ∑ a ∈ t, g a • a ∈ ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ ↑(closure ↑(t.erase j))
hfg : ∀ j ∈ t', f j ≤ g j
⊢ ∑ a ∈ t', g a • a + ∑ a ∈ t \ t', g a • a = ∑ x ∈ t, if x ∈ t' then (g x - f x) • x else (g x + f x) • x
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case inr
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id ↑{b}
⊢ ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ a +ᵥ ↑(closure ↑{b}) ↔ x + p ∈ a +ᵥ ↑(closure ↑{b})

Tactic:
· have hb : b ≠ 0 := by simpa [ne_comm] using ht.zero_notMem_image
        rw [Nat.ne_zero_iff_zero_lt] at hb
        refine ⟨a, b, hb, fun x hx => ?_⟩
        simp only [Finset.coe_singleton, mem_vadd_set, SetLike.mem_coe,
          AddSubmonoid.mem_closure_singleton, smul_eq_mul, vadd_eq_add, exists_exists_eq_and]
        constructor
        · rintro ⟨x, rfl⟩
          exact ⟨x + 1, by grind⟩
        · rintro ⟨y, heq⟩
          cases y with
          | zero => exact ⟨0, by grind⟩
          | succ y => exact ⟨y, by grind⟩

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 : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
hf : μ.Integrable f
l : Filter ι
s : ι → Set X
hs : Tendsto (⇑μ.variation ∘ s) l (𝓝 0)
this : Tendsto (fun i ↦ ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation) l (𝓝 0)
i : ι
⊢ (fun a ↦ ↑‖∫ᵛ (x : X) in s a, f x ∂[B; μ]‖₊) i ≤ (fun i ↦ ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation) i

Tactic:
apply enorm_integral_le_lintegral_enorm.trans

Goal state after:
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
hf : μ.Integrable f
l : Filter ι
s : ι → Set X
hs : Tendsto (⇑μ.variation ∘ s) l (𝓝 0)
this : Tendsto (fun i ↦ ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation) l (𝓝 0)
i : ι
⊢ ‖B‖ₑ * ∫⁻ (a : X), ‖f a‖ₑ ∂(μ.restrict (s i)).variation ≤ (fun i ↦ ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation) i
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
⊢ ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s

Tactic:
simp_all [f]

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: α : Type u_1
s : Set (α → ℕ)
A : Set ℕ
inst✝ : Finite α
hs : IsSemilinearSet s
⊢ A.Definable presburger s

Tactic:
isSemilinearSet_iff

Goal state after:
α : Type u_1
s : Set (α → ℕ)
A : Set ℕ
inst✝ : Finite α
hs : ∃ S, (∀ t ∈ S, IsLinearSet t) ∧ s = ⋃₀ ↑S
⊢ A.Definable presburger s