Theorem: Set.sub_eq_neg_add (src/Pre.lean)

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

State before:
case h
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
⊢ y ∈ S - {x} ↔ y ∈ S + {-x}
Tactic:
simp only [sub_singleton, mem_image, add_singleton, image_add_right, neg_neg, mem_preimage]
State after:
case h
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
⊢ (∃ x_1 ∈ S, x_1 - x = y) ↔ y + x ∈ S

State before:
case h
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
⊢ (∃ x_1 ∈ S, x_1 - x = y) ↔ y + x ∈ S
Tactic:
refine ⟨ ?_, fun h => ⟨y + x, h, by rw [add_sub_cancel]⟩ ⟩
State after:
case h
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
⊢ (∃ x_1 ∈ S, x_1 - x = y) → y + x ∈ S

State before:
case h
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
⊢ (∃ x_1 ∈ S, x_1 - x = y) → y + x ∈ S
Tactic:
rintro ⟨z, hz, rfl⟩
State after:
case h.intro.intro
α : Type
inst✝ : AddGroup α
S : Set α
x z : α
hz : z ∈ S
⊢ z - x + x ∈ S

State before:
case h.intro.intro
α : Type
inst✝ : AddGroup α
S : Set α
x z : α
hz : z ∈ S
⊢ z - x + x ∈ S
Tactic:
rw [sub_add_cancel]
State after:
case h.intro.intro
α : Type
inst✝ : AddGroup α
S : Set α
x z : α
hz : z ∈ S
⊢ z ∈ S

State before:
case h.intro.intro
α : Type
inst✝ : AddGroup α
S : Set α
x z : α
hz : z ∈ S
⊢ z ∈ S
Tactic:
exact hz
State after:
no goals

State before:
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
h : y + x ∈ S
⊢ y + x - x = y
Tactic:
rw [add_sub_cancel]
State after:
no goals