Theorem: Probly.FDRand.pure.arg_x.randFwdDeriv_rule_simple (Probly/RandFwdDeriv.lean)

State before:
W : Type ?u.8184
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.8419
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.8536
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.8653
inst✝¹ : MeasurableSpace α
β : Type ?u.8659
inst✝ : MeasurableSpace β
⊢ (randFwdDeriv fun x => Rand.pure x) = fun x dx => fdpure x dx
Tactic:
unfold randFwdDeriv fdpure
State after:
W : Type ?u.8184
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.8419
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.8536
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.8653
inst✝¹ : MeasurableSpace α
β : Type ?u.8659
inst✝ : MeasurableSpace β
⊢ (fun x dx => { val := (fun x => Rand.pure x) x, dval := randDeriv (fun x => Rand.pure x) x dx }) = fun x dx =>
    { val := Rand.pure x, dval := dpure x dx }

State before:
W : Type ?u.8184
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.8419
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.8536
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.8653
inst✝¹ : MeasurableSpace α
β : Type ?u.8659
inst✝ : MeasurableSpace β
⊢ (fun x dx => { val := (fun x => Rand.pure x) x, dval := randDeriv (fun x => Rand.pure x) x dx }) = fun x dx =>
    { val := Rand.pure x, dval := dpure x dx }
Tactic:
simp (disch:=first | apply hx | sorry) [rand_simp]
State after:
W : Type ?u.8184
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.8419
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.8536
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.8653
inst✝¹ : MeasurableSpace α
β : Type ?u.8659
inst✝ : MeasurableSpace β
⊢ (fun x dx => { val := Rand.pure x, dval := randDeriv (fun x => Rand.pure x) x dx }) = fun x dx =>
    { val := Rand.pure x, dval := dpure x dx }

State before:
W : Type ?u.8184
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.8419
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.8536
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.8653
inst✝¹ : MeasurableSpace α
β : Type ?u.8659
inst✝ : MeasurableSpace β
⊢ (fun x dx => { val := Rand.pure x, dval := randDeriv (fun x => Rand.pure x) x dx }) = fun x dx =>
    { val := Rand.pure x, dval := dpure x dx }
Tactic:
funext w dw
State after:
case h.h
W : Type ?u.8184
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.8419
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.8536
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.8653
inst✝¹ : MeasurableSpace α
β : Type ?u.8659
inst✝ : MeasurableSpace β
w dw : X
⊢ { val := Rand.pure w, dval := randDeriv (fun x => Rand.pure x) w dw } = { val := Rand.pure w, dval := dpure w dw }

State before:
case h.h
W : Type ?u.8184
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.8419
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.8536
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.8653
inst✝¹ : MeasurableSpace α
β : Type ?u.8659
inst✝ : MeasurableSpace β
w dw : X
⊢ { val := Rand.pure w, dval := randDeriv (fun x => Rand.pure x) w dw } = { val := Rand.pure w, dval := dpure w dw }
Tactic:
rw [Rand.pure.arg_x.randDeriv_rule _ differentiable_id']
State after:
case h.h
W : Type ?u.8184
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.8419
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.8536
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.8653
inst✝¹ : MeasurableSpace α
β : Type ?u.8659
inst✝ : MeasurableSpace β
w dw : X
⊢ { val := Rand.pure w, dval := (fun w dw => dpure w ((fderiv ℝ (fun x => x) w) dw)) w dw } =
    { val := Rand.pure w, dval := dpure w dw }

State before:
case h.h
W : Type ?u.8184
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.8419
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.8536
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.8653
inst✝¹ : MeasurableSpace α
β : Type ?u.8659
inst✝ : MeasurableSpace β
w dw : X
⊢ { val := Rand.pure w, dval := (fun w dw => dpure w ((fderiv ℝ (fun x => x) w) dw)) w dw } =
    { val := Rand.pure w, dval := dpure w dw }
Tactic:
simp (disch:=first | apply hx | sorry) [rand_simp]
State after:
no goals