α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
h : 0 < multiplicativeEnergy s t
H : s = ∅ ∨ t = ∅
⊢ False
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
h : 0 < multiplicativeEnergy s t
H : ¬(Finset.Nonempty s ∧ Finset.Nonempty t)
⊢ False
simp_rw [not_and_or, not_nonempty_iff_eq_empty] at H
no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
h : 0 < multiplicativeEnergy s t
H : s = ∅ ∨ t = ∅
⊢ False
obtain rfl | rfl := H <;> simp [Nat.not_lt_zero] at h