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

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
s : Set X
hs : MeasurableSet s
a : ℝ≥0∞
ha : a < (variation μ) s
P : Finset (Set X)
Ps : ∀ t ∈ P, t ⊆ s
P_disj : (↑P).PairwiseDisjoint id
P_meas : ∀ t ∈ P, MeasurableSet t
hP : a < ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ + ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ
I : ∑ p ∈ P with 0 ≤ μ p, ‖μ p‖ₑ = ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ
J : ∑ p ∈ P with ¬0 ≤ μ p, ‖μ p‖ₑ = ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ
h : ‖μ (⋃ p ∈ {p ∈ P | 0 ≤ μ p}, p)‖ₑ ≤ ‖μ (⋃ p ∈ {p ∈ P | ¬0 ≤ μ p}, p)‖ₑ
⊢ ∀ b ∈ {p ∈ P | ¬0 ≤ μ p}, MeasurableSet b

Tactic:
grind

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

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
ht : MeasurableSet t
hfs : μ.IntegrableOn f s
hts : t ⊆ s
⊢ Disjoint (s \ t) t

Tactic:
grind

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
h'α : Nonempty α
m : AddContent E {s | ∃ u v, u ≤ v ∧ s = Ioc u v} := AddContent.onIoc (Function.rightLim f)
u v : α
huv : u ≤ v
⊢ v ∈ Icc u v

Tactic:
grind

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
h'α : Nonempty α
m : AddContent E {s | ∃ u v, u ≤ v ∧ s = Ioc u v} := AddContent.onIoc (Function.rightLim f)
u v : α
huv : u ≤ v
⊢ u ∈ Icc u v

Tactic:
grind

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

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
ht : MeasurableSet t
hst : s =ᵐ[μ.variation] t
x : X
hx : x ∈ s ↔ x ∈ t
⊢ (if x ∈ s then f x else 0) = if x ∈ t then f x else 0

Tactic:
grind

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
a b : α
hf : BoundedVariationOn f univ
h : a < b
this :
  hf.vectorMeasure (Ioo a b) + (Function.rightLim f b - Function.leftLim f b) =
    Function.rightLim f b - Function.rightLim f a
⊢ hf.vectorMeasure (Ioo a b) = Function.leftLim f b - Function.rightLim f a

Tactic:
grind

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 : 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‖ₑ < δ
⊢ s' ∩ t' ⊆ ↑s ∩ ↑t ∪ s' ∆ ↑s ∪ t' ∆ ↑t

Tactic:
grind

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 : α
this : Function.rightLim f a - Function.leftLim f a + hf.vectorMeasure (Ioi a) = atTop.limUnder f - Function.leftLim f a
⊢ hf.vectorMeasure (Ioi a) = atTop.limUnder f - Function.rightLim f a

Tactic:
grind

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 : α
this :
  hf.vectorMeasure (Iio a) + (Function.rightLim f a - Function.leftLim f a) = Function.rightLim f a - atBot.limUnder f
⊢ hf.vectorMeasure (Iio a) = Function.leftLim f a - atBot.limUnder f

Tactic:
grind

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

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
ht : MeasurableSet t
ht_eq : ∀ᵐ (x : X) ∂μ.variation, x ∈ t → f x = 0
x : X
hx : x ∈ t → f x = 0
⊢ (if x ∈ s ∨ x ∈ t then f x else 0) = if x ∈ s then f x else 0

Tactic:
grind

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
hf : C ∫ᵛ (y : X), f y ∂[B; μ] = ∫ᵛ (y : X), f y ∂[(compL ℝ F G H) C ∘SL B; μ]
hg : C ∫ᵛ (y : X), g y ∂[B; μ] = ∫ᵛ (y : X), g y ∂[(compL ℝ F G H) C ∘SL B; μ]
⊢ C ∫ᵛ (y : X), f y + g y ∂[B; μ] = ∫ᵛ (y : X), f y + g y ∂[(compL ℝ F G H) C ∘SL B; μ]

Tactic:
simp [integral_fun_add, f_int, g_int, hf, hg]

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)
hu : ∀ (n : ℕ), 1 ≤ ‖μ (u n)‖ₑ
s_anti : Antitone s
m n : ℕ
hmn : m < n
this : Disjoint (u m) (s (m + 1))
⊢ m + 1 ≤ n

Tactic:
grind

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
f : ℕ → Set (X × Y)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
⊢ HasSum (fun i ↦ if MeasurableSet (f i) then ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' f i) ∂[B.flip; μ] else 0)
    (if MeasurableSet (⋃ i, f i) then ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' ⋃ i, f i) ∂[B.flip; μ] else 0)

Tactic:
simp only [f_meas, ↓reduceIte, implies_true, MeasurableSet.iUnion, preimage_iUnion,
      HasSum, SummationFilter.unconditional_filter]

Goal state after:
ι : 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
f : ℕ → Set (X × Y)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
⊢ Tendsto (fun s ↦ ∑ x ∈ s, ∫ᵛ (x_1 : X), ν (Prod.mk x_1 ⁻¹' f x) ∂[B.flip; μ]) atTop
    (𝓝 ∫ᵛ (x : X), ν (⋃ i, Prod.mk x ⁻¹' f i) ∂[B.flip; μ])
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
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
hc : μ.variation s < ∞
this : IsFiniteMeasure (μ.variation.restrict s)
x✝ : X
⊢ C (if x✝ ∈ s then c else 0) = if x✝ ∈ s then C c else 0

Tactic:
grind

Goal state after:
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
hs : MeasurableSet s
hc : μ.variation s < ∞
this✝ : IsFiniteMeasure (μ.variation.restrict s)
this : (fun y ↦ C (s.indicator (fun x ↦ c) y)) = s.indicator fun x ↦ C c
⊢ (B (C c)) (μ s) = ((B ∘SL C) c) (μ s)

Tactic:
rfl

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

Goal state before:
pp: case neg
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 : ℝ
h : IsFiniteMeasure (μ.variation.restrict s)
hC : ∀ᵐ (x : X) ∂μ.variation.restrict s, ‖f x‖ ≤ C
hs : ¬MeasurableSet s
h's : ¬μ.variation s = 0
⊢ 0 ≤ C * ‖B‖ * μ.variation.real s

Tactic:
have : NeBot (ae (μ.variation.restrict s)) := by simpa using h's

Goal state after:
case neg
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 : ℝ
h : IsFiniteMeasure (μ.variation.restrict s)
hC : ∀ᵐ (x : X) ∂μ.variation.restrict s, ‖f x‖ ≤ C
hs : ¬MeasurableSet s
h's : ¬μ.variation s = 0
this : (ae (μ.variation.restrict s)).NeBot
⊢ 0 ≤ C * ‖B‖ * μ.variation.real s
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
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 (integrable_const 1).indicator (h'C s hs)

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

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
r : Set X
hr : MeasurableSet r
s : Set X
hs : MeasurableSet s
hpos : 0 ≤[s] μ
hneg : μ ≤[sᶜ] 0
hposPart : μ.toJordanDecomposition.posPart = μ.toMeasureOfZeroLE s hs hpos
hnegPart : μ.toJordanDecomposition.negPart = μ.toMeasureOfLEZero sᶜ ⋯ hneg
⊢ Disjoint (s ∩ r) (sᶜ ∩ r)

Tactic:
grind

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

Goal state before:
pp: case e_6
X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
r : Set X
hr : MeasurableSet r
s : Set X
hs : MeasurableSet s
hpos : 0 ≤[s] μ
hneg : μ ≤[sᶜ] 0
hposPart : μ.toJordanDecomposition.posPart = μ.toMeasureOfZeroLE s hs hpos
hnegPart : μ.toJordanDecomposition.negPart = μ.toMeasureOfLEZero sᶜ ⋯ hneg
⊢ s ∩ r ∪ sᶜ ∩ r = r

Tactic:
grind

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
⊢ ⇑(μ.transpose B) = cbmApplyMeasure μ B

Tactic:
rfl

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
s : Set X
x : E
⊢ (cbmApplyMeasure μ B s) x = (B x) (μ s)

Tactic:
rfl

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

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hG : CompleteSpace G
I : ∑' (i : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation < ∞
this : Summable fun n ↦ ∫ᵛ (x : X) in s n, f x ∂[B; μ]
N : ℕ
x : X
x✝ : ∃ i, x ∈ s (i + N)
i : ℕ
hi : x ∈ s (i + N)
⊢ i + N ≥ N ∧ x ∈ s (i + N)

Tactic:
grind

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

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hG : CompleteSpace G
I : ∑' (i : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation < ∞
this : Summable fun n ↦ ∫ᵛ (x : X) in s n, f x ∂[B; μ]
N : ℕ
x : X
x✝ : ∃ i ≥ N, x ∈ s i
i : ℕ
hi : i ≥ N
h'i : x ∈ s i
⊢ x ∈ s (i - N + N)

Tactic:
grind

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

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hG : CompleteSpace G
I : ∑' (i : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation < ∞
this✝ : Summable fun n ↦ ∫ᵛ (x : X) in s n, f x ∂[B; μ]
N : ℕ
x : X
this : (∃ i, x ∈ s (i + N)) ↔ ∃ i ≥ N, x ∈ s i
⊢ (∃ i, x ∈ s i) ↔ (∃ i < N, x ∈ s i) ∨ ∃ i, N ≤ i ∧ x ∈ s i

Tactic:
grind

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
a : M
x✝ : ∃ P, P.FG ∧ s = a +ᵥ ↑P
P : AddSubmonoid M
t : Finset M
hP : closure ↑t = P
hs : s = a +ᵥ ↑P
⊢ s = a +ᵥ ↑(closure ↑t)

Tactic:
by rwa [hP]

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

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hG : CompleteSpace G
I : ∑' (i : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation < ∞
this✝ : Summable fun n ↦ ∫ᵛ (x : X) in s n, f x ∂[B; μ]
N : ℕ
this : ⋃ n, s n = (⋃ n ∈ Finset.range N, s n) ∪ ⋃ n, s (n + N)
i j : ℕ
hi : j < N
⊢ j ≠ i + N

Tactic:
grind

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
⊢ ∫ᵛ (x : X), f x ∂[B; μ] = setToFun μ.variation ⇑(μ.transpose B) ⋯ f

Tactic:
rfl

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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
f : X → E
c : ℝ
hG : CompleteSpace G
this✝ : (c • μ).variation = ‖c‖₊ • μ.variation
this : DominatedFinMeasAdditive μ.variation (⇑((c • μ).transpose B)) (‖c‖ * ‖B‖)
⊢ (setToFun μ.variation ⇑(c • μ.transpose B) ⋯ fun x ↦ f x) =
    setToFun μ.variation (fun s ↦ c • (μ.transpose B) s) ⋯ fun x ↦ f x

Tactic:
rfl

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
β : Type u_8
f : β → X → E
s : Set β
b : β
⊢ ∫ᵛ (y : X), s.indicator (fun x ↦ f x y) b ∂[B; μ] = s.indicator (fun x ↦ ∫ᵛ (y : X), f x y ∂[B; μ]) b

Tactic:
by
  by_cases hb : b ∈ s <;> simp [hb]

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

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hG : CompleteSpace G
I : ∑' (i : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation < ∞
this✝ : Summable fun n ↦ ∫ᵛ (x : X) in s n, f x ∂[B; μ]
N : ℕ
this : ⋃ n, s n = (⋃ n ∈ Finset.range N, s n) ∪ ⋃ n, s (n + N)
i j : ℕ
hij : i ≠ j
⊢ i + N ≠ j + N

Tactic:
grind

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

Goal state before:
pp: S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id ↑∅
x : ℕ
hx : x ≥ a + 1
⊢ x ≠ a

Tactic:
grind

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

Goal state before:
pp: S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id ↑∅
x : ℕ
hx : x ≥ a + 1
⊢ x + 1 ≠ a

Tactic:
grind

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

Goal state before:
pp: S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id ↑{b}
hb : 0 < b
x : ℕ
hx : a + x * b ≥ a
⊢ a + (x + 1) * b = a + x * b + b

Tactic:
grind

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

Goal state before:
pp: S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id ↑{b}
hb : 0 < b
x : ℕ
hx : x ≥ a
heq : a + 0 * b = x + b
⊢ a + 0 * b = x

Tactic:
grind

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

Goal state before:
pp: S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id ↑{b}
hb : 0 < b
x : ℕ
hx : x ≥ a
y : ℕ
heq : a + (y + 1) * b = x + b
⊢ a + y * b = x

Tactic:
grind

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

Goal state before:
pp: 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
s : Set X
hs : MeasurableSet s
h's : μ s < ∞
⊢ (lsmul ℝ ℝ) (μ.real s) = μ.real s • ContinuousLinearMap.id ℝ G

Tactic:
rfl

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

Goal state before:
pp: case _1.zero
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
hx' : k ≤ x
hx : k + (x - k) % p + 0 * p ∈ s
⊢ k + (x - k) % p ∈ s

Tactic:
grind

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

Goal state before:
pp: case _1.succ
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
hx' : k ≤ x
n✝ : ℕ
a✝ : k + (x - k) % p + n✝ * p ∈ s → k + (x - k) % p ∈ s
hx : k + (x - k) % p + (n✝ + 1) * p ∈ s
⊢ k + (x - k) % p ∈ s

Tactic:
grind

Goal state after: