mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Portmanteau

Goal state before:
pp: case h
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h₂ : ∀ (F : Set Ω), IsCompact F → limsup (fun x ↦ (μs x) F) L ≤ μ F
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
ε : ℝ≥0
hε : 0 < ε
x✝ : ↑(μ F) < ∞
K : Set Ω
hKc : IsCompact K
hK_le : ∀ μ ∈ range (ProbabilityMeasure.toMeasure ∘ μs), μ Kᶜ ≤ ↑ε
i : ι
⊢ ↑(μs i) (F ∩ K) + ↑(μs i) (F \ K) ≤ ↑(μs i) (F ∩ K) + ↑ε

Tactic:
]

Goal state after:
case h
Ω : Type u_1
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ι → ProbabilityMeasure Ω
L : Filter ι
inst✝ : L.IsCountablyGenerated
h₁ : IsTightMeasureSet (range (ProbabilityMeasure.toMeasure ∘ μs))
h₂ : ∀ (F : Set Ω), IsCompact F → limsup (fun x ↦ (μs x) F) L ≤ μ F
h✝ : L.NeBot
F : Set Ω
hF_closed : IsClosed[inst✝²] F
ε : ℝ≥0
hε : 0 < ε
x✝ : ↑(μ F) < ∞
K : Set Ω
hKc : IsCompact K
hK_le : ∀ μ ∈ range (ProbabilityMeasure.toMeasure ∘ μs), μ Kᶜ ≤ ↑ε
i : ι
⊢ ↑(μs i) (F ∩ K) + ↑(μs i) (F \ K) ≤ ↑(μs i) (F ∩ K) + ↑ε
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: ι : 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, Y i ⁻¹' t i) ∩ ⋂ i, if i ∈ s then f i else univ) = (⋂ i, Y i ⁻¹' t i) ∩ ⋂ i, if i ∈ s then f i else univ

Tactic:
]

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

Goal state before:
pp: case refine_2
α : 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
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u → (μ ⊗ₘ κ.map fun ω ↦ (f ω, g ω)) (s ×ˢ t ×ˢ u) = (μ ⊗ₘ (κ.map f ×ₖ κ.map g)) (s ×ˢ t ×ˢ u)
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)

Tactic:
]

Goal state after:
case refine_2
α : 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
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u → (μ ⊗ₘ κ.map fun ω ↦ (f ω, g ω)) (s ×ˢ t ×ˢ u) = (μ ⊗ₘ (κ.map f ×ₖ κ.map g)) (s ×ˢ t ×ˢ u)
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: ι : 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, μ (Y i ⁻¹' t i))⁻¹ * μ (⋂ i, g i) = (∏ i, μ (Y i ⁻¹' t i))⁻¹ * μ (⋂ i, g i)

pp: ι : 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 : ι), MeasurableSet (Y i ⁻¹' t i)

Tactic:
]

Goal state after:
ι : 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 : ι), MeasurableSet (Y i ⁻¹' t i)
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : ↑p1 ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : ↑p2 ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : ι → Set Ω := fun i ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
hgm : ∀ i ∈ p1 ∪ p2, g i ∈ s i
h_p1_inter_p2 :
  (⋂ x ∈ p1, f1 x) ∩ ⋂ x ∈ p2, f2 x = ⋂ i ∈ p1 ∪ p2, (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
a : α
ha : (κ a) (⋂ i ∈ p1 ∪ p2, g i) = ∏ i ∈ p1 ∪ p2, (κ a) (g i)
⊢ (κ a) (⋂ i ∈ p1 ∪ p2, (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ) = (κ a) (⋂ i ∈ p1 ∪ p2, g i)

Tactic:
]

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

Goal state before:
pp: ι : 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, μ (Y i ⁻¹' t i))⁻¹ * ∏ i, μ (g i) = (∏ i, μ (Y i ⁻¹' t i))⁻¹ * ∏ i, μ (g i)

pp: ι : 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 : ι), MeasurableSet (g i)

Tactic:
]

Goal state after:
ι : 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 : ι), MeasurableSet (g i)
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case refine_2.refine_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 < ⊤
⊢ ∫⁻ (x : α) in u, (κ x) (f ⁻¹' s ∩ g ⁻¹' t) ∂μ = ∫⁻ (x : α) in u, (κ x) (f ⁻¹' s) * (κ x) (g ⁻¹' t) ∂μ

Tactic:
]

Goal state after:
case refine_2.refine_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 < ⊤
⊢ ∫⁻ (x : α) in u, (κ x) (f ⁻¹' s ∩ g ⁻¹' t) ∂μ = ∫⁻ (x : α) in u, (κ x) (f ⁻¹' s) * (κ x) (g ⁻¹' t) ∂μ
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case e'_2
α : 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) = ((κ.map fun ω ↦ (f ω, g ω)) ω) (s ×ˢ t)

Tactic:
map_apply' _ (by fun_prop) _ (hs.prod ht),

Goal state after:
case e'_2
α : 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) = (κ ω) ((fun ω ↦ (f ω, g ω)) ⁻¹' s ×ˢ t)
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: case e'_2
α : 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)

Tactic:
]

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) * (κ ω) (g ⁻¹' t)

Tactic:
]

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

Goal state before:
pp: ι : 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, (μ (Y i ⁻¹' t i))⁻¹) * ∏ i, μ (g i) = (∏ x, (μ (Y x ⁻¹' t x))⁻¹) * ∏ x, μ (g x)

pp: ι : 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'
⊢ (↑Finset.univ).Pairwise fun i j ↦ μ (Y i ⁻¹' t i) ≠ 0 ∨ μ (Y j ⁻¹' t j) ≠ ∞

Tactic:
]

Goal state after:
ι : 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'
⊢ (↑Finset.univ).Pairwise fun i j ↦ μ (Y i ⁻¹' t i) ≠ 0 ∨ μ (Y j ⁻¹' t j) ≠ ∞
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
⊢ generateFrom ((preimage fun a i ↦ f (↑i) a) '' univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}) = generateFrom πS

Tactic:
]

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
⊢ generateFrom ((preimage fun a i ↦ f (↑i) a) '' univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}) = generateFrom πS
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: ι : 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 Ω},
    (∀ i ∈ s, MeasurableSet (f' i)) → μ[⋂ i ∈ s, f' i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, μ[f' i | ⋂ i, Y i ⁻¹' t i]

Tactic:
]

Goal state after:
ι : 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 Ω},
    (∀ i ∈ s, MeasurableSet (f' i)) → μ[⋂ i ∈ s, f' i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, μ[f' i | ⋂ i, Y i ⁻¹' t i]
Module: Mathlib.Probability.Independence.Kernel.IndepFun

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
⊢ generateFrom ((preimage fun a i ↦ f (↑i) a) '' univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}) = generateFrom πT

Tactic:
]

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : ↥S) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : ↥T) → β ↑i)) := univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
⊢ generateFrom ((preimage fun a i ↦ f (↑i) a) '' univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}) = generateFrom π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 ω ∂↑μ))
room₂ : ∫ (a : Ω), fs M a ∂↑μ < ∫ (a : Ω), fs M a ∂↑μ + ε / 2
x : γ
hx : ∫ (ω : Ω), fs M ω ∂↑(μs x) ≤ ∫ (a : Ω), fs M a ∂↑μ + ε / 2
⊢ ∫ (x : Ω), s.indicator 1 x ∂↑(μs x) ≤ ∫ (ω : Ω), fs M ω ∂↑(μs x)

Tactic:
]

Goal state after:
γ : 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 ω ∂↑μ))
room₂ : ∫ (a : Ω), fs M a ∂↑μ < ∫ (a : Ω), fs M a ∂↑μ + ε / 2
x : γ
hx : ∫ (ω : Ω), fs M ω ∂↑(μs x) ≤ ∫ (a : Ω), fs M a ∂↑μ + ε / 2
⊢ ∫ (x : Ω), s.indicator 1 x ∂↑(μs x) ≤ ∫ (ω : Ω), fs M ω ∂↑(μs x)
Module: Mathlib.Probability.Independence.Basic

Goal state before:
pp: Ω : Type u_7
mΩ : MeasurableSpace Ω
μ : Measure Ω
M : Type u_10
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
f g : Ω → M
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (Measure.map f μ)
σg : SigmaFinite (Measure.map g μ)
hfg : f ⟂ᵢ[μ] g
⊢ Measure.map (fun p ↦ p.1 * p.2) ((Measure.map f μ).prod (Measure.map g μ)) =
    Measure.map (fun x ↦ x.1 * x.2) ((Measure.map f μ).prod (Measure.map g μ))

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
⊢ AEMeasurable X ℙ ∧ (map X ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ≪ μ ↔
    (map X ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ≪ μ

Tactic:
]

Goal state after:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
⊢ AEMeasurable X ℙ ∧ (map X ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ≪ μ ↔
    (map X ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ≪ μ
Module: Mathlib.Probability.Density

Goal state before:
pp: case refine_1
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ (μ.withDensity f).HaveLebesgueDecomposition μ

Tactic:
]

Goal state after:
case refine_1
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ (μ.withDensity f).HaveLebesgueDecomposition μ
Module: Mathlib.Probability.Density

Goal state before:
pp: case refine_2
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ μ.withDensity f ≪ μ

Tactic:
]

Goal state after:
case refine_2
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ μ.withDensity f ≪ μ
Module: Mathlib.Probability.Density

Goal state before:
pp: case refine_1
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ (μ.withDensity (AEMeasurable.mk f hf)).HaveLebesgueDecomposition μ

Tactic:
]

Goal state after:
case refine_1
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : AEMeasurable X ℙ
f : E → ℝ≥0∞
hf : AEMeasurable f μ
h : map X ℙ = μ.withDensity f
⊢ (μ.withDensity (AEMeasurable.mk f hf)).HaveLebesgueDecomposition μ
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : ¬AEMeasurable X ℙ
⊢ rnDeriv 0 μ =ᵐ[μ] 0

Tactic:
]

Goal state after:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : ¬AEMeasurable X ℙ
⊢ rnDeriv 0 μ =ᵐ[μ] 0
Module: Mathlib.Probability.Density

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
hX : HasPDF X ℙ μ
⊢ map X ℙ = map X ℙ

Tactic:
]

Goal state after: