Theorem: Finset.getUnique_mem (LeanSAT/Upstream/ToMathlib.lean)

State before:
α : Type u_1
xs : Finset α
h : ∃ x, xs = {x}
y : Finset α
⊢ getUnique xs h ∈ y ↔ xs ⊆ y
Tactic:
generalize hv : getUnique xs h = v
State after:
α : Type u_1
xs : Finset α
h : ∃ x, xs = {x}
y : Finset α
v : α
hv : getUnique xs h = v
⊢ v ∈ y ↔ xs ⊆ y

State before:
α : Type u_1
xs : Finset α
h : ∃ x, xs = {x}
y : Finset α
v : α
hv : getUnique xs h = v
⊢ v ∈ y ↔ xs ⊆ y
Tactic:
simp at hv
State after:
α : Type u_1
xs : Finset α
h : ∃ x, xs = {x}
y : Finset α
v : α
hv : xs = {v}
⊢ v ∈ y ↔ xs ⊆ y

State before:
α : Type u_1
xs : Finset α
h : ∃ x, xs = {x}
y : Finset α
v : α
hv : xs = {v}
⊢ v ∈ y ↔ xs ⊆ y
Tactic:
simp [hv]
State after:
no goals