no goals
G✝ : Type ?u.2524
G' : Type ?u.2527
inst✝⁵ : Group G✝
inst✝⁴ : Group G'
A : Type ?u.2536
inst✝³ : AddGroup A
S : Type u_1
G : Type u_2
inst✝² : InvolutiveNeg G
inst✝¹ : LinearOrder G
x✝ : SetLike S G
inst✝ : NegMemClass S G
H : S
x : G
⊢ abs x ∈ H ↔ x ∈ H
cases abs_choice x <;> simp [*]