mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : PseudoMetrizableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
μs : ι → Measure Ω
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i ↦ (μs i) E) L (𝓝 (μ E))
F : Set Ω
F_closed : IsClosed[inst✝³] F
this : PseudoMetricSpace Ω := pseudoMetrizableSpacePseudoMetric Ω
h✝ : L.NeBot
ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0
rs : ℕ → ℝ := Classical.choose ex
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0
Fthicks_open : ∀ (n : ℕ), IsOpen[inst✝³] (Metric.thickening (rs n) F)
key : ∀ (n : ℕ), Tendsto (fun i ↦ (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))
ε : ℝ≥0
rs_lim : (fun r ↦ μ (Metric.cthickening r F)) ⁻¹' Iio (μ F + ↑ε) ∈ map rs atTop
ε_pos : 0 < ε
μF_finite : μ F < ∞
keyB : Tendsto (fun r ↦ μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))
nhds : Iio (μ F + ↑ε) ∈ 𝓝 (μ F)
⊢ limsup (fun i ↦ (μs i) F) L ≤ μ F + ↑ε

Tactic:
simp only [mem_map, mem_atTop_sets, mem_preimage, mem_Iio] at rs_lim

Goal state after:
case inr
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : PseudoMetrizableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
μs : ι → Measure Ω
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i ↦ (μs i) E) L (𝓝 (μ E))
F : Set Ω
F_closed : IsClosed[inst✝³] F
this : PseudoMetricSpace Ω := pseudoMetrizableSpacePseudoMetric Ω
h✝ : L.NeBot
ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0
rs : ℕ → ℝ := Classical.choose ex
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0
Fthicks_open : ∀ (n : ℕ), IsOpen[inst✝³] (Metric.thickening (rs n) F)
key : ∀ (n : ℕ), Tendsto (fun i ↦ (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : μ F < ∞
keyB : Tendsto (fun r ↦ μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))
nhds : Iio (μ F + ↑ε) ∈ 𝓝 (μ F)
rs_lim : ∃ a, ∀ (b : ℕ), a ≤ b → μ (Metric.cthickening (rs b) F) < μ F + ↑ε
⊢ limsup (fun i ↦ (μs i) F) L ≤ μ F + ↑ε
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : ι → Set Ω
h : iIndepSet f μ
s : Finset ι
⊢ μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)

Tactic:
by
  simpa using Kernel.iIndepSet.meas_biInter h s

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

Goal state before:
pp: Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsFiniteMeasure μ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ f ⟂ᵢ[μ] g ↔ Measure.map (fun ω ↦ (f ω, g ω)) μ = (Measure.map f μ).prod (Measure.map g μ)

Tactic:
apply indepFun_iff_map_prod_eq_prod_map_map' hf hg <;> apply IsFiniteMeasure.toSigmaFinite

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

Goal state before:
pp: case refine_2.refine_1
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u → (μ ⊗ₘ κ.map fun ω ↦ (f ω, g ω)) (s ×ˢ t ×ˢ u) = (μ ⊗ₘ (κ.map f ×ₖ κ.map g)) (s ×ˢ t ×ˢ u)
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ Measurable fun a ↦ (κ a) (f ⁻¹' s ∩ g ⁻¹' t)

Tactic:
exact Kernel.measurable_coe _ ((hf hs).inter (hg ht))

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

Goal state before:
pp: case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
hπT_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πT
s : Set ((i : ↥S) → β ↑i)
sets_s : (i : ↥S) → Set (β ↑i)
hs2 : univ.pi sets_s = s
t : Set ((i : ↥T) → β ↑i)
sets_t : (i : ↥T) → Set (β ↑i)
ht2 : univ.pi sets_t = t
hs1 : ∀ (i : ↥S), MeasurableSet (sets_s i)
ht1 : ∀ (i : ↥T), MeasurableSet (sets_t i)
⊢ ∀ᵐ (a : α) ∂μ,
    (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_s ∩ (fun a i ↦ f (↑i) a) ⁻¹' t) =
      (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_s) * (η a) ((fun a i ↦ f (↑i) a) ⁻¹' t)

Tactic:
← ht2

Goal state after:
case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
hπT_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πT
s : Set ((i : ↥S) → β ↑i)
sets_s : (i : ↥S) → Set (β ↑i)
hs2 : univ.pi sets_s = s
t : Set ((i : ↥T) → β ↑i)
sets_t : (i : ↥T) → Set (β ↑i)
ht2 : univ.pi sets_t = t
hs1 : ∀ (i : ↥S), MeasurableSet (sets_s i)
ht1 : ∀ (i : ↥T), MeasurableSet (sets_t i)
⊢ ∀ᵐ (a : α) ∂μ,
    (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_s ∩ (fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_t) =
      (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_s) * (η a) ((fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_t)
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → F
hf : AEStronglyMeasurable f μ
⊢ ∫ (x : E), (pdf X ℙ μ x).toReal • f x ∂μ = ∫ (x : Ω), f (X x) ∂ℙ

Tactic:
by
  rw [← integral_map (HasPDF.aemeasurable X ℙ μ) (hf.mono_ac HasPDF.absolutelyContinuous),
    map_eq_withDensity_pdf X ℙ μ, pdf_def, integral_rnDeriv_smul HasPDF.absolutelyContinuous,
    withDensity_rnDeriv_eq _ _ HasPDF.absolutelyContinuous]

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν)
⊢ X ⟂ᵢ[ℙ] Y ↔ pdf (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν) =ᵐ[μ.prod ν] fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2

Tactic:
have : HasPDF X ℙ μ := quasiMeasurePreserving_hasPDF' (μ := μ.prod ν) (fun ω ↦ (X ω, Y ω))
    quasiMeasurePreserving_fst

Goal state after:
Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this : HasPDF X ℙ μ
⊢ X ⟂ᵢ[ℙ] Y ↔ pdf (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν) =ᵐ[μ.prod ν] fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
Module: Mathlib.Probability.Density

Goal state before:
pp: case hmf
Ω : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝⁴ : MeasurableSpace F
ν : Measure F
X : Ω → E
Y : Ω → F
inst✝³ : IsFiniteMeasure ℙ
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : HasPDF (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν)
this✝ : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
h₀ : (map X ℙ).prod (map Y ℙ) = (μ.prod ν).withDensity fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
⊢ AEMeasurable (fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2) (μ.prod ν)

Tactic:
exact (((measurable_pdf X ℙ μ).comp measurable_fst).mul
    ((measurable_pdf Y ℙ ν).comp measurable_snd)).aemeasurable

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 Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
f : ι → Set Ω := fun n ↦ if n = a then t2 else if n ∈ s then ft1 n else univ
h_f_mem : ∀ n ∈ insert a s, f n ∈ π n
h_f_mem_pi : ∀ n ∈ s, f n ∈ π n
h_t1 : t1 = ⋂ n ∈ s, f n
h_μ_t1 : ∀ᵐ (a' : α) ∂μ, (κ a') t1 = ∏ n ∈ s, (κ a') (f n)
h_t2 : t2 = f a
h_μ_inter : ∀ᵐ (a' : α) ∂μ, (κ a') (t1 ∩ t2) = ∏ n ∈ insert a s, (κ a') (f n)
has : a ∉ s
a' : α
ha1 : (κ a') t1 = ∏ n ∈ s, (κ a') (f n)
ha2 : (κ a') (t1 ∩ t2) = ∏ n ∈ insert a s, (κ a') (f n)
⊢ (κ a') (f a) * ∏ x ∈ s, (κ a') (f x) = (κ a') t1 * (κ a') (f a)

Tactic:
mul_comm,

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
a : ι
S : Finset ι
hp_ind : iIndepSets π κ μ
haS : a ∉ S
t1 t2 : Set Ω
s : Finset ι
hs_mem : s ⊆ S
ft1 : ι → Set Ω
hft1_mem : ∀ x ∈ s, ft1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ s, ft1 x
ht2_mem_pia : t2 ∈ π a
f : ι → Set Ω := fun n ↦ if n = a then t2 else if n ∈ s then ft1 n else univ
h_f_mem : ∀ n ∈ insert a s, f n ∈ π n
h_f_mem_pi : ∀ n ∈ s, f n ∈ π n
h_t1 : t1 = ⋂ n ∈ s, f n
h_μ_t1 : ∀ᵐ (a' : α) ∂μ, (κ a') t1 = ∏ n ∈ s, (κ a') (f n)
h_t2 : t2 = f a
h_μ_inter : ∀ᵐ (a' : α) ∂μ, (κ a') (t1 ∩ t2) = ∏ n ∈ insert a s, (κ a') (f n)
has : a ∉ s
a' : α
ha1 : (κ a') t1 = ∏ n ∈ s, (κ a') (f n)
ha2 : (κ a') (t1 ∩ t2) = ∏ n ∈ insert a s, (κ a') (f n)
⊢ (∏ x ∈ s, (κ a') (f x)) * (κ a') (f a) = (κ a') t1 * (κ a') (f a)
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ ∫ (a : Ω), X a * Y a ∂μ - ∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ -
      (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a ∂μ - ∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ

pp: case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun a ↦ (∫ (x : Ω), X x ∂μ) * Y a) μ

pp: case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun a ↦ (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ) μ

pp: case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun a ↦ X a * Y a) μ

pp: case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun a ↦ X a * ∫ (x : Ω), Y x ∂μ) μ

pp: case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun ω ↦ X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ) μ

pp: case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun ω ↦ (∫ (x : Ω), X x ∂μ) * Y ω - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ) μ

Tactic:
· simp_rw [integral_mul_const, integral_const_mul, integral_const, probReal_univ,
       one_smul]
     simp

Goal state after:
case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun a ↦ (∫ (x : Ω), X x ∂μ) * Y a) μ

case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun a ↦ (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ) μ

case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun a ↦ X a * Y a) μ

case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun a ↦ X a * ∫ (x : Ω), Y x ∂μ) μ

case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun ω ↦ X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ) μ

case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (fun ω ↦ (∫ (x : Ω), X x ∂μ) * Y ω - (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ) μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ ENNReal.ofReal eVar[X; μ].toReal = eVar[X; μ]

Tactic:
ENNReal.ofReal_toReal

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ eVar[X; μ] = eVar[X; μ]

Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ eVar[X; μ] ≠ ∞
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
⊢ ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2) = eVar[X; μ]

Tactic:
evariance_eq_top hX hℒ,

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
⊢ ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2) = ∞
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x ↦ ∫ (x : Ω), X x ∂μ) μ
⊢ eVar[X; μ] * (↑c)⁻¹ ^ 2 = (↑c)⁻¹ ^ 2 * ((∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ) ^ 2⁻¹) ^ 2

Tactic:
mul_comm,

Goal state after:
case e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x ↦ ∫ (x : Ω), X x ∂μ) μ
⊢ (↑c)⁻¹ ^ 2 * eVar[X; μ] = (↑c)⁻¹ ^ 2 * ((∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ) ^ 2⁻¹) ^ 2
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ ∀ᵐ (x : γ) ∂Measure.map f μ, id x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
rw [ae_map_iff h.aemeasurable_fst]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ ∀ᵐ (x : α) ∂μ, id (f x) ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t

α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : NormedAddCommGroup γ
inst✝¹ : NormedSpace ℝ γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ MeasurableSet {x | id x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t}
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
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
n : ℕ
a : α
⊢ ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a ≤ 1 * ↑n.succ

Tactic:
mul_comm,

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
hN₁ : ∀ (u : Finset ℕ), ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n)
f : ℕ → α → ℝ≥0∞ := fun n ↦ (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), (s k).indicator 1
hfapp : ∀ (n : ℕ) (a : α), f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a
hf : ∀ (n : ℕ), Measurable (f n)
n : ℕ
a : α
⊢ ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a ≤ ↑n.succ * 1
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁴ : (i : ι) → TopologicalSpace (β i)
inst✝³ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝² : ∀ (i : ι), BorelSpace (β i)
inst✝¹ : Preorder ι
X : ι → Type u_4
inst✝ : (i : ι) → MeasurableSpace (X i)
i j : ι
hij : i ≤ j
⊢ MeasurableSpace.comap (restrictLe i) MeasurableSpace.pi ≤ MeasurableSpace.comap (restrictLe j) MeasurableSpace.pi

Tactic:
← restrictLe₂_comp_restrictLe hij,

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
β : ι → Type u_3
inst✝⁴ : (i : ι) → TopologicalSpace (β i)
inst✝³ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝² : ∀ (i : ι), BorelSpace (β i)
inst✝¹ : Preorder ι
X : ι → Type u_4
inst✝ : (i : ι) → MeasurableSpace (X i)
i j : ι
hij : i ≤ j
⊢ MeasurableSpace.comap (restrictLe₂ hij ∘ restrictLe j) MeasurableSpace.pi ≤
    MeasurableSpace.comap (restrictLe j) MeasurableSpace.pi
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case a
ι : Type u_2
inst✝² : Preorder ι
X : ι → Type u_4
inst✝¹ : (i : ι) → MeasurableSpace (X i)
inst✝ : LocallyFiniteOrderBot ι
i : ι
⊢ ↑piLE i ≤ MeasurableSpace.comap (frestrictLe i) MeasurableSpace.pi

pp: case a
ι : Type u_2
inst✝² : Preorder ι
X : ι → Type u_4
inst✝¹ : (i : ι) → MeasurableSpace (X i)
inst✝ : LocallyFiniteOrderBot ι
i : ι
⊢ MeasurableSpace.comap (frestrictLe i) MeasurableSpace.pi ≤ ↑piLE i

Tactic:
· simp_rw [piLE, ← piCongrLeft_comp_frestrictLe, ← MeasurableEquiv.coe_piCongrLeft, ← comap_comp]
    exact MeasurableSpace.comap_mono <| Measurable.comap_le (by fun_prop)

Goal state after:
case a
ι : Type u_2
inst✝² : Preorder ι
X : ι → Type u_4
inst✝¹ : (i : ι) → MeasurableSpace (X i)
inst✝ : LocallyFiniteOrderBot ι
i : ι
⊢ MeasurableSpace.comap (frestrictLe i) MeasurableSpace.pi ≤ ↑piLE i
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hre : AEMeasurable (fun x ↦ RCLike.re (f x)) μ
him : AEMeasurable (fun x ↦ RCLike.im (f x)) μ
⊢ AEMeasurable f μ

Tactic:
convert!
    AEMeasurable.fun_add (M := 𝕜) (RCLike.measurable_ofReal.comp_aemeasurable hre)
      ((RCLike.measurable_ofReal.comp_aemeasurable him).mul_const RCLike.I)

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : MeasurableSpace α
f : α → 𝕜
μ : MeasureTheory.Measure α
hre : AEMeasurable (fun x ↦ RCLike.re (f x)) μ
him : AEMeasurable (fun x ↦ RCLike.im (f x)) μ
x✝ : α
⊢ f x✝ = (RCLike.ofReal ∘ fun x ↦ RCLike.re (f x)) x✝ + (RCLike.ofReal ∘ fun x ↦ RCLike.im (f x)) x✝ * RCLike.I
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, ⋯⟩
⊢ ↑((G b).index x) = ↑⟨y, ⋯⟩

Tactic:
← Fin.ext_iff,

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, ⋯⟩
⊢ (G b).index x = ⟨y, ⋯⟩
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
this : μ F * 2 ^ finrank ℝ E < μ ↑(S n)
⊢ ∀ x ∈ S n, -x ∈ S n

Tactic:
rintro _ ⟨y, hy, rfl⟩

Goal state after:
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
this : μ F * 2 ^ finrank ℝ E < μ ↑(S n)
y : E
hy : y ∈ ↑K
⊢ -(fun x ↦ ↑(1 + u n) • x) y ∈ S n