simp only [and_self, or_true, *]
case a.mpr.inr.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
b : a ∈ s2
c : b✝ ∈ f a
⊢ (a ∈ s1 ∨ a ∈ s2) ∧ b✝ ∈ f a
no goals