α : Type u_1
β : Type u_2
γ : Type ?u.87546
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
hf : Set.InjOn f (↑s ∪ ↑t)
⊢ f '' (↑s ∩ ↑t) = f '' ↑s ∩ f '' ↑t
α : Type u_1
β : Type u_2
γ : Type ?u.87546
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
hf : Set.InjOn f (↑s ∪ ↑t)
⊢ ↑(image f (s ∩ t)) = ↑(image f s ∩ image f t)
push_cast
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.87546
inst✝¹ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
hf : Set.InjOn f (↑s ∪ ↑t)
⊢ f '' (↑s ∩ ↑t) = f '' ↑s ∩ f '' ↑t
exact Set.image_inter_on fun a ha b hb => hf (Or.inr ha) <| Or.inl hb