mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case refine_3
α : 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) p (μ.restrict s) + eLpNorm ({x | ‖f x‖ < M}.indicator f) p (μ.restrict s) ≤
    2 * ENNReal.ofReal ε

Tactic:
two_mul

Goal state after:
case refine_3
α : 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) p (μ.restrict s) + eLpNorm ({x | ‖f x‖ < M}.indicator f) p (μ.restrict s) ≤
    ENNReal.ofReal ε + ENNReal.ofReal ε
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
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
a : Ω
ha : f a = AEStronglyMeasurable.mk f hf a
⊢ (B (f a)) (g a) = (B (AEStronglyMeasurable.mk f hf a)) (g a)

Tactic:
rw [ha]

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
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hfg : Integrable (fun ω ↦ (B (f ω)) (g ω)) μ
hg : Integrable g μ
a : Ω
ha : f a = AEStronglyMeasurable.mk f hf a
⊢ (B (AEStronglyMeasurable.mk f hf a)) (μ[g | m] a) = (B (f a)) (μ[g | m] a)

Tactic:
rw [ha]

Goal state after:
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
v w : VectorMeasure α M
⊢ v ≤[∅] w

Tactic:
by
  simp

Goal state after:
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
v w : VectorMeasure α M
⊢ v ≤[univ] w ↔ v ≤ w

Tactic:
by
  simp

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

Goal state before:
pp: case refine_2
α : 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
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
ha₃ : ⋃ n, a ∩ disjointed f n = a
ha₄ : Pairwise (Disjoint on fun n ↦ a ∩ disjointed f n)
n : ℕ
⊢ a ∩ disjointed f n ⊆ f n

Tactic:
exact Set.Subset.trans Set.inter_subset_right (disjointed_subset _ _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
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
inst✝ : Countable β
f : β → Set α
hf₁ : ∀ (b : β), MeasurableSet (f b)
hf₂ : ∀ (b : β), v ≤[f b] w
⊢ v ≤[⋃ b, f b] w

Tactic:
cases nonempty_encodable β
  rw [← Encodable.iUnion_decode₂]
  refine restrict_le_restrict_iUnion v w ?_ ?_
  · intro n
    measurability
  · intro n
    rcases Encodable.decode₂ β n with - | b
    · simp
    · simp [hf₂ b]

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 < ε
δ : ℝ
hδpos : 0 < δ
hδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal (ε / 2)
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal δ
⊢ 2 * ENNReal.ofReal (ε / 2) ≤ ENNReal.ofReal ε

Tactic:
rw [ENNReal.ofReal_div_of_pos zero_lt_two, (by simp : ENNReal.ofReal 2 = 2),
      ENNReal.mul_div_cancel] <;>
    norm_num

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

Goal state before:
pp: case mp
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : ∀ ⦃s_1 : Set α⦄, μ.ennrealToMeasure s_1 = 0 → s s_1 = 0
S : Set α
hS₁ : MeasurableSet S
hS₂ : μ.ennrealToMeasure S = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ ↑(NNReal.mk (s (i ∩ S)) ⋯) + ↑(NNReal.mk (-s (iᶜ ∩ S)) ⋯) = 0

Tactic:
simp [h (measure_mono_null (i.inter_subset_right) hS₂),
      h (measure_mono_null (iᶜ.inter_subset_right) hS₂)]

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∞
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
hε' : 0 < ε.toReal / 3
hdivp : 0 ≤ 1 / p.toReal
hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)
δ₁ : ℝ
hδ₁ : 0 < δ₁
heLpNorm₁ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
δ₂ : ℝ
hδ₂ : 0 < δ₂
heLpNorm₂ :
  ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
t : Set α
htm : MeasurableSet t
ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
n : ℕ
hn : n ≥ N
⊢ eLpNorm (t.indicator (f n - g) + tᶜ.indicator (f n - g)) p μ ≤ ε

Tactic:
grw [eLpNorm_add_le (((hf n).sub hg).indicator htm).aestronglyMeasurable
    (((hf n).sub hg).indicator htm.compl).aestronglyMeasurable hp, sub_eq_add_neg,
    Set.indicator_add' t, Set.indicator_neg', eLpNorm_add_le
    ((hf n).indicator htm).aestronglyMeasurable (hg.indicator htm).neg.aestronglyMeasurable hp]

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
hε' : 0 < ε.toReal / 3
hdivp : 0 ≤ 1 / p.toReal
hpow : 0 < measureUnivNNReal μ ^ (1 / p.toReal)
δ₁ : ℝ
hδ₁ : 0 < δ₁
heLpNorm₁ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
δ₂ : ℝ
hδ₂ : 0 < δ₂
heLpNorm₂ :
  ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
t : Set α
htm : MeasurableSet t
ht₁ : μ t ≤ ENNReal.ofReal (min δ₁ δ₂)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ x ∈ tᶜ, dist (g x) (f b x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
n : ℕ
hn : n ≥ N
⊢ eLpNorm (t.indicator (f n)) p μ + eLpNorm (-t.indicator g) p μ + eLpNorm (tᶜ.indicator (f n + -g)) p μ ≤ ε
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 μ
⊢ μ.withDensityᵥ f + μ.withDensityᵥ (-g) = μ.withDensityᵥ f + -μ.withDensityᵥ g

Tactic:
withDensityᵥ_neg

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 μ
⊢ μ.withDensityᵥ f + -μ.withDensityᵥ g = μ.withDensityᵥ f + -μ.withDensityᵥ g
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure

Tactic:
refine VectorMeasure.AbsolutelyContinuous.mk fun i hi₁ hi₂ => ?_
    rw [toENNRealVectorMeasure_apply_measurable hi₁] at hi₂
    rw [withDensityᵥ_apply hf hi₁, Measure.restrict_zero_set hi₂, integral_zero_measure]

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

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
h : f =ᵐ[μ] g
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, f x ∂μ = ∫ (x : α) in i, g x ∂μ

Tactic:
exact integral_congr_ae (ae_restrict_of_ae h)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (fun x ↦ (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, (f x).toReal ∂μ = (∫⁻ (a : α) in i, f a ∂μ).toReal

Tactic:
integral_toReal hfm.restrict

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (fun x ↦ (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ (∫⁻ (a : α) in i, f a ∂μ).toReal = (∫⁻ (a : α) in i, f a ∂μ).toReal

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfi : Integrable (fun x ↦ (f x).toReal) μ
this : IsFiniteMeasure (μ.withDensity f)
i : Set α
hi : MeasurableSet i
⊢ ∀ᵐ (x : α) ∂μ.restrict i, f x < ∞
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
hp₀ : p ≠ 0
hp : p ≠ ∞
hf : AEStronglyMeasurable f μ
⊢ (eLpNorm f p μ).toReal = (∫ (x : α), ‖f x‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹

Tactic:
eLpNorm_eq_lintegral_rpow_enorm_toReal hp₀ hp,

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hp₀ : p ≠ 0
hp : p ≠ ∞
hf : AEStronglyMeasurable f μ
⊢ ((∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)).toReal = (∫ (x : α), ‖f x‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

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

Tactic:
by
  have : ∀ n, eLpNorm (f n - g) p μ = eLpNorm ((hf n).mk (f n) - hg.1.mk g) p μ :=
    fun n => eLpNorm_congr_ae ((hf n).ae_eq_mk.sub hg.1.ae_eq_mk)
  simp_rw [this]
  refine tendsto_Lp_finite_of_tendsto_ae_of_meas hp hp' (fun n => (hf n).stronglyMeasurable_mk)
    hg.1.stronglyMeasurable_mk (hg.ae_eq hg.1.ae_eq_mk) (hui.ae_eq fun n => (hf n).ae_eq_mk) ?_
  have h_ae_forall_eq : ∀ᵐ x ∂μ, ∀ n, f n x = (hf n).mk (f n) x := by
    rw [ae_all_iff]
    exact fun n => (hf n).ae_eq_mk
  filter_upwards [hfg, h_ae_forall_eq, hg.1.ae_eq_mk] with x hx_tendsto hxf_eq hxg_eq
  rw [← hxg_eq]
  convert! hx_tendsto using 1
  ext1 n
  exact (hxf_eq n).symm

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : TopologicalSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n) ω ≤ c
fs_lim : Tendsto (fun n ω ↦ (fs n) ω) atTop (𝓝 (E.indicator fun x ↦ 1))
⊢ Tendsto (fun n ↦ ∫⁻ (ω : Ω), ↑((fs n) ω) ∂μ) atTop (𝓝 (μ E))

Tactic:
by
  have fs_lim' :
    ∀ ω, Tendsto (fun n : ℕ ↦ (fs n ω : ℝ≥0)) atTop (𝓝 (indicator E (fun _ ↦ (1 : ℝ≥0)) ω)) := by
    rw [tendsto_pi_nhds] at fs_lim
    exact fun ω ↦ fs_lim ω
  apply measure_of_cont_bdd_of_tendsto_filter_indicator μ E_mble fs
    (Eventually.of_forall fun n ↦ Eventually.of_forall (fs_bdd n)) (Eventually.of_forall fs_lim')

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ (c.singularPart μ) i + (μ.withDensityᵥ (c.rnDeriv μ)) i = { re := (re c) i, im := (im c) i }

Tactic:
apply Complex.ext

Goal state after:
case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ ((c.singularPart μ) i + (μ.withDensityᵥ (c.rnDeriv μ)) i).re = { re := (re c) i, im := (im c) i }.re

case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ComplexMeasure α
inst✝ : c.HaveLebesgueDecomposition μ
i : Set α
hi : MeasurableSet i
⊢ ((c.singularPart μ) i + (μ.withDensityᵥ (c.rnDeriv μ)) i).im = { re := (re c) i, im := (im c) i }.im
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.im ((c.singularPart μ) i) + ∫ (x : α) in i, RCLike.im (c.rnDeriv μ x) ∂μ =
    RCLike.im { re := (re c) i, im := (im c) i }

Tactic:
RCLike.im_eq_complex_im,

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
⊢ ((↑ν).real s).toNNReal = ν s

Tactic:
by
  simp

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
ι : Type u_2
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
μ : FiniteMeasure Ω
f : ι → Set Ω
⊢ Tendsto (fun i ↦ μ (accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))

Tactic:
by
  simpa [← ennreal_coeFn_eq_coeFn_toMeasure]
    using tendsto_measure_iUnion_accumulate (μ := μ.toMeasure) (ι := ι)

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set (α × β)
u : Set α
Hu : MeasurableSet u
v : Set β
Hv : MeasurableSet v
Heq : u ×ˢ v = s✝
⊢ Measurable fun a ↦ ((↑a.1).prod ↑a.2) s✝

Tactic:
simp_rw [← Heq, Measure.prod_prod]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set (α × β)
u : Set α
Hu : MeasurableSet u
v : Set β
Hv : MeasurableSet v
Heq : u ×ˢ v = s✝
⊢ Measurable fun a ↦ ↑a.1 u * ↑a.2 v
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
A : Set Ω
⊢ μ.restrict A ≠ 0 ↔ μ A ≠ 0

Tactic:
by
  simp

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ LipschitzWith μ.mass fun f ↦ μ.testAgainstNN f

Tactic:
lipschitzWith_iff_dist_le_mul

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ ∀ (x y : Ω →ᵇ ℝ≥0), dist (μ.testAgainstNN x) (μ.testAgainstNN y) ≤ ↑μ.mass * dist x y
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: case mp
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ Tendsto (fun i ↦ (μs i).normalize) F (𝓝 μ.normalize) ∧ Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass) → Tendsto μs F (𝓝 μ)

Tactic:
rintro ⟨normalized_lim, mass_lim⟩

Goal state after:
case mp
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
normalized_lim : Tendsto (fun i ↦ (μs i).normalize) F (𝓝 μ.normalize)
mass_lim : Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass)
⊢ Tendsto μs F (𝓝 μ)
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
f : α → E
p : ℝ≥0∞
hp : 1 ≤ p
hf : AEStronglyMeasurable f μ → eLpNorm f p μ = ∞
ha : AEStronglyMeasurable f μ
⊢ eLpNorm μ[f | m] p μ ≤ eLpNorm f p μ

Tactic:
simp [hf ha]

Goal state after:
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 : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
n : ι
this : μ {x | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ eLpNorm μ[g | ℱ n] 1 μ ^ 1 / ↑C
⊢ eLpNorm μ[g | ℱ n] 1 μ ^ 1 ≤ ENNReal.ofReal δ * ↑((NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal)

Tactic:
NNReal.inv_mk,

Goal state after:
α : 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 : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hCpos : 0 < C
n : ι
this : μ {x | C ≤ ‖μ[g | ℱ n] x‖₊} ≤ eLpNorm μ[g | ℱ n] 1 μ ^ 1 / ↑C
⊢ eLpNorm μ[g | ℱ n] 1 μ ^ 1 ≤ ENNReal.ofReal δ * ↑(NNReal.mk δ⁻¹ ⋯ * (eLpNorm g 1 μ).toNNReal)
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∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
set g : ι → α → β := fun i => (hfu.1 i).choose
  have hgmeas : ∀ i, StronglyMeasurable (g i) := fun i => (Exists.choose_spec <| hfu.1 i).1
  have hgunif : UniformIntegrable g p μ := hfu.ae_eq fun i => (Exists.choose_spec <| hfu.1 i).2
  obtain ⟨C, hC⟩ := hgunif.spec' hp hp' hgmeas hε
  refine ⟨C, fun i => le_trans (le_of_eq <| eLpNorm_congr_ae ?_) (hC i)⟩
  filter_upwards [(Exists.choose_spec <| hfu.1 i).2] with x hx
  by_cases hfx : x ∈ { x | C ≤ ‖f i x‖₊ }
  · rw [Set.indicator_of_mem hfx, Set.indicator_of_mem, hx]
    rwa [Set.mem_ofPred, hx] at hfx
  · rw [Set.indicator_of_notMem hfx, Set.indicator_of_notMem]
    rwa [Set.mem_ofPred, hx] at hfx

Goal state after:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr.iUnion
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
f : ℕ → Set Ω
hfd : Pairwise (Function.onFun Disjoint f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ ⋃ i, f i) = (κ a) t1 * (κ a) (⋃ i, f i)

Tactic:
← ae_all_iff

Goal state after:
case inr.iUnion
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
f : ℕ → Set Ω
hfd : Pairwise (Function.onFun Disjoint f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ ⋃ i, f i) = (κ a) t1 * (κ a) (⋃ i, f i)
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr.iUnion
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h✝ : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
h : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
⊢ ∀ᵐ (a : α) ∂μ, (κ a) ((⋃ i, f i) ∩ t2) = (κ a) (⋃ i, f i) * (κ a) t2

Tactic:
← ae_all_iff

Goal state after:
case inr.iUnion
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h✝ : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
h : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
⊢ ∀ᵐ (a : α) ∂μ, (κ a) ((⋃ i, f i) ∩ t2) = (κ a) (⋃ i, f i) * (κ a) t2