Theorem: Graph.SubgroupCover.Quot.edge_to (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.τ₀ →
    e.τ₁ = τ₁ → ∃ nxt p', ∃ (red : reduced p'), e = { τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }
Tactic:
intro h₁ 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.τ₀
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.τ₀
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₀
τ₁ : V
h₂ : e.τ₁ = τ₁
⊢ ∃ 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₀
τ₁ : V
h₂ : e.τ₁ = τ₁
⊢ ∃ nxt p', ∃ (red : reduced p'), e = { τ₀ := e.τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }
Tactic:
cases h₂
State after:
case refl.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.τ₀, τ₁ := e.τ₁, nxt := nxt, p := p', is_reduced := red }

State before:
case refl.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.τ₀, τ₁ := e.τ₁, nxt := nxt, p := p', is_reduced := red }
Tactic:
use e.nxt, e.p, e.is_reduced
State after:
no goals