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

State before:
α : Type u_1
G H : SimpleGraph α
inst✝ : Fintype ↑G.edgeSet
⊢ G.edgeFinset = ∅ ↔ G = ⊥
Tactic:
rw [← edgeFinset_bot, edgeFinset_inj]
State after:
no goals