mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
hP : P.FG
⊢ ↑P = 0 +ᵥ ↑P

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
⊢ ∅.Finite ∧ (∀ t ∈ ∅, IsLinearSet t) ∧ ∅ = ⋃₀ ∅

Tactic:
simp

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

Goal state before:
pp: case empty
M : Type u_1
inst✝ : AddCommMonoid M
S : Set (Set M)
hS' : ∀ s ∈ ∅, IsSemilinearSet s
⊢ IsSemilinearSet (⋃₀ ∅)

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
hs : s.Finite
⊢ ∀ i ∈ s, IsSemilinearSet {i}

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x✝ x : M
hx : x ∈ closure (insert a t)
hx✝ : a + x ∈ closure (a +ᵥ ↑(closure t))
hy✝ : 0 ∈ closure (a +ᵥ ↑(closure t))
⊢ a + x = a + x + 0

Tactic:
simp

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

Goal state before:
pp: 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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : Nontrivial E
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖x‖₊ * ‖y‖₊
⊢ μ.variation = 1 • μ.variation

Tactic:
simp

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

Goal state before:
pp: case mpr.inl
M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
⊢ 0 ∈ closure (a +ᵥ ↑(closure t))

Tactic:
simp

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

Goal state before:
pp: 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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
f : X → E
hf : μ.Integrable f
⊢ ↑‖B‖₊ ≠ ∞

Tactic:
simp

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

Goal state before:
pp: case empty
M : Type u_1
inst✝ : AddCommMonoid M
S : Set (Set M)
hS' : ∀ t ∈ ∅, IsLinearSet t
⊢ IsSemilinearSet ↑(closure (⋃₀ ∅))

Tactic:
simp

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

Goal state before:
pp: case empty
ι : Type u_1
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
μ : ι → VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
⊢ (∑ i ∈ ∅, μ i).transpose B = ∑ i ∈ ∅, (μ i).transpose B

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
hs : IsSemilinearSet s
⊢ IsSemilinearSet ↑(closure s)

Tactic:
by
  rcases hs with ⟨S, hS, hS', rfl⟩
  induction S, hS using Finite.induction_on with
  | empty => simp
  | insert _ _ ih =>
    simp_rw [mem_insert_iff, forall_eq_or_imp] at hS'
    simpa [closure_union, coe_sup] using hS'.1.closure.add (ih hS'.2)

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a : M
⊢ ∅.Finite ∧ LinearIndepOn ℕ id ∅ ∧ {a} = a +ᵥ ↑(closure ∅)

Tactic:
simp

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

Goal state before:
pp: case empty
ι : Type u_1
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
μ : VectorMeasure X F
B : ι → E →L[ℝ] F →L[ℝ] G
⊢ μ.transpose (∑ i ∈ ∅, B i) = ∑ i ∈ ∅, μ.transpose (B i)

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
⊢ ∅.Finite ∧ (∀ t ∈ ∅, IsProperLinearSet t) ∧ ∅ = ⋃₀ ∅

Tactic:
simp

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

Goal state before:
pp: case empty
M : Type u_1
inst✝ : AddCommMonoid M
S : Set (Set M)
hS' : ∀ s ∈ ∅, IsProperSemilinearSet s
⊢ IsProperSemilinearSet (⋃₀ ∅)

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
s : Set M
inst✝ : IsCancelAdd M
hs : IsLinearSet s
⊢ IsProperSemilinearSet s

Tactic:
isLinearSet_iff

Goal state after:
M : Type u_1
inst✝¹ : AddCommMonoid M
s : Set M
inst✝ : IsCancelAdd M
hs : ∃ a t, s = a +ᵥ ↑(closure ↑t)
⊢ IsProperSemilinearSet s
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: 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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
c : ℝ
f : X → E
⊢ ∀ (c : ℝ) (s : Set X) (x : E), ((μ.transpose B) s) (c • x) = c • ((μ.transpose B) s) x

Tactic:
simp

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

Goal state before:
pp: X : Type u_2
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E
μ : VectorMeasure X F
hμ : μ.Integrable f
⊢ (-μ).variation ≤ μ.variation

Tactic:
simp

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

Goal state before:
pp: case empty
X : Type u_2
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E
ι : Type u_8
μ : ι → VectorMeasure X F
h : ∀ i ∈ ∅, (μ i).Integrable f
⊢ (∑ i ∈ ∅, μ i).Integrable f

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
ρ : NNReal
ρpos : ρ > 0
hδ : ‖B‖₊ * ρ ≤ δ
⊢ 1 ≠ ∞

Tactic:
simp

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

Goal state before:
pp: case empty
ι : Type u_1
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
B : E →L[ℝ] F →L[ℝ] G
μ : ι → VectorMeasure X F
hf : ∀ i ∈ ∅, (μ i).Integrable f
⊢ ∫ᵛ (x : X), f x ∂[B; ∑ i ∈ ∅, μ i] = ∑ i ∈ ∅, ∫ᵛ (x : X), f x ∂[B; μ i]

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
ρ : NNReal
ρpos : ρ > 0
hδ : ‖B‖₊ * ρ ≤ δ
g : X →ₛ E
h'g : eLpNorm (f - ⇑g) 1 μ.variation < ↑ρ
gmem : MemLp (⇑g) 1 μ.variation
⊢ 1 ≠ ∞

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
⊢ ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ (μ.withDensity f B).variation s + ↑ε

Tactic:
obtain ⟨g, hg, gmem⟩ : ∃ (g : X →ₛ E), eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ δ
      ∧ MemLp (⇑g) 1 μ.variation := by
    obtain ⟨ρ, ρpos, hδ⟩ : ∃ ρ > 0, ‖B‖₊ * ρ ≤ δ := by
      rcases eq_or_ne (‖B‖₊) 0 with hB | hB
      · exact ⟨1, zero_lt_one, by simp [hB]⟩
      · refine ⟨‖B‖₊ ⁻¹ * δ, by positivity, ?_⟩
        rw [← mul_assoc]
        apply mul_le_of_le_one_left (by positivity) mul_inv_le_one
    obtain ⟨g, h'g, gmem⟩ : ∃ (g : X →ₛ E), eLpNorm (f - ⇑g) 1 μ.variation < ρ
        ∧ MemLp (⇑g) 1 μ.variation :=
      (memLp_one_iff_integrable.2 hf).exists_simpleFunc_eLpNorm_sub_lt (by simp)
        (by simpa using ρpos.ne')
    refine ⟨g, ?_, gmem⟩
    grw [variation_transpose_le]
    rw [eLpNorm_smul_measure_of_ne_top' (by simp)]
    grw [h'g.le]
    simp only [ENNReal.toReal_one, inv_one, NNReal.rpow_one, ENNReal.smul_def, smul_eq_mul]
    exact_mod_cast hδ

Goal state after:
X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
⊢ ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ (μ.withDensity f B).variation s + ↑ε
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case empty
ι : Type u_1
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
hf : μ.Integrable f
⊢ ∫ᵛ (x : X), f x ∂[∑ i ∈ ∅, B i; μ] = ∑ i ∈ ∅, ∫ᵛ (x : X), f x ∂[B i; μ]

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
⊢ ∫⁻ (a : X) in s, ‖f a - g a‖ₑ + ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ∫⁻ (a : X) in s, ‖f a - g a‖ₑ ∂(μ.transpose B).variation

Tactic:
rw [lintegral_add_right, add_comm]

Goal state after:
case hg
X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
⊢ Measurable fun a ↦ ‖g a‖ₑ
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: 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
⊢ 0 ≤ ‖B‖

Tactic:
simp

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

Goal state before:
pp: 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
⊢ ↑(NNReal.mk ‖B‖ ⋯) * (∫⁻ (a : X), ENNReal.ofReal ‖f a‖ ∂μ.variation).toReal ≤
    ‖B‖ * (∫⁻ (a : X), ENNReal.ofReal ‖f a‖ ∂μ.variation).toReal

Tactic:
simp

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

Goal state before:
pp: 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
hf : μ.Integrable f
⊢ 0 ≤ 1

Tactic:
simp

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

Goal state before:
pp: 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
hf : μ.Integrable f
⊢ ↑(NNReal.mk 1 ⋯) * ∫⁻ (x : X), ‖f x‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X), ‖f a‖ₑ ∂(μ.transpose B).variation

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
⊢ (∀ t ∈ ∅, t ⊆ ⇑g ⁻¹' {0}) ∧
    (↑∅).PairwiseDisjoint id ∧
      (∀ t ∈ ∅, MeasurableSet t) ∧
        ‖0‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {0}) ≤
          ‖0‖ₑ * (∑ p ∈ ∅, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)

Tactic:
simp

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

Goal state before:
pp: case inr.mp
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id ↑{b}
hb : 0 < b
x : ℕ
hx : x ≥ a
⊢ (∃ a_1, a + a_1 * b = x) → ∃ a_2, a + a_2 * b = x + b

pp: case inr.mpr
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id ↑{b}
hb : 0 < b
x : ℕ
hx : x ≥ a
⊢ (∃ a_1, a + a_1 * b = x + b) → ∃ a_2, a + a_2 * b = x

Tactic:
· rintro ⟨x, rfl⟩
          exact ⟨x + 1, by grind⟩

Goal state after:
case inr.mpr
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id ↑{b}
hb : 0 < b
x : ℕ
hx : x ≥ a
⊢ (∃ a_1, a + a_1 * b = x + b) → ∃ a_2, a + a_2 * b = x
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)
⊢ 0 ≠ 0 ∨ ‖B‖ₑ ≠ ∞

Tactic:
simp

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

Goal state before:
pp: X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : MeasurableSpace X
inst✝ : CompleteSpace G
a : X
v : F
hfm : StronglyMeasurable f
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : IsFiniteMeasure ((dirac a v).transpose B).variation
⊢ ∫ᵛ (x : X), f a ∂[B; dirac a v] = (B (f a)) v

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
i : E
hi : i ≠ 0
⊢ ↑‖B‖₊ ≠ ∞

Tactic:
simp

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

Goal state before:
pp: X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝² : MeasurableSpace X
inst✝¹ : MeasurableSingletonClass X
inst✝ : CompleteSpace G
a : X
v : F
this : IsFiniteMeasure ((dirac a v).transpose B).variation
⊢ ∫ᵛ (x : X), f a ∂[B; dirac a v] = (B (f a)) v

Tactic:
simp

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

Goal state before:
pp: case pos
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
hμ : μ.variation = 0
⊢ ‖B‖ * (∫⁻ (a : X), ENNReal.ofReal C ∂μ.variation).toReal = ‖B‖ * (C * μ.variation.real univ)

Tactic:
simp [hμ]

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

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

Tactic:
isLinearSet_iff

Goal state after:
α : Type u_1
s : Set (α → ℕ)
A : Set ℕ
inst✝ : Finite α
hs : ∃ a t, s = a +ᵥ ↑(AddSubmonoid.closure ↑t)
⊢ A.Definable presburger s
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: α : Type u_1
A : Set ℕ
inst✝ : Finite α
v : α → ℕ
t : Finset (α → ℕ)
x : α → ℕ
a : ↥t → ℕ
i : α
⊢ x i = (v + ∑ x ∈ t.attach, ↑x * ↑(a x)) i ↔ x i = v i + ∑ i_1 ∈ t.attach, ↑i_1 i * a i_1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
A : Set ℕ
inst✝ : Fintype α
i : α
⊢ ∀ (v : α → ℕ), v i = 0 + Pi.single i 1 ⬝ᵥ v

Tactic:
simp

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

Goal state before:
pp: case func.inl.zero
α : Type u_1
A : Set ℕ
inst✝ : Fintype α
ts : Fin 0 → presburger[[↑A]].Term α
k : Fin 0 → ℕ
u : Fin 0 → α → ℕ
ih : ∀ (a : Fin 0) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v
v : α → ℕ
⊢ (Structure.funMap presburgerFunc.zero fun i ↦ Term.realize v (ts i)) = 0 + 0 ⬝ᵥ v

Tactic:
simp

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

Goal state before:
pp: 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
C : ℝ≥0∞
h : ∀ᵐ (x : X) ∂μ.variation, ‖f x‖ₑ ≤ C
⊢ ∫⁻ (a : X), C ∂μ.variation ≤ C * μ.variation univ

Tactic:
simp

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

Goal state before:
pp: case a.inl
X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
P : E → Finset (Set X)
Pg : ∀ (i : E), ∀ t ∈ P i, t ⊆ ⇑g ⁻¹' {i}
Pdisj : ∀ (i : E), (↑(P i)).PairwiseDisjoint id
Pmeas : ∀ (i : E), ∀ t ∈ P i, MeasurableSet t
hP :
  ∀ (i : E),
    ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
      ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)
I3 :
  ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ
p : Set X
hi : ⟨0, p⟩ ∈ g.range.sigma P
⊢ ‖⟨0, p⟩.fst‖ₑ * ‖((μ.transpose B).restrict s) ⟨0, p⟩.snd‖ₑ =
    ‖∫ᵛ (x : X) in ⟨0, p⟩.snd, ⟨0, p⟩.fst ∂[B; μ.restrict s]‖ₑ

Tactic:
simp

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

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

Goal state after:
Module: Mathlib.ModelTheory.Equivalence

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α (n + 1)
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (∀' φ ⇔ ∼(∃' ∼φ)).Realize v xs

Tactic:
simp

Goal state after: