rw [sqrt_sq, sqrt_sq_eq_abs] <;> [skip; positivity]
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
h₂ : x - √(2 * x - 1) = (√(2 * x - 1) - 1) ^ 2 / 2
⊢ √((√(2 * x - 1) + 1) ^ 2) / √2 + √((√(2 * x - 1) - 1) ^ 2) / √2 = A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2
case inl
x A : ℝ
hx : 1 / 2 ≤ x
hx' : 0 ≤ 2 * x - 1
h₁ : x + √(2 * x - 1) = (√(2 * x - 1) + 1) ^ 2 / 2
h₂ : x - √(2 * x - 1) = (√(2 * x - 1) - 1) ^ 2 / 2
⊢ (√(2 * x - 1) + 1) / √2 + |√(2 * x - 1) - 1| / √2 = A ↔ √(2 * x - 1) + 1 + |√(2 * x - 1) - 1| = A * √2