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

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w v' w' : V
e : EdgeBetween G u v
p : EdgePath G v w
ph : EdgeBetween G u v'
pt : EdgePath G v' w'
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
hyp : cons e p = cons ph pt ++ cons e' (cons (EdgeBetween.bar e') p₂)
⊢ ¬reduced p
Tactic:
rw [cons_append] at hyp
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w v' w' : V
e : EdgeBetween G u v
p : EdgePath G v w
ph : EdgeBetween G u v'
pt : EdgePath G v' w'
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
⊢ ¬reduced p

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w v' w' : V
e : EdgeBetween G u v
p : EdgePath G v w
ph : EdgeBetween G u v'
pt : EdgePath G v' w'
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
⊢ ¬reduced p
Tactic:
let lhyp := congrArg EdgePath.toList hyp
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w v' w' : V
e : EdgeBetween G u v
p : EdgePath G v w
ph : EdgeBetween G u v'
pt : EdgePath G v' w'
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : toList (cons e p) = toList (cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))) := congrArg toList hyp
⊢ ¬reduced p

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w v' w' : V
e : EdgeBetween G u v
p : EdgePath G v w
ph : EdgeBetween G u v'
pt : EdgePath G v' w'
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : toList (cons e p) = toList (cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))) := congrArg toList hyp
⊢ ¬reduced p
Tactic:
simp only [cons_toList, append_toList, EdgeBetween.bar_eq_bar, List.cons.injEq] at lhyp
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w v' w' : V
e : EdgeBetween G u v
p : EdgePath G v w
ph : EdgeBetween G u v'
pt : EdgePath G v' w'
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
⊢ ¬reduced p

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w v' w' : V
e : EdgeBetween G u v
p : EdgePath G v w
ph : EdgeBetween G u v'
pt : EdgePath G v' w'
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
⊢ ¬reduced p
Tactic:
have : v' = v := by
  rw [← e.term_eq, ←ph.term_eq]
  symm
  apply congrArg G.τ lhyp.left
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w v' w' : V
e : EdgeBetween G u v
p : EdgePath G v w
ph : EdgeBetween G u v'
pt : EdgePath G v' w'
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
this : v' = v
⊢ ¬reduced p

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w v' w' : V
e : EdgeBetween G u v
p : EdgePath G v w
ph : EdgeBetween G u v'
pt : EdgePath G v' w'
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
this : v' = v
⊢ ¬reduced p
Tactic:
cases this
State after:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w w' : V
e : EdgeBetween G u v
p : EdgePath G v w
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
ph : EdgeBetween G u v
pt : EdgePath G v w'
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
⊢ ¬reduced p

State before:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w w' : V
e : EdgeBetween G u v
p : EdgePath G v w
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
ph : EdgeBetween G u v
pt : EdgePath G v w'
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
⊢ ¬reduced p
Tactic:
have : p = pt ++ (cons e' (cons  e'.bar  p₂)) := by
  apply eq_of_toList_eq
  simp [cons_toList, append_toList]
  exact lhyp.2
State after:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w w' : V
e : EdgeBetween G u v
p : EdgePath G v w
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
ph : EdgeBetween G u v
pt : EdgePath G v w'
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
this : p = pt ++ cons e' (cons (EdgeBetween.bar e') p₂)
⊢ ¬reduced p

State before:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w w' : V
e : EdgeBetween G u v
p : EdgePath G v w
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
ph : EdgeBetween G u v
pt : EdgePath G v w'
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
this : p = pt ++ cons e' (cons (EdgeBetween.bar e') p₂)
⊢ ¬reduced p
Tactic:
exact not_reduced_of_split this
State after:
no goals

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w v' w' : V
e : EdgeBetween G u v
p : EdgePath G v w
ph : EdgeBetween G u v'
pt : EdgePath G v' w'
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
⊢ v' = v
Tactic:
rw [← e.term_eq, ←ph.term_eq]
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w v' w' : V
e : EdgeBetween G u v
p : EdgePath G v w
ph : EdgeBetween G u v'
pt : EdgePath G v' w'
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
⊢ τ G ph.edge = τ G e.edge

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w v' w' : V
e : EdgeBetween G u v
p : EdgePath G v w
ph : EdgeBetween G u v'
pt : EdgePath G v' w'
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
⊢ τ G ph.edge = τ G e.edge
Tactic:
symm
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w v' w' : V
e : EdgeBetween G u v
p : EdgePath G v w
ph : EdgeBetween G u v'
pt : EdgePath G v' w'
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
⊢ τ G e.edge = τ G ph.edge

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w v' w' : V
e : EdgeBetween G u v
p : EdgePath G v w
ph : EdgeBetween G u v'
pt : EdgePath G v' w'
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
⊢ τ G e.edge = τ G ph.edge
Tactic:
apply congrArg G.τ lhyp.left
State after:
no goals

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w w' : V
e : EdgeBetween G u v
p : EdgePath G v w
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
ph : EdgeBetween G u v
pt : EdgePath G v w'
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
⊢ p = pt ++ cons e' (cons (EdgeBetween.bar e') p₂)
Tactic:
apply eq_of_toList_eq
State after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w w' : V
e : EdgeBetween G u v
p : EdgePath G v w
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
ph : EdgeBetween G u v
pt : EdgePath G v w'
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
⊢ toList p = toList (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))

State before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w w' : V
e : EdgeBetween G u v
p : EdgePath G v w
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
ph : EdgeBetween G u v
pt : EdgePath G v w'
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
⊢ toList p = toList (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
Tactic:
simp [cons_toList, append_toList]
State after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w w' : V
e : EdgeBetween G u v
p : EdgePath G v w
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
ph : EdgeBetween G u v
pt : EdgePath G v w'
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
⊢ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂

State before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w w' : V
e : EdgeBetween G u v
p : EdgePath G v w
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
ph : EdgeBetween G u v
pt : EdgePath G v w'
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
⊢ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
Tactic:
exact lhyp.2
State after:
no goals