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

State before:
W : Type ?u.12970
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type u
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type ?u.13649
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
f : {Y : Type u} → [inst : NormedAddCommGroup Y] → [inst_1 : NormedSpace ℝ Y] → [inst : CompleteSpace Y] → (X → Y) → Y
φ : X → Y
⊢ ⟪{ action := fun {Y} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y] => f }, φ⟫ = f φ
Tactic:
rfl
State after:
no goals