Theorem: Set.Finite.translation (src/Pre.lean)

State before:
α : Type
inst✝ : AddGroup α
S : Set α
hS : Set.Finite S
x : α
⊢ Set.Finite (S + {x})
Tactic:
rw [Set.add_singleton]
State after:
α : Type
inst✝ : AddGroup α
S : Set α
hS : Set.Finite S
x : α
⊢ Set.Finite ((fun x_1 => x_1 + x) '' S)

State before:
α : Type
inst✝ : AddGroup α
S : Set α
hS : Set.Finite S
x : α
⊢ Set.Finite ((fun x_1 => x_1 + x) '' S)
Tactic:
exact Set.Finite.image _ hS
State after:
no goals