α : Type u_1
β : Type u_2
γ : Type ?u.69600
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
hf : Injective f
h : f a ∈ image f s
⊢ a ∈ s
α : Type u_1
β : Type u_2
γ : Type ?u.69600
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
hf : Injective f
⊢ f a ∈ image f s ↔ a ∈ s
refine' ⟨fun h => _, Finset.mem_image_of_mem f⟩
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.69600
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
hf : Injective f
h : f a ∈ image f s
y : α
hy : y ∈ s
heq : f y = f a
⊢ a ∈ s
α : Type u_1
β : Type u_2
γ : Type ?u.69600
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
hf : Injective f
h : f a ∈ image f s
⊢ a ∈ s
obtain ⟨y, hy, heq⟩ := mem_image.1 h
no goals
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.69600
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c : β
hf : Injective f
h : f a ∈ image f s
y : α
hy : y ∈ s
heq : f y = f a
⊢ a ∈ s
exact hf heq ▸ hy