intro ⟨h₁, h₂⟩ a ha
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 α
h₁ : ∀ a ∈ s₁, f a
h₂ : ∀ a ∈ s₂, f a
a : α
ha : a ∈ s₁ ∨ a ∈ s₂
⊢ f a