Theorem: SciLean.Prob.action_is_integral (SciLean/Modules/Prob/DistribDeriv/Distribution.lean)

State before:
W : Type ?u.38907
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : CompleteSpace W
X✝ : Type ?u.39134
inst✝¹⁰ : NormedAddCommGroup X✝
inst✝⁹ : NormedSpace ℝ X✝
inst✝⁸ : CompleteSpace X✝
Y✝ : Type ?u.39360
inst✝⁷ : NormedAddCommGroup Y✝
inst✝⁶ : NormedSpace ℝ Y✝
inst✝⁵ : CompleteSpace Y✝
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : CompleteSpace Z
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_1
inst✝ : TopologicalSpace Y
x : Measure X
f : X → Measure Y
φ : Y → Z
hφ : ∀ (x : X), Integrable φ (f x)
⊢ ⟪do
      let x ← ↑x
      ↑(f x), φ⟫ =
    ∫ (y : Y), φ y ∂Measure.bind x f
Tactic:
simp
State after:
W : Type ?u.38907
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : CompleteSpace W
X✝ : Type ?u.39134
inst✝¹⁰ : NormedAddCommGroup X✝
inst✝⁹ : NormedSpace ℝ X✝
inst✝⁸ : CompleteSpace X✝
Y✝ : Type ?u.39360
inst✝⁷ : NormedAddCommGroup Y✝
inst✝⁶ : NormedSpace ℝ Y✝
inst✝⁵ : CompleteSpace Y✝
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : CompleteSpace Z
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_1
inst✝ : TopologicalSpace Y
x : Measure X
f : X → Measure Y
φ : Y → Z
hφ : ∀ (x : X), Integrable φ (f x)
⊢ ∫ (x' : X), ∫ (x : Y), φ x ∂f x' ∂x = ∫ (x : Y), φ x ∂Measure.bind x f

State before:
W : Type ?u.38907
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : CompleteSpace W
X✝ : Type ?u.39134
inst✝¹⁰ : NormedAddCommGroup X✝
inst✝⁹ : NormedSpace ℝ X✝
inst✝⁸ : CompleteSpace X✝
Y✝ : Type ?u.39360
inst✝⁷ : NormedAddCommGroup Y✝
inst✝⁶ : NormedSpace ℝ Y✝
inst✝⁵ : CompleteSpace Y✝
Z : Type u_1
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : CompleteSpace Z
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_1
inst✝ : TopologicalSpace Y
x : Measure X
f : X → Measure Y
φ : Y → Z
hφ : ∀ (x : X), Integrable φ (f x)
⊢ ∫ (x' : X), ∫ (x : Y), φ x ∂f x' ∂x = ∫ (x : Y), φ x ∂Measure.bind x f
Tactic:
sorry
State after:
no goals