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

Goal state before:
pp: case refine_2.refine_1
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✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
D : Set ↥(Lp E p μ) := {s | ∃ n d t, s = key n d t}
a : E
s : Set X
ms : MeasurableSet s
hμs✝ : μ s < ∞
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : μ t ≠ ∞
hst : ‖indicatorConstLp p ms hμs b - indicatorConstLp p ⋯ hμt b‖ < ε / 3
mt : MeasurableSet t
⊢ ‖indicatorConstLp p ms ⋯ a - indicatorConstLp p ms hμs b‖ ≤ ε / 3

Tactic:
indicatorConstLp_sub,

Goal state after:
case refine_2.refine_1
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✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
D : Set ↥(Lp E p μ) := {s | ∃ n d t, s = key n d t}
a : E
s : Set X
ms : MeasurableSet s
hμs✝ : μ s < ∞
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal)
approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
b : E
b_mem : b ∈ u
hb : ‖a - b‖ < ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))
t : Set X
ht : t ∈ 𝒜₀
hμt : μ t ≠ ∞
hst : ‖indicatorConstLp p ms hμs b - indicatorConstLp p ⋯ hμt b‖ < ε / 3
mt : MeasurableSet t
⊢ ‖indicatorConstLp p ms ⋯ (a - b)‖ ≤ ε / 3
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: case refine_2
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 : MeasurableSet s
a : ℝ≥0∞
ha : a < preVariationFun (fun x ↦ ‖μ x‖ₑ) s
P : Finpartition ⟨s, hs⟩
hP : a < ∑ p ∈ P.parts, (fun x ↦ ‖μ x‖ₑ) ↑p
⊢ (↑(Finset.map (Function.Embedding.subtype MeasurableSet) P.parts)).PairwiseDisjoint id

pp: case refine_3
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 : MeasurableSet s
a : ℝ≥0∞
ha : a < preVariationFun (fun x ↦ ‖μ x‖ₑ) s
P : Finpartition ⟨s, hs⟩
hP : a < ∑ p ∈ P.parts, (fun x ↦ ‖μ x‖ₑ) ↑p
⊢ ∀ t ∈ Finset.map (Function.Embedding.subtype MeasurableSet) P.parts, MeasurableSet t

pp: case refine_4
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 : MeasurableSet s
a : ℝ≥0∞
ha : a < preVariationFun (fun x ↦ ‖μ x‖ₑ) s
P : Finpartition ⟨s, hs⟩
hP : a < ∑ p ∈ P.parts, (fun x ↦ ‖μ x‖ₑ) ↑p
⊢ a < ∑ p ∈ Finset.map (Function.Embedding.subtype MeasurableSet) P.parts, ‖μ p‖ₑ

Tactic:
· intro i hi  j hj hij
    simp only [coe_map, Function.Embedding.subtype_apply, Set.mem_image, SetLike.mem_coe,
      Subtype.exists, exists_and_right, exists_eq_right] at hi hj
    rcases hi with ⟨h'i, i_mem⟩
    rcases hj with ⟨h'j, j_mem⟩
    exact (disjoint_subtype_iff (fun _ _ hs ht ↦ hs.inter ht) _).1
      (P.disjoint i_mem j_mem (by simpa using hij))

Goal state after:
case refine_3
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 : MeasurableSet s
a : ℝ≥0∞
ha : a < preVariationFun (fun x ↦ ‖μ x‖ₑ) s
P : Finpartition ⟨s, hs⟩
hP : a < ∑ p ∈ P.parts, (fun x ↦ ‖μ x‖ₑ) ↑p
⊢ ∀ t ∈ Finset.map (Function.Embedding.subtype MeasurableSet) P.parts, MeasurableSet t

case refine_4
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 : MeasurableSet s
a : ℝ≥0∞
ha : a < preVariationFun (fun x ↦ ‖μ x‖ₑ) s
P : Finpartition ⟨s, hs⟩
hP : a < ∑ p ∈ P.parts, (fun x ↦ ‖μ x‖ₑ) ↑p
⊢ a < ∑ p ∈ Finset.map (Function.Embedding.subtype MeasurableSet) P.parts, ‖μ p‖ₑ
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: case refine_2
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 : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
hμ : preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≠ ∞
P : Finpartition ⟨s, hs⟩
hP : preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≤ ∑ p ∈ P.parts, (fun x ↦ ‖μ x‖ₑ) ↑p + ε
⊢ (↑(Finset.map (Function.Embedding.subtype MeasurableSet) P.parts)).PairwiseDisjoint id

pp: case refine_3
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 : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
hμ : preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≠ ∞
P : Finpartition ⟨s, hs⟩
hP : preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≤ ∑ p ∈ P.parts, (fun x ↦ ‖μ x‖ₑ) ↑p + ε
⊢ ∀ t ∈ Finset.map (Function.Embedding.subtype MeasurableSet) P.parts, MeasurableSet t

pp: case refine_4
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 : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
hμ : preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≠ ∞
P : Finpartition ⟨s, hs⟩
hP : preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≤ ∑ p ∈ P.parts, (fun x ↦ ‖μ x‖ₑ) ↑p + ε
⊢ preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≤ ∑ x ∈ Finset.map (Function.Embedding.subtype MeasurableSet) P.parts, ‖μ x‖ₑ + ε

Tactic:
· intro i hi  j hj hij
    simp only [coe_map, Function.Embedding.subtype_apply, Set.mem_image, SetLike.mem_coe,
      Subtype.exists, exists_and_right, exists_eq_right] at hi hj
    rcases hi with ⟨h'i, i_mem⟩
    rcases hj with ⟨h'j, j_mem⟩
    exact (disjoint_subtype_iff (fun _ _ hs ht ↦ hs.inter ht) _).1
      (P.disjoint i_mem j_mem (by simpa using hij))

Goal state after:
case refine_3
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 : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
hμ : preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≠ ∞
P : Finpartition ⟨s, hs⟩
hP : preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≤ ∑ p ∈ P.parts, (fun x ↦ ‖μ x‖ₑ) ↑p + ε
⊢ ∀ t ∈ Finset.map (Function.Embedding.subtype MeasurableSet) P.parts, MeasurableSet t

case refine_4
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 : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
hμ : preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≠ ∞
P : Finpartition ⟨s, hs⟩
hP : preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≤ ∑ p ∈ P.parts, (fun x ↦ ‖μ x‖ₑ) ↑p + ε
⊢ preVariationFun (fun x ↦ ‖μ x‖ₑ) s ≤ ∑ x ∈ Finset.map (Function.Embedding.subtype MeasurableSet) P.parts, ‖μ x‖ₑ + ε
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 : 𝕜
hc : c ≠ 0
⊢ ‖c‖₊ • ‖c⁻¹‖₊ • (c • μ).variation = (c • μ).variation

Tactic:
by
    simp [smul_smul, mul_inv_cancel₀ (nnnorm_ne_zero_iff.mpr hc)]

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

Goal state before:
pp: case succ.a
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ μ s
inst✝ : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
n : ℕ
ih : m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
⊢ MeasurableSet (⋃ x ∈ Finset.range n, f x)

Tactic:
exact Finset.measurableSet_biUnion _ (fun i hi ↦ f_meas i)

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

Goal state before:
pp: case a
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
m : Set α → E
hm : ∀ (s : Set α), ‖m s‖ₑ ≤ μ s
inst✝ : IsFiniteMeasure μ
h'm : ∀ (s t : Set α), MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t
h''m : ∀ (s : Set α), ¬MeasurableSet s → m s = 0
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Function.onFun Disjoint f)
A : ∀ (n : ℕ), m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i)
n : ℕ
this : ⋃ i, f i = (⋃ i ∈ Finset.range n, f i) ∪ ⋃ i ∈ Set.Ici n, f i
⊢ MeasurableSet (⋃ i ∈ Finset.range n, f i)

Tactic:
exact Finset.measurableSet_biUnion _ (fun i hi ↦ f_meas i)

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∞), 0 < ε → ∃ y ∈ C', edist x y < ε

Tactic:
intro x

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∞), 0 < ε → ∃ y ∈ C', edist x y < ε
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
ι : Type u_7
inst✝ : Fintype ι
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), μ.IntegrableOn f (s i)
⊢ ∫ᵛ (x : X) in ⋃ i, s i, f x ∂[B; μ] = ∑ i, ∫ᵛ (x : X) in s i, f x ∂[B; μ]

Tactic:
convert setIntegral_biUnion_finset Finset.univ (fun i _ => hs i) _ fun i _ => hf i

Goal state after:
case e'_2.e'_12
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
inst✝ : Fintype ι
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), μ.IntegrableOn f (s i)
x✝ : ι
⊢ s x✝ = ⋃ (_ : x✝ ∈ Finset.univ), s x✝

case convert_5
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
inst✝ : Fintype ι
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), μ.IntegrableOn f (s i)
⊢ (↑Finset.univ).Pairwise (Disjoint on s)
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 : Nonempty α
hlim : Tendsto f atTop (𝓝 (atTop.limUnder f))
u : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
⊢ Ici a ⊆ ⋃ n, Icc a (u n)

Tactic:
intro 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
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atTop (𝓝 (atTop.limUnder f))
u : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
x : α
⊢ x ∈ Ici a → x ∈ ⋃ n, Icc a (u n)
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 : Nonempty α
hlim : Tendsto f atTop (𝓝 (atTop.limUnder f))
u : ℕ → α
u_mono : Monotone u
hu : Tendsto u atTop atTop
A : Tendsto (fun n ↦ hf.vectorMeasure (Icc a (u n))) atTop (𝓝 (hf.vectorMeasure (Ici a)))
⊢ ∀ᶠ (n : ℕ) in atTop, a ≤ u n

Tactic:
simp only [tendsto_atTop, eventually_atTop] at hu

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
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atTop (𝓝 (atTop.limUnder f))
u : ℕ → α
u_mono : Monotone u
A : Tendsto (fun n ↦ hf.vectorMeasure (Icc a (u n))) atTop (𝓝 (hf.vectorMeasure (Ici a)))
hu : ∀ (b : α), ∃ a, ∀ (b_1 : ℕ), a ≤ b_1 → b ≤ u b_1
⊢ ∀ᶠ (n : ℕ) in atTop, a ≤ u n
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 : Nonempty α
hlim : Tendsto f atBot (𝓝 (atBot.limUnder f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
⊢ Iic a ⊆ ⋃ n, Icc (u n) a

Tactic:
intro 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
hf : BoundedVariationOn f univ
a : α
this : Nonempty α
hlim : Tendsto f atBot (𝓝 (atBot.limUnder f))
u : ℕ → α
u_anti : Antitone u
hu : Tendsto u atTop atBot
x : α
⊢ x ∈ Iic a → x ∈ ⋃ n, Icc (u n) a
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
ℓ : StrongDual ℝ E
hℓ : ℓ ∈ {ℓ | ‖ℓ‖ₑ ≤ 1}
⊢ (μ.mapRange ↑ℓ ⋯).variation s ≤ μ.variation s

Tactic:
suffices (μ.mapRange (ℓ : E →+ ℝ) ℓ.continuous).variation ≤ μ.variation from this s

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 ≤ μ.variation
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
⊢ ‖μ s‖₊ ≤ μ.bound

Tactic:
by
  rw [← ENNReal.coe_le_coe, ← enorm_eq_nnnorm]
  exact enorm_apply_le_bound

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

Goal state before:
pp: X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
inst✝² : CompleteSpace G
inst✝¹ : IsFiniteMeasure μ.variation
inst✝ : SFinite ν.variation
s : Set (X × Y)
hs : MeasurableSet s
⊢ ‖B.flip‖ₑ * ∫⁻ (a : X), ‖ν (Prod.mk a ⁻¹' s)‖ₑ ∂μ.variation ≤
    ‖B‖ₑ * ∫⁻ (x : X), ν.variation (Prod.mk x ⁻¹' s) ∂μ.variation

Tactic:
ContinuousLinearMap.opENorm_flip,

Goal state after:
X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
inst✝² : CompleteSpace G
inst✝¹ : IsFiniteMeasure μ.variation
inst✝ : SFinite ν.variation
s : Set (X × Y)
hs : MeasurableSet s
⊢ ‖B‖ₑ * ∫⁻ (a : X), ‖ν (Prod.mk a ⁻¹' s)‖ₑ ∂μ.variation ≤ ‖B‖ₑ * ∫⁻ (x : X), ν.variation (Prod.mk x ⁻¹' s) ∂μ.variation
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‖ * ‖μ s‖ * ‖x‖

Tactic:
intro x

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
s : Set X
x : E
⊢ ‖(cbmApplyMeasure μ B s) x‖ ≤ ‖B‖ * ‖μ s‖ * ‖x‖
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: case neg
α : 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 : ¬MeasurableSet s
⊢ ‖m'' s‖ₑ ≤ μ s

Tactic:
simp [not_measurable _ hs]

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

Goal state before:
pp: M : Type u_1
ι : Type u_3
inst✝ : AddCommMonoid M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsSemilinearSet (t i)
⊢ IsSemilinearSet (⋃₀ (t '' s))

Tactic:
apply sUnion (hs.image t)

Goal state after:
M : Type u_1
ι : Type u_3
inst✝ : AddCommMonoid M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsSemilinearSet (t i)
⊢ ∀ s_1 ∈ t '' s, IsSemilinearSet s_1
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
inst✝ : Nontrivial E
C : ℝ≥0
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = C * ‖x‖₊ * ‖y‖₊
hC : C ≠ 0
s : Set X
hs : MeasurableSet s
x : E
hx : x ≠ 0
this : ‖μ s‖₊ ≤ ‖B.flip (μ s)‖₊ / C
⊢ ‖μ s‖ₑ ≤ C⁻¹ • ‖B.flip (μ s)‖ₑ

Tactic:
div_eq_inv_mul

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
inst✝ : Nontrivial E
C : ℝ≥0
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = C * ‖x‖₊ * ‖y‖₊
hC : C ≠ 0
s : Set X
hs : MeasurableSet s
x : E
hx : x ≠ 0
this : ‖μ s‖₊ ≤ C⁻¹ * ‖B.flip (μ s)‖₊
⊢ ‖μ s‖ₑ ≤ C⁻¹ • ‖B.flip (μ s)‖ₑ
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: M : Type u_1
ι : Type u_3
inst✝ : AddCommMonoid M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsProperSemilinearSet (t i)
⊢ IsProperSemilinearSet (⋃₀ (t '' s))

Tactic:
apply sUnion (hs.image t)

Goal state after:
M : Type u_1
ι : Type u_3
inst✝ : AddCommMonoid M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsProperSemilinearSet (t i)
⊢ ∀ s_1 ∈ t '' s, IsProperSemilinearSet s_1
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
⊢ ↑δ * (∑ i ∈ g.range, ‖i‖ₑ)⁻¹ > 0

Tactic:
by simp [δpos]

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

Goal state before:
pp: case neg
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 : x ∈ s
hx' : k ≤ 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

Tactic:
refine Or.inr ⟨k + (x - k) % p, ⟨⟨?_1, ?_2⟩, ?_1, ?_3⟩, (x - k) / p, ?_4⟩

Goal state after:
case _1
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 : x ∈ s
hx' : k ≤ x
⊢ k + (x - k) % p ∈ s

case _2
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 : x ∈ s
hx' : k ≤ x
⊢ k ≤ k + (x - k) % p

case _3
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 : x ∈ s
hx' : k ≤ x
⊢ k + (x - k) % p < k + p

case _4
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 : x ∈ s
hx' : k ≤ x
⊢ k + (x - k) % p + (x - k) / p * p = x