Theorem: C03S05.MyAbs.abs_addαα (MIL/C03_Logic/S05_Disjunction.lean)

State before:
x✝ y✝ x y : ℝ
⊢ |x + y| ≤ |x| + |y|
Tactic:
rcases le_or_gt 0 (x + y) with h | h
State after:
case inl
x✝ y✝ x y : ℝ
h : 0 ≤ x + y
⊢ |x + y| ≤ |x| + |y|

case inr
x✝ y✝ x y : ℝ
h : 0 > x + y
⊢ |x + y| ≤ |x| + |y|

State before:
case inr
x✝ y✝ x y : ℝ
h : 0 > x + y
⊢ |x + y| ≤ |x| + |y|
Tactic:
. rw [abs_of_neg h]
  linarith [neg_le_abs_self x, neg_le_abs_self y]
State after:
no goals

State before:
case inl
x✝ y✝ x y : ℝ
h : 0 ≤ x + y
⊢ |x + y| ≤ |x| + |y|
Tactic:
rw [abs_of_nonneg h]
State after:
case inl
x✝ y✝ x y : ℝ
h : 0 ≤ x + y
⊢ x + y ≤ |x| + |y|

State before:
case inl
x✝ y✝ x y : ℝ
h : 0 ≤ x + y
⊢ x + y ≤ |x| + |y|
Tactic:
linarith [le_abs_self x, le_abs_self y]
State after:
no goals

State before:
case inr
x✝ y✝ x y : ℝ
h : 0 > x + y
⊢ |x + y| ≤ |x| + |y|
Tactic:
rw [abs_of_neg h]
State after:
case inr
x✝ y✝ x y : ℝ
h : 0 > x + y
⊢ -(x + y) ≤ |x| + |y|

State before:
case inr
x✝ y✝ x y : ℝ
h : 0 > x + y
⊢ -(x + y) ≤ |x| + |y|
Tactic:
linarith [neg_le_abs_self x, neg_le_abs_self y]
State after:
no goals