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

Goal state before:
pp: case a
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
congr
        · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_negPart_neg _ _ hr, singularPart_smul]

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real

Goal state before:
pp: case pos.refine_2.refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f μ
h : 0 < μ {x | ↑R < |μ[f | m] x|}
⊢ MeasurableSet {x | ↑R < ‖μ[f | m] x‖}

Tactic:
exact @measurableSet_lt _ _ _ _ _ m _ _ _ _ _ measurable_const
      stronglyMeasurable_condExp.norm.measurable

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

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i ↦ ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : ⇑f₀ = NNReal.toReal ∘ ⇑f
f₀_nn : 0 ≤ ⇑f₀
f₀_ae_nn : 0 ≤ᵐ[↑μ] ⇑f₀
⊢ Tendsto (fun n ↦ (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal)

Tactic:
have f₀_ae_nns : ∀ i, 0 ≤ᵐ[(μs i : Measure Ω)] ⇑f₀ := fun i ↦ .of_forall f₀_nn

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i ↦ ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : ⇑f₀ = NNReal.toReal ∘ ⇑f
f₀_nn : 0 ≤ ⇑f₀
f₀_ae_nn : 0 ≤ᵐ[↑μ] ⇑f₀
f₀_ae_nns : ∀ (i : γ), 0 ≤ᵐ[↑(μs i)] ⇑f₀
⊢ Tendsto (fun n ↦ (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal)
Module: Mathlib.MeasureTheory.Measure.Tight

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst✝³ : TopologicalSpace 𝓧
inst✝² : T2Space 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegular
s : Set 𝓧
hs : MeasurableSet s
r : ENNReal
⊢ r < μ s → ∃ K ⊆ s, (fun s ↦ IsCompact s ∧ IsClosed[inst✝³] s) K ∧ r < μ K

Tactic:
hr

Goal state after:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst✝³ : TopologicalSpace 𝓧
inst✝² : T2Space 𝓧
inst✝¹ : OpensMeasurableSpace 𝓧
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegular
s : Set 𝓧
hs : MeasurableSet s
r : ENNReal
hr : r < μ s
⊢ ∃ K ⊆ s, (fun s ↦ IsCompact s ∧ IsClosed[inst✝³] s) K ∧ r < μ K
Module: Mathlib.MeasureTheory.Measure.FiniteMeasure

Goal state before:
pp: case refine_1.refine_2
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
γ : Type u_2
𝕜 : Type u_3
inst✝ : RCLike 𝕜
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i ↦ ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))
f : Ω →ᵇ 𝕜
⊢ Tendsto (fun i ↦ ↑(∫ (x : Ω), RCLike.im (f x) ∂↑(μs i)) * RCLike.I) F
    (𝓝 (↑(∫ (x : Ω), RCLike.im (f x) ∂↑μ) * RCLike.I))

Tactic:
· exact (Tendsto.comp (RCLike.continuous_ofReal.tendsto _)
        (h (f.comp RCLike.im RCLike.lipschitzWith_im))).mul_const _

Goal state after:
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 [ha] using h'a

Goal state after:
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 [ha] using h'a

Goal state after:
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 [ha] using h'a

Goal state after:
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 [ha] using h'a

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsZeroOrMarkovKernel κ
hf : Measurable f
hg : Measurable g
⊢ (∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)) ↔
    ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ

Tactic:
constructor <;> intro h s t hs ht <;> specialize h s t hs ht

Goal state after:
case mp
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsZeroOrMarkovKernel κ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set β'
h : ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
hs : MeasurableSet s
ht : MeasurableSet t
⊢ IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ

case mpr
α : Type u_1
Ω : Type u_2
β : Type u_4
β' : Type u_5
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsZeroOrMarkovKernel κ
hf : Measurable f
hg : Measurable g
s : Set β
t : Set β'
h : IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ
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_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : ι → Type u_10
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) μ
⊢ ∀ (i : ι), AEMeasurable (f i) (⇑(Kernel.const Unit μ) ∘ₘ Measure.dirac ())

Tactic:
by simp [hf_meas]

Goal state after:
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
hf_Indep : iIndepFun f μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) μ
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ ∀ (i : ι), AEMeasurable (f i) (⇑(Kernel.const Unit μ) ∘ₘ Measure.dirac ())

Tactic:
by simp [hf_meas]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_10
m : MeasurableSpace β
inst✝¹ : Mul β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun f μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) μ
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ ∀ (i : ι), AEMeasurable (f i) (⇑(Kernel.const Unit μ) ∘ₘ Measure.dirac ())

Tactic:
by simp [hf_meas]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_10
m : MeasurableSpace β
inst✝¹ : Mul β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun f μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) μ
i j k : ι
hij : i ≠ j
hik : i ≠ k
⊢ ∀ (i : ι), AEMeasurable (f i) (⇑(Kernel.const Unit μ) ∘ₘ Measure.dirac ())

Tactic:
by simp [hf_meas]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_10
m : MeasurableSpace β
inst✝¹ : Mul β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_indep : iIndepFun f μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) μ
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
⊢ ∀ (i : ι), AEMeasurable (f i) (⇑(Kernel.const Unit μ) ∘ₘ Measure.dirac ())

Tactic:
by simp [hf_meas]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_10
m : MeasurableSpace β
inst✝¹ : Div β
inst✝ : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun f μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) μ
i j k : ι
hik : i ≠ k
hjk : j ≠ k
⊢ ∀ (i : ι), AEMeasurable (f i) (⇑(Kernel.const Unit μ) ∘ₘ Measure.dirac ())

Tactic:
by simp [hf_meas]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_10
m : MeasurableSpace β
inst✝¹ : Div β
inst✝ : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun f μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) μ
i j k : ι
hij : i ≠ j
hik : i ≠ k
⊢ ∀ (i : ι), AEMeasurable (f i) (⇑(Kernel.const Unit μ) ∘ₘ Measure.dirac ())

Tactic:
by simp [hf_meas]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_10
m : MeasurableSpace β
inst✝¹ : Div β
inst✝ : MeasurableDiv₂ β
f : ι → Ω → β
hf_indep : iIndepFun f μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) μ
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
⊢ ∀ (i : ι), AEMeasurable (f i) (⇑(Kernel.const Unit μ) ∘ₘ Measure.dirac ())

Tactic:
by simp [hf_meas]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
β : Type u_10
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun f μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) μ
s : Finset ι
i : ι
hi : i ∉ s
⊢ ∀ (i : ι), AEMeasurable (f i) (⇑(Kernel.const Unit μ) ∘ₘ Measure.dirac ())

Tactic:
by simp [hf_meas]

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 ∩ if i ∈ s then f i else univ) = g i

Tactic:
by_cases hi : i ∈ s <;> simp [hi, g]

Goal state after:
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
h_P_inter✝ : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
a : α
h_P_inter : (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
ha1 : (κ a) (⋂ i ∈ p1, f1 i) = ∏ i ∈ p1, (κ a) (f1 i)
ha2 : (κ a) (⋂ i ∈ p2, f2 i) = ∏ i ∈ p2, (κ a) (f2 i)
h' : IsProbabilityMeasure (κ a)
n : ι
⊢ (κ a) (g n) = (if n ∈ p1 then (κ a) (f1 n) else 1) * if n ∈ p2 then (κ a) (f2 n) else 1

Tactic:
dsimp only [g]

Goal state after:
α : 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
h_P_inter✝ : ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
a : α
h_P_inter : (κ a) (t1 ∩ t2) = ∏ n ∈ p1 ∪ p2, (κ a) (g n)
ha1 : (κ a) (⋂ i ∈ p1, f1 i) = ∏ i ∈ p1, (κ a) (f1 i)
ha2 : (κ a) (⋂ i ∈ p2, f2 i) = ∏ i ∈ p2, (κ a) (f2 i)
h' : IsProbabilityMeasure (κ a)
n : ι
⊢ (κ a) ((if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ) =
    (if n ∈ p1 then (κ a) (f1 n) else 1) * if n ∈ p2 then (κ a) (f2 n) else 1
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
⊢ MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πS

Tactic:
generateFrom_pi.symm,

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
⊢ MeasurableSpace.comap (fun a i ↦ f (↑i) a) (generateFrom (univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s})) =
    generateFrom πS
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
⊢ MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi = generateFrom πT

Tactic:
generateFrom_pi.symm,

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
⊢ MeasurableSpace.comap (fun a i ↦ f (↑i) a) (generateFrom (univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s})) =
    generateFrom πT
Module: Mathlib.Probability.Independence.Kernel.Indep

Goal state before:
pp: case inr.refine_2.refine_1
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
π : ι → Set (Set Ω)
h_pi : ∀ (n : ι), IsPiSystem (π n)
h_generate : ∀ (i : ι), m i = generateFrom (π i)
h_ind : iIndepSets π κ μ
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μ] ⇑η
hη : IsMarkovKernel η
s : Finset ι
f : ι → Set Ω
a : ι
S : Finset ι
ha_notin_S : a ∉ S
h_rec : (∀ i ∈ S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (η a) (f i)
hf_m : ∀ i ∈ insert a S, f i ∈ (fun x ↦ {s | MeasurableSet s}) i
hf_m_S : ∀ x ∈ S, MeasurableSet (f x)
p : Set (Set Ω) := piiUnionInter π ↑S
m_p : MeasurableSpace Ω := generateFrom p
hS_eq_generate : m_p = generateFrom p
h_indep : Indep m_p (m a) η μ
h_le_p : ∀ i ∈ S, m i ≤ m_p
h_S_f : ∀ i ∈ S, MeasurableSet (f i)
⊢ ⋂ n ∈ S, f n ∈ {s | MeasurableSet s}

Tactic:
exact S.measurableSet_biInter h_S_f

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

Goal state before:
pp: case empty
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ≥0∞
hX : iIndepFun X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
⊢ ∫⁻ (ω : Ω), ∏ i ∈ ∅, X i ω ∂μ = ∏ i ∈ ∅, ∫⁻ (ω : Ω), X i ω ∂μ

Tactic:
simp only [Finset.prod_empty, lintegral_const, measure_univ, mul_one]

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

Goal state before:
pp: case cons
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ≥0∞
hX : iIndepFun X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ ∫⁻ (ω : Ω), (X j * ∏ c ∈ s, X c) ω ∂μ = (∫⁻ (ω : Ω), X j ω ∂μ) * ∫⁻ (ω : Ω), (∏ c ∈ s, X c) ω ∂μ

Tactic:
apply lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'

Goal state after:
case cons.h_meas_f
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ≥0∞
hX : iIndepFun X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ AEMeasurable (X j) μ

case cons.h_meas_g
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ≥0∞
hX : iIndepFun X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ AEMeasurable (∏ c ∈ s, X c) μ

case cons.h_indep_fun
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ≥0∞
hX : iIndepFun X μ
x_mea : ∀ (i : ι), Measurable (X i)
this : IsProbabilityMeasure μ
j : ι
s : Finset ι
hj : j ∉ s
ihs : ∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
⊢ X j ⟂ᵢ[μ] ∏ c ∈ s, X c
Module: Mathlib.Probability.HasLaw

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
P : Measure Ω
X : Ω → 𝓧
hX : HasLaw X μ P
f : 𝓧 → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (ω : Ω), f (X ω) ∂P = ∫⁻ (x : 𝓧), f x ∂μ

Tactic:
rw [← hX.map_eq, lintegral_map' _ hX.aemeasurable]
  rwa [hX.map_eq]

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

Goal state before:
pp: ι : Type u_1
E : Type u_2
Ω' : Type u_3
Ω'' : Type u_4
m' : MeasurableSpace Ω'
μ' : Measure Ω'
inst✝⁵ : IsProbabilityMeasure μ'
m'' : MeasurableSpace Ω''
μ'' : Measure Ω''
inst✝⁴ : IsProbabilityMeasure μ''
mE : MeasurableSpace E
l : Filter ι
inst✝³ : SeminormedAddCommGroup E
inst✝² : SecondCountableTopology E
inst✝¹ : BorelSpace E
X : ι → Ω'' → E
inst✝ : l.IsCountablyGenerated
Y : ι → Ω'' → E
Z : Ω' → E
hXZ : TendstoInDistribution X l Z (fun x ↦ μ'') μ'
hXY : TendstoInMeasure μ'' (Y - X) l 0
hY : ∀ (i : ι), AEMeasurable (Y i) μ''
hZ : AEMeasurable Z μ'
hX : ∀ (i : ι), AEMeasurable (X i) μ''
hE : Nonempty E
x₀ : E := hE.some
F : E → ℝ
M : ℝ
hF_bounded : ∀ (x y : E), dist (F x) (F y) ≤ M
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
this : ∀ ε > 0, ∀ᶠ (n : ι) in l, |∫ (ω : E), F ω ∂Measure.map (Y n) μ'' - ∫ (ω : E), F ω ∂Measure.map Z μ'| < ↑L * ε
ε : ℝ
hε : ε > 0
x✝ : ι
⊢ ε = ↑L * (ε / ↑L)

Tactic:
field_simp

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
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✝ : ∀ᵐ (a : α) ∂μ, ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
val✝ : Fintype ι
g : ι → Set Ω := fun i' ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt✝ : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
hg✝ : ∀ (i : ι), MeasurableSet (g i)
a : α
hy : ∀ i ∉ s, (κ a) (Y i ⁻¹' t i) ≠ 0
a✝ : IsProbabilityMeasure (κ a)
hYt : (κ a) (⋂ i, Y i ⁻¹' t i) = ∏ i, (κ a) (Y i ⁻¹' t i)
hg : (κ a) (⋂ i, g i) = ∏ i, (κ a) (g i)
i : ι
⊢ (Y i ⁻¹' t i ∩ if i ∈ s then f i else univ) = g i

Tactic:
by_cases hi : i ∈ s <;> simp [hi, g]

Goal state after: