no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
⊢ multiplicativeEnergy s t = 0 ↔ s = ∅ ∨ t = ∅
simp [← (Nat.zero_le _).not_gt_iff_eq, not_and_or, imp_iff_or_not, or_comm]