mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.OuterMeasure.OfAddContent

Goal state before:
pp: case refine_1
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ (inducedOuterMeasure (fun x x_1 ↦ m x) ⋯ ⋯) s = (OuterMeasure.ofFunction ⇑(AddContent.extend hC m) ⋯) s

pp: case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ (AddContent.extend hC m).IsSigmaSubadditive

pp: case refine_3
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ ∀ s ∉ C, (AddContent.extend hC m) s = ∞

Tactic:
· congr

Goal state after:
case refine_2
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ (AddContent.extend hC m).IsSigmaSubadditive

case refine_3
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
m : AddContent ℝ≥0∞ C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ ∀ s ∉ C, (AddContent.extend hC m) s = ∞
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Defs

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
V : Type u_2
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : ℕ → { t // MeasurableSet t }
⊢ Pairwise (Function.onFun Disjoint (Subtype.val ∘ s)) →
    (fun x ↦ ‖μ x‖ₑ) (⋃ i, ↑(s i)) ≤ ∑' (i : ℕ), (fun x ↦ ‖μ x‖ₑ) ↑(s i)

Tactic:
hs

Goal state after:
X : Type u_1
mX : MeasurableSpace X
V : Type u_2
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : ℕ → { t // MeasurableSet t }
hs : Pairwise (Function.onFun Disjoint (Subtype.val ∘ s))
⊢ (fun x ↦ ‖μ x‖ₑ) (⋃ i, ↑(s i)) ≤ ∑' (i : ℕ), (fun x ↦ ‖μ x‖ₑ) ↑(s i)
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
⊢ μ.ennrealVariation s = 0 → μ s = 0

Tactic:
hs

Goal state after:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : μ.ennrealVariation s = 0
⊢ μ s = 0
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
s : Set X
hs : μ.ennrealVariation s = 0
hsm : MeasurableSet s
⊢ μ.ennrealVariation s ≤ 0

Tactic:
hs

Goal state after:
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
s : Set X
hs : μ.ennrealVariation s = 0
hsm : MeasurableSet s
⊢ 0 ≤ 0
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₁
this : IsClosed {s | ‖m₁ s‖ₑ ≤ μ ↑s}
s : MeasuredSets μ
⊢ s ∈ C' → s ∈ {s | ‖m₁ s‖ₑ ≤ μ ↑s}

Tactic:
hs

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 : 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₁
this : IsClosed {s | ‖m₁ s‖ₑ ≤ μ ↑s}
s : MeasuredSets μ
hs : s ∈ C'
⊢ s ∈ {s | ‖m₁ s‖ₑ ≤ μ ↑s}
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
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
hfi : μ.IntegrableOn f s
⊢ s.indicator f =ᵐ[(μ.restrict sᶜ).variation] fun x ↦ 0

Tactic:
variation_restrict hs.compl

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
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
hfi : μ.IntegrableOn f s
⊢ s.indicator f =ᵐ[μ.variation.restrict sᶜ] fun x ↦ 0
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
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
f : X → E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
inst✝³ : MeasurableSpace X
inst✝² : MeasurableSingletonClass X
inst✝¹ : CompleteSpace G
a : X
v : F
s : Set X
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ ∫ᵛ (x : X) in s, f x ∂[B; dirac a v] = if a ∈ s then (B (f a)) v else 0

Tactic:
by
  rw [restrict_dirac hs]
  split_ifs
  · exact integral_dirac
  · exact integral_zero_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
s t : Set X
⊢ ∀ i ∈ {ℓ | ‖ℓ‖ₑ ≤ 1},
    (μ.mapRange ↑i ⋯).variation (s ∪ t) ≤
      (⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation s) + ⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation t

Tactic:
intro ℓ hℓ

Goal state after:
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s t : Set X
ℓ : StrongDual ℝ E
hℓ : ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}
⊢ (μ.mapRange ↑ℓ ⋯).variation (s ∪ t) ≤
    (⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation s) + ⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation t
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
hst : s ⊆ t
⊢ ∀ i ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑i ⋯).variation s ≤ ⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation t

Tactic:
intro ℓ hℓ

Goal state after:
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s t : Set X
hst : s ⊆ t
ℓ : StrongDual ℝ E
hℓ : ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}
⊢ (μ.mapRange ↑ℓ ⋯).variation s ≤ ⨆ ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑ℓ ⋯).variation t
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
⊢ ∀ i ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange ↑i ⋯).variation s ≤ μ.variation s

Tactic:
intro ℓ hℓ

Goal state after:
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
s : Set X
ℓ : StrongDual ℝ E
hℓ : ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}
⊢ (μ.mapRange ↑ℓ ⋯).variation s ≤ μ.variation s
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‖ₑ
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ μ.semivariation t = ∞ ∧ 1 ≤ ‖μ (s \ t)‖ₑ

Tactic:
have h't : 1 + ‖μ s‖ₑ ≤ ‖μ t‖ₑ := by
    apply (ENNReal.mul_le_mul_iff_right (a := 2) (by simp) (by simp)).1
    rw [mul_add, add_comm, mul_one]
    exact ht.le

Goal state after:
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‖ₑ
⊢ ∃ t, MeasurableSet t ∧ t ⊆ s ∧ μ.semivariation t = ∞ ∧ 1 ≤ ‖μ (s \ t)‖ₑ
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case h_ind
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
c : E
s : Set X
⊢ MeasurableSet s →
    μ.variation s < ∞ →
      C ∫ᵛ (y : X), s.indicator (fun x ↦ c) y ∂[B; μ] =
        ∫ᵛ (y : X), s.indicator (fun x ↦ c) y ∂[(compL ℝ F G H) C ∘SL B; μ]

Tactic:
hs

Goal state after:
case h_ind
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
c : E
s : Set X
hs : MeasurableSet s
⊢ μ.variation s < ∞ →
    C ∫ᵛ (y : X), s.indicator (fun x ↦ c) y ∂[B; μ] =
      ∫ᵛ (y : X), s.indicator (fun x ↦ c) y ∂[(compL ℝ F G H) C ∘SL B; μ]
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: case h'm
α : 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
hAddit : ∀ (s t : MeasuredSets μ), Disjoint ↑s ↑t → m₁ ⟨↑s ∪ ↑t, ⋯⟩ = m₁ s + m₁ t
m' : Set α → E := fun s ↦ if hs : MeasurableSet s then m₁ ⟨s, hs⟩ else 0
s t : Set α
⊢ MeasurableSet s → MeasurableSet t → Disjoint s t → m' (s ∪ t) = m' s + m' t

Tactic:
hs

Goal state after:
case h'm
α : 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
hAddit : ∀ (s t : MeasuredSets μ), Disjoint ↑s ↑t → m₁ ⟨↑s ∪ ↑t, ⋯⟩ = m₁ s + m₁ t
m' : Set α → E := fun s ↦ if hs : MeasurableSet s then m₁ ⟨s, hs⟩ else 0
s t : Set α
hs : MeasurableSet s
⊢ MeasurableSet t → Disjoint s t → m' (s ∪ t) = m' s + m' t
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: case h''m
α : 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
hAddit : ∀ (s t : MeasuredSets μ), Disjoint ↑s ↑t → m₁ ⟨↑s ∪ ↑t, ⋯⟩ = m₁ s + m₁ t
m' : Set α → E := fun s ↦ if hs : MeasurableSet s then m₁ ⟨s, hs⟩ else 0
s : Set α
⊢ ¬MeasurableSet s → m' s = 0

Tactic:
hs

Goal state after:
case h''m
α : 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
hAddit : ∀ (s t : MeasuredSets μ), Disjoint ↑s ↑t → m₁ ⟨↑s ∪ ↑t, ⋯⟩ = m₁ s + m₁ t
m' : Set α → E := fun s ↦ if hs : MeasurableSet s then m₁ ⟨s, hs⟩ else 0
s : Set α
hs : ¬MeasurableSet s
⊢ m' s = 0
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
A : ∀ s ∈ supClosure C, ‖m₀ s‖ₑ ≤ μ s
s : Set α
P : Finpartition s
PC : ↑P.parts ⊆ C
⊢ MeasurableSet (⋃ x ∈ P.parts, id x)

Tactic:
exact Finset.measurableSet_biUnion _ (fun b hb ↦ hCmeas _ (PC hb))

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✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : hα = generateFrom C
h''C : ∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0
s : Set α
⊢ s ∈ C → MeasurableSet s

Tactic:
hs

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
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : hα = generateFrom C
h''C : ∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0
s : Set α
hs : s ∈ C
⊢ MeasurableSet s
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
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : hα = generateFrom C
M : ∀ s ∈ C, MeasurableSet s
⊢ ∃ m', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s

Tactic:
rcases Measure.exists_ae_subset_biUnion_countable μ M with ⟨D, DC, D_count, hD⟩

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
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : hα = generateFrom C
M : ∀ s ∈ C, MeasurableSet s
D : Set (Set α)
DC : D ⊆ C
D_count : D.Countable
hD : ∀ s ∈ C, s ≤ᵐ[μ] ⋃₀ D
⊢ ∃ m', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case pos.h_ind
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
c : H
s : Set X
⊢ MeasurableSet s →
    μ.variation s < ∞ →
      ∫ᵛ (y : X), C (s.indicator (fun x ↦ c) y) ∂[B; μ] = ∫ᵛ (y : X), s.indicator (fun x ↦ c) y ∂[B ∘SL C; μ]

Tactic:
hs

Goal state after:
case pos.h_ind
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
c : H
s : Set X
hs : MeasurableSet s
⊢ μ.variation s < ∞ →
    ∫ᵛ (y : X), C (s.indicator (fun x ↦ c) y) ∂[B; μ] = ∫ᵛ (y : X), s.indicator (fun x ↦ c) y ∂[B ∘SL C; μ]
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 ≤ μ'
⊢ ∃ m', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s

Tactic:
let : MeasurableSpace α := hα

Goal state after:
α : 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', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
s₁ s₂ : Set M
hs₁ : IsSemilinearSet s₁
hs₂ : IsSemilinearSet s₂
⊢ IsSemilinearSet (s₁ ∪ s₂)

Tactic:
rcases hs₁ with ⟨S₁, hS₁, hS₁', rfl⟩
  rcases hs₂ with ⟨S₂, hS₂, hS₂', rfl⟩
  rw [← sUnion_union]
  refine ⟨S₁ ∪ S₂, hS₁.union hS₂, fun s hs => ?_, rfl⟩
  rw [mem_union] at hs
  exact hs.elim (hS₁' s) (hS₂' s)

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
s₁ s₂ : Set M
hs₁ : IsProperSemilinearSet s₁
hs₂ : IsProperSemilinearSet s₂
⊢ IsProperSemilinearSet (s₁ ∪ s₂)

Tactic:
rcases hs₁ with ⟨S₁, hS₁, hS₁', rfl⟩
  rcases hs₂ with ⟨S₂, hS₂, hS₂', rfl⟩
  rw [← sUnion_union]
  refine ⟨S₁ ∪ S₂, hS₁.union hS₂, fun s hs => ?_, rfl⟩
  rw [mem_union] at hs
  exact hs.elim (hS₁' s) (hS₂' s)

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

Goal state before:
pp: case inr
X : Type u_2
G : Type u_6
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X → G
h'G : Nontrivial G
⊢ ∫ᵛ (x : X), f x ∂<•μ.toSignedMeasure = ∫ (x : X), f x ∂μ

Tactic:
rw [integral_eq_setToFun, MeasureTheory.integral_eq_setToFun]

Goal state after:
case inr
X : Type u_2
G : Type u_6
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X → G
h'G : Nontrivial G
⊢ setToFun (variation μ.toSignedMeasure) ⇑(transpose μ.toSignedMeasure (lsmul ℝ ℝ).flip) ⋯ f =
    setToFun μ (weightedSMul μ) ⋯ f
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
⊢ ∃ x ∈ s, IsSemilinearSet {y | y ∈ s ∧ x ≤ y}

Tactic:
let f (x : M) : AddSubmonoid M :=
    if hx : x ∈ s then
      { carrier := { y | x + y ∈ s }
        zero_mem' := by simpa
        add_mem' := by
          intro a b ha hb
          simp only [mem_ofPred_eq] at *
          rw [← add_assoc]
          exact hs _ hx _ _ ha hb }
    else ⊥

Goal state after:
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, IsSemilinearSet {y | y ∈ s ∧ x ≤ y}
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 ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
⊢ ∃ x ∈ s, IsSemilinearSet {y | y ∈ s ∧ x ≤ y}

Tactic:
let g (x : M) : AddSemigroupIdeal M := .closure (f x \ {0})

Goal state after:
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 ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
⊢ ∃ x ∈ s, IsSemilinearSet {y | y ∈ s ∧ x ≤ y}
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
β : Type u_10
inst✝ : MeasurableSpace β
φ : X → β
hφ : Measurable φ
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ.variation)
hfi' : μ.Integrable (f ∘ φ)
s : Set β
x : E
⊢ MeasurableSet s → (((μ.map φ).transpose B) s) x = ((μ.transpose B) (φ ⁻¹' s)) x

Tactic:
hs

Goal state after:
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
β : Type u_10
inst✝ : MeasurableSpace β
φ : X → β
hφ : Measurable φ
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ.variation)
hfi' : μ.Integrable (f ∘ φ)
s : Set β
x : E
hs : MeasurableSet s
⊢ (((μ.map φ).transpose B) s) x = ((μ.transpose B) (φ ⁻¹' s)) x