exact if c: a ≤ b 
  then by
    unfold max
    unfold Nat.instMaxNat
    unfold maxOfLe
    simp [if_pos c]
  else by
    unfold max
    unfold Nat.instMaxNat
    unfold maxOfLe
    simp [if_neg c]
R : Type ?u.126771
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.126786
inst✝ : DecidableEq X
a b : ℕ
⊢ max a b = a ∨ max a b = b
no goals