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

Goal state before:
pp: case e'_3.e'_6
Ω : Type u_1
S : Type u_2
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
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✝⁶ : (t : T) → TopologicalSpace (F t)
inst✝⁵ : (t : T) → MeasurableSpace (F t)
inst✝⁴ : ∀ (t : T), BorelSpace (F t)
inst✝³ : ∀ (t : T), HasOuterApproxClosed (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst✝² : Fintype S
inst✝¹ : Fintype T
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ∏ t, ⇑(g t) ∘ Y t) x ∂P =
      (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P
f : (i : S) → E i →ᵇ ℝ
g : (j : T) → F j →ᵇ ℝ
x✝ : Ω
⊢ ∏ j, (g j) ((fun a ↦ Y a x✝) j) = (∏ t, ⇑(g t) ∘ Y t) x✝

Tactic:
simp

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

Goal state before:
pp: case e'_2
Ω : Type u_1
S : Type u_2
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
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✝⁶ : (t : T) → TopologicalSpace (F t)
inst✝⁵ : (t : T) → MeasurableSpace (F t)
inst✝⁴ : ∀ (t : T), BorelSpace (F t)
inst✝³ : ∀ (t : T), HasOuterApproxClosed (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst✝² : IsFiniteMeasure P
inst✝¹ : Finite S
inst✝ : Finite T
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ) (g : ((t : T) → F t) →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ (f fun x ↦ X x ω) * g fun x ↦ Y x ω) x ∂P =
      (∫ (x : Ω), (fun ω ↦ f fun x ↦ X x ω) x ∂P) * ∫ (x : Ω), (fun ω ↦ g fun x ↦ Y x ω) x ∂P
this✝ : Fintype S
this : Fintype T
f : (s : S) → E s →ᵇ ℝ
g : (t : T) → F t →ᵇ ℝ
x✝¹ x✝ : Ω
⊢ ((∏ s, ⇑(f s) ∘ X s) * ∏ t, ⇑(g t) ∘ Y t) x✝ =
    ((∏ s, (f s).compContinuous { toFun := Function.eval s, continuous_toFun := ⋯ }) fun x ↦ X x x✝) *
      (∏ t, (g t).compContinuous { toFun := Function.eval t, continuous_toFun := ⋯ }) fun x ↦ Y x x✝

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_5
Ω : Type u_1
S : Type u_2
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
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✝⁶ : (t : T) → TopologicalSpace (F t)
inst✝⁵ : (t : T) → MeasurableSpace (F t)
inst✝⁴ : ∀ (t : T), BorelSpace (F t)
inst✝³ : ∀ (t : T), HasOuterApproxClosed (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst✝² : IsFiniteMeasure P
inst✝¹ : Finite S
inst✝ : Finite T
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ) (g : ((t : T) → F t) →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ (f fun x ↦ X x ω) * g fun x ↦ Y x ω) x ∂P =
      (∫ (x : Ω), (fun ω ↦ f fun x ↦ X x ω) x ∂P) * ∫ (x : Ω), (fun ω ↦ g fun x ↦ Y x ω) x ∂P
this✝ : Fintype S
this : Fintype T
f : (s : S) → E s →ᵇ ℝ
g : (t : T) → F t →ᵇ ℝ
x✝¹ x✝ : Ω
⊢ (∏ s, ⇑(f s) ∘ X s) x✝ =
    (∏ s, (f s).compContinuous { toFun := Function.eval s, continuous_toFun := ⋯ }) fun x ↦ X x x✝

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_6
Ω : Type u_1
S : Type u_2
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
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✝⁶ : (t : T) → TopologicalSpace (F t)
inst✝⁵ : (t : T) → MeasurableSpace (F t)
inst✝⁴ : ∀ (t : T), BorelSpace (F t)
inst✝³ : ∀ (t : T), HasOuterApproxClosed (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst✝² : IsFiniteMeasure P
inst✝¹ : Finite S
inst✝ : Finite T
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ) (g : ((t : T) → F t) →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ (f fun x ↦ X x ω) * g fun x ↦ Y x ω) x ∂P =
      (∫ (x : Ω), (fun ω ↦ f fun x ↦ X x ω) x ∂P) * ∫ (x : Ω), (fun ω ↦ g fun x ↦ Y x ω) x ∂P
this✝ : Fintype S
this : Fintype T
f : (s : S) → E s →ᵇ ℝ
g : (t : T) → F t →ᵇ ℝ
x✝¹ x✝ : Ω
⊢ (∏ t, ⇑(g t) ∘ Y t) x✝ =
    (∏ t, (g t).compContinuous { toFun := Function.eval t, continuous_toFun := ⋯ }) fun x ↦ Y x x✝

Tactic:
simp

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

Goal state before:
pp: case e'_2
Ω : 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 →ᵇ ℝ
x✝ : Ω
⊢ f (Z x✝, fun a ↦ Y a x✝).1 * ∏ j, (g j) ((Z x✝, fun a ↦ Y a x✝).2 j) = (⇑f ∘ Z * ∏ t, ⇑(g t) ∘ Y t) x✝

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_6
Ω : 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 →ᵇ ℝ
x✝ : Ω
⊢ ∏ j, (g j) ((fun a ↦ Y a x✝) j) = (∏ t, ⇑(g t) ∘ Y t) x✝

Tactic:
simp

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

Goal state before:
pp: X Y : Stoch
κ✝ : X ⟶ Y
X✝ Y✝ : Stoch
κ : X✝ ⟶ Y✝
⊢ (κ ≫ ε).hom.hom = ε.hom.hom

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
inst✝ : IsMarkovKernel κ
π : Measure α
h_rev : κ.IsReversible π
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, (κ x) Set.univ ∂π = π s

Tactic:
simp

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

Goal state before:
pp: case e'_2
Ω : 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 →ᵇ ℝ
x✝¹ x✝ : Ω
⊢ (⇑f ∘ Z * ∏ t, ⇑(g t) ∘ Y t) x✝ =
    f (Z x✝) * (∏ t, (g t).compContinuous { toFun := Function.eval t, continuous_toFun := ⋯ }) fun x ↦ Y x x✝

Tactic:
simp

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

Goal state before:
pp: case e'_3
Ω : 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 →ᵇ ℝ
x✝¹ x✝ : Ω
⊢ (∏ t, ⇑(g t) ∘ Y t) x✝ =
    (∏ t, (g t).compContinuous { toFun := Function.eval t, continuous_toFun := ⋯ }) fun x ↦ Y x x✝

Tactic:
simp

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

Goal state before:
pp: case e'_2
Ω : 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 →ᵇ ℝ
x✝ : Ω
⊢ (∏ i, (f i) ((fun a ↦ X a x✝, U x✝).1 i)) * g (fun a ↦ X a x✝, U x✝).2 = ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x✝

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_5
Ω : 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 →ᵇ ℝ
x✝ : Ω
⊢ ∏ i, (f i) ((fun a ↦ X a x✝) i) = (∏ s, ⇑(f s) ∘ X s) x✝

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (∀ (t1 t2 : Set Ω),
      t1 ∈ {s} →
        t2 ∈ {t} →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']) ↔
    μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']

Tactic:
simp

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

Goal state before:
pp: case e'_2
Ω : 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 →ᵇ ℝ
x✝¹ x✝ : Ω
⊢ ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x✝ =
    ((∏ s, (f s).compContinuous { toFun := Function.eval s, continuous_toFun := ⋯ }) fun x ↦ X x x✝) * g (U x✝)

Tactic:
simp

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

Goal state before:
pp: case e'_3
Ω : 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 →ᵇ ℝ
x✝¹ x✝ : Ω
⊢ (∏ s, ⇑(f s) ∘ X s) x✝ =
    (∏ s, (f s).compContinuous { toFun := Function.eval s, continuous_toFun := ⋯ }) fun x ↦ X x x✝

Tactic:
simp

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

Goal state before:
pp: case refine_1
X Y : SFinKer
⊢ ({ hom := Kernel.swap X.carrier Y.carrier, property := ⋯ } ≫
        { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }).hom =
    (𝟙 (X ⊗ Y)).hom

Tactic:
simp

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

Goal state before:
pp: case refine_2
X Y : SFinKer
⊢ ({ hom := Kernel.swap Y.carrier X.carrier, property := ⋯ } ≫
        { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ }).hom =
    (𝟙 (Y ⊗ X)).hom

Tactic:
simp

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

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
ω : Ω
h : ω ∈ X ⁻¹' s
⊢ ‖1 ω‖ ≤ 1

Tactic:
simp

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

Goal state before:
pp: case neg
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
ω : Ω
h : ω ∉ X ⁻¹' s
⊢ ‖0‖ ≤ 1

Tactic:
simp

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

Goal state before:
pp: X Y : SFinKer
⊢ ({ hom := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ },
            inv := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        { hom := { hom := Kernel.swap Y.carrier X.carrier, property := ⋯ },
            inv := { hom := Kernel.swap X.carrier Y.carrier, property := ⋯ }, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom).hom =
    (𝟙 (X ⊗ Y)).hom

Tactic:
simp

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

Goal state before:
pp: case hf
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
⊢ StronglyMeasurable ((X ⁻¹' s).indicator 1)

Tactic:
exact stronglyMeasurable_const.indicator (hX hs)

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

Goal state before:
pp: 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}
measurable_f : Measurable (uncurry f)
a : X
x x✝ : ↑I
⊢ x✝ ∈ Iic x ↔ x✝ ∈ Icc 0 x

Tactic:
simp

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

Goal state before:
pp: case e_6.mp
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := ⋯
measurable_f : Measurable (uncurry f)
a : X
x : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
ξ : ↑I
⊢ f a ξ ≤ x → ξ ≤ ⟨(κ a).real (Icc 0 x), κ_in_I⟩

Tactic:
intro (hξ : f a ξ ≤ x)
    change ξ ≤ (κ a).real (Icc 0 x)
    by_cases hx : x = 1
    · simp [hx, ← univ_eq_Icc, ξ.2.2]
    let g := fun y ↦ (κ a).real (Icc 0 y)
    let nebot : NeBot (𝓝[>] x) := by
      refine nhdsGT_neBot_of_exists_gt ?_
      use 1
      exact lt_of_le_of_ne x.2.2 hx
    refine le_of_tendsto_of_tendsto (b := 𝓝[>] x) (g := g) continuousWithinAt_const ?_ ?_
    · let h := cdf ((κ a).map Subtype.val)
      have h_continuousWithinAt := continuousWithinAt_Ioi_iff_Ici.mpr (h.right_continuous x)
      simp_rw [g, ← unitInterval.cdf_eq_real (κ a)]
      exact h_continuousWithinAt.comp (Continuous.continuousWithinAt (by fun_prop)) (fun y hy ↦ hy)
    · refine eventually_nhdsWithin_of_forall fun y hy ↦ ?_
      by_contra! h
      simp only [sSup_le_iff, f] at hξ
      specialize hξ y h
      grind

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

Goal state before:
pp: case h₂
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := ⋯
measurable_f : Measurable (uncurry f)
a : X
x : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
ξ : ↑I
hξ : ↑ξ ≤ (κ a).real (Icc 0 x)
c : ↑I
hc : c ∈ {x | (κ a).real (Icc 0 x) < ↑ξ}
h : x < c
h_lt : ¬(κ a).real (Icc 0 x) ≤ (κ a).real (Icc 0 c)
⊢ autoParam ((κ a) (Icc 0 c) ≠ ∞) measureReal_mono._auto_1

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst✝² : Nonempty Y
mY : MeasurableSpace Y
inst✝¹ : StandardBorelSpace Y
κ : Kernel X Y
inst✝ : IsMarkovKernel κ
g : Y → ↑I := sigmoid ∘ embeddingReal Y
⊢ ∃ f, Measurable (uncurry f) ∧ ∀ (a : X), Measure.map (f a) volume = κ a

Tactic:
have hg := measurableEmbedding_sigmoid_comp_embeddingReal Y

Goal state after:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst✝² : Nonempty Y
mY : MeasurableSpace Y
inst✝¹ : StandardBorelSpace Y
κ : Kernel X Y
inst✝ : IsMarkovKernel κ
g : Y → ↑I := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
⊢ ∃ f, Measurable (uncurry f) ∧ ∀ (a : X), Measure.map (f a) volume = κ a
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inl
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (fun ω ↦ rexp (t * X ω)) 0
⊢ (Measure.tilted 0 fun x ↦ t * X x) s = ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X 0 t)) ∂0

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inl
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
inst✝ : SFinite 0
ht : Integrable (fun ω ↦ rexp (t * X ω)) 0
⊢ (Measure.tilted 0 fun x ↦ t * X x) s = ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X 0 t)) ∂0

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inl
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (fun ω ↦ rexp (t * X ω)) 0
⊢ (Measure.tilted 0 fun x ↦ t * X x) s = ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X 0 t) ∂0)

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inl
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
inst✝ : SFinite 0
ht : Integrable (fun ω ↦ rexp (t * X ω)) 0
⊢ (Measure.tilted 0 fun x ↦ t * X x) s = ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X 0 t) ∂0)

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inl
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : Ω → E
s : Set Ω
hs : MeasurableSet s
ht : Integrable (fun ω ↦ rexp (t * X ω)) 0
⊢ (∫ (x : Ω) in s, g x ∂Measure.tilted 0 fun x ↦ t * X x) = ∫ (x : Ω) in s, rexp (t * X x - cgf X 0 t) • g x ∂0

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inl
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : Ω → E
s : Set Ω
inst✝ : SFinite 0
ht : Integrable (fun ω ↦ rexp (t * X ω)) 0
⊢ (∫ (x : Ω) in s, g x ∂Measure.tilted 0 fun x ↦ t * X x) = ∫ (x : Ω) in s, rexp (t * X x - cgf X 0 t) • g x ∂0

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : Ω → E
s : Set Ω
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ (∫ (x : Ω) in s, g x ∂μ.tilted fun x ↦ t * X x) = ∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ

Tactic:
simp_rw [setIntegral_tilted_mul_eq_mgf, exp_sub, exp_cgf ht]

Goal state after:
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inl
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : Ω → E
ht : Integrable (fun ω ↦ rexp (t * X ω)) 0
⊢ (∫ (ω : Ω), g ω ∂Measure.tilted 0 fun x ↦ t * X x) = ∫ (ω : Ω), rexp (t * X ω - cgf X 0 t) • g ω ∂0

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
hp : ¬p = 0
⊢ ↑p ≠ ∞

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case neg.hp_ne_top
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ ↑p ≠ ∞

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
⊢ ↑p ≠ ∞

Tactic:
simp

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

Goal state before:
pp: case e'_2
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : IsProbabilityMeasure P
inst✝ : Finite S
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : ((s : S) → E s) →ᵇ ℝ), ∫ (ω : Ω) in A, f fun x ↦ X x ω ∂P = P.real A * ∫ (ω : Ω), f fun x ↦ X x ω ∂P
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
x✝ : Ω
⊢ ∏ s, (f s) (X s x✝) = (∏ s, (f s).compContinuous { toFun := Function.eval s, continuous_toFun := ⋯ }) fun x ↦ X x x✝

Tactic:
simp

Goal state after: