cases le_or_lt (1 / 2) x with
| inl hx =>
  have hx' : 0 ≤ 2 * x - 1 := by linarith
  have h₁ : x + sqrt (2 * x - 1) = (sqrt (2 * x - 1) + 1) ^ 2 / 2 := by
    rw [add_sq, sq_sqrt hx']; field_simp; ring
  have h₂ : x - sqrt (2 * x - 1) = (sqrt (2 * x - 1) - 1) ^ 2 / 2 := by
    rw [sub_sq, sq_sqrt hx']; field_simp; ring
  simp only [IsGood, *, div_nonneg (sq_nonneg _) (zero_le_two (α := ℝ)), sqrt_div (sq_nonneg _),
    and_true]
  rw [sqrt_sq, sqrt_sq_eq_abs] <;> [skip; positivity]
  field_simp
| inr hx =>
  have : 2 * x - 1 < 0 := by linarith
  simp only [IsGood, this.not_le, hx.not_le]; simp
x A : ℝ
⊢ IsGood x A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2 ∧ 1 / 2 ≤ x
no goals