Theorem: Graph.PathClass.mul_id (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 : PathClass G u v), p * PathClass.id' G v = p
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
u v : V
⊢ ∀ (p : EdgePath G u v), [[p]] * PathClass.id' G v = [[p]]

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
u v : V
⊢ ∀ (p : EdgePath G u v), [[p]] * PathClass.id' G v = [[p]]
Tactic:
aesop
State after:
no goals