case inl
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b c a : α
h : 0 ≤ a
⊢ -abs a ≤ a

case inr
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b c a : α
h : a ≤ 0
⊢ -abs a ≤ a
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b c a : α
⊢ -abs a ≤ a
cases' le_total 0 a with h h
no goals
case inl
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b c a : α
h : 0 ≤ a
⊢ -abs a ≤ a
calc
  -|a| = -a := congr_arg Neg.neg (abs_of_nonneg h)
  _ ≤ 0 := neg_nonpos.mpr h
  _ ≤ a := h
no goals
case inr
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b c a : α
h : a ≤ 0
⊢ -abs a ≤ a
calc
  -|a| = - -a := congr_arg Neg.neg (abs_of_nonpos h)
  _ ≤ a := (neg_neg a).le