n m : Nat
⊢ n - m = n - if n ≤ m then n else m
n m : Nat
⊢ n - m = n - min n m
rw [Nat.min_def]
case inl
n m : Nat
h✝ : n ≤ m
⊢ n - m = n - n

case inr
n m : Nat
h✝ : ¬n ≤ m
⊢ n - m = n - m
n m : Nat
⊢ n - m = n - if n ≤ m then n else m
split
no goals
case inl
n m : Nat
h✝ : n ≤ m
⊢ n - m = n - n
rw [Nat.sub_eq_zero_of_le ‹n ≤ m›, Nat.sub_self]
no goals
case inr
n m : Nat
h✝ : ¬n ≤ m
⊢ n - m = n - m
rfl