Theorem: Graph.redCons_parity_neq (GroupComp/Graph/ReducedPaths.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 u v
p : EdgePath G v w
⊢ Even (List.length (toList (redCons e p))) ↔ ¬Even (List.length (toList p))
Tactic:
cases prepend_cases e p with
| inl h =>
  rw [h]
  simp only [cons_toList, List.length_cons]
  apply Nat.even_add_one
| inr h =>
  let ⟨t, h₁, h₂⟩ := h
  rw [h₂, h₁]
  simp  [cons_toList, List.length_cons, Nat.even_add_one]
State after:
no goals

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

State before:
case inl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : redCons e p = cons e p
⊢ Even (List.length (toList (cons e p))) ↔ ¬Even (List.length (toList p))
Tactic:
simp only [cons_toList, List.length_cons]
State after:
case inl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : redCons e p = cons e p
⊢ Even (Nat.succ (List.length (toList p))) ↔ ¬Even (List.length (toList p))

State before:
case inl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : redCons e p = cons e p
⊢ Even (Nat.succ (List.length (toList p))) ↔ ¬Even (List.length (toList p))
Tactic:
apply Nat.even_add_one
State after:
no goals

State before:
case inr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
⊢ Even (List.length (toList (redCons e p))) ↔ ¬Even (List.length (toList p))
Tactic:
let ⟨t, h₁, h₂⟩ := h
State after:
case inr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
⊢ Even (List.length (toList (redCons e p))) ↔ ¬Even (List.length (toList p))

State before:
case inr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
⊢ Even (List.length (toList (redCons e p))) ↔ ¬Even (List.length (toList p))
Tactic:
rw [h₂, h₁]
State after:
case inr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
⊢ Even (List.length (toList t)) ↔ ¬Even (List.length (toList (cons (EdgeBetween.bar e) t)))

State before:
case inr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
h : ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
⊢ Even (List.length (toList t)) ↔ ¬Even (List.length (toList (cons (EdgeBetween.bar e) t)))
Tactic:
simp  [cons_toList, List.length_cons, Nat.even_add_one]
State after:
no goals