mathlib-initiative/mathlib-tactics huggingface dataset:
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 α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun i ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun i ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun i ↦ ⋃ j, ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬μ W = 0
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (fun j ↦ μ (W ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : ℕ → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun j ↦ closedBall (w j) (M * r₁ (f j))
⊢ ∀ᶠ (j : ℕ) in atTop, μ (W ∩ closedBall (w j) (r₁ (f j))) / μ (closedBall (w j) (r₁ (f j))) ≤ ↑(1 - C⁻¹)

Tactic:
let B : ℕ → Set α := fun j => closedBall (w j) (r₁ (f j))

Goal state after:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun i ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun i ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun i ↦ ⋃ j, ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬μ W = 0
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (fun j ↦ μ (W ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : ℕ → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun j ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun j ↦ closedBall (w j) (r₁ (f j))
⊢ ∀ᶠ (j : ℕ) in atTop, μ (W ∩ closedBall (w j) (r₁ (f j))) / μ (closedBall (w j) (r₁ (f j))) ≤ ↑(1 - C⁻¹)
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, disjointed f i)))

Tactic:
m_iUnion _ (hC.disjointed_mem hf) (by rwa [iUnion_disjointed])
      (disjoint_disjointed f)

Goal state after:
α : 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 (𝓝 (∑' (i : ℕ), m (disjointed f i)))
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: 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✝)

Tactic:
simp only [Pi.zero_def, Function.apply_extend v, Function.comp_def, empty]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ (r • μ).real i = r • μ.real i

Tactic:
measureReal_nnreal_smul_apply

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ ↑r * μ.real i = r • μ.real i
Module: Mathlib.MeasureTheory.Measure.Complex

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
⊢ { re := s ∅, im := t ∅ } = 0

Tactic:
rw [s.empty, t.empty]; rfl

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

Goal state before:
pp: case e'_5
α : Type u_1
β : Type u_2
m mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
f : α → β
hf : Measurable f
g : ℕ → Set β
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
x✝ : ℕ
⊢ (if MeasurableSet (g x✝) then v (f ⁻¹' g x✝) else 0) = v (f ⁻¹' g x✝)

Tactic:
if_pos (hg₁ _)

Goal state after:
case e'_5
α : Type u_1
β : Type u_2
m mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
f : α → β
hf : Measurable f
g : ℕ → Set β
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
x✝ : ℕ
⊢ v (f ⁻¹' g x✝) = v (f ⁻¹' g x✝)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
f : α → β
hf : Measurable f
⊢ ∀ ⦃f_1 : ℕ → Set β⦄,
    (∀ (i : ℕ), MeasurableSet (f_1 i)) →
      Pairwise (Disjoint on f_1) →
        HasSum (fun i ↦ if MeasurableSet (f_1 i) then v (f ⁻¹' f_1 i) else 0)
          (if MeasurableSet (⋃ i, f_1 i) then v (f ⁻¹' ⋃ i, f_1 i) else 0)

Tactic:
intro g hg₁ hg₂
        convert! v.m_iUnion (fun i => hf (hg₁ i)) fun i j hij => (hg₂ hij).preimage _
        · rw [if_pos (hg₁ _)]
        · rw [Set.preimage_iUnion, if_pos (MeasurableSet.iUnion hg₁)]

Goal state after:
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
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
⊢ v.restrict t + v.restrict (s \ t) + v.restrict (s ∩ t) = v.restrict (s ∩ t) + v.restrict (s \ t) + v.restrict t

Tactic:
add_comm,

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
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
⊢ v.restrict (s ∩ t) + (v.restrict t + v.restrict (s \ t)) = v.restrict (s ∩ t) + v.restrict (s \ t) + v.restrict t
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ ↑r * j.posPart.real i - (r • j.negPart).real i = r • j.posPart.real i - r • j.negPart.real i

Tactic:
measureReal_nnreal_smul_apply

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ ↑r * j.posPart.real i - ↑r * j.negPart.real i = r • j.posPart.real i - r • j.negPart.real i
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : s (u ∆ v) = 0
⊢ s (w ∩ u) = s (w ∩ v)

Tactic:
have := of_inter_eq_of_symmDiff_eq_zero_positive hu hv hw hsu hsv

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : s (u ∆ v) = 0
this : (-s) (u ∆ v) = 0 → (-s) (w ∩ u) = (-s) (w ∩ v)
⊢ s (w ∩ u) = s (w ∩ v)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case negPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure

Tactic:
unfold toSignedMeasure at hj'

Goal state after:
case negPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.posPart.toSignedMeasure - j₁.negPart.toSignedMeasure = j₂.posPart.toSignedMeasure - j₂.negPart.toSignedMeasure
⊢ j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition

Tactic:
by_cases! hr : 0 ≤ r

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : 0 ≤ r
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition

case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ (lowerBounds s.measureOfNegatives).Nonempty

Tactic:
Set.Nonempty,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ ∃ x, x ∈ lowerBounds s.measureOfNegatives
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

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

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

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : ¬Integrable f μ
⊢ (if hf : Integrable (-f) μ then
      { measureOf' := fun s ↦ if MeasurableSet s then ∫ (x : α) in s, (-f) x ∂μ else 0, empty' := ⋯,
        not_measurable' := ⋯, m_iUnion' := ⋯ }
    else 0) =
    -0

Tactic:
dif_neg,

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : ¬Integrable f μ
⊢ 0 = -0

case neg.hnc
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : ¬Integrable f μ
⊢ ¬Integrable (-f) μ
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f μ
hr : ¬r = 0
⊢ (if hf : Integrable (r • f) μ then
      { measureOf' := fun s ↦ if MeasurableSet s then ∫ (x : α) in s, (r • f) x ∂μ else 0, empty' := ⋯,
        not_measurable' := ⋯, m_iUnion' := ⋯ }
    else 0) =
    r • 0

Tactic:
dif_neg,

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f μ
hr : ¬r = 0
⊢ 0 = r • 0

case neg.hnc
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f μ
hr : ¬r = 0
⊢ ¬Integrable (r • f) μ
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
hs : s ≤[univ] 0
⊢ (s.toMeasureOfLEZero univ ⋯ hs).toSignedMeasure = -s

Tactic:
by
  ext i hi
  simp [hi, toMeasureOfLEZero_apply _ _ _ hi, measureReal_def]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
⊢ 0 ≤[univ] μ.toSignedMeasure

Tactic:
refine restrict_le_restrict_of_subset_le _ _ fun j hj₁ _ => ?_

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
j : Set α
hj₁ : MeasurableSet j
x✝ : j ⊆ univ
⊢ 0 j ≤ μ.toSignedMeasure j
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case h₁
α : 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 n : ℕ
hN : ∀ x ∈ tᶜ, dist (g x) (f n x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
hn : n ≥ N
hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
hng : eLpNorm (t.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
this✝ : 0 ≤ ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
this :
  eLpNorm (tᶜ.indicator (f n - g)) p μ ≤
    ENNReal.ofReal (ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))) * μ tᶜ ^ (1 / p.toReal)
⊢ μ tᶜ ≤ ↑(measureUnivNNReal μ)

Tactic:
coe_measureUnivNNReal

Goal state after:
case h₁
α : 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 n : ℕ
hN : ∀ x ∈ tᶜ, dist (g x) (f n x) < ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
hn : n ≥ N
hnf : eLpNorm (t.indicator (f n)) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
hng : eLpNorm (t.indicator g) p μ ≤ ENNReal.ofReal (ε.toReal / 3)
this✝ : 0 ≤ ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))
this :
  eLpNorm (tᶜ.indicator (f n - g)) p μ ≤
    ENNReal.ofReal (ε.toReal / (3 * ↑(measureUnivNNReal μ) ^ (1 / p.toReal))) * μ tᶜ ^ (1 / p.toReal)
⊢ μ tᶜ ≤ μ univ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
r : ℝ
⊢ (r • s).HaveLebesgueDecomposition μ

Tactic:
by_cases! hr : 0 ≤ r

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
r : ℝ
hr : 0 ≤ r
⊢ (r • s).HaveLebesgueDecomposition μ

case neg
α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
r : ℝ
hr : r < 0
⊢ (r • s).HaveLebesgueDecomposition μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i = s i

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

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    s.toJordanDecomposition.toSignedMeasure 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 : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : Tendsto (fun n ↦ eLpNorm (f n) p μ) atTop (𝓝 0)
ε : ℝ
hε : 0 < ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ℕ) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε

Tactic:
rw [ENNReal.tendsto_atTop_zero] at hf_tendsto

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ℕ → α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), MemLp (f n) p μ
hf_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n) p μ ≤ ε
ε : ℝ
hε : 0 < ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ℕ) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
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 (f i)) p μ ≤
    eLpNorm ((s ∩ {x | C ≤ ‖f i x‖₊}).indicator (f i)) p μ + eLpNorm ((s ∩ {x | ‖f i x‖₊ < C}).indicator (f i)) p μ

Tactic:
refine le_trans (Eq.le ?_) (eLpNorm_add_le
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator (hs.inter (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm))))
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator (hs.inter ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const))))
        hp)
      congr
      change _ = fun x => (s ∩ { x : α | C ≤ ‖f i x‖₊ }).indicator (f i) x +
        (s ∩ { x : α | ‖f i x‖₊ < C }).indicator (f i) x
      rw [← Set.indicator_union_of_disjoint]
      · rw [← Set.inter_union_distrib_left, (by ext; simp [le_or_gt] :
            { x : α | C ≤ ‖f i x‖₊ } ∪ { x : α | ‖f i x‖₊ < C } = Set.univ),
          Set.inter_univ]
      · refine (Disjoint.inf_right' _ ?_).inf_left' _
        rw [disjoint_iff_inf_le]
        rintro x ⟨hx₁, hx₂⟩
        rw [Set.mem_ofPred_eq] at hx₁ hx₂
        exact False.elim (hx₂.ne (eq_of_le_of_not_lt hx₁ (not_lt.2 hx₂.le)).symm)

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

Goal state before:
pp: Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : Measure Ω
⊢ μ ∈ {μ | IsFiniteMeasure μ} ↔ μ ∈ (fun μ ↦ μ univ) ⁻¹' Ico 0 ∞

Tactic:
simp only [mem_ofPred_eq, mem_preimage, mem_Ico, zero_le, true_and]

Goal state after:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : Measure Ω
⊢ IsFiniteMeasure μ ↔ μ univ < ∞
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: case left
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key : μ.testAgainstNN f₂ ≤ μ.testAgainstNN f₁ + μ.mass * nndist f₂ f₁
⊢ -(↑μ.mass * dist f₁ f₂) ≤ ↑(μ.testAgainstNN f₁) - ↑(μ.testAgainstNN f₂)

Tactic:
suffices ↑(μ.testAgainstNN f₂) ≤ ↑(μ.testAgainstNN f₁) + ↑μ.mass * dist f₁ f₂ by linarith

Goal state after:
case left
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key : μ.testAgainstNN f₂ ≤ μ.testAgainstNN f₁ + μ.mass * nndist f₂ f₁
⊢ ↑(μ.testAgainstNN f₂) ≤ ↑(μ.testAgainstNN f₁) + ↑μ.mass * dist f₁ f₂
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : μ E ≤ liminf (fun i ↦ (μs i) E) L
⊢ limsup (fun i ↦ (μs i) Eᶜ) L ≤ μ Eᶜ

Tactic:
rcases L.eq_or_neBot with rfl | hne
  · simp only [limsup_bot, bot_le]
  have meas_Ec : μ Eᶜ = 1 - μ E := by
    simpa only [measure_univ] using measure_compl E_mble (measure_lt_top μ E).ne
  have meas_i_Ec : ∀ i, μs i Eᶜ = 1 - μs i E := by
    intro i
    simpa only [measure_univ] using measure_compl E_mble (measure_lt_top (μs i) E).ne
  simp_rw [meas_Ec, meas_i_Ec]
  rw [show (L.limsup fun i : ι ↦ 1 - μs i E) = L.limsup ((fun x ↦ 1 - x) ∘ fun i : ι ↦ μs i E)
      from rfl]
  have key := antitone_const_tsub.map_liminf_of_continuousAt (F := L)
    (fun i ↦ μs i E) (ENNReal.continuous_sub_left ENNReal.one_ne_top).continuousAt
  simpa [← key] using antitone_const_tsub h

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
c : ℝ≥0
ν : FiniteMeasure Ω
s : Set Ω'
a✝ : MeasurableSet s
⊢ ↑((c • ν).map f) s = ↑(c • ν.map f) s

Tactic:
simp [toMeasure_smul]

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
s : ι → Set Ω
inst✝ : Fintype ι
h : iIndepSets π κ μ
hs : ∀ (i : ι), s i ∈ π i
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i, s i) = ∏ i, (κ a) (s i)

Tactic:
filter_upwards [h.meas_biInter Finset.univ (fun _i _ ↦ hs _)] with a ha using by simp [← ha]

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
inst✝ : Fintype ι
h : iIndep m κ μ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i, s i) = ∏ i, (κ a) (s i)

Tactic:
by
  filter_upwards [h.meas_biInter (fun i (_ : i ∈ Finset.univ) ↦ hs _)] with a ha
  simp [← ha]

Goal state after: