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

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