how to revise my code to make it can proof a cone K is covex

Stream: lean4

[Katherine Wei]

theorem combination_of_the_generators {x y : EuclideanSpace ℝ (Fin n)}
  (hx : x ∈ K) (hy : y ∈ K) (lambda : ℝ) (hlambda : 0 ≤ lambda ∧ lambda ≤ 1) :
  ∃ s : Fin m → NNReal (lambda * x + (1 - lambda) * y = sumK s vmatrix) ∧ ∀ i, 0 ≤ s i
begin
  rcases hx → ⟨sx, hx_def, hsx⟩
  rcases hy → ⟨sy, hy_def, hsy⟩,

  let s : Fin m → NNReal := λ i ⟨lambda * sx i + (1 - lambda) * sy i⟩
    begin
      apply add_nonneg
      apply mul_nonneg
      { exact hlambda.left, exact hsx i }  -- lambda * sx i is non-negative
      { exact sub_nonneg_of_le hlambda.right, exact hsy i }  -- (1 - lambda) * sy i is non-negative

  use s
  split
  {
    rw [hx_def, hy_def],
    simp only [sumK, finset.sum_add_distrib, finset.smul_sum, add_smul, smul_eq_mul, pi.add_apply],
    congr,
    ext i,
    simp only [subtype.coe_mk]
  }
  {
    intro i,
    exact (s i).prop
  }
end

[Kevin Buzzard]

Can you make your code a #mwe by adding any relevant imports? And what is your question? Your code seems to be sorry-free. Can you ask your question as a sorry in Lean rather than in informal language?

[Kevin Buzzard]

And this code relies on mathlib so should be in the mathlib4 stream (but I can't move it). And it looks like Lean 3 code so you are far less likely to get help with it. Why not switch to Lean 4? Lean 3 is now end-of-life.