mathlib-initiative/mathlib-tactics huggingface dataset:
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
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → (↑S).PairwiseDisjoint s → m (⋃ i ∈ S, s i) = ∑ i ∈ S, m (s i)
hs : ∀ n ∈ insert i S, s n ∈ C
hS : (↑(insert i S)).PairwiseDisjoint s
⊢ m (⋃ i_1 ∈ insert i S, s i_1) = ∑ i ∈ insert i S, m (s i)

Tactic:
| insert i S hiS h =>

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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝² : AddCommMonoid G
m : AddContent G C
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ m s + m (t \ s) ≤ m s + m t

pp: α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝² : AddCommMonoid G
m : AddContent G C
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ Disjoint s (t \ s)

Tactic:
· exact add_le_add_right (addContent_mono hC.isSetSemiring (hC.sdiff_mem ht hs) ht sdiff_subset) _

Goal state after:
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝² : AddCommMonoid G
m : AddContent G C
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ Disjoint s (t \ s)
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:
| insert i S hiS h =>

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
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
ι : Type u_3
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hs : ∀ n ∈ S, s n ∈ C
⊢ m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i)

Tactic:
induction S using Finset.induction with
  | empty => simp
  | insert i S hiS h =>
    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.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
n✝ : ℕ
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
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
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn_pos : n > 0
he' : auxTransvection hf * e ∉ transvections K V ^ n * dilatransvections K V
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
g : Dual K V
hg0 : g ≠ 0
hg2 : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v ≤ ker g
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
⊢ finrank K (V ⧸ (↑(auxTransvection hg * e)).fixedSubmodule) = n + 1

Tactic:
auxTransvection_mul_fixed hfgv,

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
n✝ : ℕ
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    (∀ (a : K), ∃ x, ¬e.fixedReduce x = a • x) →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1 → e ∈ transvections K V ^ n * dilatransvections K V
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 2
f : Dual K V
v : V
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
hv_notMem : v ∉ (↑e).fixedSubmodule
hrank : finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
hn_pos : n > 0
he' : auxTransvection hf * e ∉ transvections K V ^ n * dilatransvections K V
hne_top : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤
g : Dual K V
hg0 : g ≠ 0
hg2 : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v ≤ ker g
hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker (f + g)
hfgv : (f + g) v = 1
⊢ finrank K (V ⧸ (↑e).fixedSubmodule ⊔ K ∙ v) = n + 1
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M ↦ {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
hbound : HasFiniteIntegral (fun x ↦ ‖f x‖) μ
n : ℕ
x : α
hx : ↑n ≤ ‖f x‖
⊢ x ∈ {x | (fun a ↦ ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a‖ ≤ ‖f a‖) x}

Tactic:
dsimp

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M ↦ {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
hbound : HasFiniteIntegral (fun x ↦ ‖f x‖) μ
n : ℕ
x : α
hx : ↑n ≤ ‖f x‖
⊢ ‖{x | ↑n ≤ ‖f x‖₊}.indicator f x‖ ≤ ‖f x‖
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M ↦ {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
hbound : HasFiniteIntegral (fun x ↦ ‖f x‖) μ
n : ℕ
x : α
hx : ¬↑n ≤ ‖f x‖
⊢ x ∈ {x | (fun a ↦ ‖{x | ↑n ≤ ‖f x‖₊}.indicator f a‖ ≤ ‖f a‖) x}

Tactic:
dsimp

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas✝ : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
htendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun M ↦ {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) atTop (𝓝 0)
hmeas : ∀ (M : ℕ), AEStronglyMeasurable ({x | ↑M ≤ ↑‖f x‖₊}.indicator f) μ
hbound : HasFiniteIntegral (fun x ↦ ‖f x‖) μ
n : ℕ
x : α
hx : ¬↑n ≤ ‖f x‖
⊢ ‖{x | ↑n ≤ ‖f x‖₊}.indicator f x‖ ≤ ‖f x‖
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case hB
α : 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
⊢ MeasurableSet (A ∩ B)

Tactic:
· exact hA.inter hB

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

Goal state before:
pp: case hA
α : 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
⊢ MeasurableSet (A ∩ B)

pp: case hB
α : 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
⊢ MeasurableSet (B \ A)

Tactic:
· exact hA.inter hB

Goal state after:
case hB
α : 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
⊢ MeasurableSet (B \ A)
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)
this : HasSum (fun n ↦ v (t n)) (v (⋃ n, s n))
n : ℕ
⊢ v (s n) = ((fun n ↦ ∑ i ∈ Finset.range n, v (t i)) ∘ fun a ↦ a + 1) n

Tactic:
dsimp

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)
this : HasSum (fun n ↦ v (t n)) (v (⋃ n, s n))
n : ℕ
⊢ v (s n) = ∑ i ∈ Finset.range (n + 1), v (t i)
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
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)
x : α
⊢ M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ ‖f x‖ ^ p.toReal

Tactic:
← Real.rpow_le_rpow_iff hM' (by positivity)
        (one_div_pos.2 <| ENNReal.toReal_pos hp_ne_zero hp_ne_top),

Goal state after:
α : 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)
x : α
⊢ M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ^ (1 / p.toReal) ≤ (‖f x‖ ^ p.toReal) ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ HasSum (fun i ↦ if MeasurableSet (f i) then μ.real (f i) else 0)
    (if MeasurableSet (⋃ i, f i) then μ.real (⋃ i, f i) else 0)

Tactic:
by
    simp only [*, MeasurableSet.iUnion hf₁, if_true, measure_iUnion hf₂ hf₁, measureReal_def]
    rw [ENNReal.tsum_toReal_eq]
    exacts [(summable_measure_toReal hf₁ hf₂).hasSum, fun _ ↦ measure_ne_top _ _]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
R : Type u_2
inst✝³ : Semiring R
inst✝² : Module R ℝ
inst✝¹ : ContinuousConstSMul R ℝ
inst✝ : ContinuousConstSMul R ℂ
r : R
c : ComplexMeasure α
⊢ equivSignedMeasure.toFun (r • c) = (RingHom.id R) r • equivSignedMeasure.toFun c

Tactic:
dsimp

Goal state after:
α : Type u_1
m : MeasurableSpace α
R : Type u_2
inst✝³ : Semiring R
inst✝² : Module R ℝ
inst✝¹ : ContinuousConstSMul R ℝ
inst✝ : ContinuousConstSMul R ℂ
r : R
c : ComplexMeasure α
⊢ equivSignedMeasure (r • c) = r • equivSignedMeasure c
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
i : Set α
hi : MeasurableSet i
⊢ v (i ∩ ∅) = 0 i

Tactic:
Set.inter_empty,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ v ∅ = 0 i
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : 0 ≤ r
⊢ (r • j).negPart = r.toNNReal • j.negPart

Tactic:
by
  rw [real_smul_def, ← smul_negPart, if_pos hr]

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

Goal state before:
pp: case neg
α : 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 ε
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hi : n ≤ ↑(Fin.last n)
⊢ eLpNorm (s.indicator (f (Fin.last n))) p μ ≤ ENNReal.ofReal ε

Tactic:
exact hδ₂ _ hs (le_trans hμs <| ENNReal.ofReal_le_ofReal <| min_le_right _ _)

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

Goal state before:
pp: case refine_2.a
α : 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
⊢ uᶜ ∩ t ⊆ uᶜ

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
⊢ Disjoint (uᶜ ∩ t) (vᶜ \ uᶜ ∩ t)

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:
· exact Set.inter_subset_left

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
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.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
        negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
        mutuallySingular := ⋯ }.toSignedMeasure

Tactic:
JordanDecomposition.toSignedMeasure

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
            negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
            mutuallySingular := ⋯ }.posPart.toSignedMeasure -
      { posPart := s.toJordanDecomposition.posPart.singularPart μ,
            negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
            mutuallySingular := ⋯ }.negPart.toSignedMeasure
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
| s.toJordanDecomposition.toSignedMeasure

Tactic:
JordanDecomposition.toSignedMeasure

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
| s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: case pos
α : 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 μ
⊢ (c ^ p.toReal⁻¹ • eLpNorm f p μ).toReal = c ^ p.toReal⁻¹ • (eLpNorm f p μ).toReal

Tactic:
simp [ENNReal.smul_def, NNReal.smul_def]

Goal state after:
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.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ t.toJordanDecomposition.toSignedMeasure =
    (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
JordanDecomposition.toSignedMeasure

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ t.toJordanDecomposition.posPart.toSignedMeasure - t.toJordanDecomposition.negPart.toSignedMeasure =
    (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ∞
f : α → E
c : ℝ≥0
hf : AEStronglyMeasurable f μ
⊢ (c ^ p.toReal⁻¹ • eLpNorm f p μ).toReal = c ^ p.toReal⁻¹ • (eLpNorm f p μ).toReal

Tactic:
simp [ENNReal.smul_def, NNReal.smul_def]

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)
key :
  Tendsto (fun n ↦ ⇑(thickenedIndicator ⋯ F)) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F).indicator fun x ↦ 1))
⊢ Tendsto (fun n ω ↦ (thickenedIndicator ⋯ F) ω) atTop (𝓝 (F.indicator fun x ↦ 1))

Tactic:
F_closed.closure_eq

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)
key : Tendsto (fun n ↦ ⇑(thickenedIndicator ⋯ F)) atTop (𝓝 (F.indicator fun x ↦ 1))
⊢ Tendsto (fun n ω ↦ (thickenedIndicator ⋯ F) ω) atTop (𝓝 (F.indicator fun x ↦ 1))
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
f' : α → ℝ := AEStronglyMeasurable.mk f ⋯
hadd' : s = t + μ.withDensityᵥ f'
this : s.HaveLebesgueDecomposition μ
⊢ t + μ.withDensityᵥ (s.rnDeriv μ) = t + μ.withDensityᵥ f

Tactic:
← hadd,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
f' : α → ℝ := AEStronglyMeasurable.mk f ⋯
hadd' : s = t + μ.withDensityᵥ f'
this : s.HaveLebesgueDecomposition μ
⊢ t + μ.withDensityᵥ (s.rnDeriv μ) = s
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ RCLike.re ((c.singularPart μ) i) + RCLike.re (∫ (x : α) in i, c.rnDeriv μ x ∂μ) =
    RCLike.re { re := (re c) i, im := (im c) i }

Tactic:
← integral_re (c.integrable_rnDeriv μ).integrableOn,

Goal state after:
case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ RCLike.re ((c.singularPart μ) i) + ∫ (x : α) in i, RCLike.re (c.rnDeriv μ x) ∂μ =
    RCLike.re { re := (re c) i, im := (im c) i }
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)
fs : ℕ → Ω → ℝ := fun n ω ↦ ↑((thickenedIndicator ⋯ F) ω)
h_eq : ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ = ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
h : Tendsto (fun n ↦ ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)) atTop (𝓝 (μ F))
h_eq' : (fun n ↦ ∫ (ω : Ω), fs n ω ∂μ) = fun n ↦ (ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)).toReal
⊢ Tendsto (fun n ↦ ∫ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ) atTop (𝓝 (μ F).toReal)

Tactic:
rwa [h_eq', ENNReal.tendsto_toReal_iff (by simp) (by finiteness)]

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

Goal state before:

Tactic:
_ ≤ ∫ x, μ[|f| | m] x ∂μ :=
    integral_mono_ae integrable_condExp.abs integrable_condExp (abs_condExp_ae_le_condExp_abs f)
  _ = _ := integral_condExp hm

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

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hf : 0 ≤ᵐ[μ.restrict s] f
hm : m ≤ m0
hfint : Integrable f μ
hsig : ¬SigmaFinite (μ.trim hm)
⊢ ∫ (x : α) in s, μ[f | m] x ∂μ ≤ ∫ (x : α) in s, f x ∂μ

pp: case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hf : 0 ≤ᵐ[μ.restrict s] f
hm : m ≤ m0
hfint : Integrable f μ
hsig : SigmaFinite (μ.trim hm)
⊢ ∫ (x : α) in s, μ[f | m] x ∂μ ≤ ∫ (x : α) in s, f x ∂μ

Tactic:
· simpa [condExp_of_not_sigmaFinite hm hsig] using setIntegral_nonneg_of_ae_restrict hf

Goal state after:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hf : 0 ≤ᵐ[μ.restrict s] f
hm : m ≤ m0
hfint : Integrable f μ
hsig : SigmaFinite (μ.trim hm)
⊢ ∫ (x : α) in s, μ[f | m] x ∂μ ≤ ∫ (x : α) in s, f x ∂μ