Theorem: last'' (Sard/LocallyLipschitz.lean)

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
a : ℝ
K c : ℝ≥0
⊢ ‖a‖.toNNReal * K * c = ‖a‖.toNNReal * (K * c)
Tactic:
exact mul_assoc _ K c
State after:
no goals