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

State before:
α : Type
inst✝ : AddGroup α
S : Set α
x s : α
⊢ s ∈ S + {x} ↔ s - x ∈ S
Tactic:
rw [Set.add_singleton, Set.mem_image]
State after:
α : Type
inst✝ : AddGroup α
S : Set α
x s : α
⊢ (∃ x_1 ∈ S, x_1 + x = s) ↔ s - x ∈ S

State before:
α : Type
inst✝ : AddGroup α
S : Set α
x s : α
⊢ (∃ x_1 ∈ S, x_1 + x = s) ↔ s - x ∈ S
Tactic:
constructor
State after:
case mp
α : Type
inst✝ : AddGroup α
S : Set α
x s : α
⊢ (∃ x_1 ∈ S, x_1 + x = s) → s - x ∈ S

case mpr
α : Type
inst✝ : AddGroup α
S : Set α
x s : α
⊢ s - x ∈ S → ∃ x_1 ∈ S, x_1 + x = s

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

State before:
case mp.intro.intro
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
hy : y ∈ S
⊢ y + x - x ∈ S
Tactic:
rw [add_sub_cancel]
State after:
case mp.intro.intro
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
hy : y ∈ S
⊢ y ∈ S

State before:
case mp.intro.intro
α : Type
inst✝ : AddGroup α
S : Set α
x y : α
hy : y ∈ S
⊢ y ∈ S
Tactic:
exact hy
State after:
no goals

State before:
case mpr
α : Type
inst✝ : AddGroup α
S : Set α
x s : α
⊢ s - x ∈ S → ∃ x_1 ∈ S, x_1 + x = s
Tactic:
intro h
State after:
case mpr
α : Type
inst✝ : AddGroup α
S : Set α
x s : α
h : s - x ∈ S
⊢ ∃ x_1 ∈ S, x_1 + x = s

State before:
case mpr
α : Type
inst✝ : AddGroup α
S : Set α
x s : α
h : s - x ∈ S
⊢ ∃ x_1 ∈ S, x_1 + x = s
Tactic:
exact ⟨s - x, h, by rw [sub_add_cancel]⟩
State after:
no goals

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