[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ _root_.Disjoint (map Embedding.inl s) (map Embedding.inr t)
[PROOFSTEP]
simp_rw [disjoint_left, mem_map]
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ ∀ ⦃a : α ⊕ β⦄, (∃ a_1, a_1 ∈ s ∧ ↑Embedding.inl a_1 = a) → ¬∃ a_2, a_2 ∈ t ∧ ↑Embedding.inr a_2 = a
[PROOFSTEP]
rintro x ⟨a, _, rfl⟩ ⟨b, _, ⟨⟩⟩
