Pinching kraus ker of ne zero

theorem pinching_kraus_ker_of_ne_zero {d : Type*} [Fintype d] [DecidableEq d]    (σ : MState d) (v : d → ℂ) (hv : σ.m.mulVec v = 0)    (k : spectrum ℝ σ.m) (hk : k.val ≠ 0) :    (pinching_kraus σ k).mat *ᵥ v = 0 := by  -- Applying the equation $(pinching_kraus \sigma k).toMat * \sigma.m = k.val \bullet (pinching_kraus \sigma k).toMat$ to $v$, we get $(pinching_kraus \sigma k).toMat (\sigma.m v) = k.val (pinching_kraus \sigma k).toMat v$.  have h_eq_zero : ((pinching_kraus σ k).mat * σ.m) *ᵥ v = k.val • ((pinching_kraus σ k).mat *ᵥ v) := by    have h_eq_zero : ((pinching_kraus σ k).mat * σ.m) = k.val • (pinching_kraus σ k).mat := by      convert pinching_kraus_mul_self σ k using 1;    simp [ h_eq_zero];    ext i    simp [ Matrix.mulVec, dotProduct ] ;    simp only [mul_assoc, Finset.mul_sum];  simp_all [ ← Matrix.mulVec_mulVec ];  rw [eq_comm] at h_eq_zero  aesop