Theorem: Graph.concat_parity (GroupComp/Graph/ReducedPaths.lean)

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
⊢ Even (List.length (toList (p:+e))) ↔ ¬Even (List.length (toList p))
Tactic:
simp  [reducedConcat, reverse_toList]
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
⊢ Even (List.length (toList (redCons (EdgeBetween.bar e) (reverse p)))) ↔ ¬Even (List.length (toList p))

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
⊢ Even (List.length (toList (redCons (EdgeBetween.bar e) (reverse p)))) ↔ ¬Even (List.length (toList p))
Tactic:
rw [redCons_parity_neq e.bar (reverse p)]
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
⊢ ¬Even (List.length (toList (reverse p))) ↔ ¬Even (List.length (toList p))

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
⊢ ¬Even (List.length (toList (reverse p))) ↔ ¬Even (List.length (toList p))
Tactic:
simp [reverse_toList]
State after:
no goals