Theorem: Graph.PathClass.inv_mul' (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
u v : V
⊢ ∀ (p : u ⟶ v), PathClass.inv p ≫ p = 𝟙 v
Tactic:
apply Quot.ind
State after:
case mk
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
u v : V
⊢ ∀ (a : EdgePath G u v), PathClass.inv (Quot.mk Reduction a) ≫ Quot.mk Reduction a = 𝟙 v

State before:
case mk
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
u v : V
⊢ ∀ (a : EdgePath G u v), PathClass.inv (Quot.mk Reduction a) ≫ Quot.mk Reduction a = 𝟙 v
Tactic:
aesop
State after:
no goals