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

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u : V
⊢ (u ⤳[Γ] u) = 𝟙 u
Tactic:
symm
State after:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u : V
⊢ 𝟙 u = u ⤳[Γ] u

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u : V
⊢ 𝟙 u = u ⤳[Γ] u
Tactic:
apply path_class_of_contains_path
State after:
case hpΓ
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u : V
⊢ Subgraph.contains Γ.toSubgraph (EdgePath.nil u)

State before:
case hpΓ
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u : V
⊢ Subgraph.contains Γ.toSubgraph (EdgePath.nil u)
Tactic:
simp
State after:
no goals