State uncertainty squared with covariance of centered commutator

lemma state_uncertainty_squared_with_covariance_of_centered_commutator :    (covariance A B ψ hψB) ^ 2 + (c / 2) ^ 2 ≤      variance A ψ * variance B ⟨ψ, hψB⟩ := by  rw [variance_eq_centered_norm_sq, variance_eq_centered_norm_sq]  rw [show ‖centered A ψ‖ ^ 2 * ‖centered B ⟨ψ, hψB⟩‖ ^ 2 =    (‖centered A ψ‖ * ‖centered B ⟨ψ, hψB⟩‖) ^ 2 by ring]  calc    (covariance A B ψ hψB) ^ 2 + (c / 2) ^ 2 =        ‖⟪centered A ψ, centered B ⟨ψ, hψB⟩⟫_ℂ‖ ^ 2 := by          rw [inner_norm_sq_eq_re_sq_add_commutator_half_sq            (by simpa [centeredCommutatorExpectation] using h_centered)]          rfl    _ ≤ (‖centered A ψ‖ * ‖centered B ⟨ψ, hψB⟩‖) ^ 2 := by        have h_bound :=          norm_inner_le_norm (𝕜 := ℂ) (centered A ψ) (centered B ⟨ψ, hψB⟩)        have h_inner_nonneg : 0 ≤ ‖⟪centered A ψ, centered B ⟨ψ, hψB⟩⟫_ℂ‖ :=          norm_nonneg _        have h_mul_nonneg : 0 ≤ ‖centered A ψ‖ * ‖centered B ⟨ψ, hψB⟩‖ :=          mul_nonneg (norm_nonneg _) (norm_nonneg _)        nlinarith