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

Goal state before:
pp: case refine_1
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst✝ : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i ↦ ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))
f : Ω →ᵇ 𝕜
⊢ Tendsto (fun i ↦ ∫ (ω : Ω), f ω ∂↑(μs i)) F
    (𝓝 (↑(∫ (x : Ω), RCLike.re (f x) ∂↑μ) + ↑(∫ (x : Ω), RCLike.im (f x) ∂↑μ) * RCLike.I))

Tactic:
simp_rw [← integral_re_add_im (integrable (μs _) f)]

Goal state after:
case refine_1
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst✝ : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i ↦ ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))
f : Ω →ᵇ 𝕜
⊢ Tendsto (fun i ↦ ↑(∫ (x : Ω), RCLike.re (f x) ∂↑(μs i)) + ↑(∫ (x : Ω), RCLike.im (f x) ∂↑(μs i)) * RCLike.I) F
    (𝓝 (↑(∫ (x : Ω), RCLike.re (f x) ∂↑μ) + ↑(∫ (x : Ω), RCLike.im (f x) ∂↑μ) * RCLike.I))
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∉ {x | C ≤ ‖f i x‖₊}
⊢ 0 = {x | C ≤ ‖g i x‖₊}.indicator (g i) x

Tactic:
Set.indicator_of_notMem

Goal state after:
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∉ {x | C ≤ ‖f i x‖₊}
⊢ 0 = 0

case neg.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose ⋯ x
hfx : x ∉ {x | C ≤ ‖f i x‖₊}
⊢ x ∉ {x | C ≤ ‖g i x‖₊}
Module: Mathlib.Probability.Independence.Kernel.Indep

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

Tactic:
by simp [← ha]

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
x : ι
hx : x ∈ {i, j}
⊢ (if x = i then t₁ else t₂) ∈ s x

Tactic:
rcases Finset.mem_insert.mp hx with hx | hx

Goal state after:
case inl
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
x : ι
hx✝ : x ∈ {i, j}
hx : x = i
⊢ (if x = i then t₁ else t₂) ∈ s x

case inr
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
x : ι
hx✝ : x ∈ {i, j}
hx : x ∈ {j}
⊢ (if x = i then t₁ else t₂) ∈ s x
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case refine_2
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
γ : Type u_6
γ' : Type u_7
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
mγ : MeasurableSpace γ
mγ' : MeasurableSpace γ'
φ : β → γ
ψ : β' → γ'
hfg : IndepFun f g κ μ
hf : AEMeasurable f (⇑κ ∘ₘ μ)
hg : AEMeasurable g (⇑κ ∘ₘ μ)
hφ : AEMeasurable φ (Measure.map f (⇑κ ∘ₘ μ))
hψ : AEMeasurable ψ (Measure.map g (⇑κ ∘ₘ μ))
h : IndepFun (AEMeasurable.mk φ hφ ∘ f) (AEMeasurable.mk ψ hψ ∘ g) κ μ
hφ_ae : ∀ᵐ (x : Ω) ∂⇑κ ∘ₘ μ, φ (f x) = AEMeasurable.mk φ hφ (f x)
hψ_ae : ∀ᵐ (x : Ω) ∂⇑κ ∘ₘ μ, ψ (g x) = AEMeasurable.mk ψ hψ (g x)
⊢ ∀ᵐ (a : α) ∂μ, AEMeasurable.mk ψ hψ ∘ g =ᵐ[κ a] ψ ∘ g

Tactic:
filter_upwards [Measure.ae_ae_of_ae_comp (hψ_ae)] with a haψ
    filter_upwards [haψ] with ω hωψ
    simp [hωψ]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h : ∀ (F : Set Ω), IsClosed[inst✝²] F → limsup (fun i ↦ (μs i) F) L ≤ μ F
⊢ Tendsto μs L (𝓝 μ)

Tactic:
apply Filter.tendsto_of_seq_tendsto fun u hu ↦ ?_
  apply tendsto_of_forall_isClosed_limsup_le_nat fun F hF ↦ le_trans ?_ (h F hF)
  exact (limsup_comp (fun i ↦ μs i F) u _).trans_le
    (limsup_le_limsup_of_le hu (by isBoundedDefault) ⟨1, by simp⟩)

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 α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : ↑p1 ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : ↑p2 ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
let g i := ite (i ∈ p1) (f1 i) Set.univ ∩ ite (i ∈ p2) (f2 i) Set.univ

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : ↑p1 ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : ↑p2 ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set Ω := fun i ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X Y : Ω → E
hXY : X =ᵐ[ℙ] Y
⊢ pdf X ℙ μ = pdf Y ℙ μ

Tactic:
by
  rw [pdf_def, pdf_def, map_congr hXY]

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝² : SFinite μ
inst✝¹ : HasPDF X ℙ μ
inst✝ : HasPDF Y ℙ μ
σX : SigmaFinite (map X ℙ)
σY : SigmaFinite (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this✝ : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ HasPDF (X * Y) ℙ μ

Tactic:
rw [hasPDF_iff_of_aemeasurable (by fun_prop),
    hXY.map_mul_eq_map_mconv_map₀' (by fun_prop) (by fun_prop) σX σY]

Goal state after:
Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝² : SFinite μ
inst✝¹ : HasPDF X ℙ μ
inst✝ : HasPDF Y ℙ μ
σX : SigmaFinite (map X ℙ)
σY : SigmaFinite (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
this✝ : AEMeasurable X ℙ
this : AEMeasurable Y ℙ
⊢ (map X ℙ ∗ₘ map Y ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ∗ₘ map Y ℙ ≪ μ
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
⊢ t1 ∩ t2 = ⋂ n ∈ insert a s, f n

Tactic:
rw [h_t1, h_t2, Finset.set_biInter_insert, Set.inter_comm]

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : ((∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ) ^ 2⁻¹) ^ 2 < ∞
⊢ eVar[X; μ] < ∞

Tactic:
← ENNReal.rpow_mul,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : (∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ) ^ (2⁻¹ * 2) < ∞
⊢ eVar[X; μ] < ∞
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
⊢ (∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ) ^ (1 / 2) < ∞

Tactic:
exact ENNReal.rpow_lt_top_of_nonneg (by linarith) h.ne

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
⊢ Var[X; μ] = ∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ

Tactic:
simp [variance, evariance, toReal_enorm, ← integral_toReal ((hX.sub_const _).enorm.pow_const _) <|
    .of_forall fun _ ↦ ENNReal.pow_lt_top enorm_lt_top]

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

Goal state before:
pp: case add
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_measMg_f' : Measurable f'
a✝ : Measurable g
h_ind_f' : ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ
h_ind_g' : ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
h_measM_f' : Measurable f'
⊢ ∫⁻ (ω : Ω), f ω * (f' + g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), (f' + g) ω ∂μ

Tactic:
simp_rw [Pi.add_apply, left_distrib]

Goal state after:
case add
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' g : Ω → ℝ≥0∞
a✝¹ : Disjoint (Function.support f') (Function.support g)
h_measMg_f' : Measurable f'
a✝ : Measurable g
h_ind_f' : ∫⁻ (ω : Ω), f ω * f' ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω ∂μ
h_ind_g' : ∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
h_measM_f' : Measurable f'
⊢ ∫⁻ (ω : Ω), f ω * f' ω + f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' ω + g ω ∂μ
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst✝ : IsFiniteMeasure μ
ι' : Type u_3
Y : ι' → Ω → ℝ
t : Finset ι'
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : ∀ i ∈ t, MemLp (Y i) 2 μ
⊢ cov[∑ i ∈ s, X i, ∑ j ∈ t, Y j; μ] = ∑ i ∈ s, ∑ j ∈ t, cov[X i, Y j; μ]

Tactic:
by
  rw [covariance_sum_left' hX]
  · exact Finset.sum_congr rfl fun i hi ↦ by rw [covariance_sum_right' hY (hX i hi)]
  · exact memLp_finsetSum' t hY

Goal state after:
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case e'_4.e_a
Ω : 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; μ] = ((∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ) ^ 2⁻¹) ^ 2

Tactic:
← ENNReal.rpow_mul,

Goal state after:
case e'_4.e_a
Ω : 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; μ] = (∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ 2 ∂μ) ^ (2⁻¹ * 2)
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : 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 μ
⊢ cov[f ∘ X, g ∘ X; P] = cov[f, g; μ]

Tactic:
rw [← hX.map_eq, covariance_map]

Goal state after:
case hX
Ω : 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 μ
⊢ AEStronglyMeasurable f (map X P)

case hY
Ω : 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 μ
⊢ AEStronglyMeasurable g (map X P)

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
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : 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 p ↦ X p.1 + Y p.2; μ.prod ν] = Var[X; μ] + Var[Y; ν]

Tactic:
by
  refine (IndepFun.variance_fun_add (hfμ.comp_fst ν) (hgν.comp_snd μ) ?_).trans ?_
  · exact indepFun_prod₀ hfμ.aemeasurable hgν.aemeasurable
  · 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: case pos
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
⊢ eLpNorm ({x | ⟨C, ⋯⟩ ≤ ‖f i x‖₊}.indicator (f i)) p μ = eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ

Tactic:
have : {x | (⟨C, hC₁.le⟩ : ℝ≥0) ≤ ‖f i x‖₊} = {x | C ≤ ‖f i x‖} := by
    ext x
    simp_rw [← norm_toNNReal]
    exact Real.le_toNNReal_iff_coe_le (norm_nonneg _)

Goal state after:
case pos
α : Type u_1
inst✝⁴ : MeasurableSpace α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
ι : Type u_6
f : ι → α → E
j : ι
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
hℒp : MemLp (f j) p μ
hfmeas : ∀ (i : ι), StronglyMeasurable (f i)
hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
C : ℝ
hC₁ : 0 < C
hC₂ : eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ ≤ ENNReal.ofReal ε
i : ι
this : {x | ⟨C, ⋯⟩ ≤ ‖f i x‖₊} = {x | C ≤ ‖f i x‖}
⊢ eLpNorm ({x | ⟨C, ⋯⟩ ≤ ‖f i x‖₊}.indicator (f i)) p μ = eLpNorm ({x | C ≤ ↑‖f j x‖₊}.indicator (f j)) p μ
Module: Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : BorelSpace X
inst✝⁸ : R1Space X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
inst✝⁴ : R1Space Y
μ : Measure X
ν : Measure Y
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure ν
E : Type u_3
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
hp₀ : p ≠ 0
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun gf ↦
    (compMeasurePreserving ⇑↑gf.2 ⋯) gf.1

Tactic:
refine continuous_prod_of_dense_continuous_lipschitzWith _ 1
    (MeasureTheory.Lp.simpleFunc.dense hp) ?_ fun f ↦ (isometry_compMeasurePreserving f.2).lipschitz

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : BorelSpace X
inst✝⁸ : R1Space X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
inst✝⁴ : R1Space Y
μ : Measure X
ν : Measure Y
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure ν
E : Type u_3
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
hp₀ : p ≠ 0
⊢ ∀ a ∈ ↑(simpleFunc E p ν),
    Continuous[_, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] fun y ↦
      (compMeasurePreserving ⇑↑(a, y).2 ⋯) (a, y).1
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedAddCommGroup β
x✝ : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
⊢ UnifTight f p μ ↔ ∀ ⦃ε : ℝ≥0∞⦄, 0 < ε → ∃ s, μ s ≠ ∞ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ε

Tactic:
simp only [ENNReal.forall_ennreal, ENNReal.coe_pos]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedAddCommGroup β
x✝ : MeasurableSpace α
f : ι → α → β
p : ℝ≥0∞
μ : Measure α
⊢ UnifTight f p μ ↔
    (∀ (r : ℝ≥0), 0 < r → ∃ s, μ s ≠ ∞ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑r) ∧
      (0 < ∞ → ∃ s, μ s ≠ ∞ ∧ ∀ (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 : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
⊢ ∀ ⦃ε : ℝ≥0⦄, 0 < ε → ∃ s, μ s ≠ ∞ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (-f i)) p μ ≤ ↑ε

Tactic:
Set.indicator_neg',

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
⊢ ∀ ⦃ε : ℝ≥0⦄, 0 < ε → ∃ s, μ s ≠ ∞ ∧ ∀ (i : ι), eLpNorm (-sᶜ.indicator (f i)) p μ ≤ ↑ε
Module: Mathlib.MeasureTheory.Integral.CircleTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous (circleTransform R z w f)

Tactic:
apply_rules [Continuous.smul, continuous_const]
  · rw [funext <| deriv_circleMap _ _]
    fun_prop
  · exact continuous_circleMap_inv hw
  · apply ContinuousOn.comp_continuous hf (continuous_circleMap z R)
    exact fun _ => (circleMap_mem_sphere _ hR.le) _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᵐ[μ] AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable (fun n ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
hut' : UnifTight (fun n ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)
hgg' : g =ᵐ[μ] AEStronglyMeasurable.mk g ⋯
hg'' : MemLp (AEStronglyMeasurable.mk g ⋯) p μ
⊢ Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
have haefg' := ae_tendsto_ae_congr hff' hgg' hfg

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᵐ[μ] AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable (fun n ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
hut' : UnifTight (fun n ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)
hgg' : g =ᵐ[μ] AEStronglyMeasurable.mk g ⋯
hg'' : MemLp (AEStronglyMeasurable.mk g ⋯) p μ
haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g ⋯ x))
⊢ Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E},
    ContinuousOn f (Icc a b) →
      DifferentiableOn ℝ f (Ioo a b) →
        (∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) → CompleteSpace E → ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
hE : ¬CompleteSpace E
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t

Tactic:
set g : ℝ → UniformSpace.Completion E := (↑) ∘ f with hg

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
B : ℝ → ℝ
hab : a ≤ b
hfc : ContinuousOn f (Icc a b)
hfd : DifferentiableOn ℝ f (Ioo a b)
hfB : ∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t
hBi : IntervalIntegrable B volume a b
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E},
    ContinuousOn f (Icc a b) →
      DifferentiableOn ℝ f (Ioo a b) →
        (∀ᵐ (t : ℝ), t ∈ Ioo a b → ‖deriv f t‖ ≤ B t) → CompleteSpace E → ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
hE : ¬CompleteSpace E
g : ℝ → UniformSpace.Completion E := UniformSpace.Completion.coe' ∘ f
hg : g = UniformSpace.Completion.coe' ∘ f
⊢ ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t
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 < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
⊢ ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν

Tactic:
calc
      _ = ∫ x in s, (ρ x).toReal * f x ∂μ := by
        apply MeasureTheory.integral_congr_ae
        apply h_toReal_ae.mono
        intro x hx
        simp [hx, mul_comm]
      _ = _ := by
        have h := setIntegral_withDensity_eq_setIntegral_toReal_smul₀ hρ_ae hρ_top f hs_meas
        simp [ν, h]

Goal state after: