α : Type u_1
β : Type u_2
γ : Type ?u.93853
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
hf : Injective f
⊢ f '' (↑s \ ↑t) = f '' ↑s \ f '' ↑t
α : Type u_1
β : Type u_2
γ : Type ?u.93853
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
hf : Injective f
⊢ ↑(image f (s \ t)) = ↑(image f s \ image f t)
push_cast
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.93853
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
hf : Injective f
⊢ f '' (↑s \ ↑t) = f '' ↑s \ f '' ↑t
exact Set.image_diff hf _ _