Stability Counter Example not potential Is Stable

lemma stabilityCounterExample_not_potentialIsStable :    ¬ PotentialIsStable .stabilityCounterExample := by  simp [PotentialIsStable]  intro c  /- The angle t and properties thereof. -/  let t := Real.arctan (2 * Real.sqrt (|c| + 1))⁻¹  have t_pos : 0 < t := arctan_pos.mpr (by positivity)  have t_le_pi_div_2 : t ≤ Real.pi / 2 := by    simpa [t] using le_of_lt <| arctan_lt_pi_div_two ((√(|c| + 1))⁻¹ * 2⁻¹)  have t_ne_zero : t ≠ 0 := t_pos.ne'  have sin_t_pos : 0 < sin t :=    Real.sin_pos_of_pos_of_lt_pi t_pos (by nlinarith [Real.pi_pos])  have cos_t_pos : 0 < cos t := cos_arctan_pos (2 * Real.sqrt (|c| + 1))⁻¹  have t_mul_sin_t_nonneg : 0 ≤ 2 * t * sin t - t ^ 2 := by    have hs := Real.mul_le_sin t_pos.le t_le_pi_div_2    rw [div_mul_eq_mul_div, div_le_iff₀ Real.pi_pos] at hs    nlinarith [mul_le_mul_of_nonneg_left hs t_pos.le, Real.pi_le_four]  /- The Two Higgs doublet violating stability.    The two Higgs doublet is constructed so that for the gram vector    `v` we have:    - `v₀ = cos t/(2 * t * (sin t)^2)`    - `v₁/v₀ = (1 - t * sin t)`    - `v₂/v₀ = - t * cos t`    - `v₃ = 0` -/  let H : TwoHiggsDoublet := {    Φ1 := !₂[√(cos t/(4 * t * (sin t)^2)), 0]    Φ2 := √(cos t/(4 * t * (sin t)^2)) • !₂[1 - t * sin t - Complex.I * t * cos t,      √(2 * t * sin t - t ^ 2)] }  have Φ1_norm_sq : ‖H.Φ1‖ ^ 2 = cos t/(4 * t * (sin t)^2) := by    simp [H, PiLp.norm_sq_eq_of_L2]    rw [sq_sqrt (by positivity)]  have Φ2_norm_sq : ‖H.Φ2‖ ^ 2 = cos t/(4 * t * (sin t)^2) := by    simp [H, norm_smul, mul_pow]    rw [sq_sqrt (by positivity)]    simp [PiLp.norm_sq_eq_of_L2]    rw [sq_sqrt (by positivity)]    have h0 : ‖1 - ↑t * Complex.sin ↑t - Complex.I * ↑t * Complex.cos ↑t‖ ^ 2 =        1 + t ^ 2 - 2 * t * sin t := by      rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]      simp only [Complex.sub_re, Complex.sub_im, Complex.mul_re, Complex.mul_im, Complex.I_re,        Complex.I_im, Complex.ofReal_re, Complex.ofReal_im, Complex.one_re, Complex.one_im,        Complex.sin_ofReal_re, Complex.sin_ofReal_im, Complex.cos_ofReal_re, Complex.cos_ofReal_im]      nlinarith [Real.sin_sq_add_cos_sq t]    rw [h0]    field_simp    ring  have Φ1_inner_Φ2 : ⟪H.Φ1, H.Φ2⟫_ℂ = Complex.ofReal (cos t/(4 * t * (sin t)^2) *      (1 - t * sin t)) + Complex.I *      Complex.ofReal (cos t/(4 * t * (sin t)^2) * (- t * cos t)) := by    simp [H, PiLp.inner_apply]    trans Complex.ofReal ((√(cos t / (4 * t * sin t ^ 2))) ^ 2) *        (1 - ↑t * Complex.sin ↑t - Complex.I * ↑t * Complex.cos ↑t)    · simp      ring    rw [sq_sqrt (by positivity)]    simp only [Complex.ofReal_div, Complex.ofReal_cos, Complex.ofReal_mul, Complex.ofReal_ofNat,      Complex.ofReal_pow, Complex.ofReal_sin]    ring  have Φ1_inner_Φ2_re : (⟪H.Φ1, H.Φ2⟫_ℂ).re = cos t/(4 * t * (sin t)^2) * (1 - t * sin t) := by    rw [Φ1_inner_Φ2, Complex.add_re, Complex.ofReal_re, Complex.re_mul_ofReal]    simp  have Φ1_inner_Φ2_im : (⟪H.Φ1, H.Φ2⟫_ℂ).im = cos t/(4 * t * (sin t)^2) * (- t * cos t) := by    rw [Φ1_inner_Φ2, Complex.add_im, Complex.im_mul_ofReal, Complex.ofReal_im]    simp  have potential_H_cos_sin : potential .stabilityCounterExample H =      - (cos t) ^ 2/ (4 * (sin t)^2) := by    rw [potential, massTerm_stabilityCounterExample, quarticTerm_stabilityCounterExample]    rw [Φ1_norm_sq, Φ2_norm_sq, Φ1_inner_Φ2_re, Φ1_inner_Φ2_im]    field  have potential_eq_c : potential .stabilityCounterExample H = - (|c| + 1) := by    have htan : sin t / cos t = (2 * √(|c| + 1))⁻¹ := by      rw [← tan_eq_sin_div_cos]      exact tan_arctan _    rw [potential_H_cos_sin, show -cos t ^ 2 / (4 * sin t ^ 2) = -1 / (4 * (sin t / cos t) ^ 2) by      field, htan]    field_simp    rw [sq_sqrt (by positivity)]    ring  /- Proving potential is unbounded. -/  use H  rw [potential_eq_c]  grind