Theorem: Graph.prepend_cases (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
⊢ redCons e p = cons e p ∨ ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
Tactic:
match p with
| nil _ =>
  simp only [redCons_nil, false_and, exists_false, or_false]
| cons e' p' =>
  rename_i w' w''
  if c:w'' = u then
    cases c
    if c':e' = e.bar
      then
        simp [redCons_cons_edge_eq p' c']
        simp only [c', or_true]
      else
        simp [redCons_cons_edge_neq p' c']
  else
    simp only [redCons_cons_vertex_neq e e' p' c, cons.injEq, exists_eq_right', true_or]
State after:
no goals

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
⊢ redCons e (nil v) = cons e (nil v) ∨ ∃ t, nil v = cons (EdgeBetween.bar e) t ∧ redCons e (nil v) = t
Tactic:
simp only [redCons_nil, false_and, exists_false, or_false]
State after:
no goals

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✝¹
w w✝ : V
e' : EdgeBetween G v w✝
p' : EdgePath G w✝ w
⊢ redCons e (cons e' p') = cons e (cons e' p') ∨
    ∃ t, cons e' p' = cons (EdgeBetween.bar e) t ∧ redCons e (cons e' p') = t
Tactic:
rename_i w' w''
State after:
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'
w w'' : V
e' : EdgeBetween G v w''
p' : EdgePath G w'' w
⊢ redCons e (cons e' p') = cons e (cons e' p') ∨
    ∃ t, cons e' p' = cons (EdgeBetween.bar e) t ∧ redCons e (cons e' p') = t

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'
w w'' : V
e' : EdgeBetween G v w''
p' : EdgePath G w'' w
⊢ redCons e (cons e' p') = cons e (cons e' p') ∨
    ∃ t, cons e' p' = cons (EdgeBetween.bar e) t ∧ redCons e (cons e' p') = t
Tactic:
if c:w'' = u then
  cases c
  if c':e' = e.bar
    then
      simp [redCons_cons_edge_eq p' c']
      simp only [c', or_true]
    else
      simp [redCons_cons_edge_neq p' c']
else
  simp only [redCons_cons_vertex_neq e e' p' c, cons.injEq, exists_eq_right', true_or]
State after:
no goals

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'
w w'' : V
e' : EdgeBetween G v w''
p' : EdgePath G w'' w
c : w'' = u
⊢ redCons e (cons e' p') = cons e (cons e' p') ∨
    ∃ t, cons e' p' = cons (EdgeBetween.bar e) t ∧ redCons e (cons e' p') = t
Tactic:
cases c
State after:
case refl
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'
w : V
e' : EdgeBetween G v u
p' : EdgePath G u w
⊢ redCons e (cons e' p') = cons e (cons e' p') ∨
    ∃ t, cons e' p' = cons (EdgeBetween.bar e) t ∧ redCons e (cons e' p') = t

State before:
case refl
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'
w : V
e' : EdgeBetween G v u
p' : EdgePath G u w
⊢ redCons e (cons e' p') = cons e (cons e' p') ∨
    ∃ t, cons e' p' = cons (EdgeBetween.bar e) t ∧ redCons e (cons e' p') = t
Tactic:
if c':e' = e.bar
  then
    simp [redCons_cons_edge_eq p' c']
    simp only [c', or_true]
  else
    simp [redCons_cons_edge_neq p' c']
State after:
no goals

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'
w : V
e' : EdgeBetween G v u
p' : EdgePath G u w
c' : e' = EdgeBetween.bar e
⊢ redCons e (cons e' p') = cons e (cons e' p') ∨
    ∃ t, cons e' p' = cons (EdgeBetween.bar e) t ∧ redCons e (cons e' p') = t
Tactic:
simp [redCons_cons_edge_eq p' c']
State after:
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'
w : V
e' : EdgeBetween G v u
p' : EdgePath G u w
c' : e' = EdgeBetween.bar e
⊢ p' = cons e (cons e' p') ∨ e' = EdgeBetween.bar e

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'
w : V
e' : EdgeBetween G v u
p' : EdgePath G u w
c' : e' = EdgeBetween.bar e
⊢ p' = cons e (cons e' p') ∨ e' = EdgeBetween.bar e
Tactic:
simp only [c', or_true]
State after:
no goals

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'
w : V
e' : EdgeBetween G v u
p' : EdgePath G u w
c' : ¬e' = EdgeBetween.bar e
⊢ redCons e (cons e' p') = cons e (cons e' p') ∨
    ∃ t, cons e' p' = cons (EdgeBetween.bar e) t ∧ redCons e (cons e' p') = t
Tactic:
simp [redCons_cons_edge_neq p' c']
State after:
no goals

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'
w w'' : V
e' : EdgeBetween G v w''
p' : EdgePath G w'' w
c : ¬w'' = u
⊢ redCons e (cons e' p') = cons e (cons e' p') ∨
    ∃ t, cons e' p' = cons (EdgeBetween.bar e) t ∧ redCons e (cons e' p') = t
Tactic:
simp only [redCons_cons_vertex_neq e e' p' c, cons.injEq, exists_eq_right', true_or]
State after:
no goals