no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s t : Finset β
hs : InjOn f (f ⁻¹' ↑s)
ht : InjOn f (f ⁻¹' ↑t)
⊢ ↑(preimage (s ∩ t) f
        (_ : ∀ (x₁ : α), x₁ ∈ f ⁻¹' ↑(s ∩ t) → ∀ (x₂ : α), x₂ ∈ f ⁻¹' ↑(s ∩ t) → f x₁ = f x₂ → x₁ = x₂)) =
    ↑(preimage s f hs ∩ preimage t f ht)
simp