simp[mean]
X : Type
Y : Type ?u.98701
Z : Type ?u.98704
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : MeasurableSpace Y
R : Type ?u.98716
inst✝⁸ : RealScalar R
inst✝⁷ : AddCommGroup Y
inst✝⁶ : Module ℝ Y
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
U : Type ?u.99913
inst✝³ : AddCommGroup U
inst✝² : Module ℝ U
inst✝¹ : AddCommGroup X
inst✝ : Module ℝ X
x : X
⊢ mean (pure x) = x
no goals