mathlib-initiative/mathlib-tactics huggingface dataset:
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
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
u : V
hu : LinearIndependent K ![(↑e).fixedSubmodule.mkQ u, e.fixedReduce ((↑e).fixedSubmodule.mkQ u)]
f : Dual K V
hf : map f ((↑e).fixedSubmodule ⊔ K ∙ (e u - u)) = ⊥
hfu : f u = 0
⊢ f (e u - u) = 0

Tactic:
← Submodule.mem_bot K,

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
u : V
hu : LinearIndependent K ![(↑e).fixedSubmodule.mkQ u, e.fixedReduce ((↑e).fixedSubmodule.mkQ u)]
f : Dual K V
hf : map f ((↑e).fixedSubmodule ⊔ K ∙ (e u - u)) = ⊥
hfu : f u = 0
⊢ f (e u - u) ∈ ⊥
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
⊢ s ∩ t ∈ measurableCylinders α

Tactic:
by
  rw [mem_measurableCylinders] at *
  obtain ⟨s₁, S₁, hS₁, rfl⟩ := hs
  obtain ⟨s₂, S₂, hS₂, rfl⟩ := ht
  classical
  refine ⟨s₁ ∪ s₂,
    Finset.restrict₂ Finset.subset_union_left ⁻¹' S₁ ∩
      {f | Finset.restrict₂ Finset.subset_union_right f ∈ S₂}, ?_, ?_⟩
  · refine MeasurableSet.inter ?_ ?_
    · exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _) hS₁
    · exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _) hS₂
  · exact inter_cylinder _ _ _ _

Goal state after:
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: case union
α : Type u_1
𝒜 ℬ : Set (Set α)
h : 𝒜 ⊆ ℬ
hℬ : IsSetAlgebra ℬ
s t u : Set α
hs✝ : generateSetAlgebra 𝒜 t
ht✝ : generateSetAlgebra 𝒜 u
t_mem : t ∈ ℬ
u_mem : u ∈ ℬ
⊢ t ∪ u ∈ ℬ

Tactic:
exact hℬ.union_mem t_mem u_mem

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

Goal state before:
pp: case h_ss
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ↑(insert s (hC.disjointOfDiff ht hs)) ⊆ C

Tactic:
rw [coe_insert]

Goal state after:
case h_ss
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ insert s ↑(hC.disjointOfDiff ht hs) ⊆ C
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case h_dis
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ (↑(insert s (hC.disjointOfDiff ht hs))).PairwiseDisjoint id

Tactic:
rw [coe_insert]

Goal state after:
case h_dis
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ (insert s ↑(hC.disjointOfDiff ht hs)).PairwiseDisjoint id
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case h_mem
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ⋃₀ ↑(insert s (hC.disjointOfDiff ht hs)) ∈ C

Tactic:
rw [coe_insert]

Goal state after:
case h_mem
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ⋃₀ insert s ↑(hC.disjointOfDiff ht hs) ∈ C
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' m : AddContent G C
hC : IsSetSemiring C
⊢ m.supClosureFun ∅ = 0

Tactic:
by rw [m.supClosureFun_apply_of_mem hC hC.empty_mem, addContent_empty]

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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetRing C
s : ℕ → Set α
hs_disj : Pairwise (Disjoint on s)
hsC : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : m (accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i)
⊢ accumulate s n ∈ C

Tactic:
exact hC.accumulate_mem hsC n

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

Goal state before:
pp: case insert
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝² : AddCommMonoid G
m : AddContent G C
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i)
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ m (⋃ i_1 ∈ insert i S, s i_1) ≤ ∑ i ∈ insert i S, m (s i)

Tactic:
rw [Finset.sum_insert hiS]
    simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
    simp only [Finset.mem_insert, forall_eq_or_imp] at hs
    refine (addContent_union_le hC hs.1 (hC.biUnion_mem S hs.2)).trans ?_
    exact add_le_add le_rfl (h hs.2)

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

Goal state before:
pp: case inl
α : 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₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : ℕ → ℝ := fun i ↦ max 0 (r₁ i)
R₂ : ℕ → ℝ := fun i ↦ max 0 (r₂ i)
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
hM' : 1 ≤ M
⊢ blimsup (fun i ↦ cthickening (max 0 (r₁ i)) (s i)) atTop p ≤ᵐ[μ]
    blimsup (fun i ↦ cthickening (max 0 (r₂ i)) (s i)) atTop p

Tactic:
apply LE.le.eventuallyLE

Goal state after:
case inl
α : 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₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : ℕ → ℝ := ⋯
R₂ : ℕ → ℝ := ⋯
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
hM' : 1 ≤ M
⊢ blimsup (fun i ↦ cthickening (max 0 (r₁ i)) (s i)) atTop p ⊆
    blimsup (fun i ↦ cthickening (max 0 (r₂ i)) (s i)) atTop p
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
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ v (A ∪ B) = v A + v B

Tactic:
rw [Set.union_eq_iUnion, of_disjoint_iUnion, tsum_fintype, Fintype.sum_bool, cond, cond]

Goal state after:
case hm
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∀ (i : Bool), MeasurableSet (bif i then A else B)

case hd
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
A B : Set α
h : Disjoint A B
hA : MeasurableSet A
hB : MeasurableSet B
⊢ Pairwise (Disjoint on fun b ↦ bif b then A else B)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : 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
⊢ eLpNorm ({x | 1 ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε

Tactic:
simp [hp_ne_zero]

Goal state after:
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
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : v (B \ A) = 0
⊢ v A = v (A \ B ∪ A ∩ B)

Tactic:
by simp only [Set.sdiff_union_inter]

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

Goal state before:
pp: case neg.refine_5
Ω : 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 : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
fs : ℕ → SimpleFunc Ω F := hf.approxBounded c
hfs_tendsto : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun x ↦ (fs x) ω) atTop (𝓝 (f ω))
hμ : ¬μ = 0
this✝ : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (ω : Ω), ‖(fs n) ω‖ ≤ c
this : μ[fun ω ↦ (B (f ω)) (μ[g | m] ω) | m] = fun ω ↦ (B (f ω)) (μ[g | m] ω)
⊢ Integrable (fun x ↦ ‖B‖ * c * ‖g x‖) μ

Tactic:
exact hg.norm.const_mul _

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
⊢ blimsup (fun i ↦ cthickening (1 / 2 * r i) (s i)) atTop p ≤ᵐ[μ] blimsup (fun i ↦ thickening (r i) (s i)) atTop p

Tactic:
apply LE.le.eventuallyLE

Goal state after:
case refine_1
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
⊢ blimsup (fun i ↦ cthickening (1 / 2 * r i) (s i)) atTop p ⊆ blimsup (fun i ↦ thickening (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✝ : ContinuousAdd M
v w : VectorMeasure α M
x✝ : Set α
hi : ¬MeasurableSet x✝
⊢ 0 + w x✝ = 0

Tactic:
w.not_measurable hi,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
x✝ : Set α
hi : ¬MeasurableSet x✝
⊢ 0 + 0 = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
x✝ : Set α
hi : ¬MeasurableSet x✝
⊢ 0 - w x✝ = 0

Tactic:
w.not_measurable hi,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
x✝ : Set α
hi : ¬MeasurableSet x✝
⊢ 0 - 0 = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
⊢ μ.real i + ν.real i = (μ.toSignedMeasure + ν.toSignedMeasure) i

Tactic:
_root_.add_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
⊢ μ.real i + ν.real i = μ.toSignedMeasure i + ν.toSignedMeasure i
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
i : Set α
hi : MeasurableSet i
⊢ μ i + ν i = (μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) i

Tactic:
_root_.add_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
i : Set α
hi : MeasurableSet i
⊢ μ i + ν i = μ.toENNRealVectorMeasure i + ν.toENNRealVectorMeasure i
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 < ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε

Tactic:
obtain ⟨M, hMpos, hM⟩ := hf.eLpNorm_indicator_norm_ge_pos_le hmeas hε

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 ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid M
inst✝¹ : T2Space M
inst✝ : ContinuousAdd M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
A : Set α
hA : MeasurableSet A
⊢ (v.restrict i + v.restrict iᶜ) A = v A

Tactic:
_root_.add_apply,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid M
inst✝¹ : T2Space M
inst✝ : ContinuousAdd M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
A : Set α
hA : MeasurableSet A
⊢ (v.restrict i) A + (v.restrict iᶜ) A = v A
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_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 →
      μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
x : α
hx : ¬M ≤ ‖f x‖
⊢ f x = ({x | M ≤ ↑‖f x‖₊}.indicator f + {x | ‖f x‖ < M}.indicator f) x

Tactic:
rw [Pi.add_apply, Set.indicator_of_notMem, Set.indicator_of_mem, zero_add]

Goal state after:
case neg.h
α : 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 →
      μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
x : α
hx : ¬M ≤ ‖f x‖
⊢ x ∈ {x | ‖f x‖ < M}

case neg.h
α : 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 →
      μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ({x | ‖f x‖ < M}.indicator f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
x : α
hx : ¬M ≤ ‖f x‖
⊢ x ∉ {x | M ≤ ↑‖f x‖₊}
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
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
inst✝ : ContinuousAdd M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : w s = 0
⊢ (v₁ + v₂) s = 0

Tactic:
_root_.add_apply,

Goal state after:
α : 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
inst✝ : ContinuousAdd M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : w s = 0
⊢ v₁ s + v₂ s = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case refine_1
α : 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
x✝ : MeasurableSet t
⊢ (v₁ + v₂) t = 0

Tactic:
_root_.add_apply,

Goal state after:
case refine_1
α : 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
x✝ : MeasurableSet t
⊢ v₁ t + v₂ t = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : s.totalVariation u = 0
hu₂ : μ.ennrealToMeasure uᶜ = 0
t : Set α
htv : t ⊆ uᶜ
hmt : MeasurableSet t
⊢ μ t = 0

Tactic:
rw [← VectorMeasure.ennrealToMeasure_apply hmt]

Goal state after:
case mpr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : s.totalVariation u = 0
hu₂ : μ.ennrealToMeasure uᶜ = 0
t : Set α
htv : t ⊆ uᶜ
hmt : MeasurableSet t
⊢ μ.ennrealToMeasure t = 0
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, (f + g) x ∂μ = (μ.withDensityᵥ f + μ.withDensityᵥ g) i

Tactic:
_root_.add_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, (f + g) x ∂μ = (μ.withDensityᵥ f) i + (μ.withDensityᵥ g) i
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Integrable (s.rnDeriv μ) μ

Tactic:
refine Integrable.sub ?_ ?_

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Integrable (fun x ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ

case refine_2
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Integrable (fun x ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ (t + μ.withDensityᵥ f) i =
    t i + ((μ.withDensity fun x ↦ ENNReal.ofReal (f x)).real i - (μ.withDensity fun x ↦ ENNReal.ofReal (-f x)).real i)

Tactic:
_root_.add_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun x ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ t i + (μ.withDensityᵥ f) i =
    t i + ((μ.withDensity fun x ↦ ENNReal.ofReal (f x)).real i - (μ.withDensity fun x ↦ ENNReal.ofReal (-f x)).real i)
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
c : ℝ≥0
hc : c ≠ 0
hf : ¬AEStronglyMeasurable f μ
h : AEStronglyMeasurable f (c • μ)
⊢ AEStronglyMeasurable f μ

Tactic:
by
      simpa [hc] using h.smul_measure c⁻¹

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

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
c : E
hc : 0 ≤ c
hfc : ∀ᵐ (x : α) ∂μ, f x ≤ c
hm : ¬m ≤ m0
⊢ ∀ᵐ (x : α) ∂μ, μ[f | m] x ≤ c

pp: case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
c : E
hc : 0 ≤ c
hfc : ∀ᵐ (x : α) ∂μ, f x ≤ c
hm : m ≤ m0
⊢ ∀ᵐ (x : α) ∂μ, μ[f | m] x ≤ c

Tactic:
· filter_upwards with a using by simpa [condExp_of_not_le hm]

Goal state after:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
c : E
hc : 0 ≤ c
hfc : ∀ᵐ (x : α) ∂μ, f x ≤ c
hm : m ≤ m0
⊢ ∀ᵐ (x : α) ∂μ, μ[f | m] x ≤ c
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst✝³] F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ μ F = ∫⁻ (x : X), F.indicator (fun x ↦ 1) x ∂μ

Tactic:
rw [lintegral_indicator hF.measurableSet]

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst✝³] F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ μ F = ∫⁻ (a : X) in F, 1 ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : g =ᵐ[μ] 0
n : ι
x : α
hx : μ[g | ℱ n] x = μ[0 | ℱ n] x
⊢ {x | 0 ≤ ‖μ[g | ℱ n] x‖₊}.indicator μ[g | ℱ n] x = 0 x

Tactic:
simp [hx]

Goal state after: