Theorem: Sieve.sqrt_le_self (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean)

State before:
x : ℝ
hx : 1 ≤ x
⊢ √x ≤ x
Tactic:
refine Iff.mpr Real.sqrt_le_iff ?_
State after:
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ x ∧ x ≤ x ^ 2

State before:
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ x ∧ x ≤ x ^ 2
Tactic:
constructor
State after:
case left
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ x

case right
x : ℝ
hx : 1 ≤ x
⊢ x ≤ x ^ 2

State before:
case right
x : ℝ
hx : 1 ≤ x
⊢ x ≤ x ^ 2
Tactic:
refine le_self_pow hx ?right.h
State after:
case right.h
x : ℝ
hx : 1 ≤ x
⊢ 2 ≠ 0

State before:
case right.h
x : ℝ
hx : 1 ≤ x
⊢ 2 ≠ 0
Tactic:
norm_num
State after:
no goals

State before:
case left
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ x
Tactic:
linarith
State after:
no goals