mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Measurable ⇑prodAssoc

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y Z : SFinKer
⊢ Measurable ⇑prodAssoc.symm

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst✝⁹ : (t : T) → TopologicalSpace (F t)
inst✝⁸ : (t : T) → MeasurableSpace (F t)
inst✝⁷ : ∀ (t : T), BorelSpace (F t)
inst✝⁶ : ∀ (t : T), HasOuterApproxClosed (F t)
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst✝¹ : Fintype T
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω), (⇑f ∘ Z * ∏ t, ⇑(g t) ∘ Y t) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P
f : G →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
⊢ Measurable fun y ↦ ∏ j, (g j) (y j)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
f₁ : X.carrier → PUnit.{?u.96 + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
⊢ Measurable f₁

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
f₁ : X.carrier → PUnit.{?u.96 + 1} × X.carrier := fun x ↦ (PUnit.unit, x)
hf₁ : Measurable f₁
⊢ Measurable Prod.snd

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst✝⁹ : (t : T) → TopologicalSpace (F t)
inst✝⁸ : (t : T) → MeasurableSpace (F t)
inst✝⁷ : ∀ (t : T), BorelSpace (F t)
inst✝⁶ : ∀ (t : T), HasOuterApproxClosed (F t)
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst✝¹ : Fintype T
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω), (⇑f ∘ Z * ∏ t, ⇑(g t) ∘ Y t) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P
f : G →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
⊢ Measurable fun p ↦ f p.1 * ∏ j, (g j) (p.2 j)

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst✝⁹ : (t : T) → TopologicalSpace (F t)
inst✝⁸ : (t : T) → MeasurableSpace (F t)
inst✝⁷ : ∀ (t : T), BorelSpace (F t)
inst✝⁶ : ∀ (t : T), HasOuterApproxClosed (F t)
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst✝¹ : IsFiniteMeasure P
inst✝ : Finite T
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : ((t : T) → F t) →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ f (Z ω) * g fun x ↦ Y x ω) x ∂P =
      (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (fun ω ↦ g fun x ↦ Y x ω) x ∂P
this : Fintype T
f : G →ᵇ ℝ
g : (t : T) → F t →ᵇ ℝ
t : T
⊢ Continuous (Function.eval t)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{?u.182 + 1} := fun x ↦ (x, PUnit.unit)
⊢ Measurable f₁

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
f₁ : X.carrier → X.carrier × PUnit.{?u.182 + 1} := fun x ↦ (x, PUnit.unit)
hf₁ : Measurable f₁
⊢ Measurable Prod.fst

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
a✝ : (X₁✝.carrier × X₂✝.carrier) × X₃✝.carrier
s✝ : Set (Y₁✝.carrier × Y₂✝.carrier × Y₃✝.carrier)
hs : MeasurableSet s✝
⊢ Measurable ⇑prodAssoc

Tactic:
fun_prop

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

Goal state before:
pp: case hφ
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁹ : (s : S) → TopologicalSpace (E s)
inst✝⁸ : (s : S) → MeasurableSpace (E s)
inst✝⁷ : ∀ (s : S), BorelSpace (E s)
inst✝⁶ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : Fintype S
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : (i : S) → E i →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEMeasurable U P

Tactic:
fun_prop

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

Goal state before:
pp: case hfm
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁹ : (s : S) → TopologicalSpace (E s)
inst✝⁸ : (s : S) → MeasurableSpace (E s)
inst✝⁷ : ∀ (s : S), BorelSpace (E s)
inst✝⁶ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : Fintype S
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : (i : S) → E i →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEStronglyMeasurable (⇑g) (map U P)

Tactic:
fun_prop

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

Goal state before:
pp: case hφ
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁹ : (s : S) → TopologicalSpace (E s)
inst✝⁸ : (s : S) → MeasurableSpace (E s)
inst✝⁷ : ∀ (s : S), BorelSpace (E s)
inst✝⁶ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : Fintype S
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : (i : S) → E i →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEMeasurable (fun c a ↦ X a c) P

Tactic:
fun_prop

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

Goal state before:
pp: case hfm
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁹ : (s : S) → TopologicalSpace (E s)
inst✝⁸ : (s : S) → MeasurableSpace (E s)
inst✝⁷ : ∀ (s : S), BorelSpace (E s)
inst✝⁶ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : Fintype S
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : (i : S) → E i →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEStronglyMeasurable (fun x ↦ ∏ i, (f i) (x i)) (map (fun c a ↦ X a c) P)

Tactic:
fun_prop

Goal state after:
case hfm
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁹ : (s : S) → TopologicalSpace (E s)
inst✝⁸ : (s : S) → MeasurableSpace (E s)
inst✝⁷ : ∀ (s : S), BorelSpace (E s)
inst✝⁶ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : Fintype S
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : (i : S) → E i →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEStronglyMeasurable (fun x ↦ ∏ i, (f i) (x i)) (map (fun c a ↦ X a c) P)
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: case hφ
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁹ : (s : S) → TopologicalSpace (E s)
inst✝⁸ : (s : S) → MeasurableSpace (E s)
inst✝⁷ : ∀ (s : S), BorelSpace (E s)
inst✝⁶ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : Fintype S
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : (i : S) → E i →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEMeasurable (fun ω ↦ (fun a ↦ X a ω, U ω)) P

Tactic:
fun_prop

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

Goal state before:
pp: case hfm
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁹ : (s : S) → TopologicalSpace (E s)
inst✝⁸ : (s : S) → MeasurableSpace (E s)
inst✝⁷ : ∀ (s : S), BorelSpace (E s)
inst✝⁶ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : Fintype S
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : (i : S) → E i →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEStronglyMeasurable (fun p ↦ (∏ i, (f i) (p.1 i)) * g p.2) (map (fun ω ↦ (fun a ↦ X a ω, U ω)) P)

Tactic:
fun_prop

Goal state after:
case hfm
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁹ : (s : S) → TopologicalSpace (E s)
inst✝⁸ : (s : S) → MeasurableSpace (E s)
inst✝⁷ : ∀ (s : S), BorelSpace (E s)
inst✝⁶ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : Fintype S
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : (i : S) → E i →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEStronglyMeasurable (fun p ↦ (∏ i, (f i) (p.1 i)) * g p.2) (map (fun ω ↦ (fun a ↦ X a ω, U ω)) P)
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁹ : (s : S) → TopologicalSpace (E s)
inst✝⁸ : (s : S) → MeasurableSpace (E s)
inst✝⁷ : ∀ (s : S), BorelSpace (E s)
inst✝⁶ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : Fintype S
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : (i : S) → E i →ᵇ ℝ
g : H →ᵇ ℝ
⊢ Measurable fun x ↦ ∏ i, (f i) (x i)

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁹ : (s : S) → TopologicalSpace (E s)
inst✝⁸ : (s : S) → MeasurableSpace (E s)
inst✝⁷ : ∀ (s : S), BorelSpace (E s)
inst✝⁶ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : Fintype S
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : (i : S) → E i →ᵇ ℝ
g : H →ᵇ ℝ
⊢ Measurable fun p ↦ (∏ i, (f i) (p.1 i)) * g p.2

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
⊢ Measurable Prod.snd

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁹ : (s : S) → TopologicalSpace (E s)
inst✝⁸ : (s : S) → MeasurableSpace (E s)
inst✝⁷ : ∀ (s : S), BorelSpace (E s)
inst✝⁶ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : IsFiniteMeasure P
inst✝ : Finite S
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ (f fun x ↦ X x ω) * g (U ω)) x ∂P =
      (∫ (x : Ω), (fun ω ↦ f fun x ↦ X x ω) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
g : H →ᵇ ℝ
s : S
⊢ Continuous (Function.eval s)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
a✝ : PUnit.{u + 1} × X✝.carrier
s✝ : Set Y✝.carrier
hs : MeasurableSet s✝
this : IsSFiniteKernel κ.hom
⊢ Measurable Prod.snd

Tactic:
fun_prop

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

Goal state before:
pp: case hπ
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
m : ι → MeasurableSpace Ω
hm : ∀ (i : ι), m i ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ (i : ι), ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s

Tactic:
· exact hm

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
⊢ Measurable Prod.fst

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X✝ Y✝ : SFinKer
κ : X✝ ⟶ Y✝
a✝ : X✝.carrier × PUnit.{u + 1}
s✝ : Set Y✝.carrier
hs : MeasurableSet s✝
this : IsSFiniteKernel κ.hom
⊢ Measurable Prod.fst

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: W X Y Z : SFinKer
⊢ Measurable id

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: W X Y Z : SFinKer
⊢ Measurable ⇑prodAssoc

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Measurable id

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Measurable Prod.snd

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Measurable Prod.fst

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Measurable (Prod.snd ∘ id)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
⊢ Measurable (Prod.fst ∘ id)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: case mp
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
a : ↑I
h_monotone : ∀ (s : X), Monotone fun x ↦ (κ s).real (Icc 0 x)
e : X × ↑I
y : ℝ
hyI : 0 ≤ y ∧ y ≤ 1
y_mem : (κ e.1).real (Icc 0 ⟨y, ⋯⟩) < ↑e.2
hy : ↑a < y
q : ℚ
hqa : ↑a < ↑q
hqy : ↑q < y
⊢ ∃ i, ↑a < ↑i ∧ ∃ (x : 0 ≤ i ∧ ↑i ≤ 1), (κ e.1).real (Icc 0 ⟨↑i, ⋯⟩) < ↑e.2

Tactic:
refine ⟨q, hqa, ⟨?_, hqy.le.trans hyI.2⟩, lt_of_lt_of_le' y_mem (h_monotone e.1 hqy.le)⟩

Goal state after:
case mp
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
a : ↑I
h_monotone : ∀ (s : X), Monotone fun x ↦ (κ s).real (Icc 0 x)
e : X × ↑I
y : ℝ
hyI : 0 ≤ y ∧ y ≤ 1
y_mem : (κ e.1).real (Icc 0 ⟨y, ⋯⟩) < ↑e.2
hy : ↑a < y
q : ℚ
hqa : ↑a < ↑q
hqy : ↑q < y
⊢ 0 ≤ q
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: case hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEMeasurable U P

Tactic:
fun_prop

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

Goal state before:
pp: case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEStronglyMeasurable (⇑g) (map U P)

Tactic:
fun_prop

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

Goal state before:
pp: case hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEMeasurable Z P

Tactic:
fun_prop

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

Goal state before:
pp: case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEStronglyMeasurable (⇑f) (map Z P)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ Measurable fun x ↦ (PUnit.unit, x)

Tactic:
fun_prop

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

Goal state before:
pp: case hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEMeasurable (fun ω ↦ (Z ω, U ω)) P

Tactic:
fun_prop

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

Goal state before:
pp: case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEStronglyMeasurable (fun p ↦ f p.1 * g p.2) (map (fun ω ↦ (Z ω, U ω)) P)

Tactic:
fun_prop

Goal state after:
case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ AEStronglyMeasurable (fun p ↦ f p.1 * g p.2) (map (fun ω ↦ (Z ω, U ω)) P)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ Measurable fun x ↦ (x, PUnit.unit)

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
H : Type u_7
inst✝⁸ : TopologicalSpace G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : HasOuterApproxClosed G
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : HasOuterApproxClosed H
Z : Ω → G
U : Ω → H
inst✝ : IsFiniteMeasure P
mZ : AEMeasurable Z P
mU : AEMeasurable U P
h :
  ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), ∫ (x : Ω), (⇑f ∘ Z * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
f : G →ᵇ ℝ
g : H →ᵇ ℝ
⊢ Measurable fun p ↦ f p.1 * g p.2

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ Measurable fun ω ↦ (f ω, g ω)

Tactic:
fun_prop

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

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ Measurable (Prod.map id fun ω ↦ (f ω, g ω))

Tactic:
fun_prop

Goal state after: