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

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

State before:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : { x // x ∈ map f s }
⊢ f.toFun ↑((mapEquiv s f).symm x) = ↑x
Tactic:
rcases x with ⟨x,hx⟩
State after:
case mk
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α'
hx : x ∈ map f s
⊢ f.toFun ↑((mapEquiv s f).symm { val := x, property := hx }) = ↑{ val := x, property := hx }

State before:
case mk
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α'
hx : x ∈ map f s
⊢ f.toFun ↑((mapEquiv s f).symm { val := x, property := hx }) = ↑{ val := x, property := hx }
Tactic:
simp at hx
State after:
case mk
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α'
hx✝ : x ∈ map f s
hx : ∃ a ∈ s, f a = x
⊢ f.toFun ↑((mapEquiv s f).symm { val := x, property := hx✝ }) = ↑{ val := x, property := hx✝ }

State before:
case mk
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α'
hx✝ : x ∈ map f s
hx : ∃ a ∈ s, f a = x
⊢ f.toFun ↑((mapEquiv s f).symm { val := x, property := hx✝ }) = ↑{ val := x, property := hx✝ }
Tactic:
rcases hx with ⟨y,_,rfl⟩
State after:
case mk.intro.intro
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y : α
left✝ : y ∈ s
hx : f y ∈ map f s
⊢ f.toFun ↑((mapEquiv s f).symm { val := f y, property := hx }) = ↑{ val := f y, property := hx }

State before:
case mk.intro.intro
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y : α
left✝ : y ∈ s
hx : f y ∈ map f s
⊢ f.toFun ↑((mapEquiv s f).symm { val := f y, property := hx }) = ↑{ val := f y, property := hx }
Tactic:
simp
State after:
no goals