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 : α
ha : a < 0
⊢ 0 < abs a ↔ a ≠ 0

case inr.inl
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b c : α
⊢ 0 < abs 0 ↔ 0 ≠ 0

case inr.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 : α
ha : 0 < a
⊢ 0 < abs a ↔ a ≠ 0
α : 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 : α
⊢ 0 < abs a ↔ a ≠ 0
rcases lt_trichotomy a 0 with (ha | rfl | ha)
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 : α
ha : a < 0
⊢ 0 < abs a ↔ a ≠ 0
simp [abs_of_neg ha, neg_pos, ha.ne, ha]
no goals
case inr.inl
α : Type u_1
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
b c : α
⊢ 0 < abs 0 ↔ 0 ≠ 0
simp
no goals
case inr.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 : α
ha : 0 < a
⊢ 0 < abs a ↔ a ≠ 0
simp [abs_of_pos ha, ha, ha.ne.symm]