Theorem: Graph.Subgraph.contains_head (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 → u ∈ H.verts
Tactic:
induction p with
| nil => simp
| cons e _ _ =>
  simp_rw [← e.init_eq]
  aesop
State after:
no goals

State before:
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ : V
⊢ contains H (EdgePath.nil v✝) → v✝ ∈ H.verts
Tactic:
simp
State after:
no goals

State before:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
a✝ : EdgePath G w✝ u✝
a_ih✝ : contains H a✝ → w✝ ∈ H.verts
⊢ contains H (EdgePath.cons e a✝) → v✝ ∈ H.verts
Tactic:
simp_rw [← e.init_eq]
State after:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
a✝ : EdgePath G w✝ u✝
a_ih✝ : contains H a✝ → w✝ ∈ H.verts
⊢ contains H (EdgePath.cons e a✝) → G.ι e.edge ∈ H.verts

State before:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
a✝ : EdgePath G w✝ u✝
a_ih✝ : contains H a✝ → w✝ ∈ H.verts
⊢ contains H (EdgePath.cons e a✝) → G.ι e.edge ∈ H.verts
Tactic:
aesop
State after:
no goals