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

Goal state before:
pp: E : Type u_1
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h : ∀ (y : E), ‖y‖ = 1 → Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : ¬y = 0
⊢ Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | ‖y‖⁻¹ * r < ‖⟪(↑‖y‖)⁻¹ • y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)

Tactic:
specialize h ((‖y‖⁻¹ : 𝕜) • y) ?_

Goal state after:
E : Type u_1
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsFiniteMeasure (μ i)
h : ∀ (y : E), ‖y‖ = 1 → Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | r < ‖⟪y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
y : E
hy : ¬y = 0
⊢ ‖(↑‖y‖)⁻¹ • y‖ = 1

E : Type u_1
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsFiniteMeasure (μ i)
y : E
h : Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | r < ‖⟪(↑‖y‖)⁻¹ • y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
hy : ¬y = 0
⊢ Tendsto (fun r ↦ limsup (fun n ↦ (μ n) {x | ‖y‖⁻¹ * r < ‖⟪(↑‖y‖)⁻¹ • y, x⟫_𝕜‖}) atTop) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Measure.MeasuredSets

Goal state before:
pp: case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε✝ : ℝ≥0∞
hε : 0 < ε✝
f : ℕ → Set α
f_disj : Pairwise (Function.onFun Disjoint f)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ) (ε : ℝ≥0∞), 0 < ε → ∃ t ∈ C, μ (t ∆ f i) < ε
ε : ℝ≥0∞
εpos : 0 < ε
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε / 2
t : ℕ → Set α
tC : ∀ (i : ℕ), t i ∈ C
ht : ∀ (i : ℕ), μ (t i ∆ f i) < δ i
this : Tendsto (fun n ↦ μ (⋃ i ∈ Ici n, f i)) atTop (𝓝 0)
n : ℕ
hn : μ (⋃ i ∈ Ici n, f i) < ε / 2
x : α
⊢ x ∈ (⋃ i ∈ Finset.range n, t i) ∆ ⋃ i, f i → x ∈ (⋃ i ∈ Finset.range n, t i ∆ f i) ∪ ⋃ i ∈ Ici n, f i

Tactic:
hx

Goal state after:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε✝ : ℝ≥0∞
hε : 0 < ε✝
f : ℕ → Set α
f_disj : Pairwise (Function.onFun Disjoint f)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ) (ε : ℝ≥0∞), 0 < ε → ∃ t ∈ C, μ (t ∆ f i) < ε
ε : ℝ≥0∞
εpos : 0 < ε
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε / 2
t : ℕ → Set α
tC : ∀ (i : ℕ), t i ∈ C
ht : ∀ (i : ℕ), μ (t i ∆ f i) < δ i
this : Tendsto (fun n ↦ μ (⋃ i ∈ Ici n, f i)) atTop (𝓝 0)
n : ℕ
hn : μ (⋃ i ∈ Ici n, f i) < ε / 2
x : α
hx : x ∈ (⋃ i ∈ Finset.range n, t i) ∆ ⋃ i, f i
⊢ x ∈ (⋃ i ∈ Finset.range n, t i ∆ f i) ∪ ⋃ i ∈ Ici n, f i
Module: Mathlib.MeasureTheory.Measure.MeasuredSets

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ t ∈ supClosure C, μ (t ∆ s) < ε

Tactic:
by
  apply exists_measure_symmDiff_lt_of_generateFrom_isSetRing hC.isSetRing_supClosure ?_ ?_ hs hε
  · rcases h'C with ⟨D, D_count, DC, hD⟩
    exact ⟨D, D_count, DC.trans subset_supClosure, hD⟩
  · rw [h]
    apply le_antisymm (generateFrom_mono subset_supClosure)
    apply generateFrom_le (fun t ht ↦ ?_)
    apply measurableSet_generateFrom_of_mem_supClosure ht

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : MeasurableSpace 𝕜
inst✝⁹ : CompleteSpace 𝕜
inst✝⁸ : NormedDivisionRing A
inst✝⁷ : NormedAlgebra 𝕜 A
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : OpensMeasurableSpace 𝕜
inst✝⁴ : CompleteSpace A
inst✝³ : SecondCountableTopology A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
hz : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
x : 𝕜
⊢ x ∈ μ.support → ‖resolvent a x‖ ≤ ?C

Tactic:
hx

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : MeasurableSpace 𝕜
inst✝⁹ : CompleteSpace 𝕜
inst✝⁸ : NormedDivisionRing A
inst✝⁷ : NormedAlgebra 𝕜 A
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : OpensMeasurableSpace 𝕜
inst✝⁴ : CompleteSpace A
inst✝³ : SecondCountableTopology A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
hz : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
⊢ ‖resolvent a x‖ ≤ ?C
Module: Mathlib.MeasureTheory.Measure.ResolventTransform

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : MeasurableSpace 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : RCLike A
inst✝¹ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
ha : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
s : Set A := ball a (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ (⇑(algebraMap 𝕜 A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
x : 𝕜
⊢ x ∈ μ.support → ∀ w ∈ s, ‖resolvent w x ^ 2‖ ≤ (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)⁻¹ ^ 2

Tactic:
hx

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : MeasurableSpace 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : RCLike A
inst✝¹ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
ha : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
s : Set A := ball a (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ (⇑(algebraMap 𝕜 A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
x : 𝕜
hx : x ∈ μ.support
⊢ ∀ w ∈ s, ‖resolvent w x ^ 2‖ ≤ (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)⁻¹ ^ 2
Module: Mathlib.MeasureTheory.Measure.ResolventTransform

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : MeasurableSpace 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : RCLike A
inst✝¹ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
ha : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
s : Set A := ball a (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ (⇑(algebraMap 𝕜 A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
resolvent'_bound : ∀ᵐ (x : 𝕜) ∂μ, ∀ w ∈ s, ‖resolvent w x ^ 2‖ ≤ (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)⁻¹ ^ 2
x : 𝕜
⊢ x ∈ μ.support → ∀ w ∈ s, HasDerivAt (fun w ↦ resolvent w x) (resolvent w x ^ 2) w

Tactic:
hx

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : MeasurableSpace 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : RCLike A
inst✝¹ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
ha : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
s : Set A := ball a (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ (⇑(algebraMap 𝕜 A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
resolvent'_bound : ∀ᵐ (x : 𝕜) ∂μ, ∀ w ∈ s, ‖resolvent w x ^ 2‖ ≤ (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)⁻¹ ^ 2
x : 𝕜
hx : x ∈ μ.support
⊢ ∀ w ∈ s, HasDerivAt (fun w ↦ resolvent w x) (resolvent w x ^ 2) w
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 μ
⊢ IsOpen (⇑(algebraMap 𝕜 ℂ) '' μ.support)ᶜ

Tactic:
apply isOpen_compl_iff.mpr

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

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝² : PseudoMetricSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : ⋃ i, U i = univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : ℕ → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction : ∀ (k : ℕ), ↑((μ k) (⋃ i, ⋃ (_ : i ≤ k), U i)) ≤ 1 - ↑(NNReal.mk ε hε')
μlim : ProbabilityMeasure 𝓧
left✝ : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
Measurebound : ∀ (n : ℕ), ↑(μlim (⋃ i, ⋃ (_ : i ≤ n), U i)) ≤ 1 - ε
accumulation : Tendsto (fun n ↦ μlim (⋃ i, ⋃ (_ : i ≤ n), U i)) atTop (𝓝 (μlim (⋃ i, U i)))
⊢ False

Tactic:
rw [Cov, coeFn_univ, ← NNReal.tendsto_coe] at accumulation

Goal state after:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝² : PseudoMetricSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : ⋃ i, U i = univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ
hε' : 0 ≤ ε
hε : 0 < ε
hεbound : ε ≤ 1
μ : ℕ → ProbabilityMeasure 𝓧
hμInS : ∀ (k : ℕ), μ k ∈ S
hcontradiction : ∀ (k : ℕ), ↑((μ k) (⋃ i, ⋃ (_ : i ≤ k), U i)) ≤ 1 - ↑(NNReal.mk ε hε')
μlim : ProbabilityMeasure 𝓧
left✝ : μlim ∈ closure[ProbabilityMeasure.instTopologicalSpace] S
sub : ℕ → ℕ
hsubmono : StrictMono sub
hμconverges : Tendsto (μ ∘ sub) atTop (𝓝 μlim)
Measurebound : ∀ (n : ℕ), ↑(μlim (⋃ i, ⋃ (_ : i ≤ n), U i)) ≤ 1 - ε
accumulation : Tendsto (fun a ↦ ↑(μlim (⋃ i, ⋃ (_ : i ≤ a), U i))) atTop (𝓝 ↑1)
⊢ False
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup V
μ : VectorMeasure X V
𝕜 : Type u_3
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 V
c : 𝕜
⊢ (c • μ).variation ≤ ‖c‖₊ • μ.variation

Tactic:
by
  apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)
  simp only [smul_apply, enorm_smul, Measure.smul_apply, Measure.nnreal_smul_coe_apply]
  grw [enorm_measure_le_variation, enorm_eq_nnnorm]

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
x : MeasuredSets μ
ε : ℝ≥0∞
εpos : 0 < ε
s : Set α
sC : s ∈ C
hs : μ (s ∆ ↑x) < ε
⊢ edist x ⟨s, ⋯⟩ < ε

Tactic:
edist_comm

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
x : MeasuredSets μ
ε : ℝ≥0∞
εpos : 0 < ε
s : Set α
sC : s ∈ C
hs : μ (s ∆ ↑x) < ε
⊢ edist ⟨s, ⋯⟩ x < ε
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₁
⊢ ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s

Tactic:
have : IsClosed {s | ‖m₁ s‖ₑ ≤ μ s} :=
      isClosed_le m₁_lip.continuous.enorm MeasuredSets.continuous_measure

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 μ), ‖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 t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫ᵛ (x : X) in s, t.indicator f x ∂[B; μ] = ∫ᵛ (x : X) in s ∩ t, f x ∂[B; μ]

Tactic:
integral_indicator ht,

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 t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫ᵛ (x : X) in t, f x ∂[B; μ.restrict s] = ∫ᵛ (x : X) in s ∩ t, f x ∂[B; μ]
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
⊢ s x = t x → s.indicator f x = t.indicator f x

Tactic:
hx

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 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 : s x = t x
⊢ s.indicator f x = t.indicator f x
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
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 : AEStronglyMeasurable f (μ.variation.restrict t)
x : X
⊢ (x ∈ t → f x = AEStronglyMeasurable.mk f hf x) → (x ∈ t → f x = 0) → x ∈ t → AEStronglyMeasurable.mk f hf x = 0 x

Tactic:
hx

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
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 : AEStronglyMeasurable f (μ.variation.restrict t)
x : X
hx : x ∈ t → f x = AEStronglyMeasurable.mk f hf x
⊢ (x ∈ t → f x = 0) → x ∈ t → AEStronglyMeasurable.mk f hf x = 0 x
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
s : Set X
μ ν : Measure X
hs : IsHahnDecomposition μ ν s
⊢ (μ - ν) s = 0

Tactic:
rw [← restrict_eq_zero, restrict_sub_eq_restrict_sub_restrict hs.measurableSet]
  exact sub_eq_zero_of_le hs.le_on

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
⊢ (x ∈ t → f x = 0) → (s ∪ t).indicator f x = s.indicator f x

Tactic:
hx

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 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
⊢ (s ∪ t).indicator f x = s.indicator f x
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

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

Tactic:
hx

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
h : ∀ᵐ (x : X) ∂μ.variation, x ∉ s → f x = 0
x : X
hx : x ∉ s → f x = 0
⊢ x ∈ univ \ s → f x = 0
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 = ∞
⊢ 1 + ‖μ s‖ₑ ≤ ‖μ (s \ t)‖ₑ + ‖μ s‖ₑ

Tactic:
apply h't.trans

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‖ₑ
hI : μ.semivariation t = ∞
⊢ ‖μ t‖ₑ ≤ ‖μ (s \ t)‖ₑ + ‖μ s‖ₑ
Module: Mathlib.MeasureTheory.VectorMeasure.Prod

Goal state before:
pp: case neg
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
t : Set Y
hs : s ≠ ∅
ht : t ≠ ∅
h's : MeasurableSet s
h't : ¬MeasurableSet t
⊢ (μ.prod ν B) (s ×ˢ t) = (B (μ s)) (ν t)

pp: case pos
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
t : Set Y
hs : s ≠ ∅
ht : t ≠ ∅
h's : MeasurableSet s
h't : MeasurableSet t
⊢ (μ.prod ν B) (s ×ˢ t) = (B (μ s)) (ν t)

Tactic:
· simp only [h't, not_false_eq_true, not_measurable, _root_.map_zero]
    rw [not_measurable]
    simp [measurableSet_prod, hs, ht, h't]

Goal state after:
case pos
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
t : Set Y
hs : s ≠ ∅
ht : t ≠ ∅
h's : MeasurableSet s
h't : MeasurableSet t
⊢ (μ.prod ν B) (s ×ˢ t) = (B (μ s)) (ν t)
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
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; μ]
x : X
⊢ f x = g x → C (f x) = C (g x)

Tactic:
hx

Goal state after:
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; μ]
x : X
hx : f x = g x
⊢ C (f x) = C (g x)
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
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 ∈ s, ‖f x‖ ≤ C
x✝ : X
hx : x✝ ∈ s
hs : MeasurableSet s
x : X
⊢ x ∈ s → ‖f x‖ ≤ C

Tactic:
hx

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
C : ℝ
h : IsFiniteMeasure (μ.variation.restrict s)
hC : ∀ x ∈ s, ‖f x‖ ≤ C
x✝ : X
hx✝ : x✝ ∈ s
hs : MeasurableSet s
x : X
hx : x ∈ s
⊢ ‖f x‖ ≤ C