Theorem: Graph.SpanningSubtree.path_class_of_contains_path (GroupComp/Subgraph.lean)

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
p : EdgePath G u v
hpΓ : Subgraph.contains Γ.toSubgraph p
⊢ [[p]] = u ⤳[Γ] v
Tactic:
apply Γ.path_unique (Γ.vertex_coe u) (Γ.vertex_coe v)
State after:
case a
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
p : EdgePath G u v
hpΓ : Subgraph.contains Γ.toSubgraph p
⊢ Subgraph.contains Γ.toSubgraph p

State before:
case a
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
p : EdgePath G u v
hpΓ : Subgraph.contains Γ.toSubgraph p
⊢ Subgraph.contains Γ.toSubgraph p
Tactic:
assumption
State after:
no goals