α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
hb : 0 ≤ b
⊢ a = b ∨ a = -b → abs a = b
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
hb : 0 ≤ b
⊢ abs a = b ↔ a = b ∨ a = -b
refine' ⟨eq_or_eq_neg_of_abs_eq, _⟩
no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
hb : 0 ≤ b
⊢ a = b ∨ a = -b → abs a = b
rintro (rfl | rfl) <;> simp only [abs_neg, abs_of_nonneg hb]