[GOAL]
n : ℕ
⊢ pair (unpair n).fst (unpair n).snd = n
[PROOFSTEP]
dsimp only [unpair]
[GOAL]
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
[PROOFSTEP]
let s := sqrt n
[GOAL]
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
[PROOFSTEP]
have sm : s * s + (n - s * s) = n := add_tsub_cancel_of_le (sqrt_le _)
[GOAL]
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
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
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
[PROOFSTEP]
simp [pair, h, sm]
[GOAL]
case neg
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
[PROOFSTEP]
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)
[GOAL]
n : ℕ
s : ℕ := sqrt n
sm : s * s + (n - s * s) = n
h : ¬n - sqrt n * sqrt n < sqrt n
⊢ n ≤ s * s + (s + s)
[PROOFSTEP]
rw [← add_assoc]
[GOAL]
n : ℕ
s : ℕ := sqrt n
sm : s * s + (n - s * s) = n
h : ¬n - sqrt n * sqrt n < sqrt n
⊢ n ≤ s * s + s + s
[PROOFSTEP]
apply sqrt_le_add
[GOAL]
case neg
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
[PROOFSTEP]
simp [pair, hl.not_lt, add_assoc, add_tsub_cancel_of_le (le_of_not_gt h), sm]
[GOAL]
n a b : ℕ
H : unpair n = (a, b)
⊢ pair a b = n
[PROOFSTEP]
simpa [H] using pair_unpair n
[GOAL]
a b : ℕ
⊢ unpair (pair a b) = (a, b)
[PROOFSTEP]
dsimp only [pair]
[GOAL]
a b : ℕ
⊢ unpair (if a < b then b * b + a else a * a + a + b) = (a, b)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
a b : ℕ
h : a < b
⊢ unpair (b * b + a) = (a, b)
[PROOFSTEP]
show unpair (b * b + a) = (a, b)
[GOAL]
case pos
a b : ℕ
h : a < b
⊢ unpair (b * b + a) = (a, b)
[PROOFSTEP]
have be : sqrt (b * b + a) = b := sqrt_add_eq _ (le_trans (le_of_lt h) (Nat.le_add_left _ _))
[GOAL]
case pos
a b : ℕ
h : a < b
be : sqrt (b * b + a) = b
⊢ unpair (b * b + a) = (a, b)
[PROOFSTEP]
simp [unpair, be, add_tsub_cancel_right, h]
[GOAL]
case neg
a b : ℕ
h : ¬a < b
⊢ unpair (a * a + a + b) = (a, b)
[PROOFSTEP]
show unpair (a * a + a + b) = (a, b)
[GOAL]
case neg
a b : ℕ
h : ¬a < b
⊢ unpair (a * a + a + b) = (a, b)
[PROOFSTEP]
have ae : sqrt (a * a + (a + b)) = a := by
  rw [sqrt_add_eq]
  exact add_le_add_left (le_of_not_gt h) _
[GOAL]
a b : ℕ
h : ¬a < b
⊢ sqrt (a * a + (a + b)) = a
[PROOFSTEP]
rw [sqrt_add_eq]
[GOAL]
case h
a b : ℕ
h : ¬a < b
⊢ a + b ≤ a + a
[PROOFSTEP]
exact add_le_add_left (le_of_not_gt h) _
[GOAL]
case neg
a b : ℕ
h : ¬a < b
ae : sqrt (a * a + (a + b)) = a
⊢ unpair (a * a + a + b) = (a, b)
[PROOFSTEP]
simp [unpair, ae, Nat.not_lt_zero, add_assoc]
[GOAL]
n : ℕ
n1 : 1 ≤ n
⊢ (unpair n).fst < n
[PROOFSTEP]
let s := sqrt n
[GOAL]
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
⊢ (unpair n).fst < n
[PROOFSTEP]
simp [unpair]
[GOAL]
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
[PROOFSTEP]
by_cases h : n - s * s < s
[GOAL]
case pos
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : n - s * s < s
⊢ (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
[PROOFSTEP]
simp [h]
[GOAL]
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : ¬n - s * s < s
⊢ (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
[PROOFSTEP]
simp [h]
[GOAL]
case pos
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : n - s * s < s
⊢ n - sqrt n * sqrt n < n
[PROOFSTEP]
exact lt_of_lt_of_le h (sqrt_le_self _)
[GOAL]
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : ¬n - s * s < s
⊢ sqrt n < n
[PROOFSTEP]
simp at h 
[GOAL]
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : sqrt n ≤ n - sqrt n * sqrt n
⊢ sqrt n < n
[PROOFSTEP]
have s0 : 0 < s := sqrt_pos.2 n1
[GOAL]
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := sqrt n
h : sqrt n ≤ n - sqrt n * sqrt n
s0 : 0 < s
⊢ sqrt n < n
[PROOFSTEP]
exact lt_of_le_of_lt h (tsub_lt_self n1 (mul_pos s0 s0))
[GOAL]
⊢ unpair 0 = 0
[PROOFSTEP]
rw [unpair]
[GOAL]
⊢ (let s := sqrt 0;
    if 0 - s * s < s then (0 - s * s, s) else (s, 0 - s * s - s)) =
    0
[PROOFSTEP]
simp
[GOAL]
⊢ (unpair 0).fst ≤ 0
[PROOFSTEP]
simp
[GOAL]
a b : ℕ
⊢ a ≤ pair a b
[PROOFSTEP]
simpa using unpair_left_le (pair a b)
[GOAL]
a b : ℕ
⊢ b ≤ pair a b
[PROOFSTEP]
by_cases h : a < b
[GOAL]
case pos
a b : ℕ
h : a < b
⊢ b ≤ pair a b
[PROOFSTEP]
simp [pair, h]
[GOAL]
case neg
a b : ℕ
h : ¬a < b
⊢ b ≤ pair a b
[PROOFSTEP]
simp [pair, h]
[GOAL]
case pos
a b : ℕ
h : a < b
⊢ b ≤ b * b + a
[PROOFSTEP]
exact le_trans (le_mul_self _) (Nat.le_add_right _ _)
[GOAL]
n : ℕ
⊢ (unpair n).snd ≤ n
[PROOFSTEP]
simpa using right_le_pair n.unpair.1 n.unpair.2
[GOAL]
a₁ a₂ b : ℕ
h : a₁ < a₂
⊢ pair a₁ b < pair a₂ b
[PROOFSTEP]
by_cases h₁ : a₁ < b
[GOAL]
case pos
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
⊢ pair a₁ b < pair a₂ b
[PROOFSTEP]
simp [pair, h₁, add_assoc]
[GOAL]
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ pair a₁ b < pair a₂ b
[PROOFSTEP]
simp [pair, h₁, add_assoc]
[GOAL]
case pos
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
[PROOFSTEP]
by_cases h₂ : a₂ < b
[GOAL]
case pos
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : a₂ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
[PROOFSTEP]
simp [pair, h₂, h]
[GOAL]
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
[PROOFSTEP]
simp [pair, h₂, h]
[GOAL]
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : ¬a₂ < b
⊢ b * b + a₁ < a₂ * a₂ + (a₂ + b)
[PROOFSTEP]
simp at h₂ 
[GOAL]
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ b * b + a₁ < a₂ * a₂ + (a₂ + b)
[PROOFSTEP]
apply add_lt_add_of_le_of_lt
[GOAL]
case neg.h₁
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ b * b ≤ a₂ * a₂
case neg.h₂ a₁ a₂ b : ℕ h : a₁ < a₂ h₁ : a₁ < b h₂ : b ≤ a₂ ⊢ a₁ < a₂ + b
[PROOFSTEP]
exact mul_self_le_mul_self h₂
[GOAL]
case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : b ≤ a₂
⊢ a₁ < a₂ + b
[PROOFSTEP]
exact Nat.lt_add_right _ _ _ h
[GOAL]
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : ¬a₁ < b
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
[PROOFSTEP]
simp at h₁ 
[GOAL]
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
[PROOFSTEP]
simp [not_lt_of_gt (lt_of_le_of_lt h₁ h)]
[GOAL]
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ + (a₁ + b) < a₂ * a₂ + (a₂ + b)
[PROOFSTEP]
apply add_lt_add
[GOAL]
case neg.h₁
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ < a₂ * a₂
case neg.h₂ a₁ a₂ b : ℕ h : a₁ < a₂ h₁ : b ≤ a₁ ⊢ a₁ + b < a₂ + b
[PROOFSTEP]
exact mul_self_lt_mul_self h
[GOAL]
case neg.h₂
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ + b < a₂ + b
[PROOFSTEP]
apply add_lt_add_right
[GOAL]
case neg.h₂.bc
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ < a₂
[PROOFSTEP]
assumption
[GOAL]
a b₁ b₂ : ℕ
h : b₁ < b₂
⊢ pair a b₁ < pair a b₂
[PROOFSTEP]
by_cases h₁ : a < b₁
[GOAL]
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : a < b₁
⊢ pair a b₁ < pair a b₂
[PROOFSTEP]
simp [pair, h₁, add_assoc]
[GOAL]
case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
⊢ pair a b₁ < pair a b₂
[PROOFSTEP]
simp [pair, h₁, add_assoc]
[GOAL]
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : a < b₁
⊢ b₁ * b₁ + a < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
[PROOFSTEP]
simp [pair, lt_trans h₁ h, h]
[GOAL]
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : a < b₁
⊢ b₁ * b₁ < b₂ * b₂
[PROOFSTEP]
exact mul_self_lt_mul_self h
[GOAL]
case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
[PROOFSTEP]
by_cases h₂ : a < b₂
[GOAL]
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
[PROOFSTEP]
simp [pair, h₂, h]
[GOAL]
case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : ¬a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
[PROOFSTEP]
simp [pair, h₂, h]
[GOAL]
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < b₂ * b₂ + a
[PROOFSTEP]
simp at h₁ 
[GOAL]
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₂ : a < b₂
h₁ : b₁ ≤ a
⊢ a * a + (a + b₁) < b₂ * b₂ + a
[PROOFSTEP]
rw [add_comm, add_comm _ a, add_assoc, add_lt_add_iff_left]
[GOAL]
case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₂ : a < b₂
h₁ : b₁ ≤ a
⊢ b₁ + a * a < b₂ * b₂
[PROOFSTEP]
rwa [add_comm, ← sqrt_lt, sqrt_add_eq]
[GOAL]
case pos.h
a b₁ b₂ : ℕ
h : b₁ < b₂
h₂ : a < b₂
h₁ : b₁ ≤ a
⊢ b₁ ≤ a + a
[PROOFSTEP]
exact le_trans h₁ (Nat.le_add_left _ _)
[GOAL]
m n : ℕ
⊢ pair m n < (max m n + 1) ^ 2
[PROOFSTEP]
rw [pair, add_sq, mul_one, two_mul, sq, add_assoc, add_assoc]
[GOAL]
m n : ℕ
⊢ (if m < n then n * n + m else m * m + (m + n)) < max m n * max m n + (max m n + max m n + 1 ^ 2)
[PROOFSTEP]
cases' (lt_or_le m n) with h h
[GOAL]
case inl
m n : ℕ
h : m < n
⊢ (if m < n then n * n + m else m * m + (m + n)) < max m n * max m n + (max m n + max m n + 1 ^ 2)
case inr
m n : ℕ
h : n ≤ m
⊢ (if m < n then n * n + m else m * m + (m + n)) < max m n * max m n + (max m n + max m n + 1 ^ 2)
[PROOFSTEP]
rw [if_pos h, max_eq_right h.le, add_lt_add_iff_left, add_assoc]
[GOAL]
case inl
m n : ℕ
h : m < n
⊢ m < n + (n + 1 ^ 2)
case inr
m n : ℕ
h : n ≤ m
⊢ (if m < n then n * n + m else m * m + (m + n)) < max m n * max m n + (max m n + max m n + 1 ^ 2)
[PROOFSTEP]
exact h.trans_le (self_le_add_right n _)
[GOAL]
case inr
m n : ℕ
h : n ≤ m
⊢ (if m < n then n * n + m else m * m + (m + n)) < max m n * max m n + (max m n + max m n + 1 ^ 2)
[PROOFSTEP]
rw [if_neg h.not_lt, max_eq_left h, add_lt_add_iff_left, add_assoc, add_lt_add_iff_left]
[GOAL]
case inr
m n : ℕ
h : n ≤ m
⊢ n < m + 1 ^ 2
[PROOFSTEP]
exact lt_succ_of_le h
[GOAL]
m n : ℕ
⊢ max m n ^ 2 + min m n ≤ pair m n
[PROOFSTEP]
rw [pair]
[GOAL]
m n : ℕ
⊢ max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
[PROOFSTEP]
cases' lt_or_le m n with h h
[GOAL]
case inl
m n : ℕ
h : m < n
⊢ max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
case inr m n : ℕ h : n ≤ m ⊢ max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
[PROOFSTEP]
rw [if_pos h, max_eq_right h.le, min_eq_left h.le, sq]
[GOAL]
case inr
m n : ℕ
h : n ≤ m
⊢ max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
[PROOFSTEP]
rw [if_neg h.not_lt, max_eq_left h, min_eq_right h, sq, add_assoc, add_le_add_iff_left]
[GOAL]
case inr
m n : ℕ
h : n ≤ m
⊢ n ≤ m + n
[PROOFSTEP]
exact le_add_self
[GOAL]
m n : ℕ
⊢ m + n ≤ max m n ^ 2 + min m n
[PROOFSTEP]
rw [sq, ← min_add_max, add_comm, add_le_add_iff_right]
[GOAL]
m n : ℕ
⊢ max m n ≤ max m n * max m n
[PROOFSTEP]
exact le_mul_self _
[GOAL]
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → ℕ → α
⊢ ⨆ (n : ℕ), f (unpair n).fst (unpair n).snd = ⨆ (i : ℕ) (j : ℕ), f i j
[PROOFSTEP]
rw [← (iSup_prod : ⨆ i : ℕ × ℕ, f i.1 i.2 = _), ← Nat.surjective_unpair.iSup_comp]
[GOAL]
α : Type u_1
β : Type u_2
s : ℕ → Set α
t : ℕ → Set β
⊢ ⋃ (n : ℕ), s (unpair n).fst ×ˢ t (unpair n).snd = (⋃ (n : ℕ), s n) ×ˢ ⋃ (n : ℕ), t n
[PROOFSTEP]
rw [← Set.iUnion_prod]
[GOAL]
α : Type u_1
β : Type u_2
s : ℕ → Set α
t : ℕ → Set β
⊢ ⋃ (n : ℕ), s (unpair n).fst ×ˢ t (unpair n).snd = ⋃ (x : ℕ × ℕ), s x.fst ×ˢ t x.snd
[PROOFSTEP]
exact surjective_unpair.iUnion_comp (fun x => s x.fst ×ˢ t x.snd)
