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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
I : Finset (Set α)
hs : s ∈ C
hI : ↑I ⊆ C
t : Set α
ht : t ∈ ↑(hC.disjointOfDiffUnion hs hI)
⊢ t ⊆ s

Tactic:
by
  apply le_trans <| hC.subset_of_diffUnion_disjointOfDiffUnion hs hI t ht
  exact sdiff_le (a := s) (b := ⋃₀ I)

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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
| m s

Tactic:
← hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss

Goal state after:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
| m (⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI))
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' m : AddContent G C
hC : IsSetSemiring C
⊢ m.supClosureFun ∅ = 0

Tactic:
m.supClosureFun_apply_of_mem hC hC.empty_mem,

Goal state after:
α : Type u_1
C : Set (Set α)
s t : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m✝ m' m : AddContent G C
hC : IsSetSemiring C
⊢ m ∅ = 0
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst✝ : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    (fun ω ↦ (B (s.indicator (Function.const Ω c) ω)) (f ω)) = s.indicator fun ω ↦ (B c) (f ω)
c : F
s : Set Ω
hs : MeasurableSet s
ω : Ω
hω : (B c) (μ[g | m] ω) = μ[⇑(B c) ∘ g | m] ω
⊢ s.indicator μ[fun a ↦ (B c) (g a) | m] ω = s.indicator (fun ω ↦ (B c) (μ[g | m] ω)) ω

Tactic:
simp only [Set.indicator, hω, Function.comp_def]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      blimsup (fun i ↦ cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ cthickening (r i) (s i)) atTop p
r' : ℕ → ℝ := fun i ↦ if 0 < r i then r i else 1 / (↑i + 1)
i : ℕ
hi : 0 < r i
⊢ r' i ∈ Ioi 0

pp: case neg
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      blimsup (fun i ↦ cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ cthickening (r i) (s i)) atTop p
r' : ℕ → ℝ := fun i ↦ if 0 < r i then r i else 1 / (↑i + 1)
i : ℕ
hi : ¬0 < r i
⊢ r' i ∈ Ioi 0

Tactic:
· simp [r', hi]

Goal state after:
case neg
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      blimsup (fun i ↦ cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ cthickening (r i) (s i)) atTop p
r' : ℕ → ℝ := fun i ↦ if 0 < r i then r i else 1 / (↑i + 1)
i : ℕ
hi : ¬0 < r i
⊢ r' i ∈ Ioi 0
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
⊢ μ.toSignedMeasure i = ν.toSignedMeasure i

Tactic:
rw [h]

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ MeasurableSet (s.someExistsOneDivLT (i \ ∅))

Tactic:
exact someExistsOneDivLT_measurableSet

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ MeasurableSet
    (s.someExistsOneDivLT
      (i \
        ⋃ k,
          ⋃ (H : k ≤ n✝),
            have this := ⋯;
            s.restrictNonposSeq i k))

Tactic:
exact someExistsOneDivLT_measurableSet

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

Goal state before:
pp: case e'_4
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h✝ : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l)
h₁ : ∀ l < k, 0 ≤ s (s.restrictNonposSeq i l)
l : ℕ
h : l < k
x : α
⊢ (∃ (_ : l < k), x ∈ s.restrictNonposSeq i l) ↔ x ∈ s.restrictNonposSeq i l

Tactic:
exists_prop,

Goal state after:
case e'_4
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : s i < 0
h✝ : ¬s ≤[i] 0
hn : ∃ n, s ≤[i \ ⋃ l, ⋃ (_ : l < n), s.restrictNonposSeq i l] 0
k : ℕ := Nat.find hn
hk₂ : s ≤[i \ ⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l] 0
hmeas : MeasurableSet (⋃ l, ⋃ (_ : l < k), s.restrictNonposSeq i l)
h₁ : ∀ l < k, 0 ≤ s (s.restrictNonposSeq i l)
l : ℕ
h : l < k
x : α
⊢ l < k ∧ x ∈ s.restrictNonposSeq i l ↔ x ∈ s.restrictNonposSeq i l
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s✝ s : SignedMeasure α
i : Set α := ⋯.choose
hi : MeasurableSet ⋯.choose ∧ 0 ≤[⋯.choose] s ∧ s ≤[⋯.chooseᶜ] 0
⊢ s.toMeasureOfZeroLE i ⋯ ⋯ ⟂ₘ s.toMeasureOfLEZero iᶜ ⋯ ⋯

Tactic:
by
      refine ⟨iᶜ, hi.1.compl, ?_, ?_⟩
      · rw [toMeasureOfZeroLE_apply _ _ hi.1 hi.1.compl]; simp
      · rw [toMeasureOfLEZero_apply _ _ hi.1.compl hi.1.compl.compl]; simp

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

Goal state before:
pp: case negPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₂.posPart.toSignedMeasure - j₁.negPart.toSignedMeasure = j₂.posPart.toSignedMeasure - j₂.negPart.toSignedMeasure
⊢ j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure

Tactic:
sub_right_inj

Goal state after:
case negPart
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure
⊢ j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: case e_a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ t.toJordanDecomposition.negPart = s.toJordanDecomposition.negPart.singularPart μ

Tactic:
have hfneg : Measurable fun x => ENNReal.ofReal (-f x) := by fun_prop

Goal state after:
case e_a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
hfneg : Measurable fun x ↦ ENNReal.ofReal (-f x)
⊢ t.toJordanDecomposition.negPart = s.toJordanDecomposition.negPart.singularPart μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ (-s).singularPart μ = -s.singularPart μ

Tactic:
simp [singularPart, toJordanDecomposition_neg]

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

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : g =ᵐ[μ] 0
n : ι
⊢ {x | 0 ≤ ‖μ[g | ℱ n] x‖₊}.indicator μ[g | ℱ n] =ᵐ[μ] 0

Tactic:
filter_upwards [condExp_congr_ae (m := ℱ n) hne] with x hx

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : g =ᵐ[μ] 0
n : ι
x : α
hx : μ[g | ℱ n] x = μ[0 | ℱ n] x
⊢ {x | 0 ≤ ‖μ[g | ℱ n] x‖₊}.indicator μ[g | ℱ n] x = 0 x
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
c : ℝ≥0
ν : FiniteMeasure Ω
⊢ (c • ν).map f = c • ν.map f

Tactic:
by
  ext s _
  simp [toMeasure_smul]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set Ω
⊢ (∀ (S : Finset ι),
      ∀ᵐ (a : Unit) ∂Measure.dirac (),
        ((Kernel.const Unit μ) a) (⋂ i ∈ S, s i) = ∏ i ∈ S, ((Kernel.const Unit μ) a) (s i)) ↔
    ∀ (t : Finset ι), μ (⋂ i ∈ t, s i) = ∏ i ∈ t, μ (s i)

Tactic:
ae_dirac_eq,

Goal state after:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set Ω
⊢ (∀ (S : Finset ι),
      ∀ᶠ (a : Unit) in pure (), ((Kernel.const Unit μ) a) (⋂ i ∈ S, s i) = ∏ i ∈ S, ((Kernel.const Unit μ) a) (s i)) ↔
    ∀ (t : Finset ι), μ (⋂ i ∈ t, s i) = ∏ i ∈ t, μ (s i)
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : ι → Set Ω
hf : ∀ (i : ι), MeasurableSet (f i)
⊢ (∀ (s : Finset ι),
      ∀ᵐ (a : Unit) ∂Measure.dirac (),
        ((Kernel.const Unit μ) a) (⋂ i ∈ s, f i) = ∏ i ∈ s, ((Kernel.const Unit μ) a) (f i)) ↔
    ∀ (s : Finset ι), μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)

Tactic:
ae_dirac_eq,

Goal state after:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : ι → Set Ω
hf : ∀ (i : ι), MeasurableSet (f i)
⊢ (∀ (s : Finset ι),
      ∀ᶠ (a : Unit) in pure (), ((Kernel.const Unit μ) a) (⋂ i ∈ s, f i) = ∏ i ∈ s, ((Kernel.const Unit μ) a) (f i)) ↔
    ∀ (s : Finset ι), μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case refine_2.h
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun ω ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun ω ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable.mk Y mY =ᵐ[Measure.map Prod.snd (μ.prod ν)] Y

Tactic:
rw [measurePreserving_snd.map_eq]

Goal state after:
case refine_2.h
Ω : Type u_10
Ω' : Type u_11
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure ν
𝓧 : Type u_12
𝓨 : Type u_13
inst✝¹ : MeasurableSpace 𝓧
inst✝ : MeasurableSpace 𝓨
X : Ω → 𝓧
Y : Ω' → 𝓨
mX : AEMeasurable X μ
mY : AEMeasurable Y ν
this : (fun ω ↦ AEMeasurable.mk X mX ω.1) ⟂ᵢ[μ.prod ν] fun ω ↦ AEMeasurable.mk Y mY ω.2
⊢ AEMeasurable.mk Y mY =ᵐ[ν] Y
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h : ∀ (s : Finset ι), iIndepFun (s.restrict f) μ
⊢ iIndepFun f μ

Tactic:
by
    rw [iIndepFun_iff]
    intro s f hs
    have : ⋂ i ∈ s, f i = ⋂ i : s, f i := by ext; simp
    rw [← Finset.prod_coe_sort, this]
    exact (h s).meas_iInter fun i ↦ hs i i.2

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₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
ε : ℝ≥0
hε : 0 < ε
x✝ : ↑(μ F) < ∞
K : Set Ω
h₂ : limsup (fun x ↦ (μs x) (F ∩ K)) L ≤ μ (F ∩ K)
hKc : IsCompact K
hK_le : ∀ μ ∈ range (ProbabilityMeasure.toMeasure ∘ μs), μ Kᶜ ≤ ↑ε
⊢ limsup (fun i ↦ ↑((μs i) (F ∩ K))) L ≤ ↑(μ F)

Tactic:
rw [← ENNReal.coe_le_coe, ENNReal.ofNNReal_limsup <|
      isBoundedUnder_of_eventually_le (a := 1) (by simp)] at h₂

Goal state after:
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
ε : ℝ≥0
hε : 0 < ε
x✝ : ↑(μ F) < ∞
K : Set Ω
h₂ : limsup (fun i ↦ ↑((μs i) (F ∩ K))) L ≤ ↑(μ (F ∩ K))
hKc : IsCompact K
hK_le : ∀ μ ∈ range (ProbabilityMeasure.toMeasure ∘ μs), μ Kᶜ ≤ ↑ε
⊢ limsup (fun i ↦ ↑((μs i) (F ∩ K))) L ≤ ↑(μ F)
Module: Mathlib.Probability.Density

Goal state before:
pp: case refine_1
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ (map X ℙ).HaveLebesgueDecomposition μ

Tactic:
rw [h]

Goal state after:
case refine_1
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ (μ.withDensity f).HaveLebesgueDecomposition μ
Module: Mathlib.Probability.Density

Goal state before:
pp: case refine_2
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ map X ℙ ≪ μ

Tactic:
rw [h]

Goal state after:
case refine_2
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ μ.withDensity f ≪ μ
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case mpr.inr.refine_2
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
F : Filter γ
inst✝ : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ C, ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ L, LipschitzWith L f) → Tendsto (fun i ↦ ∫ (ω : Ω), f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), f ω ∂↑μ))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun n ω ↦ ↑((thickenedIndicator ⋯ s) ω)
key₁ : Tendsto (fun n ↦ ∫ (ω : Ω), fs n ω ∂↑μ) atTop (𝓝 ((↑μ).real s))
room₁ : (↑μ).real s < (↑μ).real s + ε / 2
M : ℕ
hM : ∀ (b : ℕ), M ≤ b → ∫ (ω : Ω), fs b ω ∂↑μ < (↑μ).real s + ε / 2
key₂ : Tendsto (fun i ↦ ∫ (ω : Ω), fs M ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), fs M ω ∂↑μ))
room₂ : ∫ (a : Ω), fs M a ∂↑μ < ∫ (a : Ω), fs M a ∂↑μ + ε / 2
⊢ limsup (fun i ↦ (↑(μs i)).real s) F ≤ (↑μ).real s + ε

Tactic:
have ev_near : ∀ᶠ x in F, (μs x : Measure Ω).real s ≤ ∫ a, fs M a ∂μ + ε / 2 := by
    refine (key₂.eventually_le_const room₂).mono fun x hx ↦ le_trans ?_ hx
    rw [← integral_indicator_one hs.measurableSet]
    refine integral_mono ?_ (integrable_thickenedIndicator _ _) ?_
    · exact (integrable_indicator_iff hs.measurableSet).mpr (integrable_const _).integrableOn
    · have h : _ ≤ fs M :=
        indicator_le_thickenedIndicator (δ := (1 : ℝ) / (M + 1)) (by positivity) s
      simpa using! h

Goal state after:
case mpr.inr.refine_2
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
F : Filter γ
inst✝ : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ C, ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ L, LipschitzWith L f) → Tendsto (fun i ↦ ∫ (ω : Ω), f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), f ω ∂↑μ))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun n ω ↦ ↑((thickenedIndicator ⋯ s) ω)
key₁ : Tendsto (fun n ↦ ∫ (ω : Ω), fs n ω ∂↑μ) atTop (𝓝 ((↑μ).real s))
room₁ : (↑μ).real s < (↑μ).real s + ε / 2
M : ℕ
hM : ∀ (b : ℕ), M ≤ b → ∫ (ω : Ω), fs b ω ∂↑μ < (↑μ).real s + ε / 2
key₂ : Tendsto (fun i ↦ ∫ (ω : Ω), fs M ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), fs M ω ∂↑μ))
room₂ : ∫ (a : Ω), fs M a ∂↑μ < ∫ (a : Ω), fs M a ∂↑μ + ε / 2
ev_near : ∀ᶠ (x : γ) in F, (↑(μs x)).real s ≤ ∫ (a : Ω), fs M a ∂↑μ + ε / 2
⊢ limsup (fun i ↦ (↑(μs i)).real s) F ≤ (↑μ).real s + ε
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 ν)
this✝ : HasPDF X ℙ μ
this : HasPDF Y ℙ ν
s : Set E
t : Set F
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((μ.prod ν).withDensity fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2) (s ×ˢ t) = (map X ℙ) s * (map Y ℙ) t

Tactic:
withDensity_apply _ (hs.prod ht),

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 ℙ μ
this : HasPDF Y ℙ ν
s : Set E
t : Set F
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (a : E × F) in s ×ˢ t, pdf X ℙ μ a.1 * pdf Y ℙ ν a.2 ∂μ.prod ν = (map X ℙ) s * (map Y ℙ) t
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_t1_inter_t2 : t1 ∩ t2 = ⋂ n ∈ insert a s, f n
⊢ ∀ᵐ (a' : α) ∂μ, (κ a') (t1 ∩ t2) = ∏ n ∈ insert a s, (κ a') (f n)

Tactic:
filter_upwards [hp_ind (insert a s) h_f_mem] with a' ha'

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_t1_inter_t2 : t1 ∩ t2 = ⋂ n ∈ insert a s, f n
a' : α
ha' : (κ a') (⋂ i ∈ insert a s, f i) = ∏ i ∈ insert a s, (κ a') (f i)
⊢ (κ a') (t1 ∩ t2) = ∏ n ∈ insert a s, (κ a') (f n)
Module: Mathlib.Probability.Moments.Variance

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

Tactic:
have := ENNReal.pow_lt_top (hX.sub <| memLp_const <| μ[X]).2 (n := 2)
  rw [eLpNorm_eq_lintegral_rpow_enorm_toReal two_ne_zero ENNReal.ofNat_ne_top, ← ENNReal.rpow_two]
    at this
  simp only [ENNReal.toReal_ofNat, Pi.sub_apply, one_div] at this
  rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (two_ne_zero : (2 : ℝ) ≠ 0), ENNReal.rpow_one] at this
  simp_rw [ENNReal.rpow_two] at this
  exact this

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
⊢ Var[fun ω ↦ X ω - c; μ] = Var[X; μ]

Tactic:
simp_rw [sub_eq_add_neg, variance_add_const hX (-c)]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
hX : AEMeasurable X (Measure.map Y μ)
hY : AEMeasurable Y μ
⊢ Var[X; Measure.map Y μ] = Var[X ∘ Y; μ]

Tactic:
rw [variance_eq_integral hX, integral_map hY, variance_eq_integral (hX.comp_aemeasurable hY),
    integral_map hY]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
hX : AEMeasurable X (Measure.map Y μ)
hY : AEMeasurable Y μ
⊢ ∫ (x : Ω'), (X (Y x) - ∫ (x : Ω'), X (Y x) ∂μ) ^ 2 ∂μ = ∫ (ω : Ω'), ((X ∘ Y) ω - ∫ (x : Ω'), (X ∘ Y) x ∂μ) ^ 2 ∂μ

Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
hX : AEMeasurable X (Measure.map Y μ)
hY : AEMeasurable Y μ
⊢ AEStronglyMeasurable X (Measure.map Y μ)

Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
hX : AEMeasurable X (Measure.map Y μ)
hY : AEMeasurable Y μ
⊢ AEStronglyMeasurable (fun ω ↦ (X ω - ∫ (x : Ω), X x ∂Measure.map Y μ) ^ 2) (Measure.map Y μ)