a b : Int
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b
a b : Int
⊢ max a b = max b a
simp only [Int.max_def]
case pos
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
⊢ b = a

case neg
a b : Int
h₁ : ¬a ≤ b
h₂ : ¬b ≤ a
⊢ a = b
a b : Int
⊢ (if a ≤ b then b else a) = if b ≤ a then a else b
by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]
no goals
case pos
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
⊢ b = a
exact Int.le_antisymm h₂ h₁
no goals
case neg
a b : Int
h₁ : ¬a ≤ b
h₂ : ¬b ≤ a
⊢ a = b
cases not_or_intro h₁ h₂ <| Int.le_total ..