α : Type u_1
β : Type u_2
γ : Type ?u.94769
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.94769
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.94769
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_symm_diff hf _ _