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

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 ↔ ↑x = f y
Tactic:
rcases x with ⟨x,hx⟩
State after:
case mk
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y : α
x : α'
hx : x ∈ map f s
⊢ ↑((mapEquiv s f).symm { val := x, property := hx }) = y ↔ ↑{ val := x, property := hx } = f y

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

State before:
case mk
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y : α
x : α'
hx : x ∈ map f s
⊢ filter (fun x_1 => f x_1 = x) s = {y} ↔ x = f y
Tactic:
simp at hx
State after:
case mk
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y : α
x : α'
hx : ∃ a ∈ s, f a = x
⊢ filter (fun x_1 => f x_1 = x) s = {y} ↔ x = f y

State before:
case mk
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y : α
x : α'
hx : ∃ a ∈ s, f a = x
⊢ filter (fun x_1 => f x_1 = x) s = {y} ↔ x = f y
Tactic:
rcases hx with ⟨y',h1,rfl⟩
State after:
case mk.intro.intro
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y y' : α
h1 : y' ∈ s
⊢ filter (fun x => f x = f y') s = {y} ↔ f y' = f y

State before:
case mk.intro.intro
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y y' : α
h1 : y' ∈ s
⊢ filter (fun x => f x = f y') s = {y} ↔ f y' = f y
Tactic:
simp [eq_singleton_iff_unique_mem]
State after:
case mk.intro.intro
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y y' : α
h1 : y' ∈ s
⊢ ((y ∈ s ∧ y = y') ∧ ∀ x ∈ s, x = y' → x = y) ↔ y' = y

State before:
case mk.intro.intro
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y y' : α
h1 : y' ∈ s
⊢ ((y ∈ s ∧ y = y') ∧ ∀ x ∈ s, x = y' → x = y) ↔ y' = y
Tactic:
aesop
State after:
no goals