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

State before:
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e : EdgeBetween G u v
heΓ : e.edge ∈ Γ.edges
⊢ [[singletonPath e]] = u ⤳[Γ] v
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 : V
e : EdgeBetween G u v
heΓ : e.edge ∈ Γ.edges
⊢ Subgraph.contains Γ.toSubgraph (singletonPath e)

State before:
case hpΓ
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e : EdgeBetween G u v
heΓ : e.edge ∈ Γ.edges
⊢ Subgraph.contains Γ.toSubgraph (singletonPath e)
Tactic:
simp
State after:
case hpΓ
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e : EdgeBetween G u v
heΓ : e.edge ∈ Γ.edges
⊢ e.edge ∈ Γ.edges

State before:
case hpΓ
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e : EdgeBetween G u v
heΓ : e.edge ∈ Γ.edges
⊢ e.edge ∈ Γ.edges
Tactic:
assumption
State after:
no goals