mathlib-initiative/mathlib-tactics huggingface dataset:
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
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
μ : FiniteMeasure E
⊢ μ ∈ ProbabilityMeasure.toFiniteMeasure '' {μ | ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ↔
    μ ∈ {μ | μ.mass = 1 ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}

Tactic:
simp only [mem_image, mem_ofPred_eq]

Goal state after:
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
μ : FiniteMeasure E
⊢ (∃ x, (∀ (n : ℕ), x (K n)ᶜ ≤ u n) ∧ x.toFiniteMeasure = μ) ↔ μ.mass = 1 ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this : Filter.Tendsto (fun n ↦ (μ (accumulate f n)).toReal) Filter.atTop (nhds (μ (⋃ i, f i)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist (μ (accumulate f n)).toReal (μ (⋃ i, f i)).toReal < ε / 2
g : ℕ → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * (↑N + 1))
⊢ (μ ((⋃ 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 <
    ε

Tactic:
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 μ

pp: case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
h : μ univ = 1
⊢ IsProbabilityMeasure μ

Tactic:
· simp_all

Goal state after:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsZeroOneMeasure μ
inst✝¹ : StandardBorelSpace α
inst✝ : NeZero μ
h : μ univ = 1
⊢ IsProbabilityMeasure μ
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

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)
n : ℕ
h : ¬μ (A n) = 1
⊢ μ (A n)ᶜᶜ = 0

Tactic:
· simp_all

Goal state after:
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)
n : ℕ
h : ¬μ (A n) = 1
⊢ μ (A n)ᶜᶜ = 0
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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet {x | ∃ μ ∈ S, ↑μ = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
K : ℕ → Set E
K_comp : ∀ (n : ℕ), IsCompact (K n)
hK : ∀ (n : ℕ), ∀ μ ∈ S, μ (K n)ᶜ ≤ u n
K' : ℕ → Set E := fun n ↦ ⋃ i ∈ Iic n, K i
h'K : IsCompact {μ | ∀ (n : ℕ), μ (K' n)ᶜ ≤ u n}
⊢ IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)

Tactic:
apply IsCompact.closure_of_subset h'K

Goal state after:
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet {x | ∃ μ ∈ S, ↑μ = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
K : ℕ → Set E
K_comp : ∀ (n : ℕ), IsCompact (K n)
hK : ∀ (n : ℕ), ∀ μ ∈ S, μ (K n)ᶜ ≤ u n
K' : ℕ → Set E := ⋯
h'K : IsCompact {μ | ∀ (n : ℕ), μ (K' n)ᶜ ≤ u n}
⊢ S ⊆ {μ | ∀ (n : ℕ), μ (K' n)ᶜ ≤ u n}
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.SeparableMeasure

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

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

Tactic:
· rw [measure_sdiff
                    (inter_subset_left ..)
                    (ms.inter (hgen ▸ measurableSet_generateFrom (T_mem N))).nullMeasurableSet
                    (ne_top_of_le_ne_top hμs (measure_mono (inter_subset_left ..))),
                  lt_ofReal_iff_toReal_lt (sub_ne_top hμs),
                  toReal_sub_of_le (measure_mono (inter_subset_left ..)) hμs]
                apply lt_of_le_of_lt (sub_le_dist ..)
                nth_rw 1 [← univ_inter s]
                rw [inter_comm s, dist_comm, ← T_spanning, iUnion_inter _ T]
                apply hN N (le_refl _)

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

Goal state before:
pp: case h
ι : 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 : ℕ
⊢ closure s ∩ closedBall x (ε n) ⊆ closedBall x (ε n) \ closedBall (f (ε n) ⋯) (ε n / 4)

Tactic:
rw [sdiff_eq_compl_inter]

Goal state after:
case h
ι : 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 : ℕ
⊢ closure s ∩ closedBall x (ε n) ⊆ (closedBall (f (ε n) ⋯) (ε n / 4))ᶜ ∩ closedBall x (ε n)
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

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
⊢ NullMeasurableSet (closedBall (f (ε n) ⋯) (ε n / 4)) volume

Tactic:
· simp_all

Goal state after:
ι : 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
⊢ NullMeasurableSet (closedBall (f (ε n) ⋯) (ε n / 4)) volume
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

pp: case inr
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
hp : s \ (filter MeasurableSet Q.parts).sup id ∈ (Q'.extendOfLE ⋯).parts
⊢ MeasurableSet (s \ (filter MeasurableSet Q.parts).sup id)

Tactic:
· simp_all

Goal state after:
case inr
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
hp : s \ (filter MeasurableSet Q.parts).sup id ∈ (Q'.extendOfLE ⋯).parts
⊢ MeasurableSet (s \ (filter MeasurableSet Q.parts).sup id)
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

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
E : Set X
hE : MeasurableSet E
hE' : ¬⟨E, hE⟩ = ⊥
⊢ ‖μ E‖ₑ ≤ μ.variation E

Tactic:
· simp_all

Goal state after:
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
E : Set X
hE : MeasurableSet E
hE' : ¬⟨E, hE⟩ = ⊥
⊢ ‖μ E‖ₑ ≤ μ.variation E
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:
by
  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:
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 : α
⊢ hf.vectorMeasure (Ioi a) = atTop.limUnder f - Function.rightLim f a

Tactic:
have := hf.vectorMeasure_Ici a
  rw [← Icc_union_Ioi_eq_Ici le_rfl, VectorMeasure.of_union (by simp) measurableSet_Icc
    measurableSet_Ioi, hf.vectorMeasure_Icc le_rfl] at this
  grind

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
h₂' : ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0
partition₁ :
  VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ = (μ - ν).toSignedMeasure
partition₂ :
  VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s + 0 = (ν - μ).toSignedMeasure
⊢ VectorMeasure.restrict μ.toSignedMeasure s + VectorMeasure.restrict μ.toSignedMeasure sᶜ -
      (VectorMeasure.restrict ν.toSignedMeasure s + VectorMeasure.restrict ν.toSignedMeasure sᶜ) =
    (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure

Tactic:
← partition₁,

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
h₂' : ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0
partition₁ :
  VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ = (μ - ν).toSignedMeasure
partition₂ :
  VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s + 0 = (ν - μ).toSignedMeasure
⊢ VectorMeasure.restrict μ.toSignedMeasure s + VectorMeasure.restrict μ.toSignedMeasure sᶜ -
      (VectorMeasure.restrict ν.toSignedMeasure s + VectorMeasure.restrict ν.toSignedMeasure sᶜ) =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ - (ν - μ).toSignedMeasure
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
v : α → M
inst✝ : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
| Term.realize v (List.map f s.toList).sum = ∑ i ∈ s, Term.realize v (f i)

Tactic:
rhs

Goal state after:
α : Type u_1
M : Type u_2
v : α → M
inst✝ : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
| ∑ i ∈ s, Term.realize v (f i)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: M : Type u_1
ι : Type u_3
inst✝ : AddCommMonoid M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsSemilinearSet (t i)
⊢ IsSemilinearSet (⋃ i ∈ s, t i)

Tactic:
← sUnion_image

Goal state after:
M : Type u_1
ι : Type u_3
inst✝ : AddCommMonoid M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsSemilinearSet (t i)
⊢ IsSemilinearSet (⋃₀ (t '' s))
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: M : Type u_1
ι : Type u_3
inst✝ : AddCommMonoid M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsProperSemilinearSet (t i)
⊢ IsProperSemilinearSet (⋃ i ∈ s, t i)

Tactic:
← sUnion_image

Goal state after:
M : Type u_1
ι : Type u_3
inst✝ : AddCommMonoid M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsProperSemilinearSet (t i)
⊢ IsProperSemilinearSet (⋃₀ (t '' s))
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case hbc.hb
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : IsFiniteMeasure μ.variation
C : ℝ
h : ∀ᵐ (x : X) ∂μ.variation, ‖f x‖ ≤ C
⊢ ∫⁻ (a : X), ENNReal.ofReal C ∂μ.variation ≠ ∞

Tactic:
simp only [lintegral_const, ne_eq]
      finiteness

Goal state after:
Module: Mathlib.ModelTheory.Equivalence

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⊓ ψ ⟹ ψ).Realize v xs

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_inf]
  exact And.right

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

Goal state before:
pp: A : Set ℕ
hmul : A.Definable presburger {v | v 0 = v 1 * v 2}
hsqr : A.Definable₁ presburger {x | ∃ x_1, x_1 * x_1 = x}
⊢ False

Tactic:
rw [definable₁_iff_ultimately_periodic] at hsqr

Goal state after:
A : Set ℕ
hmul : A.Definable presburger {v | v 0 = v 1 * v 2}
hsqr : ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ {x | ∃ x_1, x_1 * x_1 = x} ↔ x + p ∈ {x | ∃ x_1, x_1 * x_1 = x}
⊢ False
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : FG L M
f : M →[L] N
hs : f.range = ⊤
⊢ f.range.FG

Tactic:
exact h.range f

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : CG L M
f : M →[L] N
hs : f.range = ⊤
⊢ f.range.CG

Tactic:
exact h.range f

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
s₁ s₂ : Set (ι → ℕ)
hs₁ : IsLinearSet s₁
hs₂ : IsLinearSet s₂
⊢ IsSemilinearSet (s₁ ∩ s₂)

Tactic:
have := Fintype.ofFinite ι
  rw [isLinearSet_iff_exists_matrix] at hs₁ hs₂
  rcases hs₁ with ⟨u, n, A, rfl⟩
  rcases hs₂ with ⟨v, m, B, rfl⟩
  simp_rw [← ofPred_and, exists_and_exists_comm]
  refine IsSemilinearSet.proj' (IsSemilinearSet.proj' ?_)
  convert!
    isSemilinearSet_setOfPred_mulVec_eq (κ := (ι ⊕ Fin n) ⊕ Fin m) (Sum.elim u v) 0
      (fromBlocks (fromCols 0 A) 0 0 B) (fromBlocks (fromCols 1 0) 0 (fromCols 1 0) 0)
  simp [fromBlocks_mulVec, fromCols_mulVec, ← Sum.elim_add_add, Sum.elim_eq_iff]

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
N : Type u_1
inst✝ : L.Structure N
f : M ≃ₚ[L] N
⊢ Structure.FG L ↥f.dom ↔ f.cod.FG

Tactic:
f.toEquiv.fg_iff,

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
N : Type u_1
inst✝ : L.Structure N
f : M ≃ₚ[L] N
⊢ Structure.FG L ↥f.cod ↔ f.cod.FG