Theorem: Probly.flip.arg_x.randFwdDeriv_rule_siple (Probly/Flip.lean)

State before:
W : Type ?u.42250
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.42368
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.42485
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.42602
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.42719
inst✝¹ : MeasurableSpace α
β : Type ?u.42725
inst✝ : MeasurableSpace β
⊢ (randFwdDeriv fun x => flip x) = fun x dx => { val := flip x, dval := dx • dflip }
Tactic:
unfold randFwdDeriv
State after:
W : Type ?u.42250
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.42368
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.42485
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.42602
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.42719
inst✝¹ : MeasurableSpace α
β : Type ?u.42725
inst✝ : MeasurableSpace β
⊢ (fun x dx => { val := (fun x => flip x) x, dval := randDeriv (fun x => flip x) x dx }) = fun x dx =>
    { val := flip x, dval := dx • dflip }

State before:
W : Type ?u.42250
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.42368
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.42485
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.42602
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.42719
inst✝¹ : MeasurableSpace α
β : Type ?u.42725
inst✝ : MeasurableSpace β
⊢ (fun x dx => { val := (fun x => flip x) x, dval := randDeriv (fun x => flip x) x dx }) = fun x dx =>
    { val := flip x, dval := dx • dflip }
Tactic:
simp (disch:= first | apply hf | sorry) [rand_simp]
State after:
W : Type ?u.42250
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.42368
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.42485
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.42602
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.42719
inst✝¹ : MeasurableSpace α
β : Type ?u.42725
inst✝ : MeasurableSpace β
⊢ (fun x dx => { val := flip x, dval := randDeriv (fun x => flip x) x dx }) = fun x dx =>
    { val := flip x, dval := dx • dflip }

State before:
W : Type ?u.42250
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.42368
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.42485
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.42602
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.42719
inst✝¹ : MeasurableSpace α
β : Type ?u.42725
inst✝ : MeasurableSpace β
⊢ (fun x dx => { val := flip x, dval := randDeriv (fun x => flip x) x dx }) = fun x dx =>
    { val := flip x, dval := dx • dflip }
Tactic:
rw[flip.arg_x.randDeriv_rule _ differentiable_id']
State after:
W : Type ?u.42250
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.42368
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.42485
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.42602
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.42719
inst✝¹ : MeasurableSpace α
β : Type ?u.42725
inst✝ : MeasurableSpace β
⊢ (fun x dx =>
      { val := flip x,
        dval :=
          (fun w dw =>
              let dx' := (fderiv ℝ (fun x => x) w) dw;
              dx' • dflip)
            x dx }) =
    fun x dx => { val := flip x, dval := dx • dflip }

State before:
W : Type ?u.42250
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.42368
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.42485
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.42602
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.42719
inst✝¹ : MeasurableSpace α
β : Type ?u.42725
inst✝ : MeasurableSpace β
⊢ (fun x dx =>
      { val := flip x,
        dval :=
          (fun w dw =>
              let dx' := (fderiv ℝ (fun x => x) w) dw;
              dx' • dflip)
            x dx }) =
    fun x dx => { val := flip x, dval := dx • dflip }
Tactic:
simp
State after:
no goals