m✝ n✝ k l m n : ℕ
h : 0 < m + n
⊢ 0 < m ∨ 0 < n
m✝ n✝ k l m n : ℕ
⊢ 0 < m + n → 0 < m ∨ 0 < n
intro h
case zero
m n✝ k l n : ℕ
h : 0 < zero + n
⊢ 0 < zero ∨ 0 < n

case succ
m✝ n✝ k l n m : ℕ
h : 0 < succ m + n
⊢ 0 < succ m ∨ 0 < n
m✝ n✝ k l m n : ℕ
h : 0 < m + n
⊢ 0 < m ∨ 0 < n
cases' m with m
no goals
case succ
m✝ n✝ k l n m : ℕ
h : 0 < succ m + n
⊢ 0 < succ m ∨ 0 < n
exact Or.inl (succ_pos _)
case zero
m n✝ k l n : ℕ
h : 0 < n
⊢ 0 < zero ∨ 0 < n
case zero
m n✝ k l n : ℕ
h : 0 < zero + n
⊢ 0 < zero ∨ 0 < n
simp [zero_add] at h
no goals
case zero
m n✝ k l n : ℕ
h : 0 < n
⊢ 0 < zero ∨ 0 < n
exact Or.inr h
m✝ n✝ k l m n : ℕ
h : 0 < m ∨ 0 < n
⊢ 0 < m + n
m✝ n✝ k l m n : ℕ
⊢ 0 < m ∨ 0 < n → 0 < m + n
intro h
case inl
m✝ n✝ k l m n : ℕ
mpos : 0 < m
⊢ 0 < m + n

case inr
m✝ n✝ k l m n : ℕ
npos : 0 < n
⊢ 0 < m + n
m✝ n✝ k l m n : ℕ
h : 0 < m ∨ 0 < n
⊢ 0 < m + n
cases' h with mpos npos
no goals
case inr
m✝ n✝ k l m n : ℕ
npos : 0 < n
⊢ 0 < m + n
apply add_pos_right _ npos
no goals
case inl
m✝ n✝ k l m n : ℕ
mpos : 0 < m
⊢ 0 < m + n
apply add_pos_left mpos