help proof this

Stream: new members

[Katherine Wei]

theorem K_polar_convex: Convex ℝ (K_polar vmatrix) := by
  rw[Convex]
  intros x hx y hy a b ha hb ha_b
  rw[K_polar] at hx
  simp at hx
  rw[K] at hx
  rw[K_polar] at hy
  rw[K] at hy
  rw[K_polar]
  simp
  rw[K]
  intro z hz
  have h_1: x ⬝ᵥ z ≤ 0 := by
    exact hx z hz
  have h_2: y ⬝ᵥ z ≤ 0 := by
    exact hy z hz
  have h': (a • x)⬝ᵥ z  + (b • y)⬝ᵥ z ≤ a • 0 + b • 0 := by
   sorry

[Patrick Massot]

Remember you will get a lot more help after reading #mwe and editing your questions accordingly. Helping people to help you is very useful. Using the relevant stream would also help, you should try the new members stream.

[Notification Bot]

This topic was moved here from #lean4 > help proof this by Mario Carneiro.