Theorem: SimpleGraph.edgeFinset_nonempty (LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Finite.lean)

State before:
α : Type u_1
G H : SimpleGraph α
inst✝ : Fintype ↑G.edgeSet
⊢ G.edgeFinset.Nonempty ↔ G ≠ ⊥
Tactic:
rw [Finset.nonempty_iff_ne_empty, edgeFinset_eq_empty.ne]
State after:
no goals