solve this calc steps

Stream: lean4

[Katherine Wei]

theorem K_polar_convex: Convex ℝ (K_polar vmatrix) := by
  rw[Convex]
  intros x y hx hy a b ha hb hab
  simp only [K_polar] at hx hy
  intro z
  intro hz
  calc
    (a • x + b • hx) ⬝ᵥ z = (a • x)⬝ᵥ z  + (b • hx)⬝ᵥ z := by sorry
    _ ≤ a • 0 + b • 0 := by sorry
    _ = 0 := sorry

[Kim Morrison]

@Katherine Wei, please read #mwe! It will help you ask questions that get much better answers.

[Yaël Dillies]

Also please don't double post: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/how.20to.20prove.20the.20convex.20here.2E/near/438880062