case pos
m✝ n✝ k m n : ℕ
h1 : m ≤ n
⊢ max (succ m) (succ n) = succ (max m n)

case neg
m✝ n✝ k m n : ℕ
h1 : ¬m ≤ n
⊢ max (succ m) (succ n) = succ (max m n)
m✝ n✝ k m n : ℕ
⊢ max (succ m) (succ n) = succ (max m n)
by_cases h1 : m ≤ n
case neg
m✝ n✝ k m n : ℕ
h1 : ¬m ≤ n
⊢ max (succ m) (succ n) = succ (max m n)
case pos
m✝ n✝ k m n : ℕ
h1 : m ≤ n
⊢ max (succ m) (succ n) = succ (max m n)

case neg
m✝ n✝ k m n : ℕ
h1 : ¬m ≤ n
⊢ max (succ m) (succ n) = succ (max m n)
rw [max_eq_right h1, max_eq_right (succ_le_succ h1)]
case neg
m✝ n✝ k m n : ℕ
h1 : n < m
⊢ max (succ m) (succ n) = succ (max m n)
case neg
m✝ n✝ k m n : ℕ
h1 : ¬m ≤ n
⊢ max (succ m) (succ n) = succ (max m n)
rw [not_le] at h1
case neg
m✝ n✝ k m n : ℕ
h1 : n < m
h2 : n ≤ m
⊢ max (succ m) (succ n) = succ (max m n)
case neg
m✝ n✝ k m n : ℕ
h1 : n < m
⊢ max (succ m) (succ n) = succ (max m n)
have h2 := le_of_lt h1
no goals
case neg
m✝ n✝ k m n : ℕ
h1 : n < m
h2 : n ≤ m
⊢ max (succ m) (succ n) = succ (max m n)
rw [max_eq_left h2, max_eq_left (succ_le_succ h2)]