mathlib-initiative/mathlib-tactics huggingface dataset:
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 := ⋯
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 : A
hw : w ∈ s
⊢ x ∈ resolventSet 𝕜 w

Tactic:
replace hw := hs_μ hw

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 : A
hw : w ∈ (⇑(algebraMap 𝕜 A) '' μ.support)ᶜ
⊢ x ∈ resolventSet 𝕜 w
Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
⊢ μ (s ∩ t) = μ s * μ t

Tactic:
cases μ.zero_one s <;> cases μ.zero_one t

Goal state after:
case inl.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝¹ : μ s = 0
h✝ : μ t = 0
⊢ μ (s ∩ t) = μ s * μ t

case inl.inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝¹ : μ s = 0
h✝ : μ t = 1
⊢ μ (s ∩ t) = μ s * μ t

case inr.inl
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝¹ : μ s = 1
h✝ : μ t = 0
⊢ μ (s ∩ t) = μ s * μ t

case inr.inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this✝ : μ (s ∩ t) ≤ μ s
this : μ (s ∩ t) ≤ μ t
h✝¹ : μ s = 1
h✝ : μ t = 1
⊢ μ (s ∩ t) = μ s * μ t
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
S : Set (ProbabilityMeasure E)
hS : IsTightMeasureSet {x | ∃ μ ∈ S, ↑μ = x}
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
n : ℕ
K : Set E
K_comp : IsCompact K
hK : ∀ μ ∈ {x | ∃ μ ∈ S, ↑μ = x}, μ Kᶜ ≤ ↑(u n)
μ : ProbabilityMeasure E
hμ : μ ∈ S
this : ↑μ Kᶜ ≤ ↑(u n)
⊢ ↑(μ Kᶜ) ≤ ↑(u n)

Tactic:
by simpa using this

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
p q : ℝ≥0∞
inst✝² : Fact (1 ≤ q)
ι : Type u_2
inst✝¹ : Fintype ι
E : ι → Type u_3
inst✝ : (i : ι) → NormedAddCommGroup (E i)
f : X → PiLp q E
⊢ MemLp f p μ ↔ MemLp (fun x ↦ (WithLp.ofLp ∘ f) x) p μ

Tactic:
exact (PiLp.lipschitzWith_ofLp q E).memLp_comp_iff_of_antilipschitz
    (PiLp.antilipschitzWith_ofLp q E) (by simp) |>.symm

Goal state after:
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf : Integrable f μ
⊢ (∫ (x : X), f x ∂μ).ofLp.1 = ∫ (x : X), (f x).fst ∂μ

Tactic:
conv => enter [1, 1]; change WithLp.prodContinuousLinearEquiv q ℝ E F _

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hf : Integrable f μ
⊢ ((WithLp.prodContinuousLinearEquiv q ℝ E F) (∫ (x : X), f x ∂μ)).1 = ∫ (x : X), (f x).fst ∂μ
Module: Mathlib.MeasureTheory.SpecificCodomains.WithLp

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
hf : Integrable f μ
⊢ (∫ (x : X), f x ∂μ).ofLp.2 = ∫ (x : X), (f x).snd ∂μ

Tactic:
conv => enter [1, 1]; change WithLp.prodContinuousLinearEquiv q ℝ E F _

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
q : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ q)
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
f : X → WithLp q (E × F)
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
hf : Integrable f μ
⊢ ((WithLp.prodContinuousLinearEquiv q ℝ E F) (∫ (x : X), f x ∂μ)).2 = ∫ (x : X), (f x).snd ∂μ
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

Tactic:
intro i hi  j hj hij

Goal state after:
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
i : Set X
hi : i ∈ ↑(Finset.map (Function.Embedding.subtype MeasurableSet) P.parts)
j : Set X
hj : j ∈ ↑(Finset.map (Function.Embedding.subtype MeasurableSet) P.parts)
hij : i ≠ j
⊢ Function.onFun Disjoint id i j
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

Tactic:
intro i hi  j hj hij

Goal state after:
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 + ε
i : Set X
hi : i ∈ ↑(Finset.map (Function.Embedding.subtype MeasurableSet) P.parts)
j : Set X
hj : j ∈ ↑(Finset.map (Function.Embedding.subtype MeasurableSet) P.parts)
hij : i ≠ j
⊢ Function.onFun Disjoint id i j
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: case succ
α : 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)
⊢ m (⋃ i ∈ Finset.range (n + 1), f i) = ∑ i ∈ Finset.range (n + 1), m (f i)

Tactic:
| succ n ih =>

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

Tactic:
by_cases h's : MeasurableSet s

Goal state after:
case pos
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
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
f : X → E
s : Set X
hs : μ.variation s = 0
h's : MeasurableSet s
⊢ ∫ᵛ (x : X) in s, f x ∂[B; μ] = 0

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
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
f : X → E
s : Set X
hs : μ.variation s = 0
h's : ¬MeasurableSet s
⊢ ∫ᵛ (x : X) in s, f x ∂[B; μ] = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation

Goal state before:
pp: case succ
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
n : ℕ
ih : MeasurableSet (s n) ∧ μ.semivariation (s n) = ∞
⊢ MeasurableSet (s (n + 1)) ∧ μ.semivariation (s (n + 1)) = ∞

Tactic:
| succ n ih =>

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

Goal state before:
pp: case inr.inr
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 ≠ ∅
⊢ (μ.prod ν B) (s ×ˢ t) = (B (μ s)) (ν t)

Tactic:
by_cases h's : MeasurableSet s

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
⊢ (μ.prod ν B) (s ×ˢ t) = (B (μ s)) (ν t)

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
⊢ (μ.prod ν B) (s ×ˢ t) = (B (μ s)) (ν t)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x : M
⊢ (x = 0 ∨ ∃ y ∈ closure (insert a t), a + y = x) → x ∈ closure (a +ᵥ ↑(closure t))

Tactic:
rintro (rfl | ⟨x, hx, rfl⟩)
    · simp
    · simp_rw [insert_eq, closure_union, mem_sup, mem_closure_singleton] at hx
      rcases hx with ⟨_, ⟨n, rfl⟩, ⟨x, hx, rfl⟩⟩
      rw [add_left_comm]
      refine add_mem (nsmul_mem (mem_closure_of_mem ?_) _)
        (mem_closure_of_mem (vadd_mem_vadd_set hx))
      nth_rw 2 [← add_zero a]
      exact vadd_mem_vadd_set (zero_mem _)

Goal state after:
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 < δ
⊢ ∃ ρ > 0, ‖B‖₊ * ρ ≤ δ

Tactic:
by
      rcases eq_or_ne (‖B‖₊) 0 with hB | hB
      · exact ⟨1, zero_lt_one, by simp [hB]⟩
      · refine ⟨‖B‖₊ ⁻¹ * δ, by positivity, ?_⟩
        rw [← mul_assoc]
        apply mul_le_of_le_one_left (by positivity) mul_inv_le_one

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)
⊢ ‖B‖ₑ * ∫⁻ (x : X) in ⋃ n, s (n + N), ‖f x‖ₑ ∂μ.variation =
    ∑' (k : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s (k + N), ‖f x‖ₑ ∂μ.variation

Tactic:
rw [lintegral_iUnion (fun i ↦ hm _), ENNReal.tsum_mul_left]

Goal state after:
case hd
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)
⊢ Pairwise (Disjoint on fun i ↦ s (i + N))
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
⊢ ‖∫ᵛ (a : X), f a ∂[B; μ]‖ ≤ ‖B‖ * ∫ (a : X), ‖f a‖ ∂μ.variation

Tactic:
have le_ae : ∀ᵐ a ∂μ.variation, 0 ≤ ‖f a‖ :=
    Eventually.of_forall fun a => norm_nonneg _
  by_cases h : AEStronglyMeasurable f μ.variation
  · calc ‖∫ᵛ a, f a ∂[B; μ]‖
    _ ≤ ‖B‖ * ENNReal.toReal (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ.variation) :=
      norm_integral_le_lintegral_norm
    _ = ‖B‖ * ∫ a, ‖f a‖ ∂μ.variation := by
      rw [integral_eq_lintegral_of_nonneg_ae le_ae <| h.norm]
  · rw [integral_non_aestronglyMeasurable h, norm_zero]
    positivity

Goal state after:
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})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
i : E
hi : i ≠ 0
this :
  ∃ P,
    (∀ t ∈ P, t ⊆ ⇑g ⁻¹' {i}) ∧
      (↑P).PairwiseDisjoint id ∧
        (∀ t ∈ P, MeasurableSet t) ∧
          ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤ ∑ p ∈ P, ‖((μ.transpose B).restrict s) p‖ₑ + ρ
⊢ ∃ P,
    (∀ t ∈ P, t ⊆ ⇑g ⁻¹' {i}) ∧
      (↑P).PairwiseDisjoint id ∧
        (∀ t ∈ P, MeasurableSet t) ∧
          ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
            ‖i‖ₑ * (∑ p ∈ P, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)

Tactic:
obtain ⟨P, hP, h'P, h''P, h'''P⟩ := this

Goal state after:
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})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
i : E
hi : i ≠ 0
P : Finset (Set X)
hP : ∀ t ∈ P, t ⊆ ⇑g ⁻¹' {i}
h'P : (↑P).PairwiseDisjoint id
h''P : ∀ t ∈ P, MeasurableSet t
h'''P : ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤ ∑ p ∈ P, ‖((μ.transpose B).restrict s) p‖ₑ + ρ
⊢ ∃ P,
    (∀ t ∈ P, t ⊆ ⇑g ⁻¹' {i}) ∧
      (↑P).PairwiseDisjoint id ∧
        (∀ t ∈ P, MeasurableSet t) ∧
          ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
            ‖i‖ₑ * (∑ p ∈ P, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case pos
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})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
y : M
hxy : a + x + y ∈ s
hy : y = 0
⊢ y ∈ f a

pp: case neg
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})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
y : M
hxy : a + x + y ∈ s
hy : ¬y = 0
⊢ y ∈ f a

Tactic:
· simp [hy]

Goal state after:
case neg
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})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
y : M
hxy : a + x + y ∈ s
hy : ¬y = 0
⊢ y ∈ f a
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: α : Type u_1
A : Set ℕ
inst✝ : Finite α
φ : presburger[[↑A]].Formula α
e : α ⊕ Fin 0 ≃ α := Equiv.sumEmpty α (Fin 0)
x : α → ℕ
⊢ φ.Realize x ↔
    ∃ x_1, BoundedFormula.Realize φ (x_1 ∘ Sum.inl) (x_1 ∘ Sum.inr) ∧ (LinearMap.funLeft ℕ ℕ ⇑e.symm) x_1 = x

Tactic:
(e.arrowCongr (.refl ℕ)).exists_congr_left

Goal state after:
α : Type u_1
A : Set ℕ
inst✝ : Finite α
φ : presburger[[↑A]].Formula α
e : α ⊕ Fin 0 ≃ α := Equiv.sumEmpty α (Fin 0)
x : α → ℕ
⊢ φ.Realize x ↔
    ∃ b,
      BoundedFormula.Realize φ ((e.arrowCongr (_root_.Equiv.refl ℕ)).symm b ∘ Sum.inl)
          ((e.arrowCongr (_root_.Equiv.refl ℕ)).symm b ∘ Sum.inr) ∧
        (LinearMap.funLeft ℕ ℕ ⇑e.symm) ((e.arrowCongr (_root_.Equiv.refl ℕ)).symm b) = x
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
⊢ a +ᵥ ↑(closure t) = ↑⟨a, ⋯⟩ +ᵥ ⇑(closure (insert a t)).subtype '' ↑(closure (⇑(closure (insert a t)).subtype ⁻¹' t))

Tactic:
← coe_map,

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
⊢ a +ᵥ ↑(closure t) =
    ↑⟨a, ⋯⟩ +ᵥ ↑(AddSubmonoid.map (closure (insert a t)).subtype (closure (⇑(closure (insert a t)).subtype ⁻¹' t)))
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
f : ↑hs.basisSet → ℕ
⊢ 0 ≤ (∑ x, hs.basis.repr (toRatVec (f x • ↑x))) i

Tactic:
Finsupp.coe_finsetSum,

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
f : ↑hs.basisSet → ℕ
⊢ 0 ≤ (∑ i, ⇑(hs.basis.repr (toRatVec (f i • ↑i)))) i
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ ∑ i, (hs.floor x i).toNat • ↑i ≤ x + ∑ i, (-hs.floor x i).toNat • ↑i

Tactic:
by
  rw [← toRatVec_mono]
  simp only [floor, map_add, map_sum, map_nsmul]
  rw [← sub_le_iff_le_add, ← Finset.sum_sub_distrib]
  conv =>
    enter [1, 2, _]
    rw [← Nat.cast_smul_eq_nsmul ℤ, ← Nat.cast_smul_eq_nsmul ℤ, ← sub_smul,
      Int.toNat_sub_toNat_neg, ← Int.cast_smul_eq_zsmul ℚ]
  trans toRatVec x - toRatVec hs.base
  · conv => rhs; rw [← hs.basis.sum_repr (toRatVec x - toRatVec hs.base)]
    refine Finset.sum_le_sum fun i _ => ?_
    rw [basis_apply]
    exact smul_le_smul_of_nonneg_right (Int.floor_le _) (toRatVec_nonneg _)
  · simp [toRatVec_nonneg]

Goal state after: