Theorem: Set.neg_add_cancel_right' (src/Pre.lean)

State before:
α : Type
inst✝ : AddGroup α
S : Set α
x : α
⊢ S - {x} + {x} = S
Tactic:
ext y
State after:
case h
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
⊢ y ∈ S - {x} + {x} ↔ y ∈ S

State before:
case h
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
⊢ y ∈ S - {x} + {x} ↔ y ∈ S
Tactic:
simp only [sub_singleton, add_singleton, mem_image, exists_exists_and_eq_and, sub_add_cancel, exists_eq_right]
State after:
no goals