Theorem: Graph.SubgroupCover.Quot.edge_from (GroupComp/Graph/SubgroupCover.lean)

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
e : Edge G x₀
τ₀ : V
⊢ τ₀ = e.τ₀ → ∃ τ₁ nxt p', ∃ (red : reduced p'), e = { τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }
Tactic:
intro h
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
e : Edge G x₀
τ₀ : V
h : τ₀ = e.τ₀
⊢ ∃ τ₁ nxt p', ∃ (red : reduced p'), e = { τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
e : Edge G x₀
τ₀ : V
h : τ₀ = e.τ₀
⊢ ∃ τ₁ nxt p', ∃ (red : reduced p'), e = { τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }
Tactic:
cases h
State after:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
e : Edge G x₀
⊢ ∃ τ₁ nxt p', ∃ (red : reduced p'), e = { τ₀ := e.τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }

State before:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
e : Edge G x₀
⊢ ∃ τ₁ nxt p', ∃ (red : reduced p'), e = { τ₀ := e.τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }
Tactic:
use e.τ₁, e.nxt, e.p, e.is_reduced
State after:
no goals