Theorem: Graph.Subgraph.contains_tail (GroupComp/Subgraph.lean)

State before:
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v : V
p : EdgePath G u v
⊢ contains H p → v ∈ H.verts
Tactic:
induction p <;> aesop
State after:
no goals