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

Goal state before:
pp: case neg
α : 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 : ℕ
x : α
⊢ a < k → x ∈ s.restrictNonposSeq i a → x ∈ i

Tactic:
intro _ hx

Goal state after:
case neg
α : 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 : ℕ
x : α
a✝ : a < k
hx : x ∈ s.restrictNonposSeq i a
⊢ x ∈ i
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case mp
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : μ.ennrealToMeasure S = 0
⊢ s.totalVariation S = 0

Tactic:
obtain ⟨i, hi₁, hi₂, hi₃, hpos, hneg⟩ := s.toJordanDecomposition_spec

Goal state after:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : μ.ennrealToMeasure S = 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₃
⊢ s.totalVariation S = 0
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan

Goal state before:
pp: case mp
α : 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
⊢ s.totalVariation ⟂ₘ μ.ennrealToMeasure

Tactic:
obtain ⟨i, hi₁, hi₂, hi₃, hpos, hneg⟩ := s.toJordanDecomposition_spec

Goal state after:
case mp
α : 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₃
⊢ s.totalVariation ⟂ₘ μ.ennrealToMeasure
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ (-s.toJordanDecomposition).negPart.HaveLebesgueDecomposition μ

Tactic:
JordanDecomposition.neg_negPart

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ (-s).toJordanDecomposition.negPart.HaveLebesgueDecomposition μ

Tactic:
by
    rw [toJordanDecomposition_neg, JordanDecomposition.neg_negPart]
    infer_instance

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ✝ : Measure α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ (r • s).toJordanDecomposition.negPart.HaveLebesgueDecomposition μ

Tactic:
by
    rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart]
    infer_instance

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✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f : α → E
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ ∫ (x : α), |μ[f | m] x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

Tactic:
calc
  _ ≤ ∫ x, μ[|f| | m] x ∂μ :=
    integral_mono_ae integrable_condExp.abs integrable_condExp (abs_condExp_ae_le_condExp_abs f)
  _ = _ := integral_condExp hm

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

Goal state before:
pp: case refine_2
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
lim_mass : Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass)
aux : {0}ᶜ ∈ 𝓝 μ.mass
eventually_nonzero : ∀ᶠ (i : γ) in F, μs i ≠ 0
eve : ∀ᶠ (i : γ) in F, (μs i).normalize.toFiniteMeasure.testAgainstNN f = (μs i).mass⁻¹ * (μs i).testAgainstNN f
⊢ Tendsto (fun n ↦ ((μs n).mass⁻¹, (μs n).testAgainstNN f).2) F (𝓝 (μ.mass⁻¹, μ.testAgainstNN f).2)

Tactic:
exact tendsto_iff_forall_testAgainstNN_tendsto.mp μs_lim f

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 : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
⊢ ↑C * μ univ ^ p.toReal⁻¹ + 1 = ↑(↑C * μ univ ^ p.toReal⁻¹ + 1).toNNReal

Tactic:
ENNReal.coe_toNNReal (by finiteness)

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
⊢ ↑C * μ univ ^ p.toReal⁻¹ + 1 = ↑C * μ univ ^ p.toReal⁻¹ + 1
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
p : ℝ≥0∞
hp : 1 ≤ p
⊢ eLpNorm μ[f | m] p μ ≤ eLpNorm f p μ

Tactic:
by_cases! hf : MemLp f p μ
  · rw [← ofReal_lpNorm hf, ← ofReal_lpNorm (hf.condExp hp)]
    exact ENNReal.ofReal_le_ofReal (hf.lpNorm_condExp_le_lpNorm hp)
  · simp only [MemLp, not_and, not_lt, top_le_iff] at hf
    by_cases! ha : AEStronglyMeasurable f μ
    · simp [hf ha]
    · simp [condExp_of_not_integrable (fun h => ha h.aestronglyMeasurable)]

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 : eLpNorm g 1 μ = 0
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖μ[g | ℱ i] x‖₊}.indicator μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε

pp: case neg
α : 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 : ¬eLpNorm g 1 μ = 0
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖μ[g | ℱ i] x‖₊}.indicator μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε

Tactic:
· rw [eLpNorm_eq_zero_iff hg.1 one_ne_zero] at hne
    refine ⟨0, fun n => (le_of_eq <|
      (eLpNorm_eq_zero_iff ((stronglyMeasurable_condExp.mono (hℱ n)).aestronglyMeasurable.indicator
        (hmeas n 0)) one_ne_zero).2 ?_).trans zero_le⟩
    filter_upwards [condExp_congr_ae (m := ℱ n) hne] with x hx
    simp [hx]

Goal state after:
case neg
α : 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 : ¬eLpNorm g 1 μ = 0
⊢ ∃ C, ∀ (i : ι), eLpNorm ({x | C ≤ ‖μ[g | ℱ i] x‖₊}.indicator μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε
Module: Mathlib.MeasureTheory.Measure.Tight

Goal state before:
pp: 𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
inst✝¹ : TopologicalSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
inst✝ : TopologicalSpace 𝓨
μ : Set (Measure (𝓧 × 𝓨))
hμ₁ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.fst '' μ, μ_1 Kᶜ ≤ ε
hμ₂ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.snd '' μ, μ_1 Kᶜ ≤ ε
ε : ENNReal
hε : 0 < ε
K₁ : Set 𝓧
hK₁_compact : IsCompact K₁
hK₁_le : ∀ μ_1 ∈ Measure.fst '' μ, μ_1 K₁ᶜ ≤ ε / 2
K₂ : Set 𝓨
hK₂_compact : IsCompact K₂
hK₂_le : ∀ μ_1 ∈ Measure.snd '' μ, μ_1 K₂ᶜ ≤ ε / 2
κ : Measure (𝓧 × 𝓨)
hκ_mem : κ ∈ μ
⊢ κ (K₁ᶜ ×ˢ univ) + κ (univ ×ˢ K₂ᶜ) ≤ ε

Tactic:
← ENNReal.add_halves (a := ε)

Goal state after:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
inst✝¹ : TopologicalSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
inst✝ : TopologicalSpace 𝓨
μ : Set (Measure (𝓧 × 𝓨))
hμ₁ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.fst '' μ, μ_1 Kᶜ ≤ ε
hμ₂ : ∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ Measure.snd '' μ, μ_1 Kᶜ ≤ ε
ε : ENNReal
hε : 0 < ε
K₁ : Set 𝓧
hK₁_compact : IsCompact K₁
hK₁_le : ∀ μ_1 ∈ Measure.fst '' μ, μ_1 K₁ᶜ ≤ ε / 2
K₂ : Set 𝓨
hK₂_compact : IsCompact K₂
hK₂_le : ∀ μ_1 ∈ Measure.snd '' μ, μ_1 K₂ᶜ ≤ ε / 2
κ : Measure (𝓧 × 𝓨)
hκ_mem : κ ∈ μ
⊢ κ (K₁ᶜ ×ˢ univ) + κ (univ ×ˢ K₂ᶜ) ≤ ε / 2 + ε / 2
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr.inr
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
h : IsMarkovKernel κ
a : α
ht : t = univ
⊢ (κ a) (s ∩ t) = (κ a) s * (κ a) t

Tactic:
rw [ht, Set.inter_univ, measure_univ, mul_one]

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
ι : Type u_8
β : ι → Type u_9
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
⊢ iIndepFun f κ μ ↔
    ∀ (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)

Tactic:
refine ⟨fun h S sets h_meas => h _ fun i hi_mem => ⟨sets i, h_meas i hi_mem, rfl⟩, ?_⟩
  intro h S setsΩ h_meas
  classical
  let setsβ : ∀ i : ι, Set (β i) := fun i =>
    dite (i ∈ S) (fun hi_mem => (h_meas i hi_mem).choose) fun _ => Set.univ
  have h_measβ : ∀ i ∈ S, MeasurableSet[m i] (setsβ i) := by
    intro i hi_mem
    simp_rw [setsβ, dif_pos hi_mem]
    exact (h_meas i hi_mem).choose_spec.1
  have h_preim : ∀ i ∈ S, setsΩ i = f i ⁻¹' setsβ i := by
    intro i hi_mem
    simp_rw [setsβ, dif_pos hi_mem]
    exact (h_meas i hi_mem).choose_spec.2.symm
  simp_all

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 β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (Measure.map f μ)
σg : SigmaFinite (Measure.map g μ)
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ μ (f ⁻¹' s) * μ (g ⁻¹' t) = (Measure.map f μ) s * (Measure.map g μ) t

Tactic:
rw [Measure.map_apply_of_aemeasurable hf hs, Measure.map_apply_of_aemeasurable hg ht]

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

Goal state before:
pp: case inr.iUnion
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₂ m : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
p1 p2 : Set (Set Ω)
h2 : m₂ ≤ m
hp2 : IsPiSystem p2
hpm2 : m₂ = generateFrom p2
hyp : IndepSets p1 p2 κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ p1
ht1m : MeasurableSet t1
h : IsMarkovKernel κ
f : ℕ → Set Ω
hfd : Pairwise (Function.onFun Disjoint f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ f i) = (κ a) t1 * (κ a) (f i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ ⋃ i, f i) = (κ a) t1 * (κ a) (⋃ i, f i)

Tactic:
rw [← ae_all_iff] at ihf
    filter_upwards [ihf] with a ha
    rw [inter_iUnion, measure_iUnion, measure_iUnion hfd fun i ↦ h2 _ (hfm i)]
    · simp only [ENNReal.tsum_mul_left, ha]
    · exact hfd.mono fun i j h ↦ (h.inter_left' _).inter_right' _
    · exact fun i ↦ .inter ht1m (h2 _ <| hfm i)

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝ : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
h₀ :
  ∀ {s : (i : ι) → Set (β i)},
    (∀ (i : ι), MeasurableSet (s i)) →
      ∏ i, μ (f i ⁻¹' s i) = ∏ i, (Measure.map (f i) μ) (s i) ∧
        μ (⋂ i, f i ⁻¹' s i) = (Measure.map (fun ω i ↦ f i ω) μ) (univ.pi s)
⊢ (Measure.map (fun ω i ↦ f i ω) μ = Measure.pi fun i ↦ Measure.map (f i) μ) →
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
      (∀ i ∈ S, MeasurableSet (sets i)) → μ (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, μ (f i ⁻¹' sets i)

Tactic:
intro h S s hs

Goal state after:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
inst✝ : IsProbabilityMeasure μ
hf : ∀ (i : ι), AEMeasurable (f i) μ
h₀ :
  ∀ {s : (i : ι) → Set (β i)},
    (∀ (i : ι), MeasurableSet (s i)) →
      ∏ i, μ (f i ⁻¹' s i) = ∏ i, (Measure.map (f i) μ) (s i) ∧
        μ (⋂ i, f i ⁻¹' s i) = (Measure.map (fun ω i ↦ f i ω) μ) (univ.pi s)
h : Measure.map (fun ω i ↦ f i ω) μ = Measure.pi fun i ↦ Measure.map (f i) μ
S : Finset ι
s : (i : ι) → Set (β i)
hs : ∀ i ∈ S, MeasurableSet (s i)
⊢ μ (⋂ i ∈ S, f i ⁻¹' s i) = ∏ i ∈ S, μ (f i ⁻¹' s i)
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: γ : 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))
⊢ (↑μ).real s < (↑μ).real s + ε / 2

Tactic:
simp [ε_pos]

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

Goal state before:
pp: case e'_3
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
h : ∫⁻ (a : α) in u, ((κ.map fun ω ↦ (f ω, g ω)) a) (s ×ˢ t) ∂μ = ∫⁻ (a : α) in u, ((κ.map f ×ₖ κ.map g) a) (s ×ˢ t) ∂μ
hu : MeasurableSet u
hμu : μ u < ⊤
ω : α
⊢ (κ ω) (f ⁻¹' s) * (κ ω) (g ⁻¹' t) = (κ ω) (f ⁻¹' s) * ((κ.map g) ω) t

Tactic:
map_apply' _ (by fun_prop) _ ht

Goal state after:
case e'_3
α : Type u_1
Ω : Type u_2
β : Type u_4
γ : Type u_6
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteKernel κ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
u : Set α
h : ∫⁻ (a : α) in u, ((κ.map fun ω ↦ (f ω, g ω)) a) (s ×ˢ t) ∂μ = ∫⁻ (a : α) in u, ((κ.map f ×ₖ κ.map g) a) (s ×ˢ t) ∂μ
hu : MeasurableSet u
hμu : μ u < ⊤
ω : α
⊢ (κ ω) (f ⁻¹' s) * (κ ω) (g ⁻¹' t) = (κ ω) (f ⁻¹' s) * (κ ω) (g ⁻¹' t)
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: γ : 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 ω ∂↑μ))
⊢ ∫ (a : Ω), fs M a ∂↑μ < ∫ (a : Ω), fs M a ∂↑μ + ε / 2

Tactic:
simp [ε_pos]

Goal state after:
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
⊢ Measurable (pdf X ℙ μ)

Tactic:
exact measurable_rnDeriv _ _

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : IsFiniteMeasure ℙ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ volume =ᵐ[volume] g
hgi : ∫⁻ (x : ℝ), ‖f x‖ₑ * g x ≠ ∞
this : (fun x ↦ ‖f x‖ₑ * g x) =ᵐ[volume] fun x ↦ ‖f x * (pdf X ℙ volume x).toReal‖ₑ
⊢ ∫⁻ (a : ℝ), ‖f a * (pdf X ℙ volume a).toReal‖ₑ < ∞

Tactic:
rwa [lt_top_iff_ne_top, ← lintegral_congr_ae this]

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

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : SecondCountableTopology Ω
inst✝¹ : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst✝ : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst✝³] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' : ∀ s ∈ S, Tendsto (fun i ↦ (μ i) s) l (𝓝 (ν s))
hl : l.NeBot
⊢ Tendsto μ l (𝓝 ν)

Tactic:
apply tendsto_of_forall_isOpen_le_liminf

Goal state after:
case inr
Ω : Type u_1
ι : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : SecondCountableTopology Ω
inst✝¹ : OpensMeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
inst✝ : l.IsCountablyGenerated
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ (u : Set Ω), IsOpen[inst✝³] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
h' : ∀ s ∈ S, Tendsto (fun i ↦ (μ i) s) l (𝓝 (ν s))
hl : l.NeBot
⊢ ∀ (G : Set Ω), IsOpen[inst✝³] G → ν G ≤ liminf (fun i ↦ (μ i) G) l
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case refine_2
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m₁ m₂ x✝ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : Indep m₁ m₂ κ μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' t' : Set Ω
hs' : s' ∈ {s_1 | MeasurableSet s_1}
ht' : t' ∈ {s | MeasurableSet s}
⊢ t' ∈ {s | MeasurableSet s}

Tactic:
· induction t', ht' using generateFrom_induction with
    | hC s hs => exact hs ▸ ht
    | empty => exact @MeasurableSet.empty _ m₂
    | compl u _ hu => exact hu.compl
    | iUnion f _ hf => exact .iUnion hf

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

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

Tactic:
simp [← evariance_lt_top_iff_memLp hX]

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

Goal state before:
pp: case iSup
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ ⨆ n, ∫⁻ (a : Ω), f a * f' n a ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), ⨆ n, f' n ω ∂μ

pp: case iSup.hf
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ ∀ (n : ℕ), Measurable fun ω ↦ f ω * f' n ω

pp: case iSup.h_mono
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ Monotone fun i ω ↦ f ω * f' i ω

Tactic:
lintegral_iSup h_measM_f' h_mono_f',

Goal state after:
case iSup
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ ⨆ n, ∫⁻ (a : Ω), f a * f' n a ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ⨆ n, ∫⁻ (a : Ω), f' n a ∂μ

case iSup.hf
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ ∀ (n : ℕ), Measurable fun ω ↦ f ω * f' n ω

case iSup.h_mono
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf Mg mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
hMg : Mg ≤ mΩ
h_ind : Indep Mf Mg μ
h_meas_f : Measurable f
h_measM_f : Measurable f
f' : ℕ → Ω → ℝ≥0∞
h_meas_f' : ∀ (n : ℕ), Measurable (f' n)
h_mono_f' : Monotone f'
h_ind_f' : ∀ (n : ℕ), ∫⁻ (ω : Ω), f ω * f' n ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), f' n ω ∂μ
h_measM_f' : ∀ (n : ℕ), Measurable (f' n)
⊢ Monotone fun i ω ↦ f ω * f' i ω
Module: Mathlib.Probability.Moments.Variance

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

Tactic:
pow_two

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