Theorem: Probly.FDRand.FDRand_mk_zero_fdE (Probly/FDRand.lean)

State before:
X✝ : Type ?u.20141
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.20259
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.20376
inst✝¹⁴ : NormedAddCommGroup Z✝
inst✝¹³ : NormedSpace ℝ Z✝
inst✝¹² : MeasurableSpace Z✝
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x : Rand X
φ : X → X
⊢ fdE { val := x, dval := 0 } φ = (E x φ, 0)
Tactic:
simp [fdE,DRand.dE]
State after:
X✝ : Type ?u.20141
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.20259
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.20376
inst✝¹⁴ : NormedAddCommGroup Z✝
inst✝¹³ : NormedSpace ℝ Z✝
inst✝¹² : MeasurableSpace Z✝
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x : Rand X
φ : X → X
⊢ testFunctionExtension 0.action φ = 0

State before:
X✝ : Type ?u.20141
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.20259
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.20376
inst✝¹⁴ : NormedAddCommGroup Z✝
inst✝¹³ : NormedSpace ℝ Z✝
inst✝¹² : MeasurableSpace Z✝
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x : Rand X
φ : X → X
⊢ testFunctionExtension 0.action φ = 0
Tactic:
apply testFunctionExtension_ext
State after:
case h
X✝ : Type ?u.20141
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.20259
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.20376
inst✝¹⁴ : NormedAddCommGroup Z✝
inst✝¹³ : NormedSpace ℝ Z✝
inst✝¹² : MeasurableSpace Z✝
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x : Rand X
φ : X → X
⊢ ∀ (φ : X → ℝ) (y : X), 0.action φ • y = 0

State before:
case h
X✝ : Type ?u.20141
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.20259
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.20376
inst✝¹⁴ : NormedAddCommGroup Z✝
inst✝¹³ : NormedSpace ℝ Z✝
inst✝¹² : MeasurableSpace Z✝
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x : Rand X
φ : X → X
⊢ ∀ (φ : X → ℝ) (y : X), 0.action φ • y = 0
Tactic:
intro _ _
State after:
case h
X✝ : Type ?u.20141
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.20259
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.20376
inst✝¹⁴ : NormedAddCommGroup Z✝
inst✝¹³ : NormedSpace ℝ Z✝
inst✝¹² : MeasurableSpace Z✝
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x : Rand X
φ : X → X
φ✝ : X → ℝ
y✝ : X
⊢ 0.action φ✝ • y✝ = 0

State before:
case h
X✝ : Type ?u.20141
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.20259
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.20376
inst✝¹⁴ : NormedAddCommGroup Z✝
inst✝¹³ : NormedSpace ℝ Z✝
inst✝¹² : MeasurableSpace Z✝
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x : Rand X
φ : X → X
φ✝ : X → ℝ
y✝ : X
⊢ 0.action φ✝ • y✝ = 0
Tactic:
simp [rand_simp,zero_smul]
State after:
no goals