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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
⊢ v j ≤ w j

Tactic:
by_cases hj₁ : MeasurableSet j

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
hj₁ : MeasurableSet j
⊢ v j ≤ w j

case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
hj₁ : ¬MeasurableSet j
⊢ v j ≤ w j
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
h : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → v j ≤ w j
⊢ v ≤[i] w

Tactic:
by_cases hi : MeasurableSet i
  · exact (restrict_le_restrict_iff _ _ hi).2 h
  · rw [restrict_not_measurable v hi, restrict_not_measurable w hi]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
⊢ j.toSignedMeasure ≤[S] 0

pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
⊢ 0 ≤[Sᶜ] j.toSignedMeasure

Tactic:
· refine restrict_le_restrict_of_subset_le _ _ fun A hA hA₁ => ?_
    rw [toSignedMeasure, toSignedMeasure_sub_apply hA, measureReal_def,
      show j.posPart A = 0 from nonpos_iff_eq_zero.1 (hS₂ ▸ measure_mono hA₁), ENNReal.toReal_zero,
      zero_sub, neg_le, zero_apply, neg_zero]
    exact ENNReal.toReal_nonneg

Goal state after:
case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
⊢ 0 ≤[Sᶜ] j.toSignedMeasure
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ (μ.withDensityᵥ (-f)) i = (-μ.withDensityᵥ f) i

Tactic:
rw [_root_.neg_apply, withDensityᵥ_apply hf hi, ← integral_neg,
      withDensityᵥ_apply hf.neg hi]

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, (-f) x ∂μ = ∫ (a : α) in i, -f a ∂μ
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
n m : ℕ
⊢ n ≠ m → (Disjoint on fun n ↦ i ∩ f n) n m

Tactic:
hnm

Goal state after:
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
n m : ℕ
hnm : n ≠ m
⊢ (Disjoint on fun n ↦ i ∩ f n) n m
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
h₂ : Pairwise (Disjoint on fun n ↦ i ∩ f n)
⊢ ↑(NNReal.mk (∑' (i_1 : ℕ), s (i ∩ f i_1)) ⋯) = ∑' (i_1 : ℕ), ↑(NNReal.mk ((VectorMeasure.restrict s i) (f i_1)) ⋯)

Tactic:
have h : ∀ n, 0 ≤ s (i ∩ f n) := fun n =>
      s.nonneg_of_zero_le_restrict (s.zero_le_restrict_subset hi₁ Set.inter_subset_left hi₂)

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
h₂ : Pairwise (Disjoint on fun n ↦ i ∩ f n)
h : ∀ (n : ℕ), 0 ≤ s (i ∩ f n)
⊢ ↑(NNReal.mk (∑' (i_1 : ℕ), s (i ∩ f i_1)) ⋯) = ∑' (i_1 : ℕ), ↑(NNReal.mk ((VectorMeasure.restrict s i) (f i_1)) ⋯)
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝¹ : s.HaveLebesgueDecomposition μ
inst✝ : t.HaveLebesgueDecomposition μ
⊢ s + t = s.singularPart μ + t.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)

Tactic:
rw [withDensityᵥ_add (integrable_rnDeriv s μ) (integrable_rnDeriv t μ), add_assoc,
    add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
    singularPart_add_withDensity_rnDeriv_eq]

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

Goal state before:
pp: case e_f.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
hμs' : ¬μ s = 0
⊢ {x | C ≤ ‖f i x‖₊} ⊓ {x | ‖f i x‖₊ < C} ⊆ ⊥

Tactic:
rintro x ⟨hx₁, hx₂⟩

Goal state after:
case e_f.h
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬μ univ = 0
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)
hμs' : ¬μ s = 0
x : α
hx₁ : x ∈ {x | C ≤ ‖f i x‖₊}
hx₂ : x ∈ {x | ‖f i x‖₊ < C}
⊢ x ∈ ⊥
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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖Exists.choose ⋯ x‖₊}.indicator (Exists.choose ⋯)) p μ ≤ ENNReal.ofReal ε

Tactic:
have hCg : ∀ i, eLpNorm ({ x | C ≤ ‖g i x‖₊ }.indicator (g i)) p μ ≤ ENNReal.ofReal ε := by
    intro i
    refine le_trans (le_of_eq <| eLpNorm_congr_ae ?_) (hC i)
    filter_upwards [(Exists.choose_spec <| hf i).2] with x hx
    by_cases hfx : x ∈ { x | C ≤ ‖f i x‖₊ }
    · rw [Set.indicator_of_mem hfx, Set.indicator_of_mem, hx]
      rwa [Set.mem_ofPred, hx] at hfx
    · rw [Set.indicator_of_notMem hfx, Set.indicator_of_notMem]
      rwa [Set.mem_ofPred, hx] at hfx

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun i ↦ Exists.choose ⋯
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hCg : ∀ (i : ι), eLpNorm ({x | C ≤ ‖g i x‖₊}.indicator (g i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖Exists.choose ⋯ x‖₊}.indicator (Exists.choose ⋯)) p μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
p : ℝ≥0∞
hp : 1 ≤ p
hf : MemLp f p μ
h✝ : NeZero μ
hp' : 0 < p
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
hpt : p ≠ ∞
⊢ lpNorm μ[f | m] p μ ≤ lpNorm f p μ

Tactic:
rw [lpNorm_eq_integral_norm_rpow_toReal hp'.ne.symm hpt hf.1,
          lpNorm_eq_integral_norm_rpow_toReal hp'.ne.symm hpt integrable_condExp.1]
        gcongr ?_ ^ ?_
        have : 1 ≤ p.toReal := by
          rwa [← ENNReal.toReal_one, ENNReal.toReal_le_toReal ENNReal.one_ne_top hpt]
        exact integral_norm_condExp_rpow_le this <|
          (integrable_norm_rpow_iff hf.1 hp'.ne.symm hpt).2 hf

Goal state after:
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
⊢ ∃ K, IsCompact K ∧ ∀ μ_1 ∈ {μ}, μ_1 Kᶜ ≤ ε

Tactic:
cases lt_or_ge ε r with
  | inl hεr =>
    have hεr' : r - ε < r := ENNReal.sub_lt_self (measure_ne_top μ _) hεr.ne_bot hε.ne'
    obtain ⟨K, _, ⟨hK_compact, hK_closed⟩, hKμ⟩ := h .univ (r - ε) hεr'
    refine ⟨K, hK_compact, ?_⟩
    simp only [mem_singleton_iff, forall_eq]
    rw [measure_compl hK_closed.measurableSet (measure_ne_top μ _), tsub_le_iff_right]
    rw [ENNReal.sub_lt_iff_lt_right (ne_top_of_lt hεr) hεr.le, add_comm] at hKμ
    exact hKμ.le
  | inr hεr => exact ⟨∅, isCompact_empty, by simpa⟩

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∞
f : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑M
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ C, ∀ (i : ι), μ {x | C ≤ ‖f i x‖₊} ≤ ENNReal.ofReal δ

Tactic:
by
    by_contra! hcon
    choose ℐ hℐ using hcon
    lift δ to ℝ≥0 using hδpos.le
    have : ∀ C : ℝ≥0, C • (δ : ℝ≥0∞) ^ (1 / p.toReal) ≤ eLpNorm (f (ℐ C)) p μ := by
      intro C
      calc
        C • (δ : ℝ≥0∞) ^ (1 / p.toReal) ≤ C • μ { x | C ≤ ‖f (ℐ C) x‖₊ } ^ (1 / p.toReal) := by
          rw [ENNReal.smul_def, ENNReal.smul_def, smul_eq_mul, smul_eq_mul]
          simp_rw [ENNReal.ofReal_coe_nnreal] at hℐ
          refine mul_le_mul' le_rfl
            (ENNReal.rpow_le_rpow (hℐ C).le (one_div_nonneg.2 ENNReal.toReal_nonneg))
        _ ≤ eLpNorm ({ x | C ≤ ‖f (ℐ C) x‖₊ }.indicator (f (ℐ C))) p μ := by
          refine le_eLpNorm_of_bddBelow hp hp' _
            (measurableSet_le measurable_const (hf _).nnnorm.measurable)
            (Eventually.of_forall fun x hx => ?_)
          rwa [nnnorm_indicator_eq_indicator_nnnorm, Set.indicator_of_mem hx]
        _ ≤ eLpNorm (f (ℐ C)) p μ := eLpNorm_indicator_le _
    specialize this (2 * max M 1 * δ⁻¹ ^ (1 / p.toReal))
    rw [← ENNReal.coe_rpow_of_nonneg _ (one_div_nonneg.2 ENNReal.toReal_nonneg), ← ENNReal.coe_smul,
      smul_eq_mul, mul_assoc, NNReal.inv_rpow,
      inv_mul_cancel₀ (NNReal.rpow_pos (NNReal.coe_pos.1 hδpos)).ne.symm, mul_one, ENNReal.coe_mul,
      ← NNReal.inv_rpow] at this
    refine (lt_of_le_of_lt (le_trans
      (hM <| ℐ <| 2 * max M 1 * δ⁻¹ ^ (1 / p.toReal)) (le_max_left (M : ℝ≥0∞) 1))
        (lt_of_lt_of_le ?_ this)).ne rfl
    rw [← ENNReal.coe_one, ← ENNReal.coe_max, ← ENNReal.coe_mul, ENNReal.coe_lt_coe]
    exact lt_two_mul_self (lt_max_of_lt_right one_pos)

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

Goal state before:
pp: Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs : Pairwise (Function.onFun Disjoint fun r ↦ frontier (Metric.thickening r s))
key : {i | 0 < μ (frontier (Metric.thickening i s))}.Countable
aux : volume (Ioo a b \ {i | 0 < μ (frontier (Metric.thickening i s))}) = volume (Ioo a b)
len_pos : 0 < volume (Ioo a b)
⊢ ∃ r ∈ Ioo a b, μ (frontier (Metric.thickening r s)) = 0

Tactic:
← aux

Goal state after:
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : SFinite μ
s : Set Ω
a b : ℝ
hab : a < b
mbles : ∀ (r : ℝ), MeasurableSet (frontier (Metric.thickening r s))
disjs : Pairwise (Function.onFun Disjoint fun r ↦ frontier (Metric.thickening r s))
key : {i | 0 < μ (frontier (Metric.thickening i s))}.Countable
aux : volume (Ioo a b \ {i | 0 < μ (frontier (Metric.thickening i s))}) = volume (Ioo a b)
len_pos : 0 < volume (Ioo a b \ {i | 0 < μ (frontier (Metric.thickening i s))})
⊢ ∃ r ∈ Ioo a b, μ (frontier (Metric.thickening r s)) = 0
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsZeroOrProbabilityMeasure μ
hf : Measurable f
hg : Measurable g
⊢ f ⟂ᵢ[μ] g ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) μ

Tactic:
simp only [IndepFun, IndepSet, Kernel.indepFun_iff_indepSet_preimage hf hg]

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

Goal state before:
pp: Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsFiniteMeasure μ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ f ⟂ᵢ[μ] g ↔ Measure.map (fun ω ↦ (f ω, g ω)) μ = (Measure.map f μ).prod (Measure.map g μ)

Tactic:
apply indepFun_iff_map_prod_eq_prod_map_map' hf hg

Goal state after:
case σf
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsFiniteMeasure μ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ SigmaFinite (Measure.map f μ)

case σg
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsFiniteMeasure μ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ SigmaFinite (Measure.map g μ)
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case e'_3.e'_5
Ω : 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 : Measurable X
mY : Measurable Y
⊢ Measure.map X (Measure.map Prod.fst (μ.prod ν)) = Measure.map X μ

Tactic:
Measure.map_fst_prod,

Goal state after:
case e'_3.e'_5
Ω : 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 : Measurable X
mY : Measurable Y
⊢ Measure.map X (ν univ • μ) = Measure.map X μ
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case e'_3.e'_5
Ω : 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 : Measurable X
mY : Measurable Y
⊢ Measure.map (fun ω ↦ X ω.1) (μ.prod ν) = Measure.map X μ

Tactic:
rw [← Function.comp_def, ← Measure.map_map mX measurable_fst, Measure.map_fst_prod,
      measure_univ, one_smul]

Goal state after:
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:
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.Kernel.Indep

Goal state before:
pp: case inr.iUnion
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h✝ : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
h : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
⊢ ∀ᵐ (a : α) ∂μ, (κ a) ((⋃ i, f i) ∩ t2) = (κ a) (⋃ i, f i) * (κ a) t2

Tactic:
rw [← ae_all_iff] at h

Goal state after:
case inr.iUnion
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m1 m2 m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h1 : m1 ≤ m
h2 : m2 ≤ m
hp1 : IsPiSystem p1
hp2 : IsPiSystem p2
hpm1 : m1 = generateFrom p1
hpm2 : m2 = generateFrom p2
hyp : IndepSets p1 p2 κ μ
h✝ : IsMarkovKernel κ
t1 t2 : Set Ω
ht2 : t2 ∈ {s | MeasurableSet s}
f : ℕ → Set Ω
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
h : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
⊢ ∀ᵐ (a : α) ∂μ, (κ a) ((⋃ i, f i) ∩ t2) = (κ a) (⋃ i, f i) * (κ a) t2
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:
refine tendsto_of_forall_isOpen_le_liminf' ?_
  rwa [← limsup_measure_closed_le_iff_liminf_measure_open_ge]

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✝⁴ : 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 ℙ ν
h₀ : (map X ℙ).prod (map Y ℙ) = (μ.prod ν).withDensity fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
⊢ map (fun ω ↦ (X ω, Y ω)) ℙ = (map X ℙ).prod (map Y ℙ) ↔
    pdf (fun ω ↦ (X ω, Y ω)) ℙ (μ.prod ν) =ᵐ[μ.prod ν] fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2

Tactic:
← eq_of_map_eq_withDensity,

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 ℙ ν
h₀ : (map X ℙ).prod (map Y ℙ) = (μ.prod ν).withDensity fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
⊢ map (fun ω ↦ (X ω, Y ω)) ℙ = (map X ℙ).prod (map Y ℙ) ↔
    map (fun ω ↦ (X ω, Y ω)) ℙ = (μ.prod ν).withDensity fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2

case hmf
Ω : 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 ℙ ν
h₀ : (map X ℙ).prod (map Y ℙ) = (μ.prod ν).withDensity fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2
⊢ AEMeasurable (fun z ↦ pdf X ℙ μ z.1 * pdf Y ℙ ν z.2) (μ.prod ν)
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst✝¹] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst✝¹] G
r : ℝ≥0
hr : r < ν G
this : ∀ (x : ↑G), ∃ s ∈ S, s ∈ 𝓝 ↑x ∧ s ⊆ G
⊢ ∃ T ⊆ S, T.Countable ∧ ⋃ t ∈ T, t = G

Tactic:
choose! s hsS hs_nhds hsG using this

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst✝¹] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst✝¹] G
r : ℝ≥0
hr : r < ν G
s : ↑G → Set Ω
hsS : ∀ (x : ↑G), s x ∈ S
hs_nhds : ∀ (x : ↑G), s x ∈ 𝓝 ↑x
hsG : ∀ (x : ↑G), s x ⊆ G
⊢ ∃ T ⊆ S, T.Countable ∧ ⋃ t ∈ T, t = G
Module: Mathlib.Probability.Moments.Covariance

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

Tactic:
exact hX.integrable_mul hY

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 ω ↦ c - X ω; μ] = Var[X; μ]

Tactic:
simp_rw [sub_eq_add_neg]
  rw [variance_const_add (by fun_prop) c, variance_fun_neg]

Goal state after: