mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : ⇑κ =ᵐ[μ] ⇑η
a✝² : Finset ι
a✝¹ : ι → Set Ω
a✝ : ∀ i ∈ a✝², a✝¹ i ∈ π i
h' : ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (η a) (a✝¹ i)
a : α
ha : κ a = η a
h'a : (η a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (η a) (a✝¹ i)
⊢ (κ a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (κ a) (a✝¹ i)

Tactic:
simpa using

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : ⇑κ =ᵐ[μ] ⇑η
a✝² : Finset ι
a✝¹ : ι → Set Ω
a✝ : ∀ i ∈ a✝², a✝¹ i ∈ π i
h' : ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (η a) (a✝¹ i)
a : α
ha : κ a = η a
h'a : (η a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (η a) (a✝¹ i)
⊢ (η a) (⋂ i ∈ a✝², a✝¹ i) = ∏ x ∈ a✝², (η a) (a✝¹ x)
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : ⇑κ =ᵐ[μ] ⇑η
a✝³ a✝² : Set Ω
a✝¹ : a✝³ ∈ s1
a✝ : a✝² ∈ s2
h' : ∀ᵐ (a : α) ∂μ, (κ a) (a✝³ ∩ a✝²) = (κ a) a✝³ * (κ a) a✝²
a : α
ha : κ a = η a
h'a : (κ a) (a✝³ ∩ a✝²) = (κ a) a✝³ * (κ a) a✝²
⊢ (η a) (a✝³ ∩ a✝²) = (η a) a✝³ * (η a) a✝²

Tactic:
simpa using

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : ⇑κ =ᵐ[μ] ⇑η
a✝³ a✝² : Set Ω
a✝¹ : a✝³ ∈ s1
a✝ : a✝² ∈ s2
h' : ∀ᵐ (a : α) ∂μ, (κ a) (a✝³ ∩ a✝²) = (κ a) a✝³ * (κ a) a✝²
a : α
ha : κ a = η a
h'a : (κ a) (a✝³ ∩ a✝²) = (κ a) a✝³ * (κ a) a✝²
⊢ (η a) (a✝³ ∩ a✝²) = (η a) a✝³ * (η a) a✝²
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : ⇑κ =ᵐ[μ] ⇑η
a✝³ a✝² : Set Ω
a✝¹ : a✝³ ∈ s1
a✝ : a✝² ∈ s2
h' : ∀ᵐ (a : α) ∂μ, (η a) (a✝³ ∩ a✝²) = (η a) a✝³ * (η a) a✝²
a : α
ha : κ a = η a
h'a : (η a) (a✝³ ∩ a✝²) = (η a) a✝³ * (η a) a✝²
⊢ (κ a) (a✝³ ∩ a✝²) = (κ a) a✝³ * (κ a) a✝²

Tactic:
simpa using

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
s1 s2 : Set (Set Ω)
h : ⇑κ =ᵐ[μ] ⇑η
a✝³ a✝² : Set Ω
a✝¹ : a✝³ ∈ s1
a✝ : a✝² ∈ s2
h' : ∀ᵐ (a : α) ∂μ, (η a) (a✝³ ∩ a✝²) = (η a) a✝³ * (η a) a✝²
a : α
ha : κ a = η a
h'a : (η a) (a✝³ ∩ a✝²) = (η a) a✝³ * (η a) a✝²
⊢ (η a) (a✝³ ∩ a✝²) = (η a) a✝³ * (η a) a✝²
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case refine_2.inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ C, ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : μ s ≤ ENNReal.ofReal δ
this : ∀ (i : ℕ), s.indicator ((↑n)⁻¹ • f i) = (↑n)⁻¹ • s.indicator (f i)
hn : n ≠ 0
⊢ ∑ i ∈ Finset.range n, eLpNorm (s.indicator (f i)) p μ ≤ ↑n * ENNReal.ofReal ε

Tactic:
simpa using

Goal state after:
case refine_2.inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ C, ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : μ s ≤ ENNReal.ofReal δ
this : ∀ (i : ℕ), s.indicator ((↑n)⁻¹ • f i) = (↑n)⁻¹ • s.indicator (f i)
hn : n ≠ 0
⊢ ∑ i ∈ Finset.range n, eLpNorm (s.indicator (f i)) p μ ≤ ↑n * ENNReal.ofReal ε
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : iIndepSets π κ μ
a : α
ha : (κ a) (⋂ i ∈ ∅, univ) = ∏ i ∈ ∅, (κ a) univ
⊢ (κ a) univ = 1

Tactic:
simpa using

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : iIndepSets π κ μ
a : α
ha : (κ a) (⋂ i ∈ ∅, univ) = ∏ i ∈ ∅, (κ a) univ
⊢ (κ a) univ = 1
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : HasOuterApproxClosed Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
E_nullbdry : μ (frontier E) = 0
⊢ ↑μ (frontier ?m.34) = 0

Tactic:
simpa using

Goal state after:
Ω : Type u_1
ι : Type u_2
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : HasOuterApproxClosed Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
μs_lim : Tendsto μs L (𝓝 μ)
E : Set Ω
E_nullbdry : μ (frontier E) = 0
⊢ ↑μ (frontier ?m.34) = 0
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 \ {i | 0 < μ (frontier (Metric.thickening i s))})
⊢ ∃ r ∈ Ioo a b, μ (frontier (Metric.thickening r s)) = 0

Tactic:
simpa using

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, (a < r ∧ r < b) ∧ μ (frontier (Metric.thickening r s)) = 0
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
inst✝¹ : Subsingleton ι
m : ι → Set (Set Ω)
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ m i
⊢ s = ∅ ∨ ∃ i, s = {i}

Tactic:
simpa using

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
inst✝¹ : Subsingleton ι
m : ι → Set (Set Ω)
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ m i
⊢ s = ∅ ∨ ∃ i, s = {i}
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: case refine_3.inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ Finset.range n, eLpNorm (f i) p μ ≤ ↑n * ↑C

Tactic:
simpa using

Goal state after:
case refine_3.inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ℕ), eLpNorm (f i) p μ ≤ ↑C
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ Finset.range n, eLpNorm (f i) p μ ≤ ↑n * ↑C
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : κ → α → β
g : α → β
hUI : UniformIntegrable f p μ
htends : TendstoInMeasure μ f u g
⊢ MemLp g p μ

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : κ → α → β
g : α → β
hUI : UniformIntegrable f p μ
htends : TendstoInMeasure μ f u g
⊢ MemLp g p μ
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π κ μ
s : Finset ι'
f : ι' → Set Ω
hf : ∀ i ∈ s, f i ∈ (π ∘ g) i
f' : ι → Set Ω := Function.extend g f fun x ↦ ∅
f'_apply : ∀ (x : ι'), f' (g x) = f x
hf' : ∀ i ∈ Finset.image g s, f' i ∈ π i
a : α
ha : (κ a) (⋂ i ∈ Finset.image g s, f' i) = ∏ i ∈ Finset.image g s, (κ a) (f' i)
⊢ (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)

Tactic:
simpa using

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
ι' : Type u_5
g : ι' → ι
hg : Function.Injective g
h : iIndepSets π κ μ
s : Finset ι'
f : ι' → Set Ω
hf : ∀ i ∈ s, f i ∈ (π ∘ g) i
f' : ι → Set Ω := Function.extend g f fun x ↦ ∅
f'_apply : ∀ (x : ι'), f' (g x) = f x
hf' : ∀ i ∈ Finset.image g s, f' i ∈ π i
a : α
ha : (κ a) (⋂ i ∈ Finset.image g s, f' i) = ∏ i ∈ Finset.image g s, (κ a) (f' i)
⊢ (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : κ → α → β
g : α → β
hUI : UniformIntegrable f p μ
htends : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
⊢ MemLp g p μ

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : κ → α → β
g : α → β
hUI : UniformIntegrable f p μ
htends : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) u (𝓝 (g x))
⊢ MemLp g p μ
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s₁ s₂ : Set (Set Ω)
h : IndepSets s₁ s₂ κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₂
ht2 : t2 ∈ s₁
a : α
ha : (κ a) (t2 ∩ t1) = (κ a) t2 * (κ a) t1
⊢ (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
Set.inter_comm,

Goal state after:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s₁ s₂ : Set (Set Ω)
h : IndepSets s₁ s₂ κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₂
ht2 : t2 ∈ s₁
a : α
ha : (κ a) (t2 ∩ t1) = (κ a) t2 * (κ a) t1
⊢ (κ a) (t2 ∩ t1) = (κ a) t1 * (κ a) t2
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
π : ι → Set (Set Ω)
x✝ : MeasurableSpace Ω
μ : Measure Ω
h : iIndepSets π μ
⊢ μ univ = 1

Tactic:
simpa using

Goal state after:
Ω : Type u_1
ι : Type u_2
π : ι → Set (Set Ω)
x✝ : MeasurableSpace Ω
μ : Measure Ω
h : iIndepSets π μ
⊢ μ univ = 1
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
_mΩ : MeasurableSpace Ω
s t : Set Ω
μ : Measure Ω
h : IndepSet s t μ
⊢ μ (s ∩ t) = μ s * μ t

Tactic:
simpa using

Goal state after:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
s t : Set Ω
μ : Measure Ω
h : IndepSet s t μ
⊢ μ (s ∩ t) = μ s * μ t
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : ι → Set Ω
h : iIndepSet f μ
s : Finset ι
⊢ μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)

Tactic:
simpa using

Goal state after:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : ι → Set Ω
h : iIndepSet f μ
s : Finset ι
⊢ μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h : iIndepFun f μ
⊢ μ univ = 1

Tactic:
simpa using

Goal state after:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h : iIndepFun f μ
⊢ μ univ = 1
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : 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}
t : Set Ω
ht : MeasurableSet t
iht : ∀ᵐ (a : α) ∂μ, (κ a) (t ∩ t2) = (κ a) t * (κ a) t2
a : α
ha : (κ a) (t ∩ t2) = (κ a) t * (κ a) t2
this : tᶜ ∩ t2 = t2 \ (t ∩ t2)
⊢ (κ a) t2 - (κ a) (t2 ∩ t) = (κ a) tᶜ * (κ a) t2

Tactic:
Set.inter_comm,

Goal state after:
α : 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}
t : Set Ω
ht : MeasurableSet t
iht : ∀ᵐ (a : α) ∂μ, (κ a) (t ∩ t2) = (κ a) t * (κ a) t2
a : α
ha : (κ a) (t ∩ t2) = (κ a) t * (κ a) t2
this : tᶜ ∩ t2 = t2 \ (t ∩ t2)
⊢ (κ a) t2 - (κ a) (t ∩ t2) = (κ a) tᶜ * (κ a) t2
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : 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 : α
ha : ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
⊢ (κ a) ((⋃ i, f i) ∩ t2) = (κ a) (⋃ i, f i) * (κ a) t2

Tactic:
Set.inter_comm,

Goal state after:
α : 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 : α
ha : ∀ (i : ℕ), (κ a) (f i ∩ t2) = (κ a) (f i) * (κ a) t2
⊢ (κ a) (t2 ∩ ⋃ i, f i) = (κ a) (⋃ i, f i) * (κ a) t2
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
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → μ (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, μ (f i ⁻¹' sets i)
this : IsProbabilityMeasure μ
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' : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (h' i)
⊢ μ (⋂ i, f i ⁻¹' h' i) = ∏ i, μ (f i ⁻¹' h' i)

Tactic:
simpa using

Goal state after:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : Fintype ι
β : ι → Type u_11
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), AEMeasurable (f i) μ
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → μ (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, μ (f i ⁻¹' sets i)
this : IsProbabilityMeasure μ
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' : (i : ι) → Set (β i)
hm : ∀ (i : ι), MeasurableSet (h' i)
⊢ μ (⋂ i, f i ⁻¹' h' i) = ∏ i, μ (f i ⁻¹' h' i)
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)).real F) L ≤ (↑μ).real F
⊢ ∀ (F : Set Ω), IsClosed[inst✝²] F → limsup (fun i ↦ (μs i) F) L ≤ μ F

Tactic:
simpa using

Goal state after:
Ω : 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)).real F) L ≤ (↑μ).real F
⊢ ∀ (F : Set Ω), IsClosed[inst✝²] F → limsup (fun i ↦ (μs i) F) L ≤ μ F
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: case neg
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
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 : ∀ i ∉ s, μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
this : IsProbabilityMeasure μ
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
hi : i ∉ s
⊢ MeasurableSet (Y i ⁻¹' t i)

Tactic:
exact ⟨.univ ×ˢ t i, MeasurableSet.univ.prod (ht _), by ext; simp⟩

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

Goal state before:
pp: case a
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
t : ι → Set β
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hy : ∀ (i : ι), μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, MeasurableSet (f i)
i : ι
hi : i ∈ s
⊢ μ[f i | ⋂ i, Y i ⁻¹' t i] = μ[f i | Y i ⁻¹' t i]

Tactic:
simpa using

Goal state after:
case a
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
t : ι → Set β
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun i ω ↦ (X i ω, Y i ω)) μ
hy : ∀ (i : ι), μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, MeasurableSet (f i)
i : ι
hi : i ∈ s
⊢ μ[f i | ⋂ i, Y i ⁻¹' t i] = μ[f i | Y i ⁻¹' t i]
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case inl
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → Measure Ω
ν : Measure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ s ∈ S, Tendsto (fun i ↦ (μ i).real s) l (𝓝 (ν.real s))
hν : ∀ s ∈ S, ν s ≠ ∞
hμ : ∀ s ∈ S, ∀ (i : ι), (μ i) s ≠ ∞
A : ∀ (i : ι), (μ i).real (⋃ s ∈ t, s) = ∑ u ∈ t.powerset with u.Nonempty, (-1) ^ (#u + 1) * (μ i).real (⋂ s ∈ u, s)
u : Finset (Set Ω)
hu : u ⊆ t ∧ u.Nonempty
h'u : ⋂ s ∈ u, s = ∅
⊢ Tendsto (fun x ↦ (μ x).real (⋂ s ∈ u, s)) l (𝓝 (ν.real (⋂ i ∈ u, i)))

Tactic:
simpa using

Goal state after:
case inl
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → Measure Ω
ν : Measure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ s ∈ S, Tendsto (fun i ↦ (μ i).real s) l (𝓝 (ν.real s))
hν : ∀ s ∈ S, ν s ≠ ∞
hμ : ∀ s ∈ S, ∀ (i : ι), (μ i) s ≠ ∞
A : ∀ (i : ι), (μ i).real (⋃ s ∈ t, s) = ∑ u ∈ t.powerset with u.Nonempty, (-1) ^ (#u + 1) * (μ i).real (⋂ s ∈ u, s)
u : Finset (Set Ω)
hu : u ⊆ t ∧ u.Nonempty
h'u : ⋂ s ∈ u, s = ∅
⊢ Tendsto (fun x ↦ 0) l (𝓝 0)
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ s ∈ S, Tendsto (fun i ↦ (μ i) s) l (𝓝 (ν s))
⊢ ∀ s ∈ S, Tendsto (fun i ↦ (↑(μ i)).real s) l (𝓝 ((↑ν).real s))

Tactic:
simpa using

Goal state after:
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ s ∈ S, Tendsto (fun i ↦ (μ i) s) l (𝓝 (ν s))
⊢ ∀ s ∈ S, Tendsto (fun a ↦ (μ a) s) l (𝓝 (ν s))
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
G : Type u_2
mΩ : MeasurableSpace Ω
ℙ : Measure Ω
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
X Y : Ω → G
inst✝² : SFinite μ
inst✝¹ : HasPDF X ℙ μ
inst✝ : HasPDF Y ℙ μ
σX : SigmaFinite (map X ℙ)
σY : SigmaFinite (map Y ℙ)
hXY : X ⟂ᵢ[ℙ] Y
⊢ HasPDF (X * Y) ℙ μ

Tactic:
by
  have : AEMeasurable X ℙ := HasPDF.aemeasurable' μ
  have : AEMeasurable Y ℙ := HasPDF.aemeasurable' μ
  rw [hasPDF_iff_of_aemeasurable (by fun_prop),
    hXY.map_mul_eq_map_mconv_map₀' (by fun_prop) (by fun_prop) σX σY]
  refine ⟨?_, mconv_absolutelyContinuous HasPDF.absolutelyContinuous⟩
  apply HaveLebesgueDecomposition.mconv <;> exact HasPDF.absolutelyContinuous

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ s ∈ S, Tendsto (fun i ↦ (μ i) s) l (𝓝 (ν s))
this : Tendsto (fun i ↦ (↑(μ i)).real (⋃ s ∈ t, s)) l (𝓝 ((↑ν).real (⋃ s ∈ t, s)))
⊢ Tendsto (fun i ↦ (μ i) (⋃ s ∈ t, s)) l (𝓝 (ν (⋃ s ∈ t, s)))

Tactic:
simpa using

Goal state after:
Ω : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace Ω
S : Set (Set Ω)
hS : IsPiSystem S
μ : ι → ProbabilityMeasure Ω
ν : ProbabilityMeasure Ω
l : Filter ι
t : Finset (Set Ω)
ht : ∀ s ∈ t, s ∈ S
hmeas : ∀ s ∈ S, MeasurableSet s
h : ∀ s ∈ S, Tendsto (fun i ↦ (μ i) s) l (𝓝 (ν s))
this : Tendsto (fun i ↦ (↑(μ i)).real (⋃ s ∈ t, s)) l (𝓝 ((↑ν).real (⋃ s ∈ t, s)))
⊢ Tendsto (fun i ↦ (μ i) (⋃ s ∈ t, s)) l (𝓝 (ν (⋃ s ∈ t, s)))