rw [← mul_two, ← div_eq_iff (by positivity), mul_div_assoc, div_sqrt, ← sqrt_mul' _ zero_le_two,
  eq_comm]
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
h₂ : 1 / 2 ≤ x
⊢ √(2 * x - 1) + √(2 * x - 1) = A * √2 ↔ A = √(4 * x - 2)
x A : ℝ
hx : 1 < x
h₁ : 1 < √(2 * x - 1)
h₂ : 1 / 2 ≤ x
⊢ A = √((2 * x - 1) * 2) ↔ A = √(4 * x - 2)