internlm/Lean-Github huggingface dataset:
Theorem: Graph.prepend_cases
Proof 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''
Proof 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
Theorem: Graph.prepend_cases
Proof 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]
Proof state after:
no goals
Theorem: Graph.prepend_cases
Proof 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
Proof 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
Theorem: Graph.prepend_cases
Proof 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']
Proof state after:
no goals
Theorem: Graph.prepend_cases
Proof 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']
Proof 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
Theorem: Graph.prepend_cases
Proof 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]
Proof state after:
no goals
Theorem: Graph.prepend_cases
Proof 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']
Proof state after:
no goals
Theorem: Graph.prepend_cases
Proof 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]
Proof state after:
no goals
Theorem: Graph.tail_reducible_of_split
Proof 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
Proof 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
Theorem: Graph.tail_reducible_of_split
Proof 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
Proof 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
Theorem: Graph.tail_reducible_of_split
Proof 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
Proof 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
Theorem: Graph.tail_reducible_of_split
Proof 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
Proof 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
Theorem: Graph.tail_reducible_of_split
Proof 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
Proof 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
Theorem: Graph.tail_reducible_of_split
Proof 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
Proof 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
Theorem: Graph.tail_reducible_of_split
Proof 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
Proof state after:
no goals
Theorem: Graph.tail_reducible_of_split
Proof 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]
Proof 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
Theorem: Graph.tail_reducible_of_split
Proof 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
Proof 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
Theorem: Graph.tail_reducible_of_split
Proof 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
Proof state after:
no goals
Theorem: Graph.tail_reducible_of_split
Proof 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
Proof 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₂))
Theorem: Graph.tail_reducible_of_split
Proof 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]
Proof 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₂
Theorem: Graph.tail_reducible_of_split
Proof 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
Proof state after:
no goals
Theorem: Graph.reduced_singleton
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v : V
e : EdgeBetween G u v
⊢ reduced (cons e (nil v))
Tactic:
intro p' red'
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v : V
e : EdgeBetween G u v
p' : EdgePath G u v
red' : Reduction (cons e (nil v)) p'
⊢ False
Theorem: Graph.reduced_singleton
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v : V
e : EdgeBetween G u v
p' : EdgePath G u v
red' : Reduction (cons e (nil v)) p'
⊢ False
Tactic:
let ⟨u, u', e, p₁, p₂, eqn⟩   := red'.property
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v : V
e✝ : EdgeBetween G u✝ v
p' : EdgePath G u✝ v
red' : Reduction (cons e✝ (nil v)) p'
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G u✝ u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (nil v)
⊢ False
Theorem: Graph.reduced_singleton
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v : V
e✝ : EdgeBetween G u✝ v
p' : EdgePath G u✝ v
red' : Reduction (cons e✝ (nil v)) p'
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G u✝ u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (nil v)
⊢ False
Tactic:
cases p₁ with
| nil _ =>
  rw [nil_append] at eqn
  let leqn := congrArg EdgePath.toList eqn
  simp [cons_toList, nil_toList] at leqn
| cons h t =>
  rw [cons_append] at eqn
  let leqn := congrArg EdgePath.toList eqn
  simp [cons_toList, nil_toList, append_toList] at leqn
Proof state after:
no goals
Theorem: Graph.reduced_singleton
Proof state before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v : V
e✝ : EdgeBetween G u v
p' : EdgePath G u v
red' : Reduction (cons e✝ (nil v)) p'
u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
eqn : nil u ++ cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (nil v)
⊢ False
Tactic:
rw [nil_append] at eqn
Proof state after:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v : V
e✝ : EdgeBetween G u v
p' : EdgePath G u v
red' : Reduction (cons e✝ (nil v)) p'
u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (nil v)
⊢ False
Theorem: Graph.reduced_singleton
Proof state before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v : V
e✝ : EdgeBetween G u v
p' : EdgePath G u v
red' : Reduction (cons e✝ (nil v)) p'
u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (nil v)
⊢ False
Tactic:
let leqn := congrArg EdgePath.toList eqn
Proof state after:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v : V
e✝ : EdgeBetween G u v
p' : EdgePath G u v
red' : Reduction (cons e✝ (nil v)) p'
u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (nil v)
leqn : toList (cons e (cons (EdgeBetween.bar e) p₂)) = toList (cons e✝ (nil v)) := congrArg toList eqn
⊢ False
Theorem: Graph.reduced_singleton
Proof state before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v : V
e✝ : EdgeBetween G u v
p' : EdgePath G u v
red' : Reduction (cons e✝ (nil v)) p'
u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (nil v)
leqn : toList (cons e (cons (EdgeBetween.bar e) p₂)) = toList (cons e✝ (nil v)) := congrArg toList eqn
⊢ False
Tactic:
simp [cons_toList, nil_toList] at leqn
Proof state after:
no goals
Theorem: Graph.reduced_singleton
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v : V
e✝ : EdgeBetween G u✝ v
p' : EdgePath G u✝ v
red' : Reduction (cons e✝ (nil v)) p'
u u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
w✝ : V
h : EdgeBetween G u✝ w✝
t : EdgePath G w✝ u
eqn : cons h t ++ cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (nil v)
⊢ False
Tactic:
rw [cons_append] at eqn
Proof state after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v : V
e✝ : EdgeBetween G u✝ v
p' : EdgePath G u✝ v
red' : Reduction (cons e✝ (nil v)) p'
u u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
w✝ : V
h : EdgeBetween G u✝ w✝
t : EdgePath G w✝ u
eqn : cons h (t ++ cons e (cons (EdgeBetween.bar e) p₂)) = cons e✝ (nil v)
⊢ False
Theorem: Graph.reduced_singleton
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v : V
e✝ : EdgeBetween G u✝ v
p' : EdgePath G u✝ v
red' : Reduction (cons e✝ (nil v)) p'
u u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
w✝ : V
h : EdgeBetween G u✝ w✝
t : EdgePath G w✝ u
eqn : cons h (t ++ cons e (cons (EdgeBetween.bar e) p₂)) = cons e✝ (nil v)
⊢ False
Tactic:
let leqn := congrArg EdgePath.toList eqn
Proof state after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v : V
e✝ : EdgeBetween G u✝ v
p' : EdgePath G u✝ v
red' : Reduction (cons e✝ (nil v)) p'
u u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
w✝ : V
h : EdgeBetween G u✝ w✝
t : EdgePath G w✝ u
eqn : cons h (t ++ cons e (cons (EdgeBetween.bar e) p₂)) = cons e✝ (nil v)
leqn : toList (cons h (t ++ cons e (cons (EdgeBetween.bar e) p₂))) = toList (cons e✝ (nil v)) := congrArg toList eqn
⊢ False
Theorem: Graph.reduced_singleton
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v : V
e✝ : EdgeBetween G u✝ v
p' : EdgePath G u✝ v
red' : Reduction (cons e✝ (nil v)) p'
u u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
w✝ : V
h : EdgeBetween G u✝ w✝
t : EdgePath G w✝ u
eqn : cons h (t ++ cons e (cons (EdgeBetween.bar e) p₂)) = cons e✝ (nil v)
leqn : toList (cons h (t ++ cons e (cons (EdgeBetween.bar e) p₂))) = toList (cons e✝ (nil v)) := congrArg toList eqn
⊢ False
Tactic:
simp [cons_toList, nil_toList, append_toList] at leqn
Proof state after:
no goals
Theorem: Graph.reduced_nil
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
⊢ reduced (nil v)
Tactic:
intro p' red'
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
⊢ False
Theorem: Graph.reduced_nil
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
⊢ False
Tactic:
let ⟨u, u', e, p₁, p₂, eqn⟩   := red'.property
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = nil v
⊢ False
Theorem: Graph.reduced_nil
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = nil v
⊢ False
Tactic:
cases p₁ with
| nil _ =>
  rw [nil_append] at eqn
  let leqn := congrArg EdgePath.toList eqn
  simp [cons_toList, nil_toList] at leqn
| cons h t =>
  rw [cons_append] at eqn
  let leqn := congrArg EdgePath.toList eqn
  simp [cons_toList, nil_toList, append_toList] at leqn
Proof state after:
no goals
Theorem: Graph.reduced_nil
Proof state before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u' : V
e : EdgeBetween G v u'
p₂ : EdgePath G v v
eqn : nil v ++ cons e (cons (EdgeBetween.bar e) p₂) = nil v
⊢ False
Tactic:
rw [nil_append] at eqn
Proof state after:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u' : V
e : EdgeBetween G v u'
p₂ : EdgePath G v v
eqn : cons e (cons (EdgeBetween.bar e) p₂) = nil v
⊢ False