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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ
hε : 0 < ε
hε2 : 0 < ε / 2
δ₁ : ℝ
hδ₁_pos : 0 < δ₁
hfδ₁ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
δ₂ : ℝ
hδ₂_pos : 0 < δ₂
hgδ₂ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hε_halves : ENNReal.ofReal ε = ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2)
⊢ eLpNorm (s.indicator (f i)) p μ + eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε

Tactic:
hε_halves

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ
hε : 0 < ε
hε2 : 0 < ε / 2
δ₁ : ℝ
hδ₁_pos : 0 < δ₁
hfδ₁ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
δ₂ : ℝ
hδ₂_pos : 0 < δ₂
hgδ₂ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → μ s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal (min δ₁ δ₂)
hε_halves : ENNReal.ofReal ε = ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2)
⊢ eLpNorm (s.indicator (f i)) p μ + eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2)
Module: Mathlib.MeasureTheory.Covering.LiminfLimsup

Goal state before:
pp: case inr
α : 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' : M < 1
⊢ 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:
simp only [← @cthickening_closure _ _ _ (s _)]

Goal state after:
case inr
α : 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' : M < 1
⊢ blimsup (fun i ↦ cthickening (max 0 (r₁ i)) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i)))
      atTop p ≤ᵐ[μ]
    blimsup (fun i ↦ cthickening (max 0 (r₂ i)) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i)))
      atTop p
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case hm
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
ι : Type u_4
s : Set ι
f : ι → Set α
hs : s.Countable
hd : s.Pairwise (Disjoint on f)
h : ∀ b ∈ s, MeasurableSet (f b)
this : Encodable ↑s
⊢ ∀ (i : ↑s), MeasurableSet (f ↑i)

pp: case hd
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
ι : Type u_4
s : Set ι
f : ι → Set α
hs : s.Countable
hd : s.Pairwise (Disjoint on f)
h : ∀ b ∈ s, MeasurableSet (f b)
this : Encodable ↑s
⊢ Pairwise (Disjoint on fun i ↦ f ↑i)

Tactic:
· exact fun x ↦ h x x.2

Goal state after:
case hd
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
v : VectorMeasure α M
inst✝ : T2Space M
ι : Type u_4
s : Set ι
f : ι → Set α
hs : s.Countable
hd : s.Pairwise (Disjoint on f)
h : ∀ b ∈ s, MeasurableSet (f b)
this : Encodable ↑s
⊢ Pairwise (Disjoint on fun i ↦ f ↑i)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : MeasurableSpace β
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousAdd M
v w : VectorMeasure α M
f : α → β
⊢ (v + w).map f = v.map f + w.map f

Tactic:
by_cases hf : Measurable f
  · ext i hi
    simp [map_apply _ hf hi]
  · simp [map, dif_neg hf]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
⊢ (c • v).map f = c • v.map f

Tactic:
simp only [map, dif_neg hf]

Goal state after:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
R : Type u_4
inst✝² : Semiring R
inst✝¹ : DistribMulAction R M
inst✝ : ContinuousConstSMul R M
v : VectorMeasure α M
f : α → β
c : R
hf : ¬Measurable f
⊢ 0 = c • 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

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

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

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

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
hj₁ : MeasurableSet j
⊢ v j ≤ w j

pp: case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
hj₁ : ¬MeasurableSet j
⊢ v j ≤ w j

Tactic:
· exact (restrict_le_restrict_iff _ _ hi).1 hi₂ hj₁ hj

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
hj₁ : ¬MeasurableSet j
⊢ v j ≤ w j
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

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

Tactic:
· simp [g]

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 (f n - g) p μ ≤ ε

Tactic:
← t.indicator_self_add_compl (f n - g)

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 - g) + tᶜ.indicator (f n - g)) p μ ≤ ε
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : 0 ≤[i] s
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ (s.toMeasureOfZeroLE i hi₁ hi).real j = s (i ∩ j)

Tactic:
by
  simp [measureReal_def, toMeasureOfZeroLE_apply, hj₁]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ μ.toSignedMeasure ≤ ν.toSignedMeasure ↔ μ ≤ ν

Tactic:
rw [Measure.le_iff, VectorMeasure.le_iff]
  congrm ∀ s, (hs : MeasurableSet s) → ?_
  simp_rw [toSignedMeasure_apply_measurable hs, real_def]
  apply ENNReal.toReal_le_toReal <;> finiteness

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

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

Tactic:
exact s.haveLebesgueDecomposition_smul μ _

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 : α), f x ∂μ

Tactic:
rw [← setLIntegral_univ]

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
| ∫⁻ (x : α) in Set.univ, 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
hp₀ : p ≠ 0
hp : p ≠ ∞
c : E
⊢ lpNorm (fun _x ↦ c) p μ = ‖c‖ * μ.real Set.univ ^ p.toReal⁻¹

Tactic:
simp [lpNorm, eLpNorm_const' c hp₀ hp, Measure.real, ENNReal.toReal_rpow,
    aestronglyMeasurable_const]

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

Goal state before:
pp: case a.μ
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
| (r • s.toJordanDecomposition).posPart.singularPart μ

Tactic:
JordanDecomposition.smul_posPart,

Goal state after:
case a.μ
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
| (r • s.toJordanDecomposition.posPart).singularPart μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case inl
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : 0 ≤ r
⊢ (r • s).singularPart μ = r • s.singularPart μ

Tactic:
lift r to ℝ≥0 using hr
    exact singularPart_smul_nnreal s μ r

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

Goal state before:
pp: case pos
α : 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 μ ≤ ENNReal.ofReal ε

pp: case neg
α : 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 μ ≤ ENNReal.ofReal ε

Tactic:
· rw [(eLpNorm_eq_zero_iff ((hf i).indicator hs).aestronglyMeasurable hpzero).2
        (indicator_meas_zero hμs')]
    simp

Goal state after:
case neg
α : 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 μ ≤ ENNReal.ofReal ε
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))
n : ℕ
⊢ ∫ (ω : Ω), fs n ω ∂μ = (ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)).toReal

Tactic:
rw [ENNReal.toReal_ofReal]

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)
fs : ℕ → Ω → ℝ := fun n ω ↦ ↑((thickenedIndicator ⋯ F) ω)
h_eq : ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑((thickenedIndicator ⋯ F) ω) ∂μ = ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
h : Tendsto (fun n ↦ ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)) atTop (𝓝 (μ F))
n : ℕ
⊢ 0 ≤ ∫ (ω : Ω), fs n ω ∂μ
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Goal state before:
pp: case h.refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
F : Set X
hF : IsClosed[inst✝¹] F
key :
  ∀ (x : X),
    Tendsto (fun i ↦ (thickenedIndicator ⋯ F) x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F).indicator (fun x ↦ 1) x))
x : X
⊢ Tendsto (fun i ↦ ((fun n ↦ thickenedIndicator ⋯ F) i) x) atTop (𝓝 (F.indicator (fun x ↦ 1) x))

Tactic:
nth_rw 2 [← IsClosed.closure_eq hF]

Goal state after:
case h.refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
F : Set X
hF : IsClosed[inst✝¹] F
key :
  ∀ (x : X),
    Tendsto (fun i ↦ (thickenedIndicator ⋯ F) x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F).indicator (fun x ↦ 1) x))
x : X
⊢ Tendsto (fun i ↦ ((fun n ↦ thickenedIndicator ⋯ F) i) x) atTop (𝓝 ((closure[inst✝¹] F).indicator (fun x ↦ 1) x))
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✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
s : Set α
hs : MeasurableSet s
f : α → E
hm : m ≤ m0
hfint : ¬Integrable f μ
⊢ ∫ (x : α) in s, |μ[f | m] x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ

Tactic:
simpa [condExp_of_not_integrable hfint] using integral_nonneg (fun x => abs_nonneg f x)

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

Goal state before:

Tactic:
_ = ∫ x in s, |(μ.restrict s)[f | m] x| ∂μ :=
    (integral_congr_ae ((condExp_restrict_ae_eq_restrict hm hs hfint).fun_comp abs)).symm
  _  ≤ _ := integral_abs_condExp_le f

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
⊢ t ∈ {s | MeasurableSet s} → ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t

Tactic:
ht

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
ht : t ∈ {s | MeasurableSet s}
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x ↦ {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i ↦ if hi_mem : i ∈ S then Exists.choose ⋯ else univ
h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, setsΩ i) = ∏ i ∈ S, (κ a) (setsΩ i)

Tactic:
have h_preim : ∀ i ∈ S, setsΩ i = f i ⁻¹' setsβ i := by
    intro i hi_mem
    simp_rw [setsβ, dif_pos hi_mem]
    exact (h_meas i hi_mem).choose_spec.2.symm

Goal state after:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
S : Finset ι
setsΩ : ι → Set Ω
h_meas : ∀ i ∈ S, setsΩ i ∈ (fun x ↦ {s | MeasurableSet s}) i
setsβ : (i : ι) → Set (β i) := fun i ↦ if hi_mem : i ∈ S then Exists.choose ⋯ else univ
h_measβ : ∀ i ∈ S, MeasurableSet (setsβ i)
h_preim : ∀ i ∈ S, setsΩ i = f i ⁻¹' setsβ i
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, setsΩ i) = ∏ i ∈ S, (κ a) (setsΩ i)
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h : ∃ n, IndepSets (s n) s' κ μ
⊢ IndepSets (⋂ n, s n) s' κ μ

Tactic:
intro t1 t2 ht1 ht2; obtain ⟨n, h⟩ := h; exact h t1 t2 (Set.mem_iInter.mp ht1 n) ht2

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h : iIndepFun f κ μ
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
⊢ iIndepFun (fun i ↦ g i ∘ f i) κ μ

Tactic:
rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at h ⊢

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
⊢ ∀ (S : Finset ι) {sets : (i : ι) → Set (γ i)},
    (∀ i ∈ S, MeasurableSet (sets i)) →
      ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, g i ∘ f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (g i ∘ f i ⁻¹' sets i)
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case mpr
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (Measure.map f μ)
σg : SigmaFinite (Measure.map g μ)
h₀ :
  ∀ {s : Set β} {t : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        μ (f ⁻¹' s) * μ (g ⁻¹' t) = (Measure.map f μ) s * (Measure.map g μ) t ∧
          μ (f ⁻¹' s ∩ g ⁻¹' t) = (Measure.map (fun ω ↦ (f ω, g ω)) μ) (s ×ˢ t)
h : Measure.map (fun ω ↦ (f ω, g ω)) μ = (Measure.map f μ).prod (Measure.map g μ)
s : Set β
t : Set β'
hs : MeasurableSet s
⊢ MeasurableSet t → μ (f ⁻¹' s ∩ g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t)

Tactic:
ht

Goal state after:
case mpr
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (Measure.map f μ)
σg : SigmaFinite (Measure.map g μ)
h₀ :
  ∀ {s : Set β} {t : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        μ (f ⁻¹' s) * μ (g ⁻¹' t) = (Measure.map f μ) s * (Measure.map g μ) t ∧
          μ (f ⁻¹' s ∩ g ⁻¹' t) = (Measure.map (fun ω ↦ (f ω, g ω)) μ) (s ×ˢ t)
h : Measure.map (fun ω ↦ (f ω, g ω)) μ = (Measure.map f μ).prod (Measure.map g μ)
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ μ (f ⁻¹' s ∩ g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t)