Theorem: SciLean.Prob.Rand.rpdf_wrt_self (SciLean/Modules/Prob/Rand.lean)

State before:
X : Type
inst✝³ : MeasurableSpace X
Y : Type ?u.44518
inst✝² : MeasurableSpace Y
Z : Type ?u.44524
inst✝¹ : MeasurableSpace Z
R : Type ?u.44530
inst✝ : RealScalar R
x : Rand X
⊢ rpdf x ↑x.μ = 1
Tactic:
funext x
State after:
case h
X : Type
inst✝³ : MeasurableSpace X
Y : Type ?u.44518
inst✝² : MeasurableSpace Y
Z : Type ?u.44524
inst✝¹ : MeasurableSpace Z
R : Type ?u.44530
inst✝ : RealScalar R
x✝ : Rand X
x : X
⊢ rpdf x✝ (↑x✝.μ) x = 1 x

State before:
case h
X : Type
inst✝³ : MeasurableSpace X
Y : Type ?u.44518
inst✝² : MeasurableSpace Y
Z : Type ?u.44524
inst✝¹ : MeasurableSpace Z
R : Type ?u.44530
inst✝ : RealScalar R
x✝ : Rand X
x : X
⊢ rpdf x✝ (↑x✝.μ) x = 1 x
Tactic:
unfold rpdf
State after:
case h
X : Type
inst✝³ : MeasurableSpace X
Y : Type ?u.44518
inst✝² : MeasurableSpace Y
Z : Type ?u.44524
inst✝¹ : MeasurableSpace Z
R : Type ?u.44530
inst✝ : RealScalar R
x✝ : Rand X
x : X
⊢ pdf ℝ x✝ (↑x✝.μ) x = 1 x

State before:
case h
X : Type
inst✝³ : MeasurableSpace X
Y : Type ?u.44518
inst✝² : MeasurableSpace Y
Z : Type ?u.44524
inst✝¹ : MeasurableSpace Z
R : Type ?u.44530
inst✝ : RealScalar R
x✝ : Rand X
x : X
⊢ pdf ℝ x✝ (↑x✝.μ) x = 1 x
Tactic:
rw[pdf_wrt_self]
State after:
no goals