rw [Set.not_nonempty_iff_eq_empty, Set.diff_eq_empty, edgeSet_subset_edgeSet] at hn
case mp.left
V : Type u_1
G G' : Digraph V
h : G < G'
hn : ¬Set.Nonempty (edgeSet G' \ edgeSet G)
⊢ False
case mp.left
V : Type u_1
G G' : Digraph V
h : G < G'
hn : G' ≤ G
⊢ False