Theorem: Digraph.Walk.map_toDeleteEdges_eq (GraphProjects/DigraphConnectivity.lean)

State before:
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
Tactic:
rw [← transfer_eq_map_of_le, transfer_transfer, transfer_self]
State after:
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

State before:
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
Tactic:
intros e
State after:
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

State before:
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
Tactic:
rw [edges_transfer]
State after:
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 p → e ∈ edgeSet G

State before:
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 p → e ∈ edgeSet G
Tactic:
apply edges_subset_edgeSet p
State after:
no goals