internlm/Lean-Github huggingface dataset:
Theorem: Graph.EdgePath.eq_of_toList_eq
Proof state before:
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₂'
Tactic:
congr
Proof state after:
case cons.cons.refl.e_a
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✝
⊢ e₁ = e₂

case cons.cons.refl.e_a
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✝
⊢ p₁' = p₂'
Theorem: Graph.EdgePath.eq_of_toList_eq
Proof state before:
case cons.cons.refl.e_a
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✝
⊢ e₁ = e₂
Tactic:
ext
Proof state after:
case cons.cons.refl.e_a.edge
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✝
⊢ e₁.edge = e₂.edge
Theorem: Graph.EdgePath.eq_of_toList_eq
Proof state before:
case cons.cons.refl.e_a.edge
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✝
⊢ e₁.edge = e₂.edge
Tactic:
exact h.1
Proof state after:
no goals
Theorem: Graph.EdgePath.eq_of_toList_eq
Proof state before:
case cons.cons.refl.e_a
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✝
⊢ p₁' = p₂'
Tactic:
apply ih
Proof state after:
case cons.cons.refl.e_a.a
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✝
⊢ toList p₁' = toList p₂'
Theorem: Graph.EdgePath.eq_of_toList_eq
Proof state before:
case cons.cons.refl.e_a.a
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✝
⊢ toList p₁' = toList p₂'
Tactic:
exact h.2
Proof state after:
no goals
Theorem: Graph.EdgePath.eq_of_edge_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
e₁ e₂ : EdgeBetween G v w
⊢ e₁.edge = e₂.edge → e₁ = e₂
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
e₁ e₂ : EdgeBetween G v w
h : e₁.edge = e₂.edge
⊢ e₁ = e₂
Theorem: Graph.EdgePath.eq_of_edge_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
e₁ e₂ : EdgeBetween G v w
h : e₁.edge = e₂.edge
⊢ e₁ = e₂
Tactic:
ext
Proof state after:
case edge
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
e₁ e₂ : EdgeBetween G v w
h : e₁.edge = e₂.edge
⊢ e₁.edge = e₂.edge
Theorem: Graph.EdgePath.eq_of_edge_eq
Proof state before:
case edge
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
e₁ e₂ : EdgeBetween G v w
h : e₁.edge = e₂.edge
⊢ e₁.edge = e₂.edge
Tactic:
exact h
Proof state after:
no goals
Theorem: Graph.EdgePath.terminal_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₁ v₂ w₁ w₂ : V
p₁ : EdgePath G v₁ w₁
p₂ : EdgePath G v₂ w₂
⊢ toList p₁ = toList p₂ → v₁ = v₂ → w₁ = w₂
Tactic:
induction p₁ with
| nil v₁' =>
  match p₂ with
  | EdgePath.nil v => 
    intro h heq
    rw [nil_toList] at h      
    exact heq
  | EdgePath.cons e₂ p₂  =>
    intro h
    simp [cons_toList, nil_toList] at h
| cons e p₁' ih =>    
  intro h heq
  match p₂ with
  | EdgePath.nil w =>
    simp [cons_toList, nil_toList] at h
  | EdgePath.cons e₂ p₂' =>
    simp [cons_toList] at h
    apply terminal_eq_of_toList_eq p₁' p₂' h.right
    rw [←e₂.term_eq, ←e.term_eq, h.left]
Proof state after:
no goals
Theorem: Graph.EdgePath.terminal_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₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v₁' : V
⊢ toList (nil v₁') = toList p₂ → v₁' = v₂ → v₁' = w₂
Tactic:
match p₂ with
| EdgePath.nil v => 
  intro h heq
  rw [nil_toList] at h      
  exact heq
| EdgePath.cons e₂ p₂  =>
  intro h
  simp [cons_toList, nil_toList] at h
Proof state after:
no goals
Theorem: Graph.EdgePath.terminal_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₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v₁' v : V
⊢ toList (nil v₁') = toList (nil v) → v₁' = v → v₁' = v
Tactic:
intro h heq
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₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v₁' v : V
h : toList (nil v₁') = toList (nil v)
heq : v₁' = v
⊢ v₁' = v
Theorem: Graph.EdgePath.terminal_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₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v₁' v : V
h : toList (nil v₁') = toList (nil v)
heq : v₁' = v
⊢ v₁' = v
Tactic:
rw [nil_toList] at 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₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v₁' v : V
h : [] = toList (nil v)
heq : v₁' = v
⊢ v₁' = v
Theorem: Graph.EdgePath.terminal_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₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v₁' v : V
h : [] = toList (nil v)
heq : v₁' = v
⊢ v₁' = v
Tactic:
exact heq
Proof state after:
no goals
Theorem: Graph.EdgePath.terminal_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₁ v₂✝ w₁ w₂✝ : V
p₂✝ : EdgePath G v₂✝ w₂✝
v₁' w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂ : EdgePath G w✝ w₂
⊢ toList (nil v₁') = toList (cons e₂ p₂) → v₁' = v₂ → v₁' = w₂
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₁ v₂✝ w₁ w₂✝ : V
p₂✝ : EdgePath G v₂✝ w₂✝
v₁' w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂ : EdgePath G w✝ w₂
h : toList (nil v₁') = toList (cons e₂ p₂)
⊢ v₁' = v₂ → v₁' = w₂
Theorem: Graph.EdgePath.terminal_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₁ v₂✝ w₁ w₂✝ : V
p₂✝ : EdgePath G v₂✝ w₂✝
v₁' w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂ : EdgePath G w✝ w₂
h : toList (nil v₁') = toList (cons e₂ p₂)
⊢ v₁' = v₂ → v₁' = w₂
Tactic:
simp [cons_toList, nil_toList] at h
Proof state after:
no goals
Theorem: Graph.EdgePath.terminal_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₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p₁' : EdgePath G w✝ u✝
ih : toList p₁' = toList p₂ → w✝ = v₂ → u✝ = w₂
⊢ toList (cons e p₁') = toList p₂ → v✝ = v₂ → u✝ = w₂
Tactic:
intro h heq
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₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p₁' : EdgePath G w✝ u✝
ih : toList p₁' = toList p₂ → w✝ = v₂ → u✝ = w₂
h : toList (cons e p₁') = toList p₂
heq : v✝ = v₂
⊢ u✝ = w₂
Theorem: Graph.EdgePath.terminal_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₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p₁' : EdgePath G w✝ u✝
ih : toList p₁' = toList p₂ → w✝ = v₂ → u✝ = w₂
h : toList (cons e p₁') = toList p₂
heq : v✝ = v₂
⊢ u✝ = w₂
Tactic:
match p₂ with
| EdgePath.nil w =>
  simp [cons_toList, nil_toList] at h
| EdgePath.cons e₂ p₂' =>
  simp [cons_toList] at h
  apply terminal_eq_of_toList_eq p₁' p₂' h.right
  rw [←e₂.term_eq, ←e.term_eq, h.left]
Proof state after:
no goals
Theorem: Graph.EdgePath.terminal_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₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p₁' : EdgePath G w✝ u✝
w : V
ih : toList p₁' = toList (nil w) → w✝ = w → u✝ = w
h : toList (cons e p₁') = toList (nil w)
heq : v✝ = w
⊢ u✝ = w
Tactic:
simp [cons_toList, nil_toList] at h
Proof state after:
no goals
Theorem: Graph.EdgePath.terminal_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₁ v₂✝ w₁ w₂✝ : V
p₂ : EdgePath G v₂✝ w₂✝
v✝ w✝¹ u✝ : V
e : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂' : EdgePath G w✝ w₂
ih : toList p₁' = toList (cons e₂ p₂') → w✝¹ = v₂ → u✝ = w₂
h : toList (cons e p₁') = toList (cons e₂ p₂')
heq : v✝ = v₂
⊢ u✝ = w₂
Tactic:
simp [cons_toList] at 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₁ v₂✝ w₁ w₂✝ : V
p₂ : EdgePath G v₂✝ w₂✝
v✝ w✝¹ u✝ : V
e : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂' : EdgePath G w✝ w₂
ih : toList p₁' = toList (cons e₂ p₂') → w✝¹ = v₂ → u✝ = w₂
heq : v✝ = v₂
h : e.edge = e₂.edge ∧ toList p₁' = toList p₂'
⊢ u✝ = w₂
Theorem: Graph.EdgePath.terminal_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₁ v₂✝ w₁ w₂✝ : V
p₂ : EdgePath G v₂✝ w₂✝
v✝ w✝¹ u✝ : V
e : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂' : EdgePath G w✝ w₂
ih : toList p₁' = toList (cons e₂ p₂') → w✝¹ = v₂ → u✝ = w₂
heq : v✝ = v₂
h : e.edge = e₂.edge ∧ toList p₁' = toList p₂'
⊢ u✝ = w₂
Tactic:
apply terminal_eq_of_toList_eq p₁' p₂' h.right
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₁ v₂✝ w₁ w₂✝ : V
p₂ : EdgePath G v₂✝ w₂✝
v✝ w✝¹ u✝ : V
e : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂' : EdgePath G w✝ w₂
ih : toList p₁' = toList (cons e₂ p₂') → w✝¹ = v₂ → u✝ = w₂
heq : v✝ = v₂
h : e.edge = e₂.edge ∧ toList p₁' = toList p₂'
⊢ w✝¹ = w✝
Theorem: Graph.EdgePath.terminal_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₁ v₂✝ w₁ w₂✝ : V
p₂ : EdgePath G v₂✝ w₂✝
v✝ w✝¹ u✝ : V
e : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂' : EdgePath G w✝ w₂
ih : toList p₁' = toList (cons e₂ p₂') → w✝¹ = v₂ → u✝ = w₂
heq : v✝ = v₂
h : e.edge = e₂.edge ∧ toList p₁' = toList p₂'
⊢ w✝¹ = w✝
Tactic:
rw [←e₂.term_eq, ←e.term_eq, h.left]
Proof state after:
no goals
Theorem: Graph.EdgePath.toList_shiftTarget
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 w' : V
p : EdgePath G v w
eql : w = w'
⊢ toList (shiftTarget p eql) = toList p
Tactic:
match p, w', eql with
| nil _, _, rfl =>
  rename_i v'
  simp only [shiftTarget]
| cons e p', w', eql =>
  simp only [shiftTarget, cons_toList, toList_shiftTarget]
Proof state after:
no goals
Theorem: Graph.EdgePath.toList_shiftTarget
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 w' : V
p : EdgePath G v w
eql : w = w'
⊢ toList (shiftTarget (nil v) (_ : v = v)) = toList (nil v)
Tactic:
rename_i v'
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝ v' : V
e : EdgeBetween G✝ v✝ v'
G : Graph V E
v w w' : V
p : EdgePath G v w
eql : w = w'
⊢ toList (shiftTarget (nil v) (_ : v = v)) = toList (nil v)
Theorem: Graph.EdgePath.toList_shiftTarget
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v✝ v' : V
e : EdgeBetween G✝ v✝ v'
G : Graph V E
v w w' : V
p : EdgePath G v w
eql : w = w'
⊢ toList (shiftTarget (nil v) (_ : v = v)) = toList (nil v)
Tactic:
simp only [shiftTarget]
Proof state after:
no goals
Theorem: Graph.EdgePath.toList_shiftTarget
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✝¹ w'✝ : V
p : EdgePath G v w✝¹
eql✝ : w✝¹ = w'✝
w w✝ : V
e : EdgeBetween G v w✝
p' : EdgePath G w✝ w
w' : V
eql : w = w'
⊢ toList (shiftTarget (cons e p') eql) = toList (cons e p')
Tactic:
simp only [shiftTarget, cons_toList, toList_shiftTarget]
Proof state after:
no goals
Theorem: Graph.EdgePath.toList_shiftEnds
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 v' w w' : V
p : EdgePath G v w
eqlv : v = v'
eqlw : w = w'
⊢ toList (shiftEnds p eqlv eqlw) = toList p
Tactic:
match p, w', eqlv, eqlw with
| nil _, _, rfl, rfl =>
  simp only [shiftEnds]
| cons e p', w', rfl,  eqlw =>
  simp only [shiftEnds, cons_toList, toList_shiftTarget]
Proof state after:
no goals
Theorem: Graph.EdgePath.toList_shiftEnds
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 v' w w' : V
p : EdgePath G v w
eqlv : v = v'
eqlw : w = w'
⊢ toList (shiftEnds (nil v) (_ : v = v) (_ : v = v)) = toList (nil v)
Tactic:
simp only [shiftEnds]
Proof state after:
no goals
Theorem: Graph.EdgePath.toList_shiftEnds
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 v' w✝¹ w'✝ : V
p : EdgePath G v w✝¹
eqlv : v = v'
eqlw✝ : w✝¹ = w'✝
w w✝ : V
e : EdgeBetween G v w✝
p' : EdgePath G w✝ w
w' : V
eqlw : w = w'
⊢ toList (shiftEnds (cons e p') (_ : v = v) eqlw) = toList (cons e p')
Tactic:
simp only [shiftEnds, cons_toList, toList_shiftTarget]
Proof state after:
no goals
Theorem: Graph.EdgePath.Reduction.property
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' p : EdgePath G v w
u u' : V
e' : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
⊢ ∃ u_1 u'_1 e p₁_1 p₂_1, p₁_1 ++ cons e (cons (EdgeBetween.bar e) p₂_1) = p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂)
Tactic:
use u, u', e', p₁, p₂
Proof state after:
no goals
Theorem: Graph.not_reduced_of_split
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
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
⊢ p = p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) → ¬reduced p
Tactic:
intro eqn red
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 u' : V
p : EdgePath G v w
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p = p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)
red : reduced p
⊢ False
Theorem: Graph.not_reduced_of_split
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
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p = p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)
red : reduced p
⊢ False
Tactic:
have red' := red (p₁ ++ p₂)
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 u' : V
p : EdgePath G v w
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p = p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)
red : reduced p
red' : ¬Reduction p (p₁ ++ p₂)
⊢ False
Theorem: Graph.not_reduced_of_split
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
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p = p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)
red : reduced p
red' : ¬Reduction p (p₁ ++ p₂)
⊢ False
Tactic:
rw [eqn] at red'
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 u' : V
p : EdgePath G v w
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p = p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)
red : reduced p
red' : ¬Reduction (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (p₁ ++ p₂)
⊢ False
Theorem: Graph.not_reduced_of_split
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
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p = p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)
red : reduced p
red' : ¬Reduction (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (p₁ ++ p₂)
⊢ False
Tactic:
apply red'
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 u' : V
p : EdgePath G v w
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p = p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)
red : reduced p
red' : ¬Reduction (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (p₁ ++ p₂)
⊢ Reduction (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (p₁ ++ p₂)
Theorem: Graph.not_reduced_of_split
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
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p = p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)
red : reduced p
red' : ¬Reduction (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (p₁ ++ p₂)
⊢ Reduction (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (p₁ ++ p₂)
Tactic:
apply Reduction.step
Proof state after:
no goals
Theorem: Graph.tail_reduced
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
e : EdgeBetween G u v
p : EdgePath G v w
⊢ reduced (cons e p) → reduced p
Tactic:
intro red p' red'
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 w : V
e : EdgeBetween G u v
p : EdgePath G v w
red : reduced (cons e p)
p' : EdgePath G v w
red' : Reduction p p'
⊢ False