case refine'_1
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
a b : α
h : abs a = abs b
⊢ a = b ∨ a = -b

case refine'_2
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
a b : α
h : a = b ∨ a = -b
⊢ abs a = abs b
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
a b : α
⊢ abs a = abs b ↔ a = b ∨ a = -b
refine' ⟨fun h => _, fun h => _⟩
no goals
case refine'_1
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
a b : α
h : abs a = abs b
⊢ a = b ∨ a = -b
obtain rfl | rfl := eq_or_eq_neg_of_abs_eq h <;>
  simpa only [neg_eq_iff_eq_neg (a := |b|), neg_inj, or_comm] using abs_choice b
no goals
case refine'_2
α : Type u_1
inst✝¹ : AddGroup α
inst✝ : LinearOrder α
a b : α
h : a = b ∨ a = -b
⊢ abs a = abs b
cases' h with h h <;>
simp [h, abs_neg]