mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
Λ : (E →C_c ℝ) → ℝ
h₀Λ : ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-↑C * ‖g.toBoundedContinuousFunction‖) (↑C * ‖g.toBoundedContinuousFunction‖)
hΛ : ∀ (g : E →C_c ℝ), Tendsto (fun μ ↦ ∫ (x : E), g x ∂↑μ) (↑f) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : μlim univ ≤ ENNReal.ofReal ↑C
μlim' : FiniteMeasure E := ⟨μlim, ⋯⟩
⊢ ∃ x ∈ {μ | μ.mass ≤ C}, ↑f ≤ 𝓝 x

Tactic:
refine ⟨μlim', ?_, ?_⟩

Goal state after:
case refine_1
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
Λ : (E →C_c ℝ) → ℝ
h₀Λ : ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-↑C * ‖g.toBoundedContinuousFunction‖) (↑C * ‖g.toBoundedContinuousFunction‖)
hΛ : ∀ (g : E →C_c ℝ), Tendsto (fun μ ↦ ∫ (x : E), g x ∂↑μ) (↑f) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : μlim univ ≤ ENNReal.ofReal ↑C
μlim' : FiniteMeasure E := ⟨μlim, ⋯⟩
⊢ μlim' ∈ {μ | μ.mass ≤ C}

case refine_2
E : Type u_1
inst✝⁴ : MeasurableSpace E
inst✝³ : TopologicalSpace E
inst✝² : T2Space E
inst✝¹ : BorelSpace E
inst✝ : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C} ∈ f
Λ : (E →C_c ℝ) → ℝ
h₀Λ : ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-↑C * ‖g.toBoundedContinuousFunction‖) (↑C * ‖g.toBoundedContinuousFunction‖)
hΛ : ∀ (g : E →C_c ℝ), Tendsto (fun μ ↦ ∫ (x : E), g x ∂↑μ) (↑f) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : μlim univ ≤ ENNReal.ofReal ↑C
μlim' : FiniteMeasure E := ⟨μlim, ⋯⟩
⊢ ↑f ≤ 𝓝 μlim'
Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℂ), 0 ≤ ∑ i, ‖x i‖ ^ p
⊢ volume {x | (∑ i, ‖x i‖ ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))

Tactic:
have h₂ : ∀ x : ι → ℂ, 0 ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p) := fun x => rpow_nonneg (h₁ x) _

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℂ), 0 ≤ ∑ i, ‖x i‖ ^ p
h₂ : ∀ (x : ι → ℂ), 0 ≤ (∑ i, ‖x i‖ ^ p) ^ (1 / p)
⊢ volume {x | (∑ i, ‖x i‖ ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
h : preVariationFun f s ≠ ∞
⊢ ∃ P, preVariationFun f s ≤ ∑ p ∈ P.parts, f ↑p + ε

Tactic:
by
  rcases eq_top_or_lt_top ε with rfl | h'ε
  · simp
  lift ε to NNReal using h'ε.ne
  exact exists_Finpartition_sum_ge _ hs (by simpa using hε) h

Goal state after:
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: case neg
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
hn : ¬n = 0
ε' : ℝ≥0
hε' : 0 < ε'
hsnetop : preVariationFun f (⋃ i, s i) < ∞
ε : ℝ≥0 := ε' / ↑n
hε : 0 < ε
⊢ ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ i, s i) + ↑ε'

Tactic:
have hs'' i : preVariationFun f (s i) ≠ ⊤ := lt_top_iff_ne_top.mp <|
    (mono f (MeasurableSet.iUnion hs) (Set.subset_iUnion s i)).trans_lt hsnetop

Goal state after:
case neg
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
hn : ¬n = 0
ε' : ℝ≥0
hε' : 0 < ε'
hsnetop : preVariationFun f (⋃ i, s i) < ∞
ε : ℝ≥0 := ε' / ↑n
hε : 0 < ε
hs'' : ∀ (i : ℕ), preVariationFun f (s i) ≠ ∞
⊢ ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ i, s i) + ↑ε'
Module: Mathlib.MeasureTheory.Measure.ResolventTransform

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : HereditarilyLindelofSpace 𝕜
inst✝⁴ : CompleteSpace 𝕜
inst✝³ : MeasurableSpace 𝕜
inst✝² : BorelSpace 𝕜
inst✝¹ : NormedAlgebra 𝕜 ℂ
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
z : ℂ
⊢ z ∈ (⇑(algebraMap 𝕜 ℂ) '' μ.support)ᶜ →
    DifferentiableWithinAt ℂ (resolventTransform μ) (⇑(algebraMap 𝕜 ℂ) '' μ.support)ᶜ z

Tactic:
hz

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : HereditarilyLindelofSpace 𝕜
inst✝⁴ : CompleteSpace 𝕜
inst✝³ : MeasurableSpace 𝕜
inst✝² : BorelSpace 𝕜
inst✝¹ : NormedAlgebra 𝕜 ℂ
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
z : ℂ
hz : z ∈ (⇑(algebraMap 𝕜 ℂ) '' μ.support)ᶜ
⊢ DifferentiableWithinAt ℂ (resolventTransform μ) (⇑(algebraMap 𝕜 ℂ) '' μ.support)ᶜ z
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

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

Tactic:
← univ_inter s

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

Goal state before:
pp: X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : CountablyGenerated X
inst✝ : SFinite μ
this✝ : IsSeparable (μ.restrict μ.sigmaFiniteSet)
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : (μ.restrict μ.sigmaFiniteSet).MeasureDense 𝒜
ℬ : Set (Set X) := {x | ∃ s ∈ 𝒜, s ∩ μ.sigmaFiniteSet = x}
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
hs : (μ.restrict μ.sigmaFiniteSetᶜ) s = 0
this : (μ.restrict μ.sigmaFiniteSet) s ≠ ∞
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict μ.sigmaFiniteSet) (s ∆ t) < ENNReal.ofReal ε
⊢ μ (μ.sigmaFiniteSetᶜ ∩ s) + μ (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) = 0

Tactic:
by
                rw [inter_comm, ← μ.restrict_apply ms, hs, ← inter_assoc, inter_comm,
                  ← inter_assoc, inter_compl_self, empty_inter, measure_empty, zero_add]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: case refine_2.inr
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : CountablyGenerated X
inst✝ : SFinite μ
this : IsSeparable (μ.restrict μ.sigmaFiniteSet)
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : (μ.restrict μ.sigmaFiniteSet).MeasureDense 𝒜
ℬ : Set (Set X) := {x | ∃ s ∈ 𝒜, s ∩ μ.sigmaFiniteSet = x}
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
hs : (μ.restrict μ.sigmaFiniteSetᶜ) s = ∞
⊢ ∞ ≤ μ s

Tactic:
← hs

Goal state after:
case refine_2.inr
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : CountablyGenerated X
inst✝ : SFinite μ
this : IsSeparable (μ.restrict μ.sigmaFiniteSet)
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : (μ.restrict μ.sigmaFiniteSet).MeasureDense 𝒜
ℬ : Set (Set X) := {x | ∃ s ∈ 𝒜, s ∩ μ.sigmaFiniteSet = x}
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
hs : (μ.restrict μ.sigmaFiniteSetᶜ) s = ∞
⊢ (μ.restrict μ.sigmaFiniteSetᶜ) s ≤ μ s
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: case neg
X : Type u_1
mX : MeasurableSpace X
μ : VectorMeasure X ℝ≥0∞
s : Set X
h : ¬MeasurableSet s
⊢ preVariationFun (⇑μ) s = μ s

Tactic:
preVariationFun_of_not_measurableSet μ h,

Goal state after:
case neg
X : Type u_1
mX : MeasurableSpace X
μ : VectorMeasure X ℝ≥0∞
s : Set X
h : ¬MeasurableSet s
⊢ 0 = μ s
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: case pos
α : 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 : Nonempty α
⊢ IsFiniteMeasure (hf.stieltjesFunctionRightLim ⋯.some).measure

Tactic:
apply StieltjesFunction.isFiniteMeasure_of_forall_abs_le
    (C := (eVariationOn f.rightLim univ).toReal) _ (fun x ↦ ?_)

Goal state after:
α : 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 : Nonempty α
x : α
⊢ |↑(hf.stieltjesFunctionRightLim ⋯.some) x| ≤ (eVariationOn (Function.rightLim f) univ).toReal
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case insert.hfs
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
s : ι → Set X
a✝ : ι
s✝ : Finset ι
hat : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, MeasurableSet (s i)) →
    (↑s✝).Pairwise (Disjoint on s) →
      (∀ i ∈ s✝, μ.IntegrableOn f (s i)) →
        ∫ᵛ (x : X) in ⋃ i ∈ s✝, s i, f x ∂[B; μ] = ∑ i ∈ s✝, ∫ᵛ (x : X) in s i, f x ∂[B; μ]
hs : MeasurableSet (s a✝) ∧ ∀ x ∈ s✝, MeasurableSet (s x)
hf : μ.IntegrableOn f (s a✝) ∧ ∀ x ∈ s✝, μ.IntegrableOn f (s x)
h's : (↑s✝).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Disjoint on s) a✝ b ∧ (Disjoint on s) b a✝
⊢ μ.IntegrableOn f (s a✝)

Tactic:
exact hf.1

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
A : ⋯.choose (Ioc a b) = Function.rightLim f b - Function.rightLim f a
⊢ hf.vectorMeasure (Ioc a b) = Function.rightLim f b - Function.rightLim f a

Tactic:
have B : (if hx : ∃ (x : α), IsBot x then VectorMeasure.dirac hx.choose
      (f.rightLim hx.choose - f hx.choose) else 0) (Ioc a b) = 0 := by
    by_cases hx : ∃ (x : α), IsBot x
    · simp only [hx, ↓reduceDIte]
      rw [VectorMeasure.dirac_apply_of_notMem]
      simp only [mem_Ioc, not_and_or, not_lt, not_le]
      exact Or.inl (hx.choose_spec _)
    · simp [hx]

Goal state after:
α : 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
A : ⋯.choose (Ioc a b) = Function.rightLim f b - Function.rightLim f a
B :
  (if hx : ∃ x, IsBot x then VectorMeasure.dirac hx.choose (Function.rightLim f hx.choose - f hx.choose) else 0)
      (Ioc a b) =
    0
⊢ hf.vectorMeasure (Ioc a b) = Function.rightLim f b - Function.rightLim f a
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
t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ht_eq : ∀ᵐ (x : X) ∂μ.variation, x ∈ t → f x = 0
ht : MeasurableSet t
hf : (μ.restrict t).Integrable f
⊢ AEStronglyMeasurable f (μ.restrict t).variation

Tactic:
exact hf.1

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

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

Tactic:
rw [h₁', h₂] at partition₁

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
h₂' : ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0
partition₁ :
  toSignedMeasure 0 + (VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ) =
    (μ - ν).toSignedMeasure
partition₂ : ((ν - μ).restrict s).toSignedMeasure + ((ν - μ).restrict sᶜ).toSignedMeasure = (ν - μ).toSignedMeasure
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
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 α
hs : s ∈ supClosure C
⊢ ‖m₀ s‖ₑ ≤ μ s

Tactic:
rw [hC.mem_supClosure_iff] at 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
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 α
hs : ∃ P, ↑P.parts ⊆ C
⊢ ‖m₀ s‖ₑ ≤ μ 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
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 α
hs : s ∈ supClosure C
⊢ MeasurableSet s

Tactic:
rw [hC.mem_supClosure_iff] at 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
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 α
hs : ∃ P, ↑P.parts ⊆ C
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.VectorMeasure.Prod

Goal state before:
pp: case h_lim.hm
ι : 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)
A :
  ∀ (a : Finset ℕ),
    ∑ y ∈ a, ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ] = ∫ᵛ (x : X), ∑ y ∈ a, ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ]
x : X
⊢ ∀ (i : ℕ), MeasurableSet (Prod.mk x ⁻¹' f i)

pp: case h_lim.hd
ι : 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)
A :
  ∀ (a : Finset ℕ),
    ∑ y ∈ a, ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ] = ∫ᵛ (x : X), ∑ y ∈ a, ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ]
x : X
⊢ Pairwise (Disjoint on fun b ↦ Prod.mk x ⁻¹' f b)

Tactic:
· exact fun i ↦ measurable_prodMk_left (f_meas i)

Goal state after:
case h_lim.hd
ι : 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)
A :
  ∀ (a : Finset ℕ),
    ∑ y ∈ a, ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ] = ∫ᵛ (x : X), ∑ y ∈ a, ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ]
x : X
⊢ Pairwise (Disjoint on fun b ↦ Prod.mk x ⁻¹' f b)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case mp.add.inr.inl
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 + 0 = 0 ∨ ∃ y ∈ closure (insert a t), a + y = a + x + 0

Tactic:
exact Or.inr ⟨x, hx, by 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
hμ : μ.Integrable f
hν : ν.Integrable f
⊢ ∫ᵛ (x : X), f x ∂[B; μ + -ν] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[B; ν]

Tactic:
integral_add_vectorMeasure hμ hν.neg_vectorMeasure,

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
f : X → E
μ ν : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hμ : μ.Integrable f
hν : ν.Integrable f
⊢ ∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[B; -ν] = ∫ᵛ (x : X), f x ∂[B; μ] - ∫ᵛ (x : X), f x ∂[B; ν]
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case mpr
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 : ℕ
⊢ (x ∈ s ∧ x < k ∨ ∃ x_1, ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ a, x_1 + a * p = x) → x ∈ s

Tactic:
· rintro (⟨hx, hx'⟩ | ⟨x, ⟨⟨hx, hx'⟩, _⟩, m, rfl⟩)
      · exact hx
      · induction m with grind

Goal state after:
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
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
x : M
hx : x ∈ s
y : M
hy : y ∈ s
hxy : x ≤ y
z : M
⊢ z ∈ g x → z ∈ g y

Tactic:
hz

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 : M
hx : x ∈ s
y : M
hy : y ∈ s
hxy : x ≤ y
z : M
hz : z ∈ g x
⊢ z ∈ g y