rw [← transfer_eq_map_of_le, transfer_transfer, transfer_self]
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w : V
s : Set (V × V)
p : Walk G v w
hp : ∀ (e : V × V), e ∈ edges p → ¬e ∈ s
⊢ Walk.map (Hom.mapSpanningSubgraphs (_ : deleteEdges G s ≤ G)) (toDeleteEdges s p hp) = p
case hp'
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w : V
s : Set (V × V)
p : Walk G v w
hp : ∀ (e : V × V), e ∈ edges p → ¬e ∈ s
⊢ ∀ (e : V × V),
    e ∈ edges (Walk.transfer p (deleteEdges G s) (_ : ∀ (e : V × V), e ∈ edges p → e ∈ edgeSet (deleteEdges G s))) →
      e ∈ edgeSet G

case hp'
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
v w : V
s : Set (V × V)
p : Walk G v w
hp : ∀ (e : V × V), e ∈ edges p → ¬e ∈ s
⊢ ∀ (e : V × V),
    e ∈ edges (Walk.transfer p (deleteEdges G s) (_ : ∀ (e : V × V), e ∈ edges p → e ∈ edgeSet (deleteEdges G s))) →
      e ∈ edgeSet G