internlm/Lean-Github huggingface dataset:
Theorem: Graph.PathClass.concat_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
⊢ [[a₁]] = [[a₂]] → [[concat a₁ b]] = [[concat a₂ b]]
Tactic:
intro rel
Proof state after:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
rel : [[a₁]] = [[a₂]]
⊢ [[concat a₁ b]] = [[concat a₂ b]]
Theorem: Graph.PathClass.concat_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
rel : [[a₁]] = [[a₂]]
⊢ [[concat a₁ b]] = [[concat a₂ b]]
Tactic:
have: concat a₁  b = a₁ ++ (concat (nil _) b) := by 
  rw [append_concat, append_nil]
Proof state after:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
rel : [[a₁]] = [[a₂]]
this : concat a₁ b = a₁ ++ concat (nil w) b
⊢ [[concat a₁ b]] = [[concat a₂ b]]
Theorem: Graph.PathClass.concat_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
rel : [[a₁]] = [[a₂]]
this : concat a₁ b = a₁ ++ concat (nil w) b
⊢ [[concat a₁ b]] = [[concat a₂ b]]
Tactic:
rw [this]
Proof state after:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
rel : [[a₁]] = [[a₂]]
this : concat a₁ b = a₁ ++ concat (nil w) b
⊢ [[a₁ ++ concat (nil w) b]] = [[concat a₂ b]]
Theorem: Graph.PathClass.concat_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
rel : [[a₁]] = [[a₂]]
this : concat a₁ b = a₁ ++ concat (nil w) b
⊢ [[a₁ ++ concat (nil w) b]] = [[concat a₂ b]]
Tactic:
have: concat a₂  b = a₂ ++ (concat (nil _) b) := by 
  rw [append_concat, append_nil]
Proof state after:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
rel : [[a₁]] = [[a₂]]
this✝ : concat a₁ b = a₁ ++ concat (nil w) b
this : concat a₂ b = a₂ ++ concat (nil w) b
⊢ [[a₁ ++ concat (nil w) b]] = [[concat a₂ b]]
Theorem: Graph.PathClass.concat_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
rel : [[a₁]] = [[a₂]]
this✝ : concat a₁ b = a₁ ++ concat (nil w) b
this : concat a₂ b = a₂ ++ concat (nil w) b
⊢ [[a₁ ++ concat (nil w) b]] = [[concat a₂ b]]
Tactic:
rw [this, append_mul, append_mul, rel]
Proof state after:
no goals
Theorem: Graph.PathClass.concat_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
rel : [[a₁]] = [[a₂]]
⊢ concat a₁ b = a₁ ++ concat (nil w) b
Tactic:
rw [append_concat, append_nil]
Proof state after:
no goals
Theorem: Graph.PathClass.concat_equiv_of_equiv
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w u : V
a₁ a₂ : EdgePath G v w
b : EdgeBetween G w u
rel : [[a₁]] = [[a₂]]
this : concat a₁ b = a₁ ++ concat (nil w) b
⊢ concat a₂ b = a₂ ++ concat (nil w) b
Tactic:
rw [append_concat, append_nil]
Proof state after:
no goals
Theorem: Graph.toFuncV_init
Proof state before:
V : Type u
E : Type v
G : Graph V E
u v w : V
e : EdgeBetween G v w
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
⊢ ∀ (e : E₁), G₂.ι (f.toFuncE e) = f.toFuncV (G₁.ι e)
Tactic:
intro e
Proof state after:
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
e : E₁
⊢ G₂.ι (f.toFuncE e) = f.toFuncV (G₁.ι e)
Theorem: Graph.toFuncV_init
Proof state before:
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
e : E₁
⊢ G₂.ι (f.toFuncE e) = f.toFuncV (G₁.ι e)
Tactic:
exact f.toFuncV_init e
Proof state after:
no goals
Theorem: Graph.toFuncE_bar
Proof state before:
V : Type u
E : Type v
G : Graph V E
u v w : V
e : EdgeBetween G v w
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
⊢ ∀ (e : E₁), f.toFuncE (G₁.bar e) = G₂.bar (f.toFuncE e)
Tactic:
intro e
Proof state after:
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
e : E₁
⊢ f.toFuncE (G₁.bar e) = G₂.bar (f.toFuncE e)
Theorem: Graph.toFuncE_bar
Proof state before:
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
e : E₁
⊢ f.toFuncE (G₁.bar e) = G₂.bar (f.toFuncE e)
Tactic:
exact f.toFuncE_bar e
Proof state after:
no goals
Theorem: Graph.morphism_terminal_commutes
Proof state before:
V : Type u
E : Type v
G : Graph V E
u v w : V
e : EdgeBetween G v w
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
⊢ ∀ (e : E₁), τ G₂ (f.toFuncE e) = f.toFuncV (τ G₁ e)
Tactic:
intro e
Proof state after:
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
e : E₁
⊢ τ G₂ (f.toFuncE e) = f.toFuncV (τ G₁ e)
Theorem: Graph.morphism_terminal_commutes
Proof state before:
V : Type u
E : Type v
G : Graph V E
u v w : V
e✝ : EdgeBetween G v w
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
e : E₁
⊢ τ G₂ (f.toFuncE e) = f.toFuncV (τ G₁ e)
Tactic:
rw [Graph.τ, Graph.τ, ←toFuncE_bar, ←toFuncV_init]
Proof state after:
no goals
Theorem: Graph.cons_eq
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e✝ : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' u : V
e : EdgeBetween G v w
e' : EdgeBetween G v w'
p : EdgePath G w u
p' : EdgePath G w' u
eq₁ : e.edge = e'.edge
eq₂ : w = w'
eq₃ : p = (_ : w' = w) ▸ p'
⊢ cons e' p' = cons e p
Tactic:
match p, p', e, e', eq₂ with
| p, p', e, e', rfl => 
  simp [cons_toList,  eq₃]
  ext
  symm
  assumption
Proof state after:
no goals
Theorem: Graph.cons_eq
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e✝¹ : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w = w'
p p' : EdgePath G w u
e e' : EdgeBetween G v w
eq₁ : e.edge = e'.edge
eq₃ : p = (_ : w = w) ▸ p'
⊢ cons e' p' = cons e p
Tactic:
simp [cons_toList,  eq₃]
Proof state after:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e✝¹ : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w = w'
p p' : EdgePath G w u
e e' : EdgeBetween G v w
eq₁ : e.edge = e'.edge
eq₃ : p = (_ : w = w) ▸ p'
⊢ e' = e
Theorem: Graph.cons_eq
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e✝¹ : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w = w'
p p' : EdgePath G w u
e e' : EdgeBetween G v w
eq₁ : e.edge = e'.edge
eq₃ : p = (_ : w = w) ▸ p'
⊢ e' = e
Tactic:
ext
Proof state after:
case edge
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e✝¹ : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w = w'
p p' : EdgePath G w u
e e' : EdgeBetween G v w
eq₁ : e.edge = e'.edge
eq₃ : p = (_ : w = w) ▸ p'
⊢ e'.edge = e.edge
Theorem: Graph.cons_eq
Proof state before:
case edge
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e✝¹ : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w = w'
p p' : EdgePath G w u
e e' : EdgeBetween G v w
eq₁ : e.edge = e'.edge
eq₃ : p = (_ : w = w) ▸ p'
⊢ e'.edge = e.edge
Tactic:
symm
Proof state after:
case edge
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e✝¹ : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w = w'
p p' : EdgePath G w u
e e' : EdgeBetween G v w
eq₁ : e.edge = e'.edge
eq₃ : p = (_ : w = w) ▸ p'
⊢ e.edge = e'.edge
Theorem: Graph.cons_eq
Proof state before:
case edge
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e✝¹ : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w = w'
p p' : EdgePath G w u
e e' : EdgeBetween G v w
eq₁ : e.edge = e'.edge
eq₃ : p = (_ : w = w) ▸ p'
⊢ e.edge = e'.edge
Tactic:
assumption
Proof state after:
no goals
Theorem: Graph.cons_eq'
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e✝ : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' u : V
e : EdgeBetween G v w
e' : EdgeBetween G v w'
p : EdgePath G w u
p' : EdgePath G w' u
eq₁ : e.edge = e'.edge
eq₂ : w' = w
eq₃ : (_ : w = w') ▸ p = p'
⊢ cons e' p' = cons e p
Tactic:
match p, p', e, e', eq₂ with
| p, p', e, e', rfl => 
  simp [cons_toList, Eq.symm eq₃]
  ext
  symm
  assumption
Proof state after:
no goals
Theorem: Graph.cons_eq'
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e✝¹ : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w' = w
p p' : EdgePath G w' u
e e' : EdgeBetween G v w'
eq₁ : e.edge = e'.edge
eq₃ : (_ : w' = w') ▸ p = p'
⊢ cons e' p' = cons e p
Tactic:
simp [cons_toList, Eq.symm eq₃]
Proof state after:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e✝¹ : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w' = w
p p' : EdgePath G w' u
e e' : EdgeBetween G v w'
eq₁ : e.edge = e'.edge
eq₃ : (_ : w' = w') ▸ p = p'
⊢ e' = e
Theorem: Graph.cons_eq'
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e✝¹ : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w' = w
p p' : EdgePath G w' u
e e' : EdgeBetween G v w'
eq₁ : e.edge = e'.edge
eq₃ : (_ : w' = w') ▸ p = p'
⊢ e' = e
Tactic:
ext
Proof state after:
case edge
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e✝¹ : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w' = w
p p' : EdgePath G w' u
e e' : EdgeBetween G v w'
eq₁ : e.edge = e'.edge
eq₃ : (_ : w' = w') ▸ p = p'
⊢ e'.edge = e.edge
Theorem: Graph.cons_eq'
Proof state before:
case edge
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e✝¹ : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w' = w
p p' : EdgePath G w' u
e e' : EdgeBetween G v w'
eq₁ : e.edge = e'.edge
eq₃ : (_ : w' = w') ▸ p = p'
⊢ e'.edge = e.edge
Tactic:
symm
Proof state after:
case edge
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e✝¹ : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w' = w
p p' : EdgePath G w' u
e e' : EdgeBetween G v w'
eq₁ : e.edge = e'.edge
eq₃ : (_ : w' = w') ▸ p = p'
⊢ e.edge = e'.edge
Theorem: Graph.cons_eq'
Proof state before:
case edge
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e✝¹ : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w' = w
p p' : EdgePath G w' u
e e' : EdgeBetween G v w'
eq₁ : e.edge = e'.edge
eq₃ : (_ : w' = w') ▸ p = p'
⊢ e.edge = e'.edge
Tactic:
assumption
Proof state after:
no goals
Theorem: Graph.toList_cast_init
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v v' w : V
p : EdgePath G v w
eqn : v = v'
⊢ toList p = toList (eqn ▸ p)
Tactic:
match p, eqn with
| p, rfl => rfl
Proof state after:
no goals
Theorem: Graph.toList_cast_init
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v v' w : V
p✝ : EdgePath G v w
eqn : v = v'
p : EdgePath G v w
⊢ toList p = toList ((_ : v = v) ▸ p)
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.toList_cast_terminal
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' : V
p : EdgePath G v w
eqn : w = w'
⊢ toList p = toList (eqn ▸ p)
Tactic:
match p, eqn with
| p, rfl => rfl
Proof state after:
no goals
Theorem: Graph.toList_cast_terminal
Proof state before:
V : Type u
E : Type v
G✝ : Graph V E
u v✝ w✝ : V
e : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' : V
p✝ : EdgePath G v w
eqn : w = w'
p : EdgePath G v w
⊢ toList p = toList ((_ : w = w) ▸ p)
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.eq_of_toList_eq
Proof state before:
case nil
V : Type u
E : Type v
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.eq_of_toList_eq
Proof state before:
V : Type u
E : Type v
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
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.eq_of_toList_eq
Proof state before:
V : Type u
E : Type v
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.eq_of_toList_eq
Proof state before:
V : Type u
E : Type v
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
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.eq_of_toList_eq
Proof state before:
V : Type u
E : Type v
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.eq_of_toList_eq
Proof state before:
case cons
V : Type u
E : Type v
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
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.eq_of_toList_eq
Proof state before:
case cons.nil
V : Type u
E : Type v
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.eq_of_toList_eq
Proof state before:
case cons.cons
V : Type u
E : Type v
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
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.eq_of_toList_eq
Proof state before:
case cons.cons
V : Type u
E : Type v
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
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.eq_of_toList_eq
Proof state before:
case cons.cons
V : Type u
E : Type v
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
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.eq_of_toList_eq
Proof state before:
case cons.cons
V : Type u
E : Type v
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
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.eq_of_toList_eq
Proof state before:
case cons.cons
V : Type u
E : Type v
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
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₂'