case pos
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : 0 ≤ a
⊢ abs a = a ∧ 0 ≤ a ∨ abs a = -a ∧ a < 0

case neg
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : ¬0 ≤ a
⊢ abs a = a ∧ 0 ≤ a ∨ abs a = -a ∧ a < 0
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ abs a = a ∧ 0 ≤ a ∨ abs a = -a ∧ a < 0
by_cases h : 0 ≤ a
case pos.h
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : 0 ≤ a
⊢ abs a = a ∧ 0 ≤ a
case pos
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : 0 ≤ a
⊢ abs a = a ∧ 0 ≤ a ∨ abs a = -a ∧ a < 0
left
no goals
case pos.h
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : 0 ≤ a
⊢ abs a = a ∧ 0 ≤ a
exact ⟨abs_eq_self.mpr h, h⟩
case neg.h
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : ¬0 ≤ a
⊢ abs a = -a ∧ a < 0
case neg
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : ¬0 ≤ a
⊢ abs a = a ∧ 0 ≤ a ∨ abs a = -a ∧ a < 0
right
case neg.h
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : a < 0
⊢ abs a = -a ∧ a < 0
case neg.h
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : ¬0 ≤ a
⊢ abs a = -a ∧ a < 0
push_neg at h
no goals
case neg.h
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
h : a < 0
⊢ abs a = -a ∧ a < 0
exact ⟨abs_eq_neg_self.mpr (le_of_lt h), h⟩