mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
J : Finset ι
T : Set ((i : ↥J) → α ↑i)
hT : MeasurableSet T
ht_eq : t = cylinder J T
S' : Set ((i : ↥(I ∪ J)) → α ↑i) := restrict₂ ⋯ ⁻¹' S
T' : Set ((i : ↥(I ∪ J)) → α ↑i) := restrict₂ ⋯ ⁻¹' T
hS' : MeasurableSet S'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (I ∪ J) S'
h_eq2 : t = cylinder (I ∪ J) T'
h_eq3 : s ∪ t = cylinder (I ∪ J) (S' ∪ T')
h : IsEmpty ((i : ι) → α i)
⊢ (P (I ∪ J)) (S' ∪ T') = (P (I ∪ J)) S' + (P (I ∪ J)) T'

Tactic:
simp [hP.eq_zero_of_isEmpty]

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
f g : Dual K V
v : V
a b : K
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
hg0 : g ≠ 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
ha : ∀ (v_1 : V), (auxTransvection hf * e) v_1 - a • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb : ∀ (v_1 : V), (auxTransvection hg * e) v_1 - b • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
c : K := b - a
hc : c = b - a
key : ∀ (x : V), g (e x) • (v - e v) - c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hc0 : c ≠ 0
x : V
a✝ : x ∈ ⊤
⊢ -g (e x) • (e v - v) = g (e x) • (v - e v)

Tactic:
neg_smul,

Goal state after:
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
f g : Dual K V
v : V
a b : K
hv : LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
hfv : f v = 1
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
hg0 : g ≠ 0
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
ha : ∀ (v_1 : V), (auxTransvection hf * e) v_1 - a • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hb : ∀ (v_1 : V), (auxTransvection hg * e) v_1 - b • v_1 ∈ (↑e).fixedSubmodule ⊔ K ∙ v
c : K := b - a
hc : c = b - a
key : ∀ (x : V), g (e x) • (v - e v) - c • x ∈ (↑e).fixedSubmodule ⊔ K ∙ v
hc0 : c ≠ 0
x : V
a✝ : x ∈ ⊤
⊢ -(g (e x) • (e v - v)) = g (e x) • (v - e v)
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
u : α
h : u ≤ u
h' : ∃ p, p.1 ≤ p.2 ∧ Set.Ioc u u = Set.Ioc p.1 p.2
u' : α := h'.choose.1
v' : α := h'.choose.2
hu'v' : u' ≤ v' ∧ Set.Ioc u u = Set.Ioc u' v'
⊢ f v' - f u' = f u - f u

Tactic:
grind [Set.Ioc_eq_empty_iff]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
⊢ ∀ (h : ∃ p, p.1 ≤ p.2 ∧ ∅ = Set.Ioc p.1 p.2), f h.choose.2 - f h.choose.1 = 0

Tactic:
grind [Set.Ioc_eq_empty_iff]

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

Goal state before:
pp: case refine_2
α : 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
⊢ (⋃ i, f i) ∩ (⋃ i, accumulate f i)ᶜ = ∅

Tactic:
Set.iUnion_accumulate

Goal state after:
case refine_2
α : 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
⊢ (⋃ i, f i) ∩ (⋃ x, f x)ᶜ = ∅
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf_mono : Monotone f
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
⊢ Tendsto (fun n ↦ m (f n)) atTop (𝓝 (m (⋃ i, f i)))

Tactic:
rw [← iUnion_disjointed, m_iUnion _ (hC.disjointed_mem hf) (by rwa [iUnion_disjointed])
      (disjoint_disjointed f)]
  have h n : m (f n) = ∑ i ∈ range (n + 1), m (disjointed f i) := by
    nth_rw 1 [← addContent_accumulate _ hC (disjoint_disjointed f) (hC.disjointed_mem hf),
    ← hf_mono.partialSups_eq, ← partialSups_disjointed, partialSups_eq_biSup, accumulate]
    rfl
  simp_rw [h]
  refine (tendsto_add_atTop_iff_nat (f := (fun k ↦ ∑ i ∈ range k, m (disjointed f i))) 1).2 ?_
  exact ENNReal.tendsto_nat_tsum _

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)
⊢ ∀ (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

Tactic:
clear p hr r

Goal state after:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
s : ℕ → Set α
M : ℝ
hM : 0 < M
⊢ ∀ (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
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ HasSum (Function.extend e (fun i ↦ v (f i)) 0) (v (⋃ i, f i))

Tactic:
convert! m_iUnion v (f := Function.extend e f fun _ ↦ ∅) _ _

Goal state after:
case e'_5
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
x✝ : ℕ
⊢ Function.extend e (fun i ↦ v (f i)) 0 x✝ = v (Function.extend e f (fun x ↦ ∅) x✝)

case e'_6
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ ⋃ i, f i = ⋃ i, Function.extend e f (fun x ↦ ∅) i

case convert_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ ∀ (i : ℕ), MeasurableSet (Function.extend e f (fun x ↦ ∅) i)

case convert_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ Pairwise (Disjoint on Function.extend e f fun x ↦ ∅)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : IsEmpty α
μ ν : VectorMeasure α M
⊢ μ = ν

Tactic:
by ext; rw [apply_eq_zero_of_isEmpty, apply_eq_zero_of_isEmpty]

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

Goal state before:
pp: Ω : 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
hm : m ≤ mΩ
inst✝ : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
⊢ μ[fun ω ↦ (B (AEStronglyMeasurable.mk f hf ω)) (g ω) | m] =ᵐ[μ] fun ω ↦
    (B (AEStronglyMeasurable.mk f hf ω)) (μ[g | m] ω)

Tactic:
refine condExp_stronglyMeasurable_bilin_of_bound B hm hf.stronglyMeasurable_mk
      hg c ?_

Goal state after:
Ω : 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
hm : m ≤ mΩ
inst✝ : IsFiniteMeasure μ
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
⊢ ∀ᵐ (ω : Ω) ∂μ, ‖AEStronglyMeasurable.mk f hf ω‖ ≤ c
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 : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
⊢ eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
eLpNorm_indicator_eq_eLpNorm_restrict hs

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
hp : ¬p = 0
⊢ eLpNorm f p (μ.restrict s) ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ (restrict μ.toSignedMeasure s) t = (μ.restrict s).toSignedMeasure t

Tactic:
rw [restrict_apply _ hs ht, Measure.toSignedMeasure_apply_measurable (ht.inter hs),
    Measure.toSignedMeasure_apply_measurable ht, measureReal_restrict_apply ht]

Goal state after:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
x : α
⊢ (if x ∈ {x | ‖f x‖ < M} then ‖f x‖ else 0) < ?m.95

Tactic:
split_ifs with h
        exacts [h, hMpos]

Goal state after:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.82 s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.82 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator ({x | M ≤ ↑‖f x‖₊}.indicator f + {x | ‖f x‖ < M}.indicator f)) p μ ≤ 2 * ENNReal.ofReal ε

Tactic:
eLpNorm_indicator_eq_eLpNorm_restrict hs

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      ?m.82 s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p ?m.82 ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f + {x | ‖f x‖ < M}.indicator f) p (μ.restrict s) ≤ 2 * ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case pos
α : 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 : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → w s = 0 → v s = 0
s : Set α
hs : w s = 0
hmeas : MeasurableSet s
⊢ v s = 0

pp: case neg
α : 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 : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → w s = 0 → v s = 0
s : Set α
hs : w s = 0
hmeas : ¬MeasurableSet s
⊢ v s = 0

Tactic:
· exact h hmeas hs

Goal state after:
case neg
α : 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 : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → w s = 0 → v s = 0
s : Set α
hs : w s = 0
hmeas : ¬MeasurableSet s
⊢ v s = 0
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
right✝ : eLpNorm f p μ < ∞
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᵐ[μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f') p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm f p (μ.restrict s) = eLpNorm (s.indicator f') p μ

Tactic:
eLpNorm_indicator_eq_eLpNorm_restrict hs

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
right✝ : eLpNorm f p μ < ∞
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᵐ[μ] f'
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f') p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f' p (μ.restrict s)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifIntegrable f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ :
  ∀ (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (f (Fin.last n))) p μ ≤ ENNReal.ofReal ε
i : Fin (n + 1)
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ↑i < n
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
rw [(_ : f i = g ⟨i.val, hi⟩)]

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifIntegrable f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ :
  ∀ (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (f (Fin.last n))) p μ ≤ ENNReal.ofReal ε
i : Fin (n + 1)
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ↑i < n
⊢ eLpNorm (s.indicator (g ⟨↑i, hi⟩)) p μ ≤ ENNReal.ofReal ε

α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifIntegrable f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun k ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ :
  ∀ (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (f (Fin.last n))) p μ ≤ ENNReal.ofReal ε
i : Fin (n + 1)
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : ↑i < n
⊢ f i = g ⟨↑i, hi⟩
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
⊢ r • s = -(-r • s)

Tactic:
neg_smul,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
⊢ r • s = - -(r • s)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case neg.posPart
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
⊢ (r • s).toJordanDecomposition.posPart = (r • s.toJordanDecomposition).posPart

Tactic:
rw [real_smul_posPart_neg _ _ hr,
        show r • s = -(-r • s) by rw [neg_smul, neg_neg], toJordanDecomposition_neg, neg_posPart,
        toJordanDecomposition_smul_real_nonneg, ← smul_negPart, real_smul_nonneg]

Goal state after:
case neg.posPart.hr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
⊢ 0 ≤ -r

case neg.posPart.hr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
⊢ 0 ≤ -r
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ (-s).totalVariation = s.totalVariation

Tactic:
simp [totalVariation, toJordanDecomposition_neg, add_comm]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Set α
hs : MeasurableSet s
⊢ VectorMeasure.restrict μ.toSignedMeasure s = (μ.restrict s).toSignedMeasure

Tactic:
by
  ext A hA
  simp [VectorMeasure.restrict_apply, hA, hs]

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

Goal state before:
pp: Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
⊢ Tendsto (fun n ↦ ∫⁻ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ) atTop (𝓝 (μ F))

Tactic:
apply measure_of_cont_bdd_of_tendsto_indicator μ F_closed.measurableSet
    (fun n ↦ thickenedIndicator (δs_pos n) F) fun n ω ↦ thickenedIndicator_le_one (δs_pos n) F ω

Goal state after:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
⊢ Tendsto (fun n ω ↦ (thickenedIndicator ⋯ F) ω) atTop (𝓝 (F.indicator fun x ↦ 1))
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
⊢ ∀ (s : Set α),
    MeasurableSet s → μ s < ∞ → IntegrableOn (SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm)) s μ

Tactic:
exact fun _ _ _ => (integrable_of_integrable_trim hm
      (SignedMeasure.integrable_rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm))).integrableOn

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝² : s.HaveLebesgueDecomposition μ
inst✝¹ : t.HaveLebesgueDecomposition μ
inst✝ : (s + t).HaveLebesgueDecomposition μ
⊢ (s + t).rnDeriv μ =ᵐ[μ] s.rnDeriv μ + t.rnDeriv μ

Tactic:
refine
    Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _)
      ((integrable_rnDeriv _ _).add (integrable_rnDeriv _ _)) ?_

Goal state after:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝² : s.HaveLebesgueDecomposition μ
inst✝¹ : t.HaveLebesgueDecomposition μ
inst✝ : (s + t).HaveLebesgueDecomposition μ
⊢ μ.withDensityᵥ ((s + t).rnDeriv μ) = μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
a✝ : μ s < ∞
| ∫ (x : α) in s, f x ∂μ

Tactic:
rw [← hf.withDensityᵥ_trim_eq_integral hm hs,
      ← SignedMeasure.withDensityᵥ_rnDeriv_eq ((μ.withDensityᵥ f).trim hm) (μ.trim hm)
        (hf.withDensityᵥ_trim_absolutelyContinuous hm)]

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
a✝ : μ s < ∞
| ((μ.trim hm).withDensityᵥ (SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm))) s
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
hμs' : ¬μ s = 0
⊢ eLpNorm (s.indicator ({x | ‖f i x‖₊ < C}.indicator (f i))) p μ ≤ ↑C * μ s ^ (1 / p.toReal)

Tactic:
eLpNorm_indicator_eq_eLpNorm_restrict hs

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
hμs' : ¬μ s = 0
⊢ eLpNorm ({x | ‖f i x‖₊ < C}.indicator (f i)) p (μ.restrict s) ≤ ↑C * μ s ^ (1 / p.toReal)