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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, m s ≠ ∞
hm_tendsto : ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n ↦ m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n ↦ (⋃ i, f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
h_tendsto : Tendsto (fun n ↦ m (s n)) atTop (𝓝 0)
n : ℕ
⊢ m (s n) = m (⋃ i, f i) - ∑ i ∈ Finset.range (n + 1), m (f i)

Tactic:
addContent_sdiff_of_ne_top m hC hm_ne_top hUf (hC.accumulate_mem hf n)
      (Set.accumulate_subset_iUnion _),

Goal state after:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, m s ≠ ∞
hm_tendsto : ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n ↦ m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n ↦ (⋃ i, f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
h_tendsto : Tendsto (fun n ↦ m (s n)) atTop (𝓝 0)
n : ℕ
⊢ m (⋃ i, f i) - m (accumulate f n) = m (⋃ i, f i) - ∑ i ∈ Finset.range (n + 1), m (f i)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
ι : Type u_4
s : Finset ι
f : ι → Set α
hd : (↑s).PairwiseDisjoint f
hm : ∀ b ∈ s, MeasurableSet (f b)
⊢ v (⋃ b ∈ s, f b) = ∑ p ∈ s, v (f p)

Tactic:
by
  rw [← Finset.sum_attach, Finset.attach_eq_univ, ← tsum_fintype (L := .unconditional s)]
  exact of_biUnion s.countable_toSet hd hm

Goal state after:
Module: Mathlib.MeasureTheory.Covering.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      blimsup (fun i ↦ cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ cthickening (r i) (s i)) atTop p
r' : ℕ → ℝ := fun i ↦ if 0 < r i then r i else 1 / (↑i + 1)
hr' : Tendsto r' atTop (𝓝[>] 0)
h₀ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)
h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)
i : ℕ
hi : r i ≤ 0
hi' : M * r i ≤ 0
⊢ cthickening (M * r i) (s i) = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i)

Tactic:
cthickening_of_nonpos hi'

Goal state after:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      blimsup (fun i ↦ cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ cthickening (r i) (s i)) atTop p
r' : ℕ → ℝ := fun i ↦ if 0 < r i then r i else 1 / (↑i + 1)
hr' : Tendsto r' atTop (𝓝[>] 0)
h₀ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)
h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)
i : ℕ
hi : r i ≤ 0
hi' : M * r i ≤ 0
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i) =
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x ↦ ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
⊢ ∃ M, eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨M ^ (1 / p.toReal), ?_⟩

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x ↦ ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
⊢ eLpNorm ({x | M ^ (1 / p.toReal) ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ HasSum (fun n ↦ v (t n)) (v (⋃ n, s n))

Tactic:
rw [← iUnion_disjointed]

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ HasSum (fun n ↦ v (t n)) (v (⋃ i, disjointed s i))
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : MeasurableSpace β
x✝ : β
v✝ : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
hx : x ∈ ⋃ i, f i
this : MeasurableSet (⋃ i, f i)
j : ℕ
hj : x ∈ f j
⊢ HasSum (fun i ↦ if x ∈ f i then v else 0) (if x ∈ f j then v else 0)

Tactic:
apply hasSum_single

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : MeasurableSpace β
x✝ : β
v✝ : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
hx : x ∈ ⋃ i, f i
this : MeasurableSet (⋃ i, f i)
j : ℕ
hj : x ∈ f j
⊢ ∀ (b' : ℕ), b' ≠ j → (if x ∈ f b' then v else 0) = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ μ.toENNRealVectorMeasure.ennrealToMeasure s = μ s

Tactic:
rw [ennrealToMeasure_apply hs, toENNRealVectorMeasure_apply_measurable hs]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: case refine_1
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝ : CompleteSpace E
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : ⋃ i, sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), μ (sets x) < ∞
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x
n : ℕ
this :
  (μ.restrict (sets n))[fun ω ↦ (B ((sets n).indicator f ω)) (g ω) | m] =ᵐ[μ.restrict (sets n)] fun ω ↦
    (B ((sets n).indicator f ω)) ((μ.restrict (sets n))[g | m] ω)
⊢ (fun ω ↦ (B (f ω)) (g ω)) =ᵐ[μ.restrict (sets n)] fun ω ↦ (B ((sets n).indicator f ω)) (g ω)

pp: case refine_2
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝ : CompleteSpace E
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : ⋃ i, sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), μ (sets x) < ∞
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x
n : ℕ
this :
  (μ.restrict (sets n))[fun ω ↦ (B ((sets n).indicator f ω)) (g ω) | m] =ᵐ[μ.restrict (sets n)] fun ω ↦
    (B ((sets n).indicator f ω)) ((μ.restrict (sets n))[g | m] ω)
⊢ (fun ω ↦ (B ((sets n).indicator f ω)) ((μ.restrict (sets n))[g | m] ω)) =ᵐ[μ.restrict (sets n)] fun ω ↦
    (B (f ω)) ((μ.restrict (sets n))[g | m] ω)

Tactic:
· filter_upwards [indicator_ae_eq_restrict (f := f) <| hm _ <| h_meas n] with ω hω
      rw [hω]

Goal state after:
case refine_2
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝ : CompleteSpace E
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : ⋃ i, sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), μ (sets x) < ∞
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x
n : ℕ
this :
  (μ.restrict (sets n))[fun ω ↦ (B ((sets n).indicator f ω)) (g ω) | m] =ᵐ[μ.restrict (sets n)] fun ω ↦
    (B ((sets n).indicator f ω)) ((μ.restrict (sets n))[g | m] ω)
⊢ (fun ω ↦ (B ((sets n).indicator f ω)) ((μ.restrict (sets n))[g | m] ω)) =ᵐ[μ.restrict (sets n)] fun ω ↦
    (B (f ω)) ((μ.restrict (sets n))[g | m] ω)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: case refine_2
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝ : CompleteSpace E
f : Ω → F
g : Ω → E
hf : StronglyMeasurable f
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
hm : m ≤ mΩ
hμm : SigmaFinite (μ.trim hm)
sets : ℕ → Set Ω
h_univ : ⋃ i, sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), μ (sets x) < ∞
h_norm : ∀ (x : ℕ), ∀ x_1 ∈ sets x, ‖f x_1‖ ≤ ↑x
n : ℕ
this :
  (μ.restrict (sets n))[fun ω ↦ (B ((sets n).indicator f ω)) (g ω) | m] =ᵐ[μ.restrict (sets n)] fun ω ↦
    (B ((sets n).indicator f ω)) ((μ.restrict (sets n))[g | m] ω)
⊢ (fun ω ↦ (B ((sets n).indicator f ω)) ((μ.restrict (sets n))[g | m] ω)) =ᵐ[μ.restrict (sets n)] fun ω ↦
    (B (f ω)) ((μ.restrict (sets n))[g | m] ω)

Tactic:
· filter_upwards [indicator_ae_eq_restrict (f := f) <| hm _ <| h_meas n] with ω hω
      rw [hω]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l)
⊢ s (i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l) < 0

Tactic:
rw [of_sdiff hmeas hi₁, s.of_disjoint_iUnion]

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l)
⊢ s i - ∑' (i_1 : ℕ), s (⋃ (_ : i_1 < k), s.restrictNonposSeq i i_1) < 0

case neg.hm
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l)
⊢ ∀ (i_1 : ℕ), MeasurableSet (⋃ (_ : i_1 < k), s.restrictNonposSeq i i_1)

case neg.hd
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l)
⊢ Pairwise (Function.onFun Disjoint fun l ↦ ⋃ (_ : l < k), s.restrictNonposSeq i l)

case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l)
⊢ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l ⊆ i
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
s✝ s : SignedMeasure α
i : Set α := ⋯.choose
hi : MeasurableSet ⋯.choose ∧ 0 ≤[⋯.choose] s ∧ s ≤[⋯.chooseᶜ] 0
⊢ (s.toMeasureOfZeroLE i ⋯ ⋯) iᶜ = 0

Tactic:
rw [toMeasureOfZeroLE_apply _ _ hi.1 hi.1.compl]

Goal state after:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
s✝ s : SignedMeasure α
i : Set α := ⋯.choose
hi : MeasurableSet ⋯.choose ∧ 0 ≤[⋯.choose] s ∧ s ≤[⋯.chooseᶜ] 0
⊢ ↑(NNReal.mk (s (⋯.choose ∩ ⋯.chooseᶜ)) ⋯) = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case neg.hd
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l)
a b : ℕ
⊢ a ≠ b → Function.onFun Disjoint (fun l ↦ ⋃ (_ : l < k), s.restrictNonposSeq i l) a b

Tactic:
hab

Goal state after:
case neg.hd
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l)
a b : ℕ
hab : a ≠ b
⊢ Function.onFun Disjoint (fun l ↦ ⋃ (_ : l < k), s.restrictNonposSeq i l) a b
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
i j : Set α
hi₁ : MeasurableSet i
hi₂ : v ≤[i] w
hj₁ : MeasurableSet j
hj₂ : v ≤[j] w
⊢ v ≤[i ∪ j] w

Tactic:
by
  rw [Set.union_eq_iUnion]
  refine restrict_le_restrict_countable_iUnion v w ?_ ?_
  · measurability
  · rintro (_ | _) <;> simpa

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

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ w (uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t) = 0

pp: α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ t = uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t

Tactic:
of_union _ (hmu.compl.inter hmt) ((hmv.compl.diff hmu.compl).inter hmt),

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ w (uᶜ ∩ t) + w (vᶜ \ uᶜ ∩ t) = 0

α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ Disjoint (uᶜ ∩ t) (vᶜ \ uᶜ ∩ t)

α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁵ : AddCommMonoid M
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid N
inst✝² : TopologicalSpace N
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
inst✝¹ : T2Space N
inst✝ : ContinuousAdd M
u : Set α
hmu : MeasurableSet u
hu₁ : ∀ t ⊆ u, v₁ t = 0
hu₂ : ∀ t ⊆ uᶜ, w t = 0
v : Set α
hmv : MeasurableSet v
hv₁ : ∀ t ⊆ v, v₂ t = 0
hv₂ : ∀ t ⊆ vᶜ, w t = 0
t : Set α
ht : t ⊆ uᶜ ∪ vᶜ
hmt : MeasurableSet t
⊢ t = uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε < ∞
hμ : μ = 0
⊢ ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε

pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε < ∞
hμ : ¬μ = 0
⊢ ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε

Tactic:
· exact ⟨0, fun n _ => by simp [hμ]⟩

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
h : ε < ∞
hμ : ¬μ = 0
⊢ ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : s i < 0
hi₁ : MeasurableSet i
h : ¬s ≤[i] 0
hn : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
A : Set α := i \ ⋃ l, s.restrictNonposSeq i l
hA : A = i \ ⋃ l, s.restrictNonposSeq i l
bdd : ℕ → ℕ := fun n ↦ s.findExistsOneDivLT (i \ ⋃ k, ⋃ (_ : k ≤ n), s.restrictNonposSeq i k)
hn' : ∀ (n : ℕ), ¬s ≤[i \ ⋃ l, ⋃ (_ : l ≤ n), s.restrictNonposSeq i l] 0
h₁ : s i = s A + ∑' (l : ℕ), s (s.restrictNonposSeq i l)
h₂ : s A ≤ s i
h₃' : Summable fun n ↦ 1 / (↑(bdd n) + 1)
h₃ : Tendsto (fun n ↦ ↑(bdd n) + 1) atTop atTop
h₄ : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ↑(bdd a)
A_meas : MeasurableSet A
E : Set α
hE₁ : MeasurableSet E
hE₂ : E ⊆ A
hE₃ : 0 E < s E
k : ℕ
hk : ∀ (a : ℕ), k ≤ a → max (1 / s E + 1) 1 ≤ ↑(bdd a)
this : (s E)⁻¹ < ↑(bdd k)
⊢ (↑(bdd k))⁻¹ < s E

Tactic:
exact inv_lt_of_inv_lt₀ hE₃ this

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ s.totalVariation ⟂ₘ μ.ennrealToMeasure → s ⟂ᵥ μ

Tactic:
· rintro ⟨u, hmeas, hu₁, hu₂⟩
    refine
      VectorMeasure.MutuallySingular.mk u hmeas
        (fun t htu _ => null_of_totalVariation_zero _ (measure_mono_null htu hu₁)) fun t htv hmt =>
        ?_
    rw [← VectorMeasure.ennrealToMeasure_apply hmt]
    exact measure_mono_null htv hu₂

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
⊢ μ.toSignedMeasure s ≤ ν.toSignedMeasure s ↔ μ s ≤ ν s

Tactic:
simp_rw [toSignedMeasure_apply_measurable hs, real_def]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
⊢ (μ s).toReal ≤ (ν s).toReal ↔ μ s ≤ ν s
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ s ≤[iᶜ] 0
hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0
⊢ s (i ∆ j) = 0 ∧ s (iᶜ ∆ jᶜ) = 0

Tactic:
rw [restrict_le_restrict_iff s 0, restrict_le_restrict_iff 0 s] at hi' hj'

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → 0 j_1 ≤ s j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ s (i ∆ j) = 0 ∧ s (iᶜ ∆ jᶜ) = 0

α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → 0 j ≤ s j) ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' : 0 ≤[j] s ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ MeasurableSet j

α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' : 0 ≤[j] s ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → s j_1 ≤ 0 j_1
⊢ MeasurableSet i

α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → s j ≤ 0 j
hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0
⊢ MeasurableSet jᶜ

α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ s ≤[iᶜ] 0
hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0
⊢ MeasurableSet iᶜ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s

Tactic:
conv_rhs =>
    rw [← toSignedMeasure_toJordanDecomposition s, JordanDecomposition.toSignedMeasure]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure