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

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v w : V
⊢ ((u ⤳[Γ] v) ≫ v ⤳[Γ] w) = u ⤳[Γ] w
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 w : V
⊢ Subgraph.contains Γ.toSubgraph
    (↑((toSubtree Γ).toPreconnectedSubgraph.path (vertex_coe Γ u) (vertex_coe Γ v)) ++
      ↑((toSubtree Γ).toPreconnectedSubgraph.path (vertex_coe Γ v) (vertex_coe Γ w)))

State before:
case hpΓ
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v w : V
⊢ Subgraph.contains Γ.toSubgraph
    (↑((toSubtree Γ).toPreconnectedSubgraph.path (vertex_coe Γ u) (vertex_coe Γ v)) ++
      ↑((toSubtree Γ).toPreconnectedSubgraph.path (vertex_coe Γ v) (vertex_coe Γ w)))
Tactic:
simp
State after:
no goals