rintro ⟨a,b|b⟩
case a.mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b : β
⊢ (∃ a, (a ∈ s1 ∨ a ∈ s2) ∧ b ∈ f a) → (∃ a ∈ s1, b ∈ f a) ∨ ∃ a ∈ s2, b ∈ f a
case a.mp.intro.intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
right✝ : b✝ ∈ f a
b : a ∈ s1
⊢ (∃ a ∈ s1, b✝ ∈ f a) ∨ ∃ a ∈ s2, b✝ ∈ f a

case a.mp.intro.intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
right✝ : b✝ ∈ f a
b : a ∈ s2
⊢ (∃ a ∈ s1, b✝ ∈ f a) ∨ ∃ a ∈ s2, b✝ ∈ f a