mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, ↑s = c}
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := fun x ↦ m ↑↑x
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
s t : MeasuredSets μ
h : Disjoint ↑s ↑t
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
hδ : 8 * δ = ε
s' : Set α
s'C : s' ∈ C
hs' : μ (s' ∆ ↑s) < δ
t' : Set α
t'C : t' ∈ C
ht' : μ (t' ∆ ↑t) < δ
It : ‖m t' - m₁ t‖ₑ < δ
hμ' : μ (s' ∩ t') < 2 * δ
s'' : Set α := s' \ t'
s''C : s'' ∈ C
hs'' : μ (s'' ∆ ↑s) < 3 * δ
Is : ‖m s'' - m₁ s‖ₑ < 3 * δ
Ist : ‖m (s'' ∪ t') - m₁ ⟨↑s ∪ ↑t, ⋯⟩‖ₑ < 4 * δ
⊢ ‖m s'' + m t' - m s'' - m t'‖ₑ + ‖m₁ ⟨↑s ∪ ↑t, ⋯⟩ - (m s'' + m t')‖ₑ + ‖m s'' - m₁ s‖ₑ + ‖m t' - m₁ t‖ₑ =
    ‖m₁ ⟨↑s ∪ ↑t, ⋯⟩ - (m s'' + m t')‖ₑ + ‖m s'' - m₁ s‖ₑ + ‖m t' - m₁ t‖ₑ

Tactic:
simp

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
s t : Set X
⊢ μ.semivariation (s ∪ t) ≤ μ.semivariation s + μ.semivariation t

Tactic:
by
  simp only [semivariation, iSup_le_iff]
  intro ℓ hℓ
  apply (measure_union_le _ _).trans
  gcongr <;> apply le_biSup _ hℓ

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
s : Set X
hs : MeasurableSet s
h's : μ.semivariation s = ∞
t : Set X
ts : t ⊆ s
t_meas : MeasurableSet t
ht : 2 * ‖μ s‖ₑ + 2 < 2 * ‖μ t‖ₑ
⊢ 2 ≠ 0

Tactic:
simp

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
s : Set X
hs : MeasurableSet s
h's : μ.semivariation s = ∞
t : Set X
ts : t ⊆ s
t_meas : MeasurableSet t
ht : 2 * ‖μ s‖ₑ + 2 < 2 * ‖μ t‖ₑ
⊢ 2 ≠ ∞

Tactic:
simp

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
s : Set X
hs : MeasurableSet s
h's : μ.semivariation s = ∞
t : Set X
ts : t ⊆ s
t_meas : MeasurableSet t
ht : 2 * ‖μ s‖ₑ + 2 < 2 * ‖μ t‖ₑ
h't : 1 + ‖μ s‖ₑ ≤ ‖μ t‖ₑ
⊢ s ⊆ t ∪ s \ t

Tactic:
simp

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
s : Set X
hs : MeasurableSet s
h's : μ.semivariation s = ∞
t : Set X
ts : t ⊆ s
t_meas : MeasurableSet t
ht : 2 * ‖μ s‖ₑ + 2 < 2 * ‖μ t‖ₑ
h't : 1 + ‖μ s‖ₑ ≤ ‖μ t‖ₑ
hI : μ.semivariation t = ∞
this : 1 + ‖μ s‖ₑ ≤ ‖μ (s \ t)‖ₑ + ‖μ s‖ₑ
⊢ ‖μ s‖ₑ ≠ ∞

Tactic:
simp

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

Goal state before:
pp: case h_add
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
f✝ : X → E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace H
C : G →L[ℝ] H
hf : Integrable f✝ μ.variation
f g : X → E
a✝ : Disjoint (support f) (support g)
f_int : Integrable f μ.variation
g_int : Integrable g μ.variation
⊢ C ∫ᵛ (y : X), f y ∂[B; μ] = ∫ᵛ (y : X), f y ∂[(compL ℝ F G H) C ∘SL B; μ] →
    C ∫ᵛ (y : X), g y ∂[B; μ] = ∫ᵛ (y : X), g y ∂[(compL ℝ F G H) C ∘SL B; μ] →
      C ∫ᵛ (y : X), (f + g) y ∂[B; μ] = ∫ᵛ (y : X), (f + g) y ∂[(compL ℝ F G H) C ∘SL B; μ]

Tactic:
hf

Goal state after:
case h_add
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
f✝ : X → E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace H
C : G →L[ℝ] H
hf✝ : Integrable f✝ μ.variation
f g : X → E
a✝ : Disjoint (support f) (support g)
f_int : Integrable f μ.variation
g_int : Integrable g μ.variation
hf : C ∫ᵛ (y : X), f y ∂[B; μ] = ∫ᵛ (y : X), f y ∂[(compL ℝ F G H) C ∘SL B; μ]
⊢ C ∫ᵛ (y : X), g y ∂[B; μ] = ∫ᵛ (y : X), g y ∂[(compL ℝ F G H) C ∘SL B; μ] →
    C ∫ᵛ (y : X), (f + g) y ∂[B; μ] = ∫ᵛ (y : X), (f + g) y ∂[(compL ℝ F G H) C ∘SL B; μ]
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
s : Set X
hs : MeasurableSet s
h's : μ.semivariation s = ∞
t : Set X
ts : t ⊆ s
t_meas : MeasurableSet t
ht : 2 * ‖μ s‖ₑ + 2 < 2 * ‖μ t‖ₑ
h't : 1 + ‖μ s‖ₑ ≤ ‖μ t‖ₑ
hI : μ.semivariation (s \ t) = ∞
⊢ 1 ≤ 1 + ‖μ s‖ₑ

Tactic:
simp

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) = ∞
u : ℕ → Set X := fun n ↦ s n \ s (n + 1)
n : ℕ
⊢ 1 ≤ ‖μ (u n)‖ₑ

Tactic:
simp only [Function.iterate_succ', Function.comp_apply, u, s]

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)
n : ℕ
⊢ 1 ≤ ‖μ (t^[n] univ \ t (t^[n] univ))‖ₑ
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ supClosure C, μ (s ∆ t) < ε
m₀ : AddContent E (supClosure C) := m.supClosure hC
hm₀ : m₀ = m.supClosure hC
s : Set α
P : Finpartition s
PC : ↑P.parts ⊆ C
⊢ ‖(m.supClosure hC) s‖ₑ ≤ μ (P.parts.sup id)

Tactic:
AddContent.supClosure_apply_finpartition hC _ PC,

Goal state after:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ supClosure C, μ (s ∆ t) < ε
m₀ : AddContent E (supClosure C) := m.supClosure hC
hm₀ : m₀ = m.supClosure hC
s : Set α
P : Finpartition s
PC : ↑P.parts ⊆ C
⊢ ‖∑ s ∈ P.parts, m s‖ₑ ≤ μ (P.parts.sup id)
Module: Mathlib.MeasureTheory.VectorMeasure.Prod

Goal state before:
pp: case inl
X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
h : μ.HasProd ν B
t : Set Y
⊢ (μ.prod ν B) (∅ ×ˢ t) = (B (μ ∅)) (ν t)

Tactic:
simp

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

Goal state before:
pp: case inr.inl
X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
h : μ.HasProd ν B
s : Set X
hs : s ≠ ∅
⊢ (μ.prod ν B) (s ×ˢ ∅) = (B (μ s)) (ν ∅)

Tactic:
simp

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

Goal state before:
pp: case 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
f✝ : X → E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace H
C : G →L[ℝ] H
hf : Integrable f✝ μ.variation
f g : X → E
hfg : f =ᵐ[μ.variation] g
a✝ : Integrable f μ.variation
⊢ C ∫ᵛ (y : X), f y ∂[B; μ] = ∫ᵛ (y : X), f y ∂[(compL ℝ F G H) C ∘SL B; μ] →
    C ∫ᵛ (y : X), g y ∂[B; μ] = ∫ᵛ (y : X), g y ∂[(compL ℝ F G H) C ∘SL B; μ]

Tactic:
hf

Goal state after:
case 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
f✝ : X → E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace H
C : G →L[ℝ] H
hf✝ : Integrable f✝ μ.variation
f g : X → E
hfg : f =ᵐ[μ.variation] g
a✝ : Integrable f μ.variation
hf : C ∫ᵛ (y : X), f y ∂[B; μ] = ∫ᵛ (y : X), f y ∂[(compL ℝ F G H) C ∘SL B; μ]
⊢ C ∫ᵛ (y : X), g y ∂[B; μ] = ∫ᵛ (y : X), g y ∂[(compL ℝ F G H) C ∘SL B; μ]
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case 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
f✝ : X → E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace H
C : G →L[ℝ] H
hf✝ : Integrable f✝ μ.variation
f g : X → E
hfg : f =ᵐ[μ.variation] g
a✝ : Integrable f μ.variation
hf : C ∫ᵛ (y : X), f y ∂[B; μ] = ∫ᵛ (y : X), f y ∂[(compL ℝ F G H) C ∘SL B; μ]
⊢ C ∫ᵛ (x : X), f x ∂[B; μ] = ∫ᵛ (x : X), f x ∂[(compL ℝ F G H) C ∘SL B; μ]

Tactic:
hf

Goal state after:
case 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
f✝ : X → E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace H
C : G →L[ℝ] H
hf✝ : Integrable f✝ μ.variation
f g : X → E
hfg : f =ᵐ[μ.variation] g
a✝ : Integrable f μ.variation
hf : C ∫ᵛ (y : X), f y ∂[B; μ] = ∫ᵛ (y : X), f y ∂[(compL ℝ F G H) C ∘SL B; μ]
⊢ ∫ᵛ (y : X), f y ∂[(compL ℝ F G H) C ∘SL B; μ] = ∫ᵛ (x : X), f x ∂[(compL ℝ F G H) C ∘SL B; μ]
Module: Mathlib.MeasureTheory.VectorMeasure.Prod

Goal state before:
pp: X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : μ.HasProd ν B
s : Set Y
t : Set X
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (μ.prod ν B) (Prod.swap ⁻¹' s ×ˢ t) = (B.flip (ν s)) (μ t)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
H : Type u_7
I : Type u_8
J : Type u_9
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : NormedAddCommGroup H
inst✝⁵ : NormedSpace ℝ H
inst✝⁴ : NormedAddCommGroup I
inst✝³ : NormedSpace ℝ I
inst✝² : NormedAddCommGroup J
inst✝¹ : NormedSpace ℝ J
μ✝ : VectorMeasure X E
ν✝ : VectorMeasure Y F
B✝ : E →L[ℝ] F →L[ℝ] G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : IsFiniteMeasure μ.variation
⊢ (if MeasurableSet ∅ then ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' ∅) ∂[B.flip; μ] else 0) = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this : MeasurableSpace α := hα
⊢ (if MeasurableSet ∅ then ∫ᵛ (x : α), μ[∅.indicator 1 | M] x ∂•m' else 0) = 0

Tactic:
simp

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

Goal state before:
pp: case pos.h_add
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
a✝ : Disjoint (support f) (support g)
f_int : Integrable f μ.variation
g_int : Integrable g μ.variation
⊢ ∫ᵛ (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; μ] →
      ∫ᵛ (y : X), C ((f + g) y) ∂[B; μ] = ∫ᵛ (y : X), (f + g) y ∂[B ∘SL C; μ]

Tactic:
hf

Goal state after:
case pos.h_add
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
a✝ : Disjoint (support f) (support g)
f_int : Integrable f μ.variation
g_int : Integrable g μ.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; μ] →
    ∫ᵛ (y : X), C ((f + g) y) ∂[B; μ] = ∫ᵛ (y : X), (f + g) y ∂[B ∘SL C; μ]
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
⊢ ∫ᵛ (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:
hf

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; μ]
⊢ ∫ᵛ (y : X), C (g y) ∂[B; μ] = ∫ᵛ (y : X), g y ∂[B ∘SL C; μ]
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; μ]
this : ∀ᵐ (x : X) ∂μ.variation, C (f x) = C (g x)
⊢ ∫ᵛ (x : X), C (f x) ∂[B; μ] = ∫ᵛ (x : X), f x ∂[B ∘SL C; μ]

Tactic:
hf

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), f y ∂[B ∘SL C; μ] = ∫ᵛ (x : X), f x ∂[B ∘SL C; μ]
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case pos
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
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
C : ℝ≥0∞
hC : ∀ᵐ (x : X) ∂(μ.restrict s).variation, ‖f x‖ₑ ≤ C
hs : MeasurableSet s
⊢ C * ‖B‖ₑ * μ.variation (univ ∩ s) ≤ C * ‖B‖ₑ * μ.variation s

Tactic:
simp

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

Goal state before:
pp: case inl
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
C : ℝ
h : IsFiniteMeasure (μ.variation.restrict ∅)
hC : ∀ x ∈ ∅, ‖f x‖ ≤ C
⊢ ‖∫ᵛ (x : X) in ∅, f x ∂[B; μ]‖ ≤ C * ‖B‖ * μ.variation.real ∅

Tactic:
simp

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

Goal state before:
pp: case hf
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this : MeasurableSpace α := hα
m'' : VectorMeasure α E :=
  { measureOf' := fun s ↦ if MeasurableSet s then ∫ᵛ (x : α), μ[s.indicator 1 | M] x ∂•m' else 0, empty' := ⋯,
    not_measurable' := ⋯, m_iUnion' := ⋯ }
s : Set α
hs : s ∈ C
x : α
⊢ StronglyMeasurable (s.indicator 1)

pp: case hfi
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this : MeasurableSpace α := hα
m'' : VectorMeasure α E :=
  { measureOf' := fun s ↦ if MeasurableSet s then ∫ᵛ (x : α), μ[s.indicator 1 | M] x ∂•m' else 0, empty' := ⋯,
    not_measurable' := ⋯, m_iUnion' := ⋯ }
s : Set α
hs : s ∈ C
x : α
⊢ Integrable (s.indicator 1) μ

Tactic:
· exact StronglyMeasurable.indicator stronglyMeasurable_const
          (measurableSet_generateFrom hs)

Goal state after:
case hfi
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this : MeasurableSpace α := hα
m'' : VectorMeasure α E :=
  { measureOf' := fun s ↦ if MeasurableSet s then ∫ᵛ (x : α), μ[s.indicator 1 | M] x ∂•m' else 0, empty' := ⋯,
    not_measurable' := ⋯, m_iUnion' := ⋯ }
s : Set α
hs : s ∈ C
x : α
⊢ Integrable (s.indicator 1) μ
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
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hG : CompleteSpace G
hfi : Integrable f (μ.variation.restrict (⋃ i, s i))
⊢ ‖B‖ₑ < ∞

Tactic:
simp

Goal state after:
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 α
l : List β
⊢ Term.realize v (List.map f l).sum = (List.map (fun i ↦ Term.realize v (f i)) l).sum

Tactic:
induction l with simp [*]

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

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

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
s : Finset M
⊢ (↑s).Finite ∧ ↑(closure ↑s) = 0 +ᵥ ↑(closure ↑s)

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
⊢ ↑(closure s) = 0 +ᵥ ↑(closure s)

Tactic:
simp

Goal state after: