n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
⊢ (unpair n).fst < n
n : ℕ
n1 : 1 ≤ n
⊢ (unpair n).fst < n
let s := sqrt n
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
⊢ (if n - sqrt n * sqrt n < sqrt n then (n - sqrt n * sqrt n, sqrt n) else (sqrt n, n - sqrt n * sqrt n - sqrt n)).fst <
    n
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
⊢ (unpair n).fst < n
simp [unpair]
case pos
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : n - s * s < s
⊢ n - sqrt n * sqrt n < n

case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : ¬n - s * s < s
⊢ sqrt n < n
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
⊢ (if n - sqrt n * sqrt n < sqrt n then (n - sqrt n * sqrt n, sqrt n) else (sqrt n, n - sqrt n * sqrt n - sqrt n)).fst <
    n
by_cases h : n - s * s < s <;> simp [h]
no goals
case pos
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : n - s * s < s
⊢ n - sqrt n * sqrt n < n
exact lt_of_lt_of_le h (sqrt_le_self _)
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : sqrt n ≤ n - sqrt n * sqrt n
⊢ sqrt n < n
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : ¬n - s * s < s
⊢ sqrt n < n
simp at h
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : sqrt n ≤ n - sqrt n * sqrt n
s0 : 0 < s
⊢ sqrt n < n
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : sqrt n ≤ n - sqrt n * sqrt n
⊢ sqrt n < n
have s0 : 0 < s := sqrt_pos.2 n1
no goals
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : sqrt n ≤ n - sqrt n * sqrt n
s0 : 0 < s
⊢ sqrt n < n
exact lt_of_le_of_lt h (tsub_lt_self n1 (mul_pos s0 s0))