Theorem: C03S05.MyAbs.le_abs_self (LeanInRome/S3_Logic/solutions/Solutions_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]
  linarith
State after:
no goals

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

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

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