. rintro ⟨a, h₁ | h₂, hb⟩;
  . left; use a;
  . right; use a;
case mp
α : 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, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a) → (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a

case mpr
α : 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 ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a) → ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a
case mpr
α : 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 ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a) → ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a