simp_all
case h
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₂ : α
h₂ : a₂ ∈ s₂ ∧ f a₂
⊢ (a₂ ∈ s₁ ∨ a₂ ∈ s₂) ∧ f a₂
no goals