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

Goal state before:
pp: case e'_3
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → μ G ≤ liminf (fun i ↦ (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), ↑‖f x‖₊ ∂μs i ≤ ↑‖f‖₊
x✝ : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x✝ ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs n
i : ℕ
hi : x✝ ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i
x : Ω
aux : ENNReal.ofReal (f x) = ↑(NNReal.mk (f x) ⋯)
⊢ ENNReal.ofReal (f x) = ↑‖f x‖₊

Tactic:
aux

Goal state after:
case e'_3
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens : ∀ (G : Set Ω), IsOpen[inst✝²] G → μ G ≤ liminf (fun i ↦ (μs i) G) atTop
same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i ↦ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), ↑‖f x‖₊ ∂μs i ≤ ↑‖f‖₊
x✝ : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x✝ ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs n
i : ℕ
hi : x✝ ≤ ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i
x : Ω
aux : ENNReal.ofReal (f x) = ↑(NNReal.mk (f x) ⋯)
⊢ ↑(NNReal.mk (f x) ⋯) = ↑‖f x‖₊
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case refine_2.hg
ι : Type u_11
inst✝² : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝¹ : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst✝ : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
i : ι
⊢ AEMeasurable (X i) (Measure.map (Function.eval i) (Measure.pi μ))

Tactic:
(measurePreserving_eval μ i).map_eq

Goal state after:
case refine_2.hg
ι : Type u_11
inst✝² : Fintype ι
Ω : ι → Type u_12
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝¹ : ∀ (i : ι), IsProbabilityMeasure (μ i)
𝓧 : ι → Type u_13
inst✝ : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), AEMeasurable (X i) (μ i)
i : ι
⊢ AEMeasurable (X i) (μ i)
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case refine_2.refine_3
α : 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
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
h : ∫⁻ (a : α) in u, ((κ.map fun ω ↦ (f ω, g ω)) a) (s ×ˢ t) ∂μ = (μ ⊗ₘ (κ.map f ×ₖ κ.map g)) (u ×ˢ s ×ˢ t)
hu : MeasurableSet u
hμu : μ u < ⊤
⊢ ∫⁻ (x : α) in u, (κ x) (f ⁻¹' s ∩ g ⁻¹' t) ∂μ = ∫⁻ (x : α) in u, (κ x) (f ⁻¹' s) * (κ x) (g ⁻¹' t) ∂μ

Tactic:
Measure.compProd_apply_prod hu (hs.prod ht)

Goal state after:
case refine_2.refine_3
α : 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
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
h : ∫⁻ (a : α) in u, ((κ.map fun ω ↦ (f ω, g ω)) a) (s ×ˢ t) ∂μ = ∫⁻ (a : α) in u, ((κ.map f ×ₖ κ.map g) a) (s ×ˢ t) ∂μ
hu : MeasurableSet u
hμu : μ u < ⊤
⊢ ∫⁻ (x : α) in u, (κ x) (f ⁻¹' s ∩ g ⁻¹' t) ∂μ = ∫⁻ (x : α) in u, (κ x) (f ⁻¹' s) * (κ x) (g ⁻¹' t) ∂μ
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → Measure Ω
ν : Measure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ s ∈ S, Tendsto (fun i ↦ (μ i).real s) l (𝓝 (ν.real s))
hν : ∀ s ∈ S, ν s ≠ ∞
hμ : ∀ s ∈ S, ∀ (i : ι), (μ i) s ≠ ∞
A : ∀ (i : ι), (μ i).real (⋃ s ∈ t, s) = ∑ u ∈ t.powerset with u.Nonempty, (-1) ^ (#u + 1) * (μ i).real (⋂ s ∈ u, s)
u : Finset (Set Ω)
hu : u ⊆ t ∧ u.Nonempty
h'u : (⋂ s ∈ u, s).Nonempty
⊢ ⋂ s ∈ u, s ∈ S

Tactic:
exact hS.biInter_mem hu.2 (fun s hs ↦ ht _ (hu.1 hs)) h'u

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

Goal state before:
pp: case neg
Ω : Type u_1
𝕜 : Type u_2
inst✝¹⁴ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : MeasurableSpace 𝓧
inst✝¹² : MeasurableSpace 𝓨
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : Integrable f (Measure.map X μ)
hg : Integrable g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
this✝³ : MeasurableSpace E := borel E
this✝² : BorelSpace E
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
this : IsProbabilityMeasure μ
⊢ ∫ (ω : Ω), (B (f (X ω))) (g (Y ω)) ∂μ = (B (∫ (ω : Ω), f (X ω) ∂μ)) (∫ (ω : Ω), g (Y ω) ∂μ)

Tactic:
rw [← integral_map (f := fun z ↦ B (f z.1) (g z.2)) (φ := fun ω ↦ (X ω, Y ω)) (by fun_prop),
    hXY.map_prod_eq_prod_map_map hX hY, integral_prod_bilin _ hf hg, integral_map hX hf.1,
    integral_map hY hg.1]

Goal state after:
case neg
Ω : Type u_1
𝕜 : Type u_2
inst✝¹⁴ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : MeasurableSpace 𝓧
inst✝¹² : MeasurableSpace 𝓨
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : Integrable f (Measure.map X μ)
hg : Integrable g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
this✝³ : MeasurableSpace E := borel E
this✝² : BorelSpace E
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
this : IsProbabilityMeasure μ
⊢ AEStronglyMeasurable (fun z ↦ (B (f z.1)) (g z.2)) (Measure.map (fun ω ↦ (X ω, Y ω)) μ)
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : HasLaw Y ν μ
hX : HasLaw X μ P
⊢ map Y (map X P) = ν

pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : HasLaw Y ν μ
hX : HasLaw X μ P
⊢ AEMeasurable Y (map X P)

Tactic:
hX.map_eq,

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : HasLaw Y ν μ
hX : HasLaw X μ P
⊢ map Y μ = ν

Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : 𝓧 → 𝓨
hY : HasLaw Y ν μ
hX : HasLaw X μ P
⊢ AEMeasurable Y (map X P)
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ map X P ∗ₘ map Y P = μ ∗ₘ ν

pp: case σf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ SigmaFinite (map X P)

pp: case σg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ SigmaFinite (map Y P)

Tactic:
hX.map_eq,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ μ ∗ₘ map Y P = μ ∗ₘ ν

case σf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ SigmaFinite (map X P)

case σg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
M : Type u_3
inst✝³ : Monoid M
mM : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
X Y : Ω → M
hX : HasLaw X μ P
hY : HasLaw Y ν P
hXY : X ⟂ᵢ[P] Y
⊢ SigmaFinite (map Y P)
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst✝ : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : X ⟂ᵢ[P] Y
⊢ (map X P).prod (map Y P) = μ.prod ν

Tactic:
hX.map_eq,

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst✝ : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : X ⟂ᵢ[P] Y
⊢ μ.prod (map Y P) = μ.prod ν
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst✝ : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : HasLaw (fun ω ↦ (X ω, Y ω)) (μ.prod ν) P
⊢ μ.prod ν = (map X P).prod (map Y P)

Tactic:
hX.map_eq,

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
X : Ω → 𝓧
μ : Measure 𝓧
P : Measure Ω
inst✝ : IsFiniteMeasure P
𝓨 : Type u_3
m𝓨 : MeasurableSpace 𝓨
ν : Measure 𝓨
Y : Ω → 𝓨
hX : HasLaw X μ P
hY : HasLaw Y ν P
h : HasLaw (fun ω ↦ (X ω, Y ω)) (μ.prod ν) P
⊢ μ.prod ν = μ.prod (map Y P)
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
X : Ω → ℝ
Y : Ω' → ℝ
hfμ : MemLp X 2 μ
hgν : MemLp Y 2 ν
⊢ Var[fun x ↦ X x.1; μ.prod ν] + Var[fun x ↦ Y x.2; μ.prod ν] = Var[X; μ] + Var[Y; ν]

Tactic:
rw [measurePreserving_fst.variance_fun_comp hfμ.aemeasurable,
      measurePreserving_snd.variance_fun_comp hgν.aemeasurable]

Goal state after:
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✝² : TopologicalSpace γ
inst✝¹ : PseudoMetrizableSpace γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
x : α
⊢ f x ∈ t → f x ∈ closure[inst✝²] t

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝² : TopologicalSpace γ
inst✝¹ : PseudoMetrizableSpace γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : AEStronglyMeasurable f μ
t : Set γ
t_sep : IsSeparable t
ht : ∀ᵐ (x : α) ∂μ, f x ∈ t
x : α
hx : f x ∈ t
⊢ f x ∈ closure[inst✝²] t
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 : α
⊢ f x ∈ t → id (f x) ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
hx

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 : α
hx : f x ∈ t
⊢ id (f x) ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case pos
Ω : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : Ω → 𝕜
Y : Ω → E
hXY : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
hE : CompleteSpace E
⊢ ∫ (x : Ω), (X • Y) x ∂μ = (∫ (x : Ω), X x ∂μ) • ∫ (x : Ω), Y x ∂μ

Tactic:
exact hXY.integral_bilin' hX hY (.lsmul ℝ 𝕜) 1 (by simp) (by simp [norm_smul])

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

Goal state before:
pp: case e'_5
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω : ι → Type u_5
m : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst✝⁶ : ∀ (i : ι), IsProbabilityMeasure (μ i)
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
mE : MeasurableSpace E
X : (i : ι) → Ω i → E
Z : Ω' → E
l : Filter ι
inst✝⁴ : TopologicalSpace E
F : Type u_6
inst✝³ : OpensMeasurableSpace E
inst✝² : TopologicalSpace F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
g : E → F
hg : Continuous[inst✝⁴, inst✝²] g
h : TendstoInDistribution X l Z μ μ'
⊢ ⟨Measure.map (g ∘ Z) μ', ⋯⟩ = ProbabilityMeasure.map ⟨Measure.map Z μ', ⋯⟩ ⋯

Tactic:
simp only [ProbabilityMeasure.map, ProbabilityMeasure.coe_mk]
      congr
      rw [AEMeasurable.map_map_of_aemeasurable hg.aemeasurable h.aemeasurable_limit]

Goal state after:
Module: Mathlib.Probability.IdentDistrib

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
⊢ eVar[g; ν] = ∫⁻ (x : β), ↑‖g x - ∫ (x : α), f x ∂μ‖₊ ^ 2 ∂ν

Tactic:
h.integral_eq

Goal state after:
case e'_3
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
⊢ eVar[g; ν] = ∫⁻ (x : β), ↑‖g x - ∫ (x : β), g x ∂ν‖₊ ^ 2 ∂ν
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: case pos
Ω : 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_eq_of_neBot_nhdsGT]
    exact le_iInf₂ fun _ he => 𝓕.mono he.le

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

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst✝ : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g ω))
⊢ liminf (fun n ↦ eLpNorm (f n) p μ) atTop ≤ ↑R

Tactic:
liminf_eq,

Goal state after:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
R : ℝ≥0
p : ℝ≥0∞
F : Type u_5
inst✝ : NormedAddCommGroup F
ℱ : Filtration ℕ m
f : ℕ → Ω → F
hfm : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g ω))
⊢ sSup {a | ∀ᶠ (n : ℕ) in atTop, a ≤ eLpNorm (f n) p μ} ≤ ↑R
Module: Mathlib.MeasureTheory.Function.Piecewise

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
μ : Measure α
inst✝¹ : MeasurableSpace β
inst✝ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
p : ι → α → β
hp : ∀ (i : ι), Measurable (p i)
hq : ∀ (i : ι), f i =ᵐ[μ] p i
x : α
⊢ (∀ (i : ι), f i x = p i x) → hs.piecewise f x = hs.piecewise p x

Tactic:
hx

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
μ : Measure α
inst✝¹ : MeasurableSpace β
inst✝ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
p : ι → α → β
hp : ∀ (i : ι), Measurable (p i)
hq : ∀ (i : ι), f i =ᵐ[μ] p i
x : α
hx : ∀ (i : ι), f i x = p i x
⊢ hs.piecewise f x = hs.piecewise p x
Module: Mathlib.MeasureTheory.Function.Piecewise

Goal state before:
pp: case neg
ι : 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 ι
⊢ StronglyMeasurable (hs.piecewise f)

Tactic:
obtain ⟨e, -⟩ := exists_true_iff_nonempty.mpr (nonempty_equiv_of_countable (α := ℕ) (β := ι))

Goal state after:
case neg
ι : 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 : ℕ ≃ ι
⊢ StronglyMeasurable (hs.piecewise f)
Module: Mathlib.MeasureTheory.Function.Piecewise

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
μ : Measure α
inst✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
p : ι → α → β
hp : ∀ (i : ι), StronglyMeasurable (p i)
hq : ∀ (i : ι), f i =ᵐ[μ] p i
x : α
⊢ (∀ (i : ι), f i x = p i x) → hs.piecewise f x = hs.piecewise p x

Tactic:
hx

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
s : ι → Set α
f : ι → α → β
μ : Measure α
inst✝¹ : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst✝ : TopologicalSpace β
p : ι → α → β
hp : ∀ (i : ι), StronglyMeasurable (p i)
hq : ∀ (i : ι), f i =ᵐ[μ] p i
x : α
hx : ∀ (i : ι), f i x = p i x
⊢ hs.piecewise f x = hs.piecewise p x
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hε_top : ε = ∞
⊢ ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ε

Tactic:
subst hε_top

Goal state after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hε : ∞ ≠ 0
⊢ ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), eLpNorm (s.indicator (f i)) p μ ≤ ∞
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 μ ≤ ↑ε
n : ι
x : α
⊢ f n x = g n x → sᶜ.indicator (g n) x = sᶜ.indicator (f n) x

Tactic:
hx

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 : ι
x : α
hx : f n x = g n x
⊢ sᶜ.indicator (g n) x = sᶜ.indicator (f n) x
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : TopologicalSpace α
δ : Type u_5
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : Zero δ
f : γ →C_c δ
g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : β
⊢ x ∈ tsupport (⇑f ∘ ⇑g) → x ∈ ⇑g ⁻¹' tsupport f.toFun

Tactic:
hx

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : TopologicalSpace α
δ : Type u_5
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : Zero δ
f : γ →C_c δ
g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : β
hx : x ∈ tsupport (⇑f ∘ ⇑g)
⊢ x ∈ ⇑g ⁻¹' tsupport f.toFun
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
x : α
⊢ x ∈ Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun →
    x ∈ Function.support f₁.toFun ∪ Function.support f₂.toFun

Tactic:
hx

Goal state after:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
x : α
hx : x ∈ Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun
⊢ x ∈ Function.support f₁.toFun ∪ Function.support f₂.toFun
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
a b : E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
ω : E → E →L[𝕜] F
γ : Path a b
x : ℝ
⊢ x ∈ Ioo 0 1 → (ω (γ.extend x)) (derivWithin ⇑γ.extend I x) = (ω (γ.extend x)) (deriv (⇑γ.extend) x)

Tactic:
hx

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
a b : E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
ω : E → E →L[𝕜] F
γ : Path a b
x : ℝ
hx : x ∈ Ioo 0 1
⊢ (ω (γ.extend x)) (derivWithin ⇑γ.extend I x) = (ω (γ.extend x)) (deriv (⇑γ.extend) x)
Module: Mathlib.MeasureTheory.Integral.MeanValue

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
x : α
⊢ 0 ≤ g x → (fun x ↦ (ρ x).toReal) x = g x

Tactic:
hx

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
x : α
hx : 0 ≤ g x
⊢ (fun x ↦ (ρ x).toReal) x = g x