Neg 𝓵 sol exists iff

lemma neg_𝓵_sol_exists_iff (h𝓵 : P.𝓵 < 0) (c : ℝ) : (∃ φ x, P.toFun φ x = c) ↔ (0 < P.μ2 ∧ c ≤ 0) ∨    (P.μ2 ≤ 0 ∧ c ≤ - P.μ2 ^ 2 / (4 * P.𝓵)) := by  refine Iff.intro (fun ⟨φ, x, hV⟩ => ?_) (fun h => ?_)  · rw [← hV]    rcases P.neg_𝓵_toFun_neg h𝓵 φ x with hr | hr    · exact Or.inl hr    · exact Or.inr ⟨hr, P.neg_𝓵_quadDiscrim_zero_bound h𝓵 φ x⟩  · simp only [toFun, neg_mul]    simp only [← sub_eq_zero, sub_zero]    let a := (P.μ2 - Real.sqrt (discrim P.𝓵 (- P.μ2) (- c))) / (2 * P.𝓵)    have ha : 0 ≤ a := by      simp only [discrim, even_two, Even.neg_pow, mul_neg, sub_neg_eq_add, a]      rw [div_nonneg_iff]      refine Or.inr ⟨?_, by linarith⟩      rw [sub_nonpos]      rcases h with h | h      · exact Real.le_sqrt_of_sq_le (by nlinarith [h.2])      · exact h.1.trans (Real.sqrt_nonneg _)    use (const (HiggsVec.ofReal a))    use 0    simp [HiggsVec.ofReal_normSq ha]    trans P.𝓵 * a * a + (- P.μ2) * a + (- c)    · ring    have hd : 0 ≤ (discrim P.𝓵 (- P.μ2) (-c)) := by      simp only [discrim, even_two, Even.neg_pow, mul_neg, sub_neg_eq_add]      rcases h with h | h      · nlinarith [sq_nonneg P.μ2, h.2]      · rw [← @neg_le_iff_add_nonneg', ← le_div_iff_of_neg']        · exact h.2        · linarith    have hdd := (Real.mul_self_sqrt hd).symm    rw [mul_assoc]    refine (quadratic_eq_zero_iff (ne_of_gt h𝓵).symm hdd _).mpr ?_    simp only [neg_neg, or_true, a]