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

case neg
a b : Int
h₁ : ¬a ≤ b
h₂ : ¬b ≤ a
⊢ b = a
a b : Int
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a
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
⊢ a = b
exact Int.le_antisymm h₁ h₂
no goals
case neg
a b : Int
h₁ : ¬a ≤ b
h₂ : ¬b ≤ a
⊢ b = a
cases not_or_intro h₁ h₂ <| Int.le_total ..