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

State before:
α' : Type ?u.103548
α : Type ?u.103533
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α
h : f x ∈ map f s
⊢ x ∈ s
Tactic:
simp at h
State after:
α' : Type ?u.103548
α : Type ?u.103533
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α
h : x ∈ s
⊢ x ∈ s

State before:
α' : Type ?u.103548
α : Type ?u.103533
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α
h : x ∈ s
⊢ x ∈ s
Tactic:
exact h
State after:
no goals

State before:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α
h : f x ∈ map f s
⊢ (mapEquiv s f).symm { val := f x, property := h } = { val := x, property := ⋯ }
Tactic:
simp [mapEquiv]
State after:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α
h : f x ∈ map f s
⊢ filter (fun x_1 => f x_1 = f x) s = {x}

State before:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α
h : f x ∈ map f s
⊢ filter (fun x_1 => f x_1 = f x) s = {x}
Tactic:
rw [eq_singleton_iff_unique_mem]
State after:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α
h : f x ∈ map f s
⊢ x ∈ filter (fun x_1 => f x_1 = f x) s ∧ ∀ x_1 ∈ filter (fun x_2 => f x_2 = f x) s, x_1 = x

State before:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α
h : f x ∈ map f s
⊢ x ∈ filter (fun x_1 => f x_1 = f x) s ∧ ∀ x_1 ∈ filter (fun x_2 => f x_2 = f x) s, x_1 = x
Tactic:
simpa using h
State after:
no goals