suffices 2 = A * sqrt 2 ↔ A = sqrt 2 by convert this using 2; ring
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ √(2 * x - 1) + 1 + (1 - √(2 * x - 1)) = A * √2 ↔ A = √2
x A : ℝ
hx : x ∈ Icc (1 / 2) 1
this : √(2 * x - 1) ≤ 1
⊢ 2 = A * √2 ↔ A = √2