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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
J : Finset ι
T : Set ((i : ↥J) → α ↑i)
hT : MeasurableSet T
ht_eq : t = cylinder J T
S' : Set ((i : ↥(I ∪ J)) → α ↑i) := restrict₂ ⋯ ⁻¹' S
⊢ projectiveFamilyFun P (s ∪ t) = projectiveFamilyFun P s + projectiveFamilyFun P t

Tactic:
let T' := restrict₂ (subset_union_right (s₁ := I)) ⁻¹' T

Goal state after:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
J : Finset ι
T : Set ((i : ↥J) → α ↑i)
hT : MeasurableSet T
ht_eq : t = cylinder J T
S' : Set ((i : ↥(I ∪ J)) → α ↑i) := restrict₂ ⋯ ⁻¹' S
T' : Set ((i : ↥(I ∪ J)) → α ↑i) := restrict₂ ⋯ ⁻¹' T
⊢ projectiveFamilyFun P (s ∪ t) = projectiveFamilyFun P s + projectiveFamilyFun P t
Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
J : Finset ι
T : Set ((i : ↥J) → α ↑i)
hT : MeasurableSet T
ht_eq : t = cylinder J T
S' : Set ((i : ↥(I ∪ J)) → α ↑i) := restrict₂ ⋯ ⁻¹' S
T' : Set ((i : ↥(I ∪ J)) → α ↑i) := restrict₂ ⋯ ⁻¹' T
hS' : MeasurableSet S'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (I ∪ J) S'
h_eq2 : t = cylinder (I ∪ J) T'
h_eq3 : s ∪ t = cylinder (I ∪ J) (S' ∪ T')
⊢ projectiveFamilyFun P (s ∪ t) = (P (I ∪ J)) S' + (P (I ∪ J)) T'

Tactic:
projectiveFamilyFun_congr hP (union_mem_measurableCylinders hs ht) h_eq3 (hS'.union hT')

Goal state after:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
I : Finset ι
S : Set ((i : ↥I) → α ↑i)
hS : MeasurableSet S
hs_eq : s = cylinder I S
J : Finset ι
T : Set ((i : ↥J) → α ↑i)
hT : MeasurableSet T
ht_eq : t = cylinder J T
S' : Set ((i : ↥(I ∪ J)) → α ↑i) := restrict₂ ⋯ ⁻¹' S
T' : Set ((i : ↥(I ∪ J)) → α ↑i) := restrict₂ ⋯ ⁻¹' T
hS' : MeasurableSet S'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (I ∪ J) S'
h_eq2 : t = cylinder (I ∪ J) T'
h_eq3 : s ∪ t = cylinder (I ∪ J) (S' ∪ T')
⊢ (P (I ∪ J)) (S' ∪ T') = (P (I ∪ J)) S' + (P (I ∪ J)) T'
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → v i = w i
i : Set α
hi : ¬MeasurableSet i
⊢ v i = w i

Tactic:
· simp_rw [not_measurable _ hi]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x ↦ ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
⊢ M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ^ (1 / p.toReal) ≤ (‖f x‖ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
← Real.rpow_mul (norm_nonneg _),

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α), ‖{x | M ≤ ↑‖‖f x‖ ^ p.toReal‖₊}.indicator (fun x ↦ ‖f x‖ ^ p.toReal) x‖ₑ ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
⊢ M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ^ (1 / p.toReal) ≤ ‖f x‖ ^ (p.toReal * (1 / p.toReal))
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case neg.hd
α : 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)
a b : ℕ
hab : a ≠ b
⊢ Function.onFun Disjoint (fun l ↦ ⋃ (_ : l < k), s.restrictNonposSeq i l) a b

Tactic:
refine Set.disjoint_iUnion_left.mpr fun _ => ?_

Goal state after:
case neg.hd
α : 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)
a b : ℕ
hab : a ≠ b
x✝ : a < k
⊢ Disjoint (s.restrictNonposSeq i a) ((fun l ↦ ⋃ (_ : l < k), s.restrictNonposSeq i l) b)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
⊢ j₁.posPart.real i = (j₁.posPart.toSignedMeasure - j₁.negPart.toSignedMeasure) (i ∩ Sᶜ)

Tactic:
toSignedMeasure_sub_apply (hi.inter hS₁.compl),

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : j₁.posPart S = 0
hS₅ : j₁.negPart Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : j₂.posPart T = 0
hT₅ : j₂.negPart Tᶜ = 0
hST₁ : j₁.toSignedMeasure (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
⊢ j₁.posPart.real i = j₁.posPart.real (i ∩ Sᶜ) - j₁.negPart.real (i ∩ Sᶜ)
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case mp
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h : ∀ ⦃s : Set α⦄, μ.ennrealToMeasure s = 0 → v s = 0
s : Set α
hmeas : MeasurableSet s
hs : μ s = 0
⊢ μ.ennrealToMeasure s = μ s

Tactic:
ennrealToMeasure_apply hmeas

Goal state after:
case mp
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h : ∀ ⦃s : Set α⦄, μ.ennrealToMeasure s = 0 → v s = 0
s : Set α
hmeas : MeasurableSet s
hs : μ s = 0
⊢ μ s = μ s
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : μ.ennrealToMeasure s = 0
hmeas : MeasurableSet s
⊢ v s = 0

Tactic:
ennrealToMeasure_apply hmeas

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
μ : VectorMeasure α ℝ≥0∞
h : v ≪ᵥ μ
s : Set α
hs : μ s = 0
hmeas : MeasurableSet s
⊢ v s = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case mp.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, s t = 0
hu₂ : ∀ t ⊆ uᶜ, μ t = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ μ uᶜ = 0

Tactic:
exact hu₂ _ (Set.Subset.refl _)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Measurable (s.rnDeriv μ)

Tactic:
by
  rw [rnDeriv_def]
  fun_prop

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hp : 1 ≤ p
⊢ lpNorm (f - g) p μ ≤ lpNorm f p μ + lpNorm g p μ

Tactic:
simpa [sub_eq_add_neg] using lpNorm_add_le hf (g := -g) hp

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

Goal state before:
pp: Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : HasOuterApproxClosed Ω
inst✝¹ : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝ : IsFiniteMeasure μ
h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν
F : Set Ω
F_closed : IsClosed[inst✝³] F
ν_finite : IsFiniteMeasure ν
obs_ν : Tendsto (fun n ↦ ∫⁻ (x : Ω), ↑((F_closed.apprSeq n) x) ∂ν) atTop (𝓝 (ν F))
obs_μ : Tendsto (fun n ↦ ∫⁻ (x : Ω), ↑((F_closed.apprSeq n) x) ∂ν) atTop (𝓝 (μ F))
⊢ μ F = ν F

Tactic:
exact tendsto_nhds_unique obs_μ obs_ν

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ↑{g | ∃ ni, TendstoInMeasure μ (fn ∘ ni) u g}) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((fun f ↦ ↑f) i)) p μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨δ, hδ, fun ⟨f, s, hs⟩ t ht ht' => ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x✝ : ↑{g | ∃ ni, TendstoInMeasure μ (fn ∘ ni) u g}
t : Set α
ht : MeasurableSet t
ht' : μ t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : TendstoInMeasure μ (fn ∘ s) u f
⊢ eLpNorm (t.indicator ((fun f ↦ ↑f) ⟨f, ⋯⟩)) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ↑{g | ∃ ni, ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (ni n) x) u (𝓝 (g x))}) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((fun f ↦ ↑f) i)) p μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨δ, hδ, fun ⟨f, s, hs⟩ t ht ht' => ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x✝ : ↑{g | ∃ ni, ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (ni n) x) u (𝓝 (g x))}
t : Set α
ht : MeasurableSet t
ht' : μ t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ fn (s n) x) u (𝓝 (f x))
⊢ eLpNorm (t.indicator ((fun f ↦ ↑f) ⟨f, ⋯⟩)) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Goal state before:
pp: Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ Tendsto (fun i ↦ (μs i).normalize) F (𝓝 μ.normalize) ∧ Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass) ↔ Tendsto μs F (𝓝 μ)

Tactic:
by
  constructor
  · rintro ⟨normalized_lim, mass_lim⟩
    exact tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass normalized_lim mass_lim
  · intro μs_lim
    exact ⟨tendsto_normalize_of_tendsto μs_lim nonzero, μs_lim.mass⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
m : Measure α
inst✝ : IsProbabilityMeasure m
f : α → Measure β
hf₀ : AEMeasurable f m
hf₁ : ∀ᵐ (μ : α) ∂m, IsProbabilityMeasure (f μ)
⊢ IsProbabilityMeasure (m.bind f)

Tactic:
simp only [isProbabilityMeasure_iff, MeasurableSet.univ, Measure.bind_apply _ hf₀]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
m : Measure α
inst✝ : IsProbabilityMeasure m
f : α → Measure β
hf₀ : AEMeasurable f m
hf₁ : ∀ᵐ (μ : α) ∂m, IsProbabilityMeasure (f μ)
⊢ ∫⁻ (a : α), (f a) univ ∂m = 1
Module: Mathlib.MeasureTheory.Measure.Tight

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst✝² : TopologicalSpace 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed[inst✝²] s) MeasurableSet
ε : ENNReal
hε : 0 < ε
r : ENNReal := μ univ
x✝ : ε < r ∨ r ≤ ε
⊢ ∃ K, IsCompact K ∧ ∀ μ_1 ∈ {μ}, μ_1 Kᶜ ≤ ε

Tactic:
cases lt_or_ge ε r with

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

Goal state before:
pp: case inr
Ω : Type u_1
inst✝² : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i ↦ (μs i) E) L ≤ μ E
hne : L.NeBot
meas_Ec : μ Eᶜ = 1 - μ E
meas_i_Ec : ∀ (i : ι), (μs i) Eᶜ = 1 - (μs i) E
⊢ 1 - μ E ≤ liminf (fun i ↦ 1 - (μs i) E) L

Tactic:
rw [show (L.liminf fun i : ι ↦ 1 - μs i E) = L.liminf ((fun x ↦ 1 - x) ∘ fun i : ι ↦ μs i E)
      from rfl]

Goal state after:
case inr
Ω : Type u_1
inst✝² : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i ↦ (μs i) E) L ≤ μ E
hne : L.NeBot
meas_Ec : μ Eᶜ = 1 - μ E
meas_i_Ec : ∀ (i : ι), (μs i) Eᶜ = 1 - (μs i) E
⊢ 1 - μ E ≤ liminf ((fun x ↦ 1 - x) ∘ fun i ↦ (μs i) E) L
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 α
inst✝¹ : Subsingleton ι
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝ : IsMarkovKernel κ
⊢ iIndepFun f κ μ

Tactic:
by
  simp [iIndepFun]

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 Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h : ∀ (S : Finset ι), ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, s i) = ∏ i ∈ S, (κ a) (s i)
S : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ S, f i ∈ (fun i ↦ {s i}) i
a : α
ha : (κ a) (⋂ i ∈ S, s i) = ∏ i ∈ S, (κ a) (s i)
⊢ (κ a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (κ a) (f i)

Tactic:
have : ∀ i ∈ S, κ a (f i) = κ a (s i) := fun i hi ↦ by rw [hf i hi]

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set Ω
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h : ∀ (S : Finset ι), ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, s i) = ∏ i ∈ S, (κ a) (s i)
S : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ S, f i ∈ (fun i ↦ {s i}) i
a : α
ha : (κ a) (⋂ i ∈ S, s i) = ∏ i ∈ S, (κ a) (s i)
this : ∀ i ∈ S, (κ a) (f i) = (κ a) (s i)
⊢ (κ a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (κ a) (f i)
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: 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

Tactic:
simp [hx, ht₁]

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

Goal state before:
pp: case refine_2.hf
ι : 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 (Function.eval i) (Measure.pi μ)

Tactic:
exact (measurable_pi_apply i).aemeasurable

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → F
hf : AEStronglyMeasurable f μ
⊢ Integrable f (map X ℙ) ↔ Integrable f (μ.withDensity ((map X ℙ).rnDeriv μ))

Tactic:
withDensity_rnDeriv_eq _ _ HasPDF.absolutelyContinuous

Goal state after:
Ω : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → F
hf : AEStronglyMeasurable f μ
⊢ Integrable f (map X ℙ) ↔ Integrable f (map X ℙ)
Module: Mathlib.Probability.Density

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

Tactic:
withDensity_rnDeriv_eq _ _ HasPDF.absolutelyContinuous

Goal state after:
Ω : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → F
hf : AEStronglyMeasurable f μ
⊢ ∫ (x : E), f x ∂map X ℙ = ∫ (y : E), f y ∂map X ℙ
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : SFinite ℙ
hX : AEMeasurable X ℙ
⊢ AEMeasurable X ℙ ∧ map X ℙ ≪ volume ↔ map X ℙ ≪ volume

Tactic:
and_iff_right hX

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : SFinite ℙ
hX : AEMeasurable X ℙ
⊢ map X ℙ ≪ volume ↔ map X ℙ ≪ volume
Module: Mathlib.Probability.Moments.Covariance

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

Tactic:
repeat rw [integral_sub]

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

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

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

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

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

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

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

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

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

Goal state after: