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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : 0 ≤[i] s
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ (s.toMeasureOfZeroLE i hi₁ hi) j = ↑(NNReal.mk (s (i ∩ j)) ⋯)

Tactic:
simp_rw [toMeasureOfZeroLE, Measure.ofMeasurable_apply _ hj₁, toMeasureOfZeroLE',
    s.restrict_apply hi₁ hj₁, Set.inter_comm]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
hs : s ≤[univ] 0
i : Set α
hi : MeasurableSet i
⊢ (s.toMeasureOfLEZero univ ⋯ hs).toSignedMeasure i = (-s) i

Tactic:
simp [hi, toMeasureOfLEZero_apply _ _ _ hi, measureReal_def]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : SigmaFinite μ
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
i : Set α
hi : MeasurableSet i
⊢ s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i =
    s.toJordanDecomposition.toSignedMeasure i

Tactic:
rw [JordanDecomposition.toSignedMeasure, _root_.sub_apply,
        toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi, measureReal_def,
        measureReal_def]

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

Goal state before:
pp: case e'_3.e'_5
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.posPart =
    s.toJordanDecomposition.posPart.singularPart μ + μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)

Tactic:
exact s.toJordanDecomposition.posPart.haveLebesgueDecomposition_add μ

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

Goal state before:
pp: case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
c : E
hc : 0 ≤ c
hfc : ∀ᵐ (x : α) ∂μ, f x ≤ c
hm : m ≤ m0
⊢ ∀ᵐ (x : α) ∂μ, μ[f | m] x ≤ c

Tactic:
by_cases! hfint : ¬ Integrable f μ

Goal state after:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
c : E
hc : 0 ≤ c
hfc : ∀ᵐ (x : α) ∂μ, f x ≤ c
hm : m ≤ m0
hfint : ¬Integrable f μ
⊢ ∀ᵐ (x : α) ∂μ, μ[f | m] x ≤ c

case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
c : E
hc : 0 ≤ c
hfc : ∀ᵐ (x : α) ∂μ, f x ≤ c
hm : m ≤ m0
hfint : Integrable f μ
⊢ ∀ᵐ (x : α) ∂μ, μ[f | m] x ≤ c
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst✝³] F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ μ F = ∫⁻ (x : X), F.indicator (fun x ↦ 1) x ∂μ

Tactic:
lintegral_indicator hF.measurableSet

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst✝³] F
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ μ F = ∫⁻ (a : X) in F, 1 ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
s : Set α
hs : MeasurableSet s
f : α → E
hm : m ≤ m0
⊢ ∫ (x : α) in s, |μ[f | m] x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ

Tactic:
by_cases! hfint : ¬ Integrable f μ

Goal state after:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
s : Set α
hs : MeasurableSet s
f : α → E
hm : m ≤ m0
hfint : ¬Integrable f μ
⊢ ∫ (x : α) in s, |μ[f | m] x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ

case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
s : Set α
hs : MeasurableSet s
f : α → E
hm : m ≤ m0
hfint : Integrable f μ
⊢ ∫ (x : α) in s, |μ[f | m] x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hf : 0 ≤ᵐ[μ.restrict s] f
hm : m ≤ m0
⊢ ∫ (x : α) in s, μ[f | m] x ∂μ ≤ ∫ (x : α) in s, f x ∂μ

Tactic:
by_cases! hfint : ¬ Integrable f μ

Goal state after:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hf : 0 ≤ᵐ[μ.restrict s] f
hm : m ≤ m0
hfint : ¬Integrable f μ
⊢ ∫ (x : α) in s, μ[f | m] x ∂μ ≤ ∫ (x : α) in s, f x ∂μ

case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hf : 0 ≤ᵐ[μ.restrict s] f
hm : m ≤ m0
hfint : Integrable f μ
⊢ ∫ (x : α) in s, μ[f | m] x ∂μ ≤ ∫ (x : α) in s, f x ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
⊢ ∫ (x : α), ‖μ[f | m] x‖ ∂μ ≤ ∫ (x : α), ‖f x‖ ∂μ

Tactic:
by_cases! hfint : ¬ Integrable f μ

Goal state after:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hfint : ¬Integrable f μ
⊢ ∫ (x : α), ‖μ[f | m] x‖ ∂μ ≤ ∫ (x : α), ‖f x‖ ∂μ

case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hfint : Integrable f μ
⊢ ∫ (x : α), ‖μ[f | m] x‖ ∂μ ≤ ∫ (x : α), ‖f x‖ ∂μ
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
s : Set α
hs : MeasurableSet s
f : α → E
⊢ ∫ (x : α) in s, ‖μ[f | m] x‖ ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ∂μ

Tactic:
by_cases! hfint : ¬ Integrable f μ

Goal state after:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
s : Set α
hs : MeasurableSet s
f : α → E
hfint : ¬Integrable f μ
⊢ ∫ (x : α) in s, ‖μ[f | m] x‖ ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ∂μ

case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
s : Set α
hs : MeasurableSet s
f : α → E
hfint : Integrable f μ
⊢ ∫ (x : α) in s, ‖μ[f | m] x‖ ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ∂μ
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := (Finset.image (fun i ↦ eLpNorm (f i) p μ) Finset.univ).max' ⋯
i : ι
⊢ eLpNorm (f i) p μ ≤ C

pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := (Finset.image (fun i ↦ eLpNorm (f i) p μ) Finset.univ).max' ⋯
i : ι
⊢ C ≠ ∞

Tactic:
· exact Finset.le_max' (α := ℝ≥0∞) _ _ (Finset.mem_image.2 ⟨i, Finset.mem_univ _, rfl⟩)

Goal state after:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := (Finset.image (fun i ↦ eLpNorm (f i) p μ) Finset.univ).max' ⋯
i : ι
⊢ C ≠ ∞
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := (Finset.image (fun i ↦ eLpNorm (f i) p μ) Finset.univ).max' ⋯
i✝ i : ι
⊢ eLpNorm (f i) p μ < ∞

Tactic:
exact hf i

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

Goal state before:
pp: case refine_2
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst✝ : TopologicalSpace 𝓧
h : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ ∈ S, μ Kᶜ ≤ ε
ε : ENNReal
hε : 0 < ε
⊢ ∃ s, (∃ t, IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ i ∈ S, i t ≤ ε

Tactic:
· obtain ⟨K, h1, h2⟩ := h ε hε
    exact ⟨Kᶜ, ⟨K, h1, subset_rfl⟩, fun A hA μ hμS ↦ (μ.mono hA).trans (h2 μ hμS)⟩

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSpace Ω'
f : Ω → Ω'
μ : FiniteMeasure Ω'
⊢ (comap f μ).mass ≤ μ.mass

Tactic:
simp only [mass, comap, mk_apply, coeFn_def, ne_eq, measure_ne_top, not_false_eq_true,
    ENNReal.toNNReal_le_toNNReal]
  apply (Measure.comap_apply_le _ _ nullMeasurableSet_univ).trans (measure_mono (subset_univ _))

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : MeasurableSpace Ω'
inst✝⁴ : TopologicalSpace Ω
inst✝³ : TopologicalSpace Ω'
inst✝² : BorelSpace Ω
inst✝¹ : BorelSpace Ω'
inst✝ : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
μ : FiniteMeasure Ω'
hμ : μ ∈ {μ | μ (range f)ᶜ = 0}
g : Ω →ᵇ ℝ
g' : Ω' →ᵇ ℝ
hg' : ⇑g' ∘ f = ⇑g
x : Ω
⊢ g x = (⇑g' ∘ f) x

Tactic:
simp only [hg']

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

Goal state before:
pp: case mp
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
h : IndepFun f g κ μ
⊢ ∀ (s : Set β) (t : Set β'),
    MeasurableSet s → MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)

Tactic:
refine fun s t hs ht => h (f ⁻¹' s) (g ⁻¹' t) ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᵐ[κ a] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᵐ[κ a] g i
a : α
ha : ∀ i ∈ S, f i =ᵐ[κ a] g i
h'a : (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
i : ι
hi : i ∈ S
⊢ g i ⁻¹' sets i =ᵐ[κ a] f i ⁻¹' sets i

Tactic:
filter_upwards [ha i hi] with ω hω

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
mβ : (i : ι) → MeasurableSpace (β i)
f g : (i : ι) → Ω → β i
hf :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
h : ∀ (i : ι), ∀ᵐ (a : α) ∂μ, f i =ᵐ[κ a] g i
S : Finset ι
sets : (i : ι) → Set (β i)
hmeas : ∀ i ∈ S, MeasurableSet (sets i)
this : ∀ᵐ (a : α) ∂μ, ∀ i ∈ S, f i =ᵐ[κ a] g i
a : α
ha : ∀ i ∈ S, f i =ᵐ[κ a] g i
h'a : (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
i : ι
hi : i ∈ S
ω : Ω
hω : f i ω = g i ω
⊢ (g i ⁻¹' sets i) ω = (f i ⁻¹' sets i) ω
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case refine_1
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
G : Set Ω
h_opens : μ G ≤ liminf (fun i ↦ (μs i) G) atTop
G_open : IsOpen[inst✝¹] G
⊢ ContinuousAt ENNReal.ofNNReal (liminf (fun x ↦ (μs x) G) atTop)

pp: case refine_2
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
G : Set Ω
h_opens : μ G ≤ liminf (fun i ↦ (μs i) G) atTop
G_open : IsOpen[inst✝¹] G
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) atTop fun x ↦ (μs x) G

pp: case refine_3
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
G : Set Ω
h_opens : μ G ≤ liminf (fun i ↦ (μs i) G) atTop
G_open : IsOpen[inst✝¹] G
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) atTop fun x ↦ (μs x) G

Tactic:
· exact ENNReal.continuous_coe.continuousAt

Goal state after:
case refine_2
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
G : Set Ω
h_opens : μ G ≤ liminf (fun i ↦ (μs i) G) atTop
G_open : IsOpen[inst✝¹] G
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) atTop fun x ↦ (μs x) G

case refine_3
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
G : Set Ω
h_opens : μ G ≤ liminf (fun i ↦ (μs i) G) atTop
G_open : IsOpen[inst✝¹] G
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) atTop fun x ↦ (μs x) G
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:
rw [(measurePreserving_eval μ i).map_eq]
    exact mX i

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
g : ι → Set Ω := fun i ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
h_P_inter✝ : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
a : α
h_P_inter : (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
ha1 : (κ a) (⋂ i ∈ p1, f1 i) = ∏ i ∈ p1, (κ a) (f1 i)
ha2 : (κ a) (⋂ i ∈ p2, f2 i) = ∏ i ∈ p2, (κ a) (f2 i)
⊢ IsProbabilityMeasure (κ a) → (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
h'

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
h_P_inter✝ : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
a : α
h_P_inter : (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
ha1 : (κ a) (⋂ i ∈ p1, f1 i) = ∏ i ∈ p1, (κ a) (f1 i)
ha2 : (κ a) (⋂ i ∈ p2, f2 i) = ∏ i ∈ p2, (κ a) (f2 i)
h' : IsProbabilityMeasure (κ 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 Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : HasPDF X ℙ μ
s : Set E
hs : MeasurableSet s
⊢ (map X ℙ) s = ∫⁻ (x : E) in s, pdf X ℙ μ x ∂μ

Tactic:
← withDensity_apply _ hs,

Goal state after:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : HasPDF X ℙ μ
s : Set E
hs : MeasurableSet s
⊢ (map X ℙ) s = (μ.withDensity (pdf X ℙ μ)) s
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 α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec : (∀ i ∈ S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a) (f i)
hf_m : ∀ i ∈ insert a S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i
hf_m_S : ∀ x ∈ S, MeasurableSet (f x)
p : Set (Set Ω) := piiUnionInter π ↑S
m_p : MeasurableSpace Ω := generateFrom p
hS_eq_generate : m_p = generateFrom p
h_indep : Indep m_p (m a) η μ
h : ∀ᵐ (a_1 : α) ∂μ, (η a_1) (f a ∩ ⋂ n ∈ S, f n) = (η a_1) (f a) * (η a_1) (⋂ n ∈ S, f n)
a' : α
ha' : (η a') (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a') (f i)
⊢ (η a') (f a ∩ ⋂ n ∈ S, f n) = (η a') (f a) * (η a') (⋂ n ∈ S, f n) →
    (η a') (⋂ i ∈ insert a S, f i) = ∏ i ∈ insert a S, (η a') (f i)

Tactic:
h'

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec : (∀ i ∈ S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a) (f i)
hf_m : ∀ i ∈ insert a S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i
hf_m_S : ∀ x ∈ S, MeasurableSet (f x)
p : Set (Set Ω) := piiUnionInter π ↑S
m_p : MeasurableSpace Ω := generateFrom p
hS_eq_generate : m_p = generateFrom p
h_indep : Indep m_p (m a) η μ
h : ∀ᵐ (a_1 : α) ∂μ, (η a_1) (f a ∩ ⋂ n ∈ S, f n) = (η a_1) (f a) * (η a_1) (⋂ n ∈ S, f n)
a' : α
ha' : (η a') (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a') (f i)
h' : (η a') (f a ∩ ⋂ n ∈ S, f n) = (η a') (f a) * (η a') (⋂ n ∈ S, f n)
⊢ (η a') (⋂ i ∈ insert a S, f i) = ∏ i ∈ insert a S, (η a') (f i)
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᵐ[μ] 0
⊢ 0 = ∑ i ∈ s, Var[X i; μ]

Tactic:
symm
      refine Finset.sum_eq_zero fun i hi ↦ ?_
      simp [variance_congr (h'' i hi)]

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

Goal state before:
pp: case inr
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
⊢ TendstoInDistribution Y l Z (fun x ↦ μ'') μ'

Tactic:
let x₀ : E := hE.some

Goal state after:
case inr
ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
⊢ TendstoInDistribution Y l Z (fun x ↦ μ'') μ'
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : ↑f i = m'
⊢ m' ≤ (fun i ↦ sSup ((fun f ↦ ↑f i) '' s)) j

Tactic:
rw [← hfm']

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : ↑f i = m'
⊢ ↑f i ≤ (fun i ↦ sSup ((fun f ↦ ↑f i) '' s)) j
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
f : Filtration ι m
left✝ : f ∈ s
hfm' : ↑f i = m'
⊢ m' ≤ m

Tactic:
rw [← hfm']

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
f : Filtration ι m
left✝ : f ∈ s
hfm' : ↑f i = m'
⊢ ↑f i ≤ m
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case neg
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
i : ι
hi : i ∉ s
⊢ MeasurableSet (Y i ⁻¹' t i)

Tactic:
exact hYt _

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Count

Goal state before:
pp: α : Type u_1
ε : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
inst✝ : Finite α
h : ∀ (i : α), ‖f i‖ₑ < ∞
this : Fintype α
⊢ ‖Finset.univ.sup fun x ↦ ‖f x‖ₑ‖ₑ ≠ ∞

Tactic:
by simp [h, LT.lt.ne]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Subsingleton ι
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ¬↑ε = ∞
hι : ¬Nonempty ι
⊢ ∃ s, μ s ≠ ∞ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
case =>

Goal state after: