simp only [isGood_iff, hx.1, abs_sub_comm _ (1 : ℝ), abs_of_nonneg (sub_nonneg.2 this), and_true]
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ IsGood x A ↔ A = √2
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ √(2 * x - 1) + 1 + (1 - √(2 * x - 1)) = A * √2 ↔ A = √2