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)
m n : ℕ
⊢ pair m n < (max m n + 1) ^ 2
rw [pair, add_sq, mul_one, two_mul, sq, add_assoc, add_assoc]
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)
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)
cases' (lt_or_le m n) with h h
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)
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)
rw [if_pos h, max_eq_right h.le, add_lt_add_iff_left, add_assoc]
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)
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)
exact h.trans_le (self_le_add_right n _)
case inr
m n : ℕ
h : n ≤ m
⊢ n < m + 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)
rw [if_neg h.not_lt, max_eq_left h, add_lt_add_iff_left, add_assoc, add_lt_add_iff_left]
no goals
case inr
m n : ℕ
h : n ≤ m
⊢ n < m + 1 ^ 2
exact lt_succ_of_le h