mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℝ
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
n : ι
a : Ω''
hF_bounded : dist (F (Y n a)) (F x₀) ≤ M
⊢ ‖F (Y n a)‖ - ‖F x₀‖ ≤ M

Tactic:
]

Goal state after:
ι : 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 : ℝ
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
n : ι
a : Ω''
hF_bounded : dist (F (Y n a)) (F x₀) ≤ M
⊢ ‖F (Y n a)‖ - ‖F x₀‖ ≤ M
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
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
i j k : ι
hik : i ≠ k
hjk : j ≠ k
h : IndepFun (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a)) (AEMeasurable.mk (f k) ⋯) κ μ
a : α
hi : ∀ᵐ (ω : Ω) ∂κ a, f i ω = AEMeasurable.mk (f i) ⋯ ω
hj : ∀ᵐ (ω : Ω) ∂κ a, f j ω = AEMeasurable.mk (f j) ⋯ ω
ω : Ω
hωi : f i ω = AEMeasurable.mk (f i) ⋯ ω
hωj : f j ω = AEMeasurable.mk (f j) ⋯ ω
⊢ (f i ω, f j ω) = (f i ω, f j ω)

Tactic:
]

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 : ℝ
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
a : Ω''
hF_bounded : dist (F (X n a)) (F x₀) ≤ M
⊢ ‖F (X n a)‖ - ‖F x₀‖ ≤ M

Tactic:
]

Goal state after:
ι : 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 : ℝ
L : NNReal
hF_lip : LipschitzWith L F
hF_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] F
hL : 0 < L
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
a : Ω''
hF_bounded : dist (F (X n a)) (F x₀) ≤ M
⊢ ‖F (X n a)‖ - ‖F x₀‖ ≤ M
Module: Mathlib.MeasureTheory.Function.FactorsThrough

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst✝¹ : MeasurableSpace Z
inst✝ : MeasurableSingletonClass Z
hg : Measurable g
x₁ x₂ : X
h : f x₁ = f x₂
s : Set Y
hs : f ⁻¹' s = g ⁻¹' {g x₂}
⊢ g x₂ = g x₂

Tactic:
]

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
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
h_int_X : Integrable (fun x ↦ F (X n x)) μ''
⊢ Integrable (fun a ↦ F (Y n a) - F (X n a)) μ''

Tactic:
]

Goal state after:
ι : 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
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
h_int_X : Integrable (fun x ↦ F (X n x)) μ''
⊢ Integrable (fun a ↦ F (Y n a) - F (X n a)) μ''
Module: Mathlib.MeasureTheory.Function.FactorsThrough

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g : X → Z
inst✝² : Nonempty Z
inst✝¹ : TopologicalSpace Z
inst✝ : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
t : Set Y
ht : MeasurableSet t
h₁ : Y → Z
mh₁ : StronglyMeasurable h₁
hg₁ : StronglyMeasurable (h₁ ∘ f)
h₂ : Y → Z
mh₂ : StronglyMeasurable h₂
hg₂ : StronglyMeasurable (h₂ ∘ f)
⊢ (f ⁻¹' t).piecewise (h₁ ∘ f) (h₂ ∘ f) = (f ⁻¹' t).piecewise (h₁ ∘ f) (h₂ ∘ f)

Tactic:
]

Goal state after:
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
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
h :
  IndepFun (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun a ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
a : α
hi : ∀ᵐ (ω : Ω) ∂κ a, f i ω = AEMeasurable.mk (f i) ⋯ ω
hj : ∀ᵐ (ω : Ω) ∂κ a, f j ω = AEMeasurable.mk (f j) ⋯ ω
ω : Ω
hωi : f i ω = AEMeasurable.mk (f i) ⋯ ω
hωj : f j ω = AEMeasurable.mk (f j) ⋯ ω
⊢ (f i ω, f j ω) = (f i ω, f j ω)

Tactic:
]

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

Goal state before:
pp: case lim
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g✝ : X → Z
inst✝² : Nonempty Z
inst✝¹ : TopologicalSpace Z
inst✝ : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g : ℕ → X → Z
i : X → Z
hg : ∀ (n : ℕ), StronglyMeasurable (g n)
hi : StronglyMeasurable i
h₂ : ∀ (x : X), Tendsto (fun x_1 ↦ g x_1 x) atTop (𝓝 (i x))
h : ℕ → Y → Z
mh : ∀ (n : ℕ), StronglyMeasurable (h n)
hh : ∀ (n : ℕ), g n = h n ∘ f
x : X
⊢ i x = ?m.209

pp: case lim
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g✝ : X → Z
inst✝² : Nonempty Z
inst✝¹ : TopologicalSpace Z
inst✝ : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g : ℕ → X → Z
i : X → Z
hg : ∀ (n : ℕ), StronglyMeasurable (g n)
hi : StronglyMeasurable i
h₂ : ∀ (x : X), Tendsto (fun x_1 ↦ g x_1 x) atTop (𝓝 (i x))
h : ℕ → Y → Z
mh : ∀ (n : ℕ), StronglyMeasurable (h n)
hh : ∀ (n : ℕ), g n = h n ∘ f
x : X
⊢ Tendsto (fun x_1 ↦ h x_1 (f x)) atTop (𝓝 ?m.209)

pp: X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g✝ : X → Z
inst✝² : Nonempty Z
inst✝¹ : TopologicalSpace Z
inst✝ : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := ⋯
g : ℕ → X → Z
i : X → Z
hg : ∀ (n : ℕ), StronglyMeasurable (g n)
hi : StronglyMeasurable i
h₂ : ∀ (x : X), Tendsto (fun x_1 ↦ g x_1 x) atTop (𝓝 (i x))
h : ℕ → Y → Z
mh : ∀ (n : ℕ), StronglyMeasurable (h n)
hh : ∀ (n : ℕ), g n = h n ∘ f
x : X
⊢ Z

Tactic:
]

Goal state after:
case lim
X : Type u_1
Y : Type u_2
Z : Type u_3
mY : MeasurableSpace Y
f : X → Y
g✝ : X → Z
inst✝² : Nonempty Z
inst✝¹ : TopologicalSpace Z
inst✝ : IsCompletelyMetrizableSpace Z
mX : MeasurableSpace X := MeasurableSpace.comap f mY
g : ℕ → X → Z
i : X → Z
hg : ∀ (n : ℕ), StronglyMeasurable (g n)
hi : StronglyMeasurable i
h₂ : ∀ (x : X), Tendsto (fun x_1 ↦ g x_1 x) atTop (𝓝 (i x))
h : ℕ → Y → Z
mh : ∀ (n : ℕ), StronglyMeasurable (h n)
hh : ∀ (n : ℕ), g n = h n ∘ f
x : X
⊢ Tendsto (fun x_1 ↦ h x_1 (f x)) atTop (𝓝 (i x))
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
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
h :
  IndepFun (fun a ↦ (AEMeasurable.mk (f i) ⋯ a, AEMeasurable.mk (f j) ⋯ a))
    (fun a ↦ (AEMeasurable.mk (f k) ⋯ a, AEMeasurable.mk (f l) ⋯ a)) κ μ
a : α
hk : ∀ᵐ (ω : Ω) ∂κ a, f k ω = AEMeasurable.mk (f k) ⋯ ω
hl : ∀ᵐ (ω : Ω) ∂κ a, f l ω = AEMeasurable.mk (f l) ⋯ ω
ω : Ω
hωk : f k ω = AEMeasurable.mk (f k) ⋯ ω
hωl : f l ω = AEMeasurable.mk (f l) ⋯ ω
⊢ (f k ω, f l ω) = (f k ω, f l ω)

Tactic:
]

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

Goal state before:
pp: case h₁
ι : 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
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
h_int_X : Integrable (fun x ↦ F (X n x)) μ''
h_int_sub : Integrable (fun a ↦ ‖F (Y n a) - F (X n a)‖) μ''
⊢ ‖∫ (a : Ω''), F (Y n a) - F (X n a) ∂μ''‖ ≤ ↑L * (ε / 2) + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖}

Tactic:
]

Goal state after:
case h₁
ι : 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
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
h_int_X : Integrable (fun x ↦ F (X n x)) μ''
h_int_sub : Integrable (fun a ↦ ‖F (Y n a) - F (X n a)‖) μ''
⊢ ‖∫ (a : Ω''), F (Y n a) - F (X n a) ∂μ''‖ ≤ ↑L * (ε / 2) + M * μ''.real {ω | ε / 2 ≤ ‖Y n ω - X n ω‖}
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 : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right : f i = (fun p ↦ p ⟨i, ⋯⟩) ∘ fun a j ↦ f (↑j) a
h_meas_right : Measurable fun p ↦ p ⟨i, ⋯⟩
a : Ω
⊢ ∏ j, f (↑j) a = ∏ c, f (↑c) a

Tactic:
]

Goal state after:
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 : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right : f i = (fun p ↦ p ⟨i, ⋯⟩) ∘ fun a j ↦ f (↑j) a
h_meas_right : Measurable fun p ↦ p ⟨i, ⋯⟩
a : Ω
this : ∏ j, f (↑j) a = (∏ j, f ↑j) a
⊢ (∏ j ∈ s, f j) a = (∏ i ∈ s, f i) a

Tactic:
]

Goal state after:
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 : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right : f i = (fun p ↦ p ⟨i, ⋯⟩) ∘ fun a j ↦ f (↑j) a
h_meas_right : Measurable fun p ↦ p ⟨i, ⋯⟩
h_left : ∏ j ∈ s, f j = (fun p ↦ ∏ j, p j) ∘ fun a j ↦ f (↑j) a
h_meas_left : Measurable fun p ↦ ∏ j, p j
⊢ IndepFun ((fun p ↦ ∏ j, p j) ∘ fun a j ↦ f (↑j) a) ((fun p ↦ p ⟨i, ⋯⟩) ∘ fun a j ↦ f (↑j) a) κ μ

Tactic:
]

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
s : Finset ι
i : ι
hi : i ∉ s
h_right : f i = (fun p ↦ p ⟨i, ⋯⟩) ∘ fun a j ↦ f (↑j) a
h_meas_right : Measurable fun p ↦ p ⟨i, ⋯⟩
h_left : ∏ j ∈ s, f j = (fun p ↦ ∏ j, p j) ∘ fun a j ↦ f (↑j) a
h_meas_left : Measurable fun p ↦ ∏ j, p j
⊢ IndepFun ((fun p ↦ ∏ j, p j) ∘ fun a j ↦ f (↑j) a) ((fun p ↦ p ⟨i, ⋯⟩) ∘ fun a j ↦ f (↑j) a) κ μ
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 : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
⊢ ∀ (i : ↥s), ∀ᵐ (a : α) ∂μ, f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯

Tactic:
]

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst✝¹ : CommMonoid β
inst✝ : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (f i) (⇑κ ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
⊢ ∀ (i : ↥s), ∀ᵐ (a : α) ∂μ, f ↑i =ᵐ[κ a] AEMeasurable.mk (f ↑i) ⋯
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 α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
⊢ ∀ (S : Finset ι) {sets : ι → Set β},
    (∀ i ∈ S, MeasurableSet (sets i)) →
      ∀ᵐ (a : α) ∂μ,
        (κ a) (⋂ i ∈ S, ((s i).indicator fun _ω ↦ 1) ⁻¹' sets i) =
          ∏ i ∈ S, (κ a) (((s i).indicator fun _ω ↦ 1) ⁻¹' sets i)

Tactic:
]

Goal state after:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
⊢ ∀ (S : Finset ι) {sets : ι → Set β},
    (∀ i ∈ S, MeasurableSet (sets i)) →
      ∀ᵐ (a : α) ∂μ,
        (κ a) (⋂ i ∈ S, ((s i).indicator fun _ω ↦ 1) ⁻¹' sets i) =
          ∏ i ∈ S, (κ a) (((s i).indicator fun _ω ↦ 1) ⁻¹' sets i)
Module: Mathlib.MeasureTheory.Function.Floor

Goal state before:
pp: R : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : OrderTopology R
inst✝² : MeasurableSpace R
inst✝¹ : IsStrictOrderedRing R
inst✝ : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet (⋃ m, (fun x ↦ x - ↑m) ⁻¹' (s ∩ Ico 0 1))

Tactic:
]

Goal state after:
R : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : OrderTopology R
inst✝² : MeasurableSpace R
inst✝¹ : IsStrictOrderedRing R
inst✝ : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet (⋃ m, (fun x ↦ x - ↑m) ⁻¹' (s ∩ Ico 0 1))
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
hm' : ∃ x ∈ s, ↑x i = m'
⊢ m' ≤ (fun i ↦ sSup ((fun f ↦ ↑f i) '' s)) j

Tactic:
]

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
hm' : ∃ x ∈ s, ↑x i = m'
⊢ m' ≤ (fun i ↦ sSup ((fun f ↦ ↑f i) '' s)) j
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : ↑f i = m'
⊢ ↑f i ≤ (fun i ↦ sSup ((fun f ↦ ↑f i) '' s)) j

Tactic:
]

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i j : ι
hij : i ≤ j
m' : MeasurableSpace Ω
f : Filtration ι m
hf_mem : f ∈ s
hfm' : ↑f i = m'
⊢ ↑f i ≤ (fun i ↦ sSup ((fun f ↦ ↑f i) '' s)) j
Module: Mathlib.MeasureTheory.Function.Floor

Goal state before:
pp: R : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorSemiring R
inst✝⁴ : TopologicalSpace R
inst✝³ : OrderTopology R
inst✝² : MeasurableSpace R
inst✝¹ : OpensMeasurableSpace R
inst✝ : IsStrictOrderedRing R
n : R
⊢ MeasurableSet (floor ⁻¹' {⌊n⌋₊})

Tactic:
rcases eq_or_ne ⌊n⌋₊ 0 with h | h <;> simp [h, Nat.preimage_floor_of_ne_zero, -floor_eq_zero]

Goal state after:
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
hm' : ∃ x ∈ s, ↑x i = m'
⊢ m' ≤ m

Tactic:
]

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
hm' : ∃ x ∈ s, ↑x i = m'
⊢ m' ≤ m
Module: Mathlib.Probability.Process.Filtration

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
f : Filtration ι m
left✝ : f ∈ s
hfm' : ↑f i = m'
⊢ ↑f i ≤ m

Tactic:
]

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝ : Preorder ι
s : Set (Filtration ι m)
i : ι
m' : MeasurableSpace Ω
f : Filtration ι m
left✝ : f ∈ s
hfm' : ↑f i = m'
⊢ ↑f i ≤ m
Module: Mathlib.MeasureTheory.Function.ConvergenceInDistribution

Goal state before:
pp: case h₂
ι : 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
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
h_int_X : Integrable (fun x ↦ F (X n x)) μ''
h_int_sub : Integrable (fun a ↦ ‖F (Y n a) - F (X n a)‖) μ''
a : Ω''
⊢ dist (F (Y n a)) (F (X n a)) ≤ M

Tactic:
]

Goal state after:
case h₂
ι : 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
ε : ℝ
hε : ε > 0
n : ι
h_int_Y : Integrable (fun x ↦ F (Y n x)) μ''
h_int_X : Integrable (fun x ↦ F (X n x)) μ''
h_int_sub : Integrable (fun a ↦ ‖F (Y n a) - F (X n a)‖) μ''
a : Ω''
⊢ dist (F (Y n a)) (F (X n a)) ≤ M