no goals
α₁ : Type u_3
α₂ : Type u_4
β₁ : Type u_5
β₂ : Type u_6
γ₁ : Type u_1
γ₂ : Type u_2
f f₁ g₁ : α₁ → β₁ → Finset γ₁
g f₂ g₂ : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
⊢ Finset.Nonempty (sumLift₂ f g a b) ↔
    (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ Finset.Nonempty (f a₁ b₁)) ∨
      ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ Finset.Nonempty (g a₂ b₂)
simp only [nonempty_iff_ne_empty, Ne, sumLift₂_eq_empty, not_and_or, not_forall, not_imp]