n : ℕ
⊢ pair
      (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
      (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)).snd =
    n
n : ℕ
⊢ pair (unpair n).fst (unpair n).snd = n
dsimp only [unpair]
n : ℕ
s : ℕ := sqrt n
⊢ pair
      (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
      (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)).snd =
    n
n : ℕ
⊢ pair
      (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
      (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)).snd =
    n
let s := sqrt n
n : ℕ
s : ℕ := sqrt n
sm : s * s + (n - s * s) = n
⊢ pair
      (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
      (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)).snd =
    n
n : ℕ
s : ℕ := sqrt n
⊢ pair
      (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
      (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)).snd =
    n
have sm : s * s + (n - s * s) = n := add_tsub_cancel_of_le (sqrt_le _)
case inl
n : ℕ
s : ℕ := sqrt n
sm : s * s + (n - s * s) = n
h : n - sqrt n * sqrt n < sqrt n
⊢ pair (n - sqrt n * sqrt n, sqrt n).fst (n - sqrt n * sqrt n, sqrt n).snd = n

case inr
n : ℕ
s : ℕ := sqrt n
sm : s * s + (n - s * s) = n
h : ¬n - sqrt n * sqrt n < sqrt n
⊢ pair (sqrt n, n - sqrt n * sqrt n - sqrt n).fst (sqrt n, n - sqrt n * sqrt n - sqrt n).snd = n
n : ℕ
s : ℕ := sqrt n
sm : s * s + (n - s * s) = n
⊢ pair
      (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
      (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)).snd =
    n
split_ifs with h
no goals
case inl
n : ℕ
s : ℕ := sqrt n
sm : s * s + (n - s * s) = n
h : n - sqrt n * sqrt n < sqrt n
⊢ pair (n - sqrt n * sqrt n, sqrt n).fst (n - sqrt n * sqrt n, sqrt n).snd = n
simp [pair, h, sm]
case inr
n : ℕ
s : ℕ := sqrt n
sm : s * s + (n - s * s) = n
h : ¬n - sqrt n * sqrt n < sqrt n
hl : n - s * s - s ≤ s
⊢ pair (sqrt n, n - sqrt n * sqrt n - sqrt n).fst (sqrt n, n - sqrt n * sqrt n - sqrt n).snd = n
case inr
n : ℕ
s : ℕ := sqrt n
sm : s * s + (n - s * s) = n
h : ¬n - sqrt n * sqrt n < sqrt n
⊢ pair (sqrt n, n - sqrt n * sqrt n - sqrt n).fst (sqrt n, n - sqrt n * sqrt n - sqrt n).snd = n
have hl : n - s * s - s ≤ s :=
  tsub_le_iff_left.mpr (tsub_le_iff_left.mpr <| by rw [← add_assoc] ; apply sqrt_le_add)
no goals
case inr
n : ℕ
s : ℕ := sqrt n
sm : s * s + (n - s * s) = n
h : ¬n - sqrt n * sqrt n < sqrt n
hl : n - s * s - s ≤ s
⊢ pair (sqrt n, n - sqrt n * sqrt n - sqrt n).fst (sqrt n, n - sqrt n * sqrt n - sqrt n).snd = n
simp [pair, hl.not_lt, add_assoc, add_tsub_cancel_of_le (le_of_not_gt h), sm]
n : ℕ
s : ℕ := sqrt n
sm : s * s + (n - s * s) = n
h : ¬n - sqrt n * sqrt n < sqrt n
⊢ n ≤ s * s + s + s
n : ℕ
s : ℕ := sqrt n
sm : s * s + (n - s * s) = n
h : ¬n - sqrt n * sqrt n < sqrt n
⊢ n ≤ s * s + (s + s)
rw [← add_assoc]
no goals
n : ℕ
s : ℕ := sqrt n
sm : s * s + (n - s * s) = n
h : ¬n - sqrt n * sqrt n < sqrt n
⊢ n ≤ s * s + s + s
apply sqrt_le_add