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

Goal state before:
pp: α : 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
R : E
f : α → E
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ R
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ R

Tactic:
by_cases! hn : {x | |f x| ≤ R} = ∅

Goal state after:
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
R : E
f : α → E
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ R
hn : {x | |f x| ≤ R} = ∅
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ R

case neg
α : 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
R : E
f : α → E
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ R
hn : {x | |f x| ≤ R}.Nonempty
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ R
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ Measurable fun μ ↦ (↑μ.1).prod ↑μ.2

Tactic:
apply Measurable.measure_of_isPiSystem_of_isProbabilityMeasure generateFrom_prod.symm
    isPiSystem_prod _
  simp only [mem_image2, mem_ofPred_eq, forall_exists_index, and_imp]
  intro _ u Hu v Hv Heq
  simp_rw [← Heq, Measure.prod_prod]
  apply Measurable.mul
  · exact (Measure.measurable_coe Hu).comp (measurable_subtype_coe.comp measurable_fst)
  · exact (Measure.measurable_coe Hv).comp (measurable_subtype_coe.comp measurable_snd)

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

Goal state before:
pp: Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
⊢ μ.normalize s = μ.mass⁻¹ * μ s

Tactic:
by
  simp only [μ.self_eq_mass_mul_normalize, μ.mass_nonzero_iff.mpr nonzero, inv_mul_cancel_left₀,
    Ne, not_false_iff]

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

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
p : ℝ≥0∞
hp : 1 ≤ p
hf : MemLp f p μ
h✝ : NeZero μ
⊢ lpNorm μ[f | m] p μ ≤ lpNorm f p μ

Tactic:
have hp' : 0 < p := zero_lt_one.trans_le hp

Goal state after:
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 : MemLp f p μ
h✝ : NeZero μ
hp' : 0 < p
⊢ lpNorm μ[f | m] p μ ≤ lpNorm f p μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : 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 : MemLp f p μ
⊢ MemLp μ[f | m] p μ

Tactic:
have hp' : 0 < p := zero_lt_one.trans_le hp

Goal state after:
α : 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 : MemLp f p μ
hp' : 0 < p
⊢ MemLp μ[f | m] p μ
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 ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
ℐ : ℝ≥0 → ι
δ : ℝ≥0
hδpos : 0 < ↑δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal ↑δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal ↑δ < μ {x | C ≤ ‖f (ℐ C) x‖₊}
C : ℝ≥0
⊢ C • ↑δ ^ (1 / p.toReal) ≤ C • μ {x | C ≤ ‖f (ℐ C) x‖₊} ^ (1 / p.toReal)

Tactic:
ENNReal.smul_def,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
ℐ : ℝ≥0 → ι
δ : ℝ≥0
hδpos : 0 < ↑δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal ↑δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal ↑δ < μ {x | C ≤ ‖f (ℐ C) x‖₊}
C : ℝ≥0
⊢ ↑C • ↑δ ^ (1 / p.toReal) ≤ C • μ {x | C ≤ ‖f (ℐ C) x‖₊} ^ (1 / p.toReal)
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 ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
ℐ : ℝ≥0 → ι
δ : ℝ≥0
hδpos : 0 < ↑δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal ↑δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal ↑δ < μ {x | C ≤ ‖f (ℐ C) x‖₊}
C : ℝ≥0
⊢ ↑C • ↑δ ^ (1 / p.toReal) ≤ C • μ {x | C ≤ ‖f (ℐ C) x‖₊} ^ (1 / p.toReal)

Tactic:
ENNReal.smul_def,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
ℐ : ℝ≥0 → ι
δ : ℝ≥0
hδpos : 0 < ↑δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal ↑δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal ↑δ < μ {x | C ≤ ‖f (ℐ C) x‖₊}
C : ℝ≥0
⊢ ↑C • ↑δ ^ (1 / p.toReal) ≤ ↑C • μ {x | C ≤ ‖f (ℐ C) x‖₊} ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
h_opens : ∀ (G : Set Ω), IsOpen[inst✝¹] G → ↑μ G ≤ liminf (fun i ↦ ↑(μs i) G) atTop
⊢ Tendsto (fun i ↦ μs i) atTop (𝓝 μ)

Tactic:
refine ProbabilityMeasure.tendsto_iff_forall_integral_tendsto.mpr ?_
  refine tendsto_integral_of_forall_integral_le_liminf_integral fun f f_nn ↦ ?_
  exact integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure f_nn h_opens

Goal state after:
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case pos
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
hi : i ∈ s
⊢ MeasurableSet (Y i ⁻¹' t i ∩ f i)

pp: case neg
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
hi : i ∉ s
⊢ MeasurableSet (Y i ⁻¹' t i)

Tactic:
· obtain ⟨A, hA, hA'⟩ := hf i hi
        exact .inter ⟨.univ ×ˢ t i, MeasurableSet.univ.prod (ht _), by ext; simp⟩
          ⟨A ×ˢ Set.univ, hA.prod .univ, by ext; simp [← hA']⟩

Goal state after:
case neg
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
hi : i ∉ s
⊢ MeasurableSet (Y i ⁻¹' t i)
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable X μ

pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable (X + Y) μ

Tactic:
· exact hX.aemeasurable

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable (X + Y) μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ ∑ i, Var[fun ω ↦ X i (ω i); Measure.pi μ] = ∑ i, Var[X i; μ i]

pp: case hs
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ ∀ i ∈ univ, MemLp (fun ω ↦ X i (ω i)) 2 (Measure.pi μ)

pp: case h
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ (↑univ).Pairwise fun i j ↦ (fun ω ↦ X i (ω i)) ⟂ᵢ[Measure.pi μ] fun ω ↦ X j (ω j)

Tactic:
· congr with i
    change Var[(X i) ∘ (fun ω ↦ ω i); Measure.pi μ] = _
    rw [← variance_map, (measurePreserving_eval _ i).map_eq]
    · rw [(measurePreserving_eval _ i).map_eq]
      exact (h i).aestronglyMeasurable.aemeasurable
    · exact Measurable.aemeasurable (by fun_prop)

Goal state after:
case hs
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ ∀ i ∈ univ, MemLp (fun ω ↦ X i (ω i)) 2 (Measure.pi μ)

case h
ι : Type u_2
inst✝¹ : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ (↑univ).Pairwise fun i j ↦ (fun ω ↦ X i (ω i)) ⟂ᵢ[Measure.pi μ] fun ω ↦ X j (ω j)
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: case hZ
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
hX : HasLaw X μ P
f g : 𝓧 → ℝ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable X P

Tactic:
· exact hX.aemeasurable

Goal state after:
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
h : iIndepFun X P
⊢ map (fun ω i ↦ X i ω) P = Measure.pi μ

Tactic:
h.map_fun_eq_pi_map (by fun_prop)

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
h : iIndepFun X P
⊢ (Measure.pi fun i ↦ map (X i) P) = Measure.pi μ
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: Ω : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (f i) (Measure.map (X i) μ)
⊢ ∫ (ω : Ω), ∏ i, f i (X i ω) ∂μ = ∏ i, ∫ (ω : Ω), f i (X i ω) ∂μ

Tactic:
have := hX.isProbabilityMeasure

Goal state after:
Ω : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
inst✝ : Fintype ι
𝓧 : ι → Type u_4
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
f : (i : ι) → 𝓧 i → 𝕜
hX : iIndepFun X μ
mX : ∀ (i : ι), AEMeasurable (X i) μ
hf : ∀ (i : ι), AEStronglyMeasurable (f i) (Measure.map (X i) μ)
this : IsProbabilityMeasure μ
⊢ ∫ (ω : Ω), ∏ i, f i (X i ω) ∂μ = ∏ i, ∫ (ω : Ω), f i (X i ω) ∂μ
Module: Mathlib.MeasureTheory.Function.Intersectivity

Goal state before:
pp: α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : μ (⋂ n ∈ u, s n) = 0
⊢ eLpNormEssSup ((⋂ n ∈ u, s n).indicator 1) μ < ↑‖(⋂ n ∈ u, s n).indicator 1 x‖₊

Tactic:
indicator_of_mem hx.1,

Goal state after:
α : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ μ (s n)
M : (α → ℝ) → Set α := fun f ↦ {x | eLpNormEssSup f μ < ↑‖f x‖₊}
N : Set α := ⋃ u, M ((⋂ n ∈ u, s n).indicator 1)
hN₀ : μ N = 0
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : μ (⋂ n ∈ u, s n) = 0
⊢ eLpNormEssSup ((⋂ n ∈ u, s n).indicator 1) μ < ↑‖1 x‖₊
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : DenselyOrdered ι
𝓕 : Filtration ι m
i : ι
hi : ¬IsMax i
this✝ : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
⊢ ↑𝓕₊ i = ⨅ j, ⨅ (_ : j > i), ↑𝓕 j

Tactic:
have : (𝓝[>] i).NeBot := nhdsGT_neBot_of_exists_gt (not_isMax_iff.mp hi)

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : DenselyOrdered ι
𝓕 : Filtration ι m
i : ι
hi : ¬IsMax i
this✝¹ : TopologicalSpace ι := Preorder.topology ι
this✝ : OrderTopology ι
this : (𝓝[>] i).NeBot
⊢ ↑𝓕₊ i = ⨅ j, ⨅ (_ : j > i), ↑𝓕 j
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this✝ : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : ¬(𝓝[>] i).NeBot
⊢ ↑𝓕 i ≤ ↑𝓕₊ i

Tactic:
rw [rightCont_apply, if_neg hne]

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
𝓕 : Filtration ι m
this✝ : TopologicalSpace ι := Preorder.topology ι
this : OrderTopology ι
i : ι
hne : ¬(𝓝[>] i).NeBot
⊢ ↑𝓕₊₊ i ≤ ↑𝓕₊ i

Tactic:
rw [rightCont_apply, if_neg hne]

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

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Finite ι
x : α
⊢ Tendsto (fun n ↦ ((fun n ↦ hs.simpleFunc_piecewise hm fun i ↦ ⋯.approx n) n) x) atTop (nhds (hs.piecewise f x))

Tactic:
simp [simpleFunc_piecewise, piecewise_apply, StronglyMeasurable.tendsto_approx]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
e : ℕ ≃ ι
g : (n : ℕ) → ι → Fin (n + 1) := fun n i ↦ if hi : ∃ m < n, i = e m then ⟨hi.choose, ⋯⟩ else Fin.last n
sg : ∀ (n : ℕ), Function.Surjective (g n)
G : (n : ℕ) → IndexedPartition fun k ↦ ⋃ i ∈ g n ⁻¹' {k}, s i
x : α
y : ℕ
hy : e y = hs.index x
b : ℕ
hb : y + 1 ≤ b
this : y = ↑⟨y, ⋯⟩
⊢ e ↑((G b).index x) = hs.index x

Tactic:
rw [← hy, EmbeddingLike.apply_eq_iff_eq, this, ← Fin.ext_iff, ← (G b).mem_iff_index_eq]

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
e : ℕ ≃ ι
g : (n : ℕ) → ι → Fin (n + 1) := fun n i ↦ if hi : ∃ m < n, i = e m then ⟨hi.choose, ⋯⟩ else Fin.last n
sg : ∀ (n : ℕ), Function.Surjective (g n)
G : (n : ℕ) → IndexedPartition fun k ↦ ⋃ i ∈ g n ⁻¹' {k}, s i
x : α
y : ℕ
hy : e y = hs.index x
b : ℕ
hb : y + 1 ≤ b
this : y = ↑⟨y, ⋯⟩
⊢ x ∈ ⋃ i ∈ g b ⁻¹' {⟨y, ⋯⟩}, s i
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hfg : ∀ (n : ι), f n =ᵐ[μ] g n
ε : ℝ≥0
hε : 0 < ε
s : Set α
hμs : μ s ≠ ∞
hfε : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
⊢ ∃ s, μ s ≠ ∞ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (g i)) p μ ≤ ↑ε

Tactic:
refine ⟨s, hμs, fun n => (le_of_eq <| eLpNorm_congr_ae ?_).trans (hfε n)⟩

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hfg : ∀ (n : ι), f n =ᵐ[μ] g n
ε : ℝ≥0
hε : 0 < ε
s : Set α
hμs : μ s ≠ ∞
hfε : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
n : ι
⊢ sᶜ.indicator (g n) =ᵐ[μ] sᶜ.indicator (f n)
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifTight f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬↑ε = ∞
g : Fin n → α → β := fun k ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : μ S ≠ ∞
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ ↑ε
s : Set α
left✝ : MeasurableSet s
hμs : μ s < ∞
hfε : eLpNorm (sᶜ.indicator (f (Fin.last n))) p μ < ↑ε
i : Fin (n + 1)
⊢ eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
by_cases! hi : i.val < n

Goal state after:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifTight f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬↑ε = ∞
g : Fin n → α → β := fun k ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : μ S ≠ ∞
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ ↑ε
s : Set α
left✝ : MeasurableSet s
hμs : μ s < ∞
hfε : eLpNorm (sᶜ.indicator (f (Fin.last n))) p μ < ↑ε
i : Fin (n + 1)
hi : ↑i < n
⊢ eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ ↑ε

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β}, (∀ (i : Fin n), MemLp (f i) p μ) → UnifTight f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬↑ε = ∞
g : Fin n → α → β := fun k ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
S : Set α
hμS : μ S ≠ ∞
hFε : ∀ (i : Fin n), eLpNorm (Sᶜ.indicator (g i)) p μ ≤ ↑ε
s : Set α
left✝ : MeasurableSet s
hμs : μ s < ∞
hfε : eLpNorm (sᶜ.indicator (f (Fin.last n))) p μ < ↑ε
i : Fin (n + 1)
hi : n ≤ ↑i
⊢ eLpNorm ((s ∪ S)ᶜ.indicator (f i)) p μ ≤ ↑ε
Module: Mathlib.MeasureTheory.Integral.CircleTransform

Goal state before:
pp: case hg
R r : ℝ
hr : r < R
z : ℂ
⊢ ContinuousOn (fun w ↦ circleMap z R w.2 - w.1) (closedBall z r ×ˢ univ)

Tactic:
exact ((continuous_circleMap z R).comp_continuousOn continuousOn_snd).sub continuousOn_fst

Goal state after:
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : AddMonoid β
inst✝¹ : StarAddMonoid β
inst✝ : ContinuousStar β
f : α →C_c β
support_star : (Function.support fun x ↦ star (f x)) = Function.support ⇑f
⊢ IsCompact (closure (Function.support fun x ↦ star (f x)))

Tactic:
support_star

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : AddMonoid β
inst✝¹ : StarAddMonoid β
inst✝ : ContinuousStar β
f : α →C_c β
support_star : (Function.support fun x ↦ star (f x)) = Function.support ⇑f
⊢ IsCompact (closure (Function.support ⇑f))
Module: Mathlib.MeasureTheory.Integral.Indicator

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
As : ι → Set α
μ : Measure α
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
inst✝ : ⊥.IsCountablyGenerated
As_le_B : ∀ᶠ (i : ι) in ⊥, As i ⊆ B
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in ⊥, x ∈ As i ↔ x ∈ A
⊢ Tendsto (fun i ↦ μ (As i)) ⊥ (𝓝 (μ A))

pp: case inr
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
h✝ : L.NeBot
⊢ Tendsto (fun i ↦ μ (As i)) L (𝓝 (μ A))

Tactic:
· exact tendsto_bot

Goal state after:
case inr
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
h✝ : L.NeBot
⊢ Tendsto (fun i ↦ μ (As i)) L (𝓝 (μ A))
Module: Mathlib.MeasureTheory.Integral.Indicator

Goal state before:
pp: case inl
α : Type u_1
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_2
As : ι → Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
inst✝ : ⊥.IsCountablyGenerated
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in ⊥, x ∈ As i ↔ x ∈ A
⊢ Tendsto (fun i ↦ μ (As i)) ⊥ (𝓝 (μ A))

pp: case inr
α : Type u_1
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
inst✝ : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
h✝ : L.NeBot
⊢ Tendsto (fun i ↦ μ (As i)) L (𝓝 (μ A))

Tactic:
· exact tendsto_bot

Goal state after:
case inr
α : Type u_1
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
inst✝ : IsFiniteMeasure μ
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
h✝ : L.NeBot
⊢ Tendsto (fun i ↦ μ (As i)) L (𝓝 (μ A))
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ ∫ (x : ℝ × ℝ) in Ioi 0 ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)) =
    (∫ (x : ℝ) in Ioi 0, x * |x| ^ q * rexp (-|x| ^ p)) * ∫ (x : ℝ) in Ioo (-π) π, 1

Tactic:
rw [← setIntegral_prod_mul, volume_eq_prod]
      simp_rw [mul_one]
      congr! 2; ring

Goal state after: