Neg weight implies neg value

lemma neg_weight_implies_neg_value {E : Type*} [AddCommGroup E] [Module ℝ E]    {q : QuadraticForm ℝ E} {w : Fin (finrank ℝ E) → SignType}    (h_equiv : QuadraticMap.Equivalent q (QuadraticMap.weightedSumSquares ℝ fun i => (w i : ℝ)))    {i : Fin (finrank ℝ E)} (hi : w i = SignType.neg) :    ∃ v : E, v ≠ 0 ∧ q v < 0 := by  let f := Classical.choice h_equiv  let v_std : Fin (finrank ℝ E) → ℝ := fun j => if j = i then 1 else 0  refine ⟨f.symm v_std, ?_, ?_⟩  · intro h    have hz : v_std = 0 := by      have hf := congrArg f h      rwa [f.apply_symm_apply, map_zero] at hf    simpa [v_std] using congrFun hz i  · have hw : QuadraticMap.weightedSumSquares ℝ (fun j => (w j : ℝ)) v_std = (w i : ℝ) :=      QuadraticMap.weightedSumSquares_basis_vector v_std fun _ => rfl    rw [QuadraticMap.IsometryEquiv.map_app f.symm v_std, hw, hi, SignType.neg_eq_neg_one,      SignType.coe_neg, SignType.coe_one]    norm_num