rw [isGood_iff_eq_sqrt]
case mpr
A : ℝ
hA : √2 < A
this : 0 < A
⊢ IsGood ((A / 2) ^ 2 + 1 / 2) A
case mpr
A : ℝ
hA : √2 < A
this : 0 < A
⊢ A = √(4 * ((A / 2) ^ 2 + 1 / 2) - 2)

case mpr
A : ℝ
hA : √2 < A
this : 0 < A
⊢ 1 < (A / 2) ^ 2 + 1 / 2