Theorem: Graph.PathClass.inv_eq (GroupComp/Graph.lean)

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G v w
⊢ ∀ {p : PathClass G u v} {q : PathClass G v u}, PathClass.inv p = q → p = PathClass.inv q
Tactic:
apply PathClass.ind
State after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G v w
⊢ ∀ (p : EdgePath G u v) {q : PathClass G v u}, PathClass.inv [[p]] = q → [[p]] = PathClass.inv q

State before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G v w
⊢ ∀ (p : EdgePath G u v) {q : PathClass G v u}, PathClass.inv [[p]] = q → [[p]] = PathClass.inv q
Tactic:
aesop
State after:
no goals