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

State before:
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
⊢ ∀ e ∈ H.edges, τ G e ∈ H.verts
Tactic:
intro e he
State after:
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ τ G e ∈ H.verts

State before:
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ τ G e ∈ H.verts
Tactic:
rw [← G.ι_bar e]
State after:
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ G.ι (G.bar e) ∈ H.verts

State before:
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ G.ι (G.bar e) ∈ H.verts
Tactic:
apply H.edges_init
State after:
case a
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ G.bar e ∈ H.edges

State before:
case a
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ G.bar e ∈ H.edges
Tactic:
apply H.edges_bar
State after:
case a.a
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ e ∈ H.edges

State before:
case a.a
V : Type u_2
E : Type u_1
G : Graph V E
H : Subgraph G
e : E
he : e ∈ H.edges
⊢ e ∈ H.edges
Tactic:
exact he
State after:
no goals