a b : Nat
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a
a b : Nat
⊢ min a b = min b a
simp [Nat.min_def]
case inl.inl
a b : Nat
h✝¹ : a ≤ b
h✝ : b ≤ a
⊢ a = b

case inr.inr
a b : Nat
h✝¹ : ¬a ≤ b
h✝ : ¬b ≤ a
⊢ b = a
a b : Nat
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a
split <;> split <;> simp [*]
no goals
case inl.inl
a b : Nat
h✝¹ : a ≤ b
h✝ : b ≤ a
⊢ a = b
next h₁ h₂ => exact Nat.le_antisymm h₁ h₂
no goals
a b : Nat
h₁ : a ≤ b
h₂ : b ≤ a
⊢ a = b
exact Nat.le_antisymm h₁ h₂
no goals
case inr.inr
a b : Nat
h✝¹ : ¬a ≤ b
h✝ : ¬b ≤ a
⊢ b = a
next h₁ h₂ => cases not_or_intro h₁ h₂ <| Nat.le_total ..
no goals
a b : Nat
h₁ : ¬a ≤ b
h₂ : ¬b ≤ a
⊢ b = a
cases not_or_intro h₁ h₂ <| Nat.le_total ..