internlm/Lean-Github huggingface dataset:
Theorem: Graph.EdgePath.reverse_concat
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 v✝ w✝
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
⊢ reverse (concat p e) = cons (EdgeBetween.bar e) (reverse p)
Tactic:
induction p <;> aesop (add norm simp [concat_cons, reverse_cons])
Proof state after:
no goals
Theorem: Graph.EdgePath.append_nil
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 v✝ w
u v : V
p : EdgePath G u v
⊢ p ++ nil v = p
Tactic:
show append _ _ = _
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 v✝ w
u v : V
p : EdgePath G u v
⊢ append p (nil v) = p
Theorem: Graph.EdgePath.append_nil
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 v✝ w
u v : V
p : EdgePath G u v
⊢ append p (nil v) = p
Tactic:
induction p <;> aesop (add norm simp [append])
Proof state after:
no goals
Theorem: Graph.EdgePath.cons_append
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 v✝ w✝
v' v w u : V
e : EdgeBetween G v' v
p : EdgePath G v w
q : EdgePath G w u
⊢ cons e p ++ q = cons e (p ++ q)
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.EdgePath.concat_append
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 v✝ w✝
v w w' u : V
e : EdgeBetween G w w'
p : EdgePath G v w
q : EdgePath G w' u
⊢ concat p e ++ q = p ++ cons e q
Tactic:
induction p <;> aesop
Proof state after:
no goals
Theorem: Graph.EdgePath.append_concat
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 v✝ w✝
v w w' u : V
e : EdgeBetween G w' u
p : EdgePath G v w
q : EdgePath G w w'
⊢ p ++ concat q e = concat (p ++ q) e
Tactic:
induction p <;> aesop
Proof state after:
no goals
Theorem: Graph.EdgePath.concat_eq_append_edge
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 v✝ w✝
v w u : V
e : EdgeBetween G w u
p : EdgePath G v w
⊢ concat p e = p ++ cons e (nil u)
Tactic:
have := concat_append e p (.nil _)
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 v✝ w✝
v w u : V
e : EdgeBetween G w u
p : EdgePath G v w
this : concat p e ++ nil u = p ++ cons e (nil u)
⊢ concat p e = p ++ cons e (nil u)
Theorem: Graph.EdgePath.concat_eq_append_edge
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 v✝ w✝
v w u : V
e : EdgeBetween G w u
p : EdgePath G v w
this : concat p e ++ nil u = p ++ cons e (nil u)
⊢ concat p e = p ++ cons e (nil u)
Tactic:
aesop
Proof state after:
no goals
Theorem: Graph.EdgePath.append_assoc
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 v✝ w✝
v w u u' : V
p : EdgePath G v w
q : EdgePath G w u
r : EdgePath G u u'
⊢ p ++ q ++ r = p ++ (q ++ r)
Tactic:
induction p <;> aesop
Proof state after:
no goals
Theorem: Graph.EdgePath.reverse_reverse
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 v✝ w✝
v w : V
p : EdgePath G v w
⊢ reverse (reverse p) = p
Tactic:
induction p <;> aesop (add norm simp [reverse_cons, reverse_concat])
Proof state after:
no goals
Theorem: Graph.EdgePath.reverse_append
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 v✝ w✝
u v w : V
p : EdgePath G u v
q : EdgePath G v w
⊢ reverse (p ++ q) = reverse q ++ reverse p
Tactic:
induction p <;>
  aesop (add norm simp [reverse_cons, concat_eq_append_edge, append_assoc])
Proof state after:
no goals
Theorem: Graph.EdgePath.append_toList
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✝ v✝ w✝
G : Graph V E
v w u : V
p₁ : EdgePath G v w
p₂ : EdgePath G w u
⊢ toList (p₁ ++ p₂) = toList p₁ ++ toList p₂
Tactic:
induction p₁ with
| nil v => 
  simp [nil_toList]
| cons e p' ih =>
  simp [cons_toList]
  apply ih
Proof state after:
no goals
Theorem: Graph.EdgePath.append_toList
Proof state before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u✝ v✝¹ w✝ : V
e : EdgeBetween G✝ v✝¹ w✝
G : Graph V E
v✝ w u v : V
p₂ : EdgePath G v u
⊢ toList (nil v ++ p₂) = toList (nil v) ++ toList p₂
Tactic:
simp [nil_toList]
Proof state after:
no goals
Theorem: Graph.EdgePath.append_toList
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u✝¹ v✝¹ w✝¹ : V
e✝ : EdgeBetween G✝ v✝¹ w✝¹
G : Graph V E
v w u v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : ∀ (p₂ : EdgePath G u✝ u), toList (p' ++ p₂) = toList p' ++ toList p₂
p₂ : EdgePath G u✝ u
⊢ toList (cons e p' ++ p₂) = toList (cons e p') ++ toList p₂
Tactic:
simp [cons_toList]
Proof state after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u✝¹ v✝¹ w✝¹ : V
e✝ : EdgeBetween G✝ v✝¹ w✝¹
G : Graph V E
v w u v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : ∀ (p₂ : EdgePath G u✝ u), toList (p' ++ p₂) = toList p' ++ toList p₂
p₂ : EdgePath G u✝ u
⊢ toList (p' ++ p₂) = toList p' ++ toList p₂
Theorem: Graph.EdgePath.append_toList
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u✝¹ v✝¹ w✝¹ : V
e✝ : EdgeBetween G✝ v✝¹ w✝¹
G : Graph V E
v w u v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : ∀ (p₂ : EdgePath G u✝ u), toList (p' ++ p₂) = toList p' ++ toList p₂
p₂ : EdgePath G u✝ u
⊢ toList (p' ++ p₂) = toList p' ++ toList p₂
Tactic:
apply ih
Proof state after:
no goals
Theorem: Graph.EdgePath.concat_toList
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✝ v✝ w✝
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
⊢ toList (concat p e) = List.concat (toList p) e.edge
Tactic:
induction p with
| nil v => 
  simp [nil_toList]
  rw [concat, cons_toList, nil_toList]
| cons e p' ih =>
  simp [cons_toList, ih]
Proof state after:
no goals
Theorem: Graph.EdgePath.concat_toList
Proof state before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u✝ v✝¹ w✝ : V
e✝ : EdgeBetween G✝ v✝¹ w✝
G : Graph V E
v✝ w u v : V
e : EdgeBetween G v u
⊢ toList (concat (nil v) e) = List.concat (toList (nil v)) e.edge
Tactic:
simp [nil_toList]
Proof state after:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u✝ v✝¹ w✝ : V
e✝ : EdgeBetween G✝ v✝¹ w✝
G : Graph V E
v✝ w u v : V
e : EdgeBetween G v u
⊢ toList (concat (nil v) e) = [e.edge]
Theorem: Graph.EdgePath.concat_toList
Proof state before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u✝ v✝¹ w✝ : V
e✝ : EdgeBetween G✝ v✝¹ w✝
G : Graph V E
v✝ w u v : V
e : EdgeBetween G v u
⊢ toList (concat (nil v) e) = [e.edge]
Tactic:
rw [concat, cons_toList, nil_toList]
Proof state after:
no goals
Theorem: Graph.EdgePath.concat_toList
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u✝¹ v✝¹ w✝¹ : V
e✝¹ : EdgeBetween G✝ v✝¹ w✝¹
G : Graph V E
v w u v✝ w✝ u✝ : V
e✝ : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : ∀ (e : EdgeBetween G u✝ u), toList (concat p' e) = List.concat (toList p') e.edge
e : EdgeBetween G u✝ u
⊢ toList (concat (cons e✝ p') e) = List.concat (toList (cons e✝ p')) e.edge
Tactic:
simp [cons_toList, ih]
Proof state after:
no goals
Theorem: Graph.EdgePath.reverse_toList
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✝ v✝ w✝
G : Graph V E
v w : V
p : EdgePath G v w
⊢ toList (reverse p) = List.map G.bar (List.reverse (toList p))
Tactic:
induction p with
| nil _ => 
  simp [nil_toList]
| cons e p' ih =>
  simp [cons_toList, reverse_cons, concat_toList]
  simp [ih, EdgeBetween.bar]
Proof state after:
no goals
Theorem: Graph.EdgePath.reverse_toList
Proof state before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝¹ w✝ : V
e : EdgeBetween G✝ v✝¹ w✝
G : Graph V E
v w v✝ : V
⊢ toList (reverse (nil v✝)) = List.map G.bar (List.reverse (toList (nil v✝)))
Tactic:
simp [nil_toList]
Proof state after:
no goals
Theorem: Graph.EdgePath.reverse_toList
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝¹ w✝¹ : V
e✝ : EdgeBetween G✝ v✝¹ w✝¹
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : toList (reverse p') = List.map G.bar (List.reverse (toList p'))
⊢ toList (reverse (cons e p')) = List.map G.bar (List.reverse (toList (cons e p')))
Tactic:
simp [cons_toList, reverse_cons, concat_toList]
Proof state after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝¹ w✝¹ : V
e✝ : EdgeBetween G✝ v✝¹ w✝¹
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : toList (reverse p') = List.map G.bar (List.reverse (toList p'))
⊢ toList (reverse p') = List.map G.bar (List.reverse (toList p'))
Theorem: Graph.EdgePath.reverse_toList
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝¹ w✝¹ : V
e✝ : EdgeBetween G✝ v✝¹ w✝¹
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : toList (reverse p') = List.map G.bar (List.reverse (toList p'))
⊢ toList (reverse p') = List.map G.bar (List.reverse (toList p'))
Tactic:
simp [ih, EdgeBetween.bar]
Proof state after:
no goals
Theorem: Graph.EdgePath.toList_reverse
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✝ v✝ w✝
G : Graph V E
v w : V
p : EdgePath G v w
⊢ List.reverse (toList p) = List.map G.bar (toList (reverse p))
Tactic:
induction p with
| nil _ => 
  simp [nil_toList]
| cons e p' ih =>
  simp [cons_toList, reverse_cons, concat_toList]
  simp [ih, EdgeBetween.bar]
Proof state after:
no goals
Theorem: Graph.EdgePath.toList_reverse
Proof state before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝¹ w✝ : V
e : EdgeBetween G✝ v✝¹ w✝
G : Graph V E
v w v✝ : V
⊢ List.reverse (toList (nil v✝)) = List.map G.bar (toList (reverse (nil v✝)))
Tactic:
simp [nil_toList]
Proof state after:
no goals
Theorem: Graph.EdgePath.toList_reverse
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝¹ w✝¹ : V
e✝ : EdgeBetween G✝ v✝¹ w✝¹
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : List.reverse (toList p') = List.map G.bar (toList (reverse p'))
⊢ List.reverse (toList (cons e p')) = List.map G.bar (toList (reverse (cons e p')))
Tactic:
simp [cons_toList, reverse_cons, concat_toList]
Proof state after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝¹ w✝¹ : V
e✝ : EdgeBetween G✝ v✝¹ w✝¹
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : List.reverse (toList p') = List.map G.bar (toList (reverse p'))
⊢ List.reverse (toList p') = List.map G.bar (toList (reverse p'))
Theorem: Graph.EdgePath.toList_reverse
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝¹ w✝¹ : V
e✝ : EdgeBetween G✝ v✝¹ w✝¹
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : List.reverse (toList p') = List.map G.bar (toList (reverse p'))
⊢ List.reverse (toList p') = List.map G.bar (toList (reverse p'))
Tactic:
simp [ih, EdgeBetween.bar]
Proof state after:
no goals
Theorem: Graph.EdgePath.eq_of_toList_eq
Proof state before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝¹ w✝ : V
e : EdgeBetween G✝ v✝¹ w✝
G : Graph V E
v✝ w v : V
p₂ : EdgePath G v v
⊢ toList (nil v) = toList p₂ → nil v = p₂
Tactic:
match p₂ with
| EdgePath.nil v => 
  intro h
  rw [nil_toList] at h      
| EdgePath.cons e₂ p₂  =>
  intro h
  simp [cons_toList, nil_toList] at h
Proof state after:
no goals
Theorem: Graph.EdgePath.eq_of_toList_eq
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✝ v✝² w✝
G : Graph V E
v✝¹ w v✝ : V
p₂ : EdgePath G v✝ v✝
v : V
⊢ toList (nil v) = toList (nil v) → nil v = nil v
Tactic:
intro h
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✝ v✝² w✝
G : Graph V E
v✝¹ w v✝ : V
p₂ : EdgePath G v✝ v✝
v : V
h : toList (nil v) = toList (nil v)
⊢ nil v = nil v
Theorem: Graph.EdgePath.eq_of_toList_eq
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✝ v✝² w✝
G : Graph V E
v✝¹ w v✝ : V
p₂ : EdgePath G v✝ v✝
v : V
h : toList (nil v) = toList (nil v)
⊢ nil v = nil v
Tactic:
rw [nil_toList] at h
Proof state after:
no goals
Theorem: Graph.EdgePath.eq_of_toList_eq
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✝ v✝² w✝¹
G : Graph V E
v✝¹ w v✝ : V
p₂✝ : EdgePath G v✝ v✝
v w✝ : V
e₂ : EdgeBetween G v w✝
p₂ : EdgePath G w✝ v
⊢ toList (nil v) = toList (cons e₂ p₂) → nil v = cons e₂ p₂
Tactic:
intro h
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✝ v✝² w✝¹
G : Graph V E
v✝¹ w v✝ : V
p₂✝ : EdgePath G v✝ v✝
v w✝ : V
e₂ : EdgeBetween G v w✝
p₂ : EdgePath G w✝ v
h : toList (nil v) = toList (cons e₂ p₂)
⊢ nil v = cons e₂ p₂
Theorem: Graph.EdgePath.eq_of_toList_eq
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✝ v✝² w✝¹
G : Graph V E
v✝¹ w v✝ : V
p₂✝ : EdgePath G v✝ v✝
v w✝ : V
e₂ : EdgeBetween G v w✝
p₂ : EdgePath G w✝ v
h : toList (nil v) = toList (cons e₂ p₂)
⊢ nil v = cons e₂ p₂
Tactic:
simp [cons_toList, nil_toList] at h
Proof state after:
no goals
Theorem: Graph.EdgePath.eq_of_toList_eq
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝¹ w✝¹ : V
e : EdgeBetween G✝ v✝¹ w✝¹
G : Graph V E
v w v✝ w✝ u✝ : V
e₁ : EdgeBetween G v✝ w✝
p₁' : EdgePath G w✝ u✝
ih : ∀ (p₂ : EdgePath G w✝ u✝), toList p₁' = toList p₂ → p₁' = p₂
p₂ : EdgePath G v✝ u✝
⊢ toList (cons e₁ p₁') = toList p₂ → cons e₁ p₁' = p₂
Tactic:
intro h
Proof state after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝¹ w✝¹ : V
e : EdgeBetween G✝ v✝¹ w✝¹
G : Graph V E
v w v✝ w✝ u✝ : V
e₁ : EdgeBetween G v✝ w✝
p₁' : EdgePath G w✝ u✝
ih : ∀ (p₂ : EdgePath G w✝ u✝), toList p₁' = toList p₂ → p₁' = p₂
p₂ : EdgePath G v✝ u✝
h : toList (cons e₁ p₁') = toList p₂
⊢ cons e₁ p₁' = p₂
Theorem: Graph.EdgePath.eq_of_toList_eq
Proof state before:
case cons.nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝¹ w✝² : V
e : EdgeBetween G✝ v✝¹ w✝²
G : Graph V E
v w✝¹ v✝ w✝ u✝ w : V
e₁ : EdgeBetween G w w✝
p₁' : EdgePath G w✝ w
ih : ∀ (p₂ : EdgePath G w✝ w), toList p₁' = toList p₂ → p₁' = p₂
h : toList (cons e₁ p₁') = toList (nil w)
⊢ cons e₁ p₁' = nil w
Tactic:
simp [cons_toList, nil_toList] at h
Proof state after:
no goals
Theorem: Graph.EdgePath.eq_of_toList_eq
Proof state before:
case cons.cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : toList (cons e₁ p₁') = toList (cons e₂ p₂')
⊢ cons e₁ p₁' = cons e₂ p₂'
Tactic:
simp [cons_toList] at h
Proof state after:
case cons.cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
⊢ cons e₁ p₁' = cons e₂ p₂'
Theorem: Graph.EdgePath.eq_of_toList_eq
Proof state before:
case cons.cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
⊢ cons e₁ p₁' = cons e₂ p₂'
Tactic:
have e1t := e₁.term_eq
Proof state after:
case cons.cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₁.edge = w✝¹
⊢ cons e₁ p₁' = cons e₂ p₂'
Theorem: Graph.EdgePath.eq_of_toList_eq
Proof state before:
case cons.cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₁.edge = w✝¹
⊢ cons e₁ p₁' = cons e₂ p₂'
Tactic:
have e2t := e₂.term_eq
Proof state after:
case cons.cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₁.edge = w✝¹
e2t : τ G e₂.edge = w✝
⊢ cons e₁ p₁' = cons e₂ p₂'
Theorem: Graph.EdgePath.eq_of_toList_eq
Proof state before:
case cons.cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₁.edge = w✝¹
e2t : τ G e₂.edge = w✝
⊢ cons e₁ p₁' = cons e₂ p₂'
Tactic:
rw [h.1] at e1t
Proof state after:
case cons.cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : τ G e₂.edge = w✝
⊢ cons e₁ p₁' = cons e₂ p₂'
Theorem: Graph.EdgePath.eq_of_toList_eq
Proof state before:
case cons.cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : τ G e₂.edge = w✝
⊢ cons e₁ p₁' = cons e₂ p₂'
Tactic:
rw [e1t] at e2t
Proof state after:
case cons.cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
⊢ cons e₁ p₁' = cons e₂ p₂'
Theorem: Graph.EdgePath.eq_of_toList_eq
Proof state before:
case cons.cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
⊢ cons e₁ p₁' = cons e₂ p₂'
Tactic:
cases e2t
Proof state after:
case cons.cons.refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝² w✝¹ : V
e : EdgeBetween G✝ v✝² w✝¹
G : Graph V E
v w v✝¹ w✝ u✝¹ v✝ u✝ : V
e₁ : EdgeBetween G v✝ w✝
p₁' : EdgePath G w✝ u✝
ih : ∀ (p₂ : EdgePath G w✝ u✝), toList p₁' = toList p₂ → p₁' = p₂
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝) (p₁' : EdgePath G w✝ u✝),
    (∀ (p₂ : EdgePath G w✝ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝
⊢ cons e₁ p₁' = cons e₂ p₂'