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

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

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

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

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

State before:
case inl
x✝ y x : ℝ
h : 0 ≤ x
⊢ -x ≤ x
Tactic:
linarith
State after:
no goals

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