internlm/Lean-Github huggingface dataset:
Theorem: SciLean.Prob.FDRand.bind_bind
Proof state before:
case a
R : Type ?u.5801
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ (bind (bind x g) f).val = (bind x fun x' => bind (g x') f).val

case a
R : Type ?u.5801
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ (bind (bind x g) f).dval = (bind (bind x g) f).dval
Tactic:
. simp (disch:=sorry) only [bind,rand_simp]
Proof state after:
case a
R : Type ?u.5801
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ (bind (bind x g) f).dval = (bind (bind x g) f).dval
Theorem: SciLean.Prob.FDRand.bind_bind
Proof state before:
case a
R : Type ?u.5801
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ (bind (bind x g) f).dval = (bind (bind x g) f).dval
Tactic:
. simp (disch:=sorry) only [bind,rand_simp]
Proof state after:
no goals
Theorem: SciLean.Prob.FDRand.bind_bind
Proof state before:
case a
R : Type ?u.5801
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ (bind (bind x g) f).val = (bind x fun x' => bind (g x') f).val
Tactic:
simp (disch:=sorry) only [bind,rand_simp]
Proof state after:
no goals
Theorem: SciLean.Prob.FDRand.bind_bind
Proof state before:
case a
R : Type ?u.5801
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
x : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ (bind (bind x g) f).dval = (bind (bind x g) f).dval
Tactic:
simp (disch:=sorry) only [bind,rand_simp]
Proof state after:
no goals
Theorem: SciLean.Prob.FDRand.bind_pure
Proof state before:
R : Type ?u.7135
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x dx : X
⊢ bind (fdpure x dx) f = { val := (f x).val, dval := randDeriv (fun x' => (f x').val) x dx + (f x).dval }
Tactic:
simp only [bind,fdpure]
Proof state after:
R : Type ?u.7135
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x dx : X
⊢ {
      val :=
        let x' ~ Rand.pure x
        (f x').val,
      dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval } =
    { val := (f x).val, dval := randDeriv (fun x' => (f x').val) x dx + (f x).dval }
Theorem: SciLean.Prob.FDRand.bind_pure
Proof state before:
R : Type ?u.7135
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x dx : X
⊢ {
      val :=
        let x' ~ Rand.pure x
        (f x').val,
      dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval } =
    { val := (f x).val, dval := randDeriv (fun x' => (f x').val) x dx + (f x).dval }
Tactic:
apply ext
Proof state after:
case a
R : Type ?u.7135
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x dx : X
⊢ {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.val =
    { val := (f x).val, dval := randDeriv (fun x' => (f x').val) x dx + (f x).dval }.val

case a
R : Type ?u.7135
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x dx : X
⊢ {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval =
    {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval
Theorem: SciLean.Prob.FDRand.bind_pure
Proof state before:
case a
R : Type ?u.7135
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x dx : X
⊢ {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.val =
    { val := (f x).val, dval := randDeriv (fun x' => (f x').val) x dx + (f x).dval }.val

case a
R : Type ?u.7135
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x dx : X
⊢ {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval =
    {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval
Tactic:
. simp (disch:=sorry) only [rand_simp]
Proof state after:
case a
R : Type ?u.7135
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x dx : X
⊢ {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval =
    {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval
Theorem: SciLean.Prob.FDRand.bind_pure
Proof state before:
case a
R : Type ?u.7135
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x dx : X
⊢ {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval =
    {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval
Tactic:
. simp only [rand_simp]
Proof state after:
no goals
Theorem: SciLean.Prob.FDRand.bind_pure
Proof state before:
case a
R : Type ?u.7135
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x dx : X
⊢ {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.val =
    { val := (f x).val, dval := randDeriv (fun x' => (f x').val) x dx + (f x).dval }.val
Tactic:
simp (disch:=sorry) only [rand_simp]
Proof state after:
no goals
Theorem: SciLean.Prob.FDRand.bind_pure
Proof state before:
case a
R : Type ?u.7135
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x dx : X
⊢ {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval =
    {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval
Tactic:
simp only [rand_simp]
Proof state after:
no goals
Theorem: SciLean.Prob.FDRand.bind_pure_zero
Proof state before:
R : Type ?u.8427
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x : X
⊢ bind (fdpure x 0) f = f x
Tactic:
simp only [bind,fdpure]
Proof state after:
R : Type ?u.8427
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x : X
⊢ {
      val :=
        let x' ~ Rand.pure x
        (f x').val,
      dval := (DRand.bindDR (dpure x 0) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval } =
    f x
Theorem: SciLean.Prob.FDRand.bind_pure_zero
Proof state before:
R : Type ?u.8427
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x : X
⊢ {
      val :=
        let x' ~ Rand.pure x
        (f x').val,
      dval := (DRand.bindDR (dpure x 0) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval } =
    f x
Tactic:
apply ext
Proof state after:
case a
R : Type ?u.8427
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x : X
⊢ {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x 0) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.val =
    (f x).val

case a
R : Type ?u.8427
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x : X
⊢ {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x 0) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval =
    {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x 0) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval
Theorem: SciLean.Prob.FDRand.bind_pure_zero
Proof state before:
case a
R : Type ?u.8427
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x : X
⊢ {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x 0) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.val =
    (f x).val

case a
R : Type ?u.8427
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x : X
⊢ {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x 0) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval =
    {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x 0) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval
Tactic:
. simp (disch:=sorry) only [rand_simp]
Proof state after:
case a
R : Type ?u.8427
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x : X
⊢ {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x 0) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval =
    {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x 0) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval
Theorem: SciLean.Prob.FDRand.bind_pure_zero
Proof state before:
case a
R : Type ?u.8427
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x : X
⊢ {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x 0) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval =
    {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x 0) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval
Tactic:
. simp only [rand_simp]
Proof state after:
no goals
Theorem: SciLean.Prob.FDRand.bind_pure_zero
Proof state before:
case a
R : Type ?u.8427
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x : X
⊢ {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x 0) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.val =
    (f x).val
Tactic:
simp (disch:=sorry) only [rand_simp]
Proof state after:
no goals
Theorem: SciLean.Prob.FDRand.bind_pure_zero
Proof state before:
case a
R : Type ?u.8427
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R Y
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R Z
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R W
inst✝ : MeasurableSpace W
f : X → FDRand Y
x : X
⊢ {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x 0) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval =
    {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x 0) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval
Tactic:
simp only [rand_simp]
Proof state after:
no goals