Theorem: Graph.UniversalCover.shift_heq (GroupComp/Graph/UniversalCover.lean)

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ τ₀ τ₁ τ₂ : V
edge : E
init_eq : G.ι edge = τ₀
term_eq₁ : τ G edge = τ₁
term_eq₂ : τ G edge = τ₂
⊢ HEq { edge := edge, init_eq := init_eq, term_eq := term_eq₁ }
    { edge := edge, init_eq := init_eq, term_eq := term_eq₂ }
Tactic:
cases term_eq₁
State after:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ τ₀ τ₂ : V
edge : E
init_eq : G.ι edge = τ₀
term_eq₂ : τ G edge = τ₂
⊢ HEq { edge := edge, init_eq := init_eq, term_eq := (_ : τ G edge = τ G edge) }
    { edge := edge, init_eq := init_eq, term_eq := term_eq₂ }

State before:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ τ₀ τ₂ : V
edge : E
init_eq : G.ι edge = τ₀
term_eq₂ : τ G edge = τ₂
⊢ HEq { edge := edge, init_eq := init_eq, term_eq := (_ : τ G edge = τ G edge) }
    { edge := edge, init_eq := init_eq, term_eq := term_eq₂ }
Tactic:
cases term_eq₂
State after:
case refl.refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ τ₀ : V
edge : E
init_eq : G.ι edge = τ₀
⊢ HEq { edge := edge, init_eq := init_eq, term_eq := (_ : τ G edge = τ G edge) }
    { edge := edge, init_eq := init_eq, term_eq := (_ : τ G edge = τ G edge) }

State before:
case refl.refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ τ₀ : V
edge : E
init_eq : G.ι edge = τ₀
⊢ HEq { edge := edge, init_eq := init_eq, term_eq := (_ : τ G edge = τ G edge) }
    { edge := edge, init_eq := init_eq, term_eq := (_ : τ G edge = τ G edge) }
Tactic:
rfl
State after:
no goals