To Fun eq zero iff

lemma toFun_eq_zero_iff (h : P.𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime) :    P.toFun φ x = 0 ↔ φ x = 0 ∨ ‖φ‖_H^2 x = P.μ2 / P.𝓵 := by  refine Iff.intro (fun hV => ?_) (fun hD => ?_)  · have h1 := P.as_quad φ x    rw [hV] at h1    have h2 : ‖φ‖_H^2 x * (P.𝓵 * ‖φ‖_H^2 x + - P.μ2) = 0 := by linear_combination h1    rcases mul_eq_zero.mp h2 with h2 | h2    · exact Or.inl (by simpa [normSq] using h2)    · exact Or.inr (by rw [eq_div_iff h]; linear_combination h2)  · cases' hD with hD hD    · simp [toFun, hD]    · simp only [toFun, hD]      field_simp      ring