Theorem: LoVe.min_add_add (LoVe/Lectures/LoVe05_FunctionalProgramming_Demo.lean)

State before:
l m n : ℕ
⊢ min (m + l) (n + l) = min m n + l
Tactic:
cases Classical.em (m ≤ n) with
| inl h => simp [min, h]
| inr h => simp [min, h]
State after:
no goals

State before:
case inl
l m n : ℕ
h : m ≤ n
⊢ min (m + l) (n + l) = min m n + l
Tactic:
simp [min, h]
State after:
no goals

State before:
case inr
l m n : ℕ
h : ¬m ≤ n
⊢ min (m + l) (n + l) = min m n + l
Tactic:
simp [min, h]
State after:
no goals