α : Type u_1
β : Type u_2
γ : Type ?u.82868
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t✝ : Finset β
a : α
b c : β
t : Finset α
hf : Injective f
⊢ ↑(image f s) ⊆ ↑(image f t) ↔ ↑s ⊆ ↑t
α : Type u_1
β : Type u_2
γ : Type ?u.82868
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t✝ : Finset β
a : α
b c : β
t : Finset α
hf : Injective f
⊢ image f s ⊆ image f t ↔ s ⊆ t
simp_rw [← coe_subset]
α : Type u_1
β : Type u_2
γ : Type ?u.82868
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t✝ : Finset β
a : α
b c : β
t : Finset α
hf : Injective f
⊢ f '' ↑s ⊆ f '' ↑t ↔ ↑s ⊆ ↑t
α : Type u_1
β : Type u_2
γ : Type ?u.82868
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t✝ : Finset β
a : α
b c : β
t : Finset α
hf : Injective f
⊢ ↑(image f s) ⊆ ↑(image f t) ↔ ↑s ⊆ ↑t
push_cast
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.82868
inst✝ : DecidableEq β
f g : α → β
s : Finset α
t✝ : Finset β
a : α
b c : β
t : Finset α
hf : Injective f
⊢ f '' ↑s ⊆ f '' ↑t ↔ ↑s ⊆ ↑t
exact Set.image_subset_image_iff hf