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

State before:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : { x // x ∈ map f s }
y : α
⊢ y = ↑((mapEquiv s f).symm x) ↔ f y = ↑x
Tactic:
rw [eq_comm]
State after:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : { x // x ∈ map f s }
y : α
⊢ ↑((mapEquiv s f).symm x) = y ↔ f y = ↑x

State before:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : { x // x ∈ map f s }
y : α
⊢ ↑((mapEquiv s f).symm x) = y ↔ f y = ↑x
Tactic:
simp
State after:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : { x // x ∈ map f s }
y : α
⊢ ↑x = f y ↔ f y = ↑x

State before:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : { x // x ∈ map f s }
y : α
⊢ ↑x = f y ↔ f y = ↑x
Tactic:
apply eq_comm
State after:
no goals