have hx : 1 < x := by rwa [h.sqrt_two_lt_iff_one_lt] at hA
case mp
x A : ℝ
hA : √2 < A
this : 0 < A
h : IsGood x A
⊢ x = (A / 2) ^ 2 + 1 / 2
case mp
x A : ℝ
hA : √2 < A
this : 0 < A
h : IsGood x A
hx : 1 < x
⊢ x = (A / 2) ^ 2 + 1 / 2