m n : ℕ
⊢ (if n ≤ m then some (m - n) else none) = psub m n
m n : ℕ
⊢ psub' m n = psub m n
rw [psub']
case inl
m n : ℕ
h : n ≤ m
⊢ some (m - n) = psub m n

case inr
m n : ℕ
h : ¬n ≤ m
⊢ none = psub m n
m n : ℕ
⊢ (if n ≤ m then some (m - n) else none) = psub m n
split_ifs with h
case inr
m n : ℕ
h : ¬n ≤ m
⊢ none = psub m n
case inl
m n : ℕ
h : n ≤ m
⊢ some (m - n) = psub m n

case inr
m n : ℕ
h : ¬n ≤ m
⊢ none = psub m n
exact (psub_eq_sub h).symm
no goals
case inr
m n : ℕ
h : ¬n ≤ m
⊢ none = psub m n
exact (psub_eq_none.2 (not_le.1 h)).symm