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 * K * c = a * (K * c)
Tactic:
exact mul_assoc a K c
State after:
no goals