rintro ⟨s, ⟨⟨v, w⟩, h⟩, hs, rfl⟩
case mpr
V : Type u_1
G G' : Digraph V
⊢ (∃ s, Set.Nonempty s ∧ s ⊆ edgeSet G' ∧ G = deleteEdges G' s) → G < G'
case mpr.intro.intro.intro.mk.intro
V : Type u_1
G' : Digraph V
s : Set (V × V)
v w : V
h : (v, w) ∈ s
hs : s ⊆ edgeSet G'
⊢ deleteEdges G' s < G'