internlm/Lean-Github huggingface dataset:
Theorem: Graph.reduced_redCons
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
hyp : reduced (cons e' p')
c' : ¬e' = EdgeBetween.bar e''
p'' : EdgePath G u✝ w
red' : Reduction (cons e'' (cons e' p')) p''
u u' : V
p₁ : EdgePath G u✝ u
e : EdgeBetween G u✝ u'
p₂ : EdgePath G u✝ w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e'' (cons e' p')
leqn : e.edge = e''.edge ∧ G.bar e.edge = e'.edge ∧ toList p₂ = toList p'
⊢ False
Tactic:
have : e' = e''.bar := by
  ext
  rw [EdgeBetween.bar_eq_bar]
  rw [← leqn.1, leqn.2.1]
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
hyp : reduced (cons e' p')
c' : ¬e' = EdgeBetween.bar e''
p'' : EdgePath G u✝ w
red' : Reduction (cons e'' (cons e' p')) p''
u u' : V
p₁ : EdgePath G u✝ u
e : EdgeBetween G u✝ u'
p₂ : EdgePath G u✝ w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e'' (cons e' p')
leqn : e.edge = e''.edge ∧ G.bar e.edge = e'.edge ∧ toList p₂ = toList p'
this : e' = EdgeBetween.bar e''
⊢ False
Theorem: Graph.reduced_redCons
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
hyp : reduced (cons e' p')
c' : ¬e' = EdgeBetween.bar e''
p'' : EdgePath G u✝ w
red' : Reduction (cons e'' (cons e' p')) p''
u u' : V
p₁ : EdgePath G u✝ u
e : EdgeBetween G u✝ u'
p₂ : EdgePath G u✝ w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e'' (cons e' p')
leqn : e.edge = e''.edge ∧ G.bar e.edge = e'.edge ∧ toList p₂ = toList p'
this : e' = EdgeBetween.bar e''
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Graph.reduced_redCons
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
hyp : reduced (cons e' p')
c' : ¬e' = EdgeBetween.bar e''
p'' : EdgePath G u✝ w
red' : Reduction (cons e'' (cons e' p')) p''
u u' : V
p₁ : EdgePath G u✝ u
e : EdgeBetween G u✝ u'
p₂ : EdgePath G u✝ w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e'' (cons e' p')
leqn : e.edge = e''.edge ∧ G.bar e.edge = e'.edge ∧ toList p₂ = toList p'
⊢ e' = EdgeBetween.bar 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 u✝ v
p : EdgePath G v w'
w : V
e' : EdgeBetween G v u✝
p' : EdgePath G u✝ w
hyp : reduced (cons e' p')
c' : ¬e' = EdgeBetween.bar e''
p'' : EdgePath G u✝ w
red' : Reduction (cons e'' (cons e' p')) p''
u u' : V
p₁ : EdgePath G u✝ u
e : EdgeBetween G u✝ u'
p₂ : EdgePath G u✝ w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e'' (cons e' p')
leqn : e.edge = e''.edge ∧ G.bar e.edge = e'.edge ∧ toList p₂ = toList p'
⊢ e'.edge = (EdgeBetween.bar e'').edge
Theorem: Graph.reduced_redCons
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 u✝ v
p : EdgePath G v w'
w : V
e' : EdgeBetween G v u✝
p' : EdgePath G u✝ w
hyp : reduced (cons e' p')
c' : ¬e' = EdgeBetween.bar e''
p'' : EdgePath G u✝ w
red' : Reduction (cons e'' (cons e' p')) p''
u u' : V
p₁ : EdgePath G u✝ u
e : EdgeBetween G u✝ u'
p₂ : EdgePath G u✝ w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e'' (cons e' p')
leqn : e.edge = e''.edge ∧ G.bar e.edge = e'.edge ∧ toList p₂ = toList p'
⊢ e'.edge = (EdgeBetween.bar e'').edge
Tactic:
rw [EdgeBetween.bar_eq_bar]
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 u✝ v
p : EdgePath G v w'
w : V
e' : EdgeBetween G v u✝
p' : EdgePath G u✝ w
hyp : reduced (cons e' p')
c' : ¬e' = EdgeBetween.bar e''
p'' : EdgePath G u✝ w
red' : Reduction (cons e'' (cons e' p')) p''
u u' : V
p₁ : EdgePath G u✝ u
e : EdgeBetween G u✝ u'
p₂ : EdgePath G u✝ w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e'' (cons e' p')
leqn : e.edge = e''.edge ∧ G.bar e.edge = e'.edge ∧ toList p₂ = toList p'
⊢ e'.edge = G.bar e''.edge
Theorem: Graph.reduced_redCons
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 u✝ v
p : EdgePath G v w'
w : V
e' : EdgeBetween G v u✝
p' : EdgePath G u✝ w
hyp : reduced (cons e' p')
c' : ¬e' = EdgeBetween.bar e''
p'' : EdgePath G u✝ w
red' : Reduction (cons e'' (cons e' p')) p''
u u' : V
p₁ : EdgePath G u✝ u
e : EdgeBetween G u✝ u'
p₂ : EdgePath G u✝ w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e'' (cons e' p')
leqn : e.edge = e''.edge ∧ G.bar e.edge = e'.edge ∧ toList p₂ = toList p'
⊢ e'.edge = G.bar e''.edge
Tactic:
rw [← leqn.1, leqn.2.1]
Proof state after:
no goals
Theorem: Graph.reduced_redCons
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
hyp : reduced (cons e' p')
c' : ¬e' = EdgeBetween.bar e✝
p'' : EdgePath G u✝¹ w
red' : Reduction (cons e✝ (cons e' p')) p''
u✝ u' : V
p₁ : EdgePath G u✝¹ u✝
u w✝ : V
ph : EdgeBetween G u✝¹ w✝
pt : EdgePath G w✝ u
e : EdgeBetween G u u'
p₂ : EdgePath G u w
eqn : cons ph pt ++ cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (cons e' p')
⊢ False
Tactic:
symm at eqn
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
hyp : reduced (cons e' p')
c' : ¬e' = EdgeBetween.bar e✝
p'' : EdgePath G u✝¹ w
red' : Reduction (cons e✝ (cons e' p')) p''
u✝ u' : V
p₁ : EdgePath G u✝¹ u✝
u w✝ : V
ph : EdgeBetween G u✝¹ w✝
pt : EdgePath G w✝ u
e : EdgeBetween G u u'
p₂ : EdgePath G u w
eqn : cons e✝ (cons e' p') = cons ph pt ++ cons e (cons (EdgeBetween.bar e) p₂)
⊢ False
Theorem: Graph.reduced_redCons
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
hyp : reduced (cons e' p')
c' : ¬e' = EdgeBetween.bar e✝
p'' : EdgePath G u✝¹ w
red' : Reduction (cons e✝ (cons e' p')) p''
u✝ u' : V
p₁ : EdgePath G u✝¹ u✝
u w✝ : V
ph : EdgeBetween G u✝¹ w✝
pt : EdgePath G w✝ u
e : EdgeBetween G u u'
p₂ : EdgePath G u w
eqn : cons e✝ (cons e' p') = cons ph pt ++ cons e (cons (EdgeBetween.bar e) p₂)
⊢ False
Tactic:
let tred : ¬ reduced (cons e' p') :=
  tail_reducible_of_split eqn
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
hyp : reduced (cons e' p')
c' : ¬e' = EdgeBetween.bar e✝
p'' : EdgePath G u✝¹ w
red' : Reduction (cons e✝ (cons e' p')) p''
u✝ u' : V
p₁ : EdgePath G u✝¹ u✝
u w✝ : V
ph : EdgeBetween G u✝¹ w✝
pt : EdgePath G w✝ u
e : EdgeBetween G u u'
p₂ : EdgePath G u w
eqn : cons e✝ (cons e' p') = cons ph pt ++ cons e (cons (EdgeBetween.bar e) p₂)
tred : ¬reduced (cons e' p') := tail_reducible_of_split eqn
⊢ False
Theorem: Graph.reduced_redCons
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
hyp : reduced (cons e' p')
c' : ¬e' = EdgeBetween.bar e✝
p'' : EdgePath G u✝¹ w
red' : Reduction (cons e✝ (cons e' p')) p''
u✝ u' : V
p₁ : EdgePath G u✝¹ u✝
u w✝ : V
ph : EdgeBetween G u✝¹ w✝
pt : EdgePath G w✝ u
e : EdgeBetween G u u'
p₂ : EdgePath G u w
eqn : cons e✝ (cons e' p') = cons ph pt ++ cons e (cons (EdgeBetween.bar e) p₂)
tred : ¬reduced (cons e' p') := tail_reducible_of_split eqn
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Graph.reduced_redCons
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
hyp : reduced (cons e' p')
c : ¬w'' = u
⊢ reduced (redCons e (cons e' p'))
Tactic:
simp [redCons_cons_vertex_neq e e' 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 w'' : V
e' : EdgeBetween G v w''
p' : EdgePath G w'' w
hyp : reduced (cons e' p')
c : ¬w'' = u
⊢ reduced (cons e (cons e' p'))
Theorem: Graph.reduced_redCons
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
hyp : reduced (cons e' p')
c : ¬w'' = u
⊢ reduced (cons e (cons e' p'))
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 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
hyp : reduced (cons e' p')
c : ¬w'' = u
p'' : EdgePath G u w
red' : Reduction (cons e (cons e' p')) p''
⊢ False
Theorem: Graph.reduced_redCons
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
hyp : reduced (cons e' p')
c : ¬w'' = u
p'' : EdgePath G u w
red' : Reduction (cons e (cons e' p')) 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 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
hyp : reduced (cons e' p')
c : ¬w'' = u✝
p'' : EdgePath G u✝ w
red' : Reduction (cons e✝ (cons e' p')) p''
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G u✝ u
p₂ : EdgePath G u w
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (cons e' p')
⊢ False
Theorem: Graph.reduced_redCons
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
hyp : reduced (cons e' p')
c : ¬w'' = u✝
p'' : EdgePath G u✝ w
red' : Reduction (cons e✝ (cons e' p')) p''
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G u✝ u
p₂ : EdgePath G u w
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (cons e' p')
⊢ False
Tactic:
match p₁ with
    | nil _ =>
      rw [nil_append] at eqn
      let leqn := congrArg EdgePath.toList eqn
      simp [cons_toList, nil_toList, append_toList] at leqn
      rename_i u'' e''
      apply c
      rw [← e.init_eq, ← e'.term_eq, ← G.ι_bar, ← leqn.2.1, bar_bar]
    | cons ph pt =>
      symm at eqn
      let tred : ¬ reduced (cons e' p') :=
        tail_reducible_of_split eqn
      contradiction
Proof state after:
no goals
Theorem: Graph.reduced_redCons
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
hyp : reduced (cons e' p')
c : ¬w'' = u✝
p'' : EdgePath G u✝ w
red' : Reduction (cons e✝ (cons e' p')) p''
u u' : V
p₁ : EdgePath G u✝ u
e : EdgeBetween G u✝ u'
p₂ : EdgePath G u✝ w
eqn : nil u✝ ++ cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (cons e' p')
⊢ False
Tactic:
rw [nil_append] at eqn
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
hyp : reduced (cons e' p')
c : ¬w'' = u✝
p'' : EdgePath G u✝ w
red' : Reduction (cons e✝ (cons e' p')) p''
u u' : V
p₁ : EdgePath G u✝ u
e : EdgeBetween G u✝ u'
p₂ : EdgePath G u✝ w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (cons e' p')
⊢ False
Theorem: Graph.reduced_redCons
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
hyp : reduced (cons e' p')
c : ¬w'' = u✝
p'' : EdgePath G u✝ w
red' : Reduction (cons e✝ (cons e' p')) p''
u u' : V
p₁ : EdgePath G u✝ u
e : EdgeBetween G u✝ u'
p₂ : EdgePath G u✝ w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (cons e' p')
⊢ False
Tactic:
let leqn := congrArg EdgePath.toList eqn
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
hyp : reduced (cons e' p')
c : ¬w'' = u✝
p'' : EdgePath G u✝ w
red' : Reduction (cons e✝ (cons e' p')) p''
u u' : V
p₁ : EdgePath G u✝ u
e : EdgeBetween G u✝ u'
p₂ : EdgePath G u✝ w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (cons e' p')
leqn : toList (cons e (cons (EdgeBetween.bar e) p₂)) = toList (cons e✝ (cons e' p')) := congrArg toList eqn
⊢ False
Theorem: Graph.reduced_redCons
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
hyp : reduced (cons e' p')
c : ¬w'' = u✝
p'' : EdgePath G u✝ w
red' : Reduction (cons e✝ (cons e' p')) p''
u u' : V
p₁ : EdgePath G u✝ u
e : EdgeBetween G u✝ u'
p₂ : EdgePath G u✝ w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (cons e' p')
leqn : toList (cons e (cons (EdgeBetween.bar e) p₂)) = toList (cons e✝ (cons e' p')) := congrArg toList eqn
⊢ False
Tactic:
simp [cons_toList, nil_toList, append_toList] at leqn
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
hyp : reduced (cons e' p')
c : ¬w'' = u✝
p'' : EdgePath G u✝ w
red' : Reduction (cons e✝ (cons e' p')) p''
u u' : V
p₁ : EdgePath G u✝ u
e : EdgeBetween G u✝ u'
p₂ : EdgePath G u✝ w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (cons e' p')
leqn : e.edge = e✝.edge ∧ G.bar e.edge = e'.edge ∧ toList p₂ = toList p'
⊢ False
Theorem: Graph.reduced_redCons
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
hyp : reduced (cons e' p')
c : ¬w'' = u✝
p'' : EdgePath G u✝ w
red' : Reduction (cons e✝ (cons e' p')) p''
u u' : V
p₁ : EdgePath G u✝ u
e : EdgeBetween G u✝ u'
p₂ : EdgePath G u✝ w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (cons e' p')
leqn : e.edge = e✝.edge ∧ G.bar e.edge = e'.edge ∧ toList p₂ = toList p'
⊢ False
Tactic:
rename_i u'' e''
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
hyp : reduced (cons e' p')
c : ¬w'' = u''
p'' : EdgePath G u'' w
red' : Reduction (cons e'' (cons e' p')) p''
u u' : V
p₁ : EdgePath G u'' u
e : EdgeBetween G u'' u'
p₂ : EdgePath G u'' w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e'' (cons e' p')
leqn : e.edge = e''.edge ∧ G.bar e.edge = e'.edge ∧ toList p₂ = toList p'
⊢ False
Theorem: Graph.reduced_redCons
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
hyp : reduced (cons e' p')
c : ¬w'' = u''
p'' : EdgePath G u'' w
red' : Reduction (cons e'' (cons e' p')) p''
u u' : V
p₁ : EdgePath G u'' u
e : EdgeBetween G u'' u'
p₂ : EdgePath G u'' w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e'' (cons e' p')
leqn : e.edge = e''.edge ∧ G.bar e.edge = e'.edge ∧ toList p₂ = toList p'
⊢ False
Tactic:
apply 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 w'' : V
e' : EdgeBetween G v w''
p' : EdgePath G w'' w
hyp : reduced (cons e' p')
c : ¬w'' = u''
p'' : EdgePath G u'' w
red' : Reduction (cons e'' (cons e' p')) p''
u u' : V
p₁ : EdgePath G u'' u
e : EdgeBetween G u'' u'
p₂ : EdgePath G u'' w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e'' (cons e' p')
leqn : e.edge = e''.edge ∧ G.bar e.edge = e'.edge ∧ toList p₂ = toList p'
⊢ w'' = u''
Theorem: Graph.reduced_redCons
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
hyp : reduced (cons e' p')
c : ¬w'' = u''
p'' : EdgePath G u'' w
red' : Reduction (cons e'' (cons e' p')) p''
u u' : V
p₁ : EdgePath G u'' u
e : EdgeBetween G u'' u'
p₂ : EdgePath G u'' w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e'' (cons e' p')
leqn : e.edge = e''.edge ∧ G.bar e.edge = e'.edge ∧ toList p₂ = toList p'
⊢ w'' = u''
Tactic:
rw [← e.init_eq, ← e'.term_eq, ← G.ι_bar, ← leqn.2.1, bar_bar]
Proof state after:
no goals
Theorem: Graph.reduced_redCons
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
hyp : reduced (cons e' p')
c : ¬w'' = u✝¹
p'' : EdgePath G u✝¹ w
red' : Reduction (cons e✝ (cons e' p')) p''
u✝ u' : V
p₁ : EdgePath G u✝¹ u✝
u w✝ : V
ph : EdgeBetween G u✝¹ w✝
pt : EdgePath G w✝ u
e : EdgeBetween G u u'
p₂ : EdgePath G u w
eqn : cons ph pt ++ cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (cons e' p')
⊢ False
Tactic:
symm at eqn
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
hyp : reduced (cons e' p')
c : ¬w'' = u✝¹
p'' : EdgePath G u✝¹ w
red' : Reduction (cons e✝ (cons e' p')) p''
u✝ u' : V
p₁ : EdgePath G u✝¹ u✝
u w✝ : V
ph : EdgeBetween G u✝¹ w✝
pt : EdgePath G w✝ u
e : EdgeBetween G u u'
p₂ : EdgePath G u w
eqn : cons e✝ (cons e' p') = cons ph pt ++ cons e (cons (EdgeBetween.bar e) p₂)
⊢ False
Theorem: Graph.reduced_redCons
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
hyp : reduced (cons e' p')
c : ¬w'' = u✝¹
p'' : EdgePath G u✝¹ w
red' : Reduction (cons e✝ (cons e' p')) p''
u✝ u' : V
p₁ : EdgePath G u✝¹ u✝
u w✝ : V
ph : EdgeBetween G u✝¹ w✝
pt : EdgePath G w✝ u
e : EdgeBetween G u u'
p₂ : EdgePath G u w
eqn : cons e✝ (cons e' p') = cons ph pt ++ cons e (cons (EdgeBetween.bar e) p₂)
⊢ False
Tactic:
let tred : ¬ reduced (cons e' p') :=
  tail_reducible_of_split eqn
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
hyp : reduced (cons e' p')
c : ¬w'' = u✝¹
p'' : EdgePath G u✝¹ w
red' : Reduction (cons e✝ (cons e' p')) p''
u✝ u' : V
p₁ : EdgePath G u✝¹ u✝
u w✝ : V
ph : EdgeBetween G u✝¹ w✝
pt : EdgePath G w✝ u
e : EdgeBetween G u u'
p₂ : EdgePath G u w
eqn : cons e✝ (cons e' p') = cons ph pt ++ cons e (cons (EdgeBetween.bar e) p₂)
tred : ¬reduced (cons e' p') := tail_reducible_of_split eqn
⊢ False
Theorem: Graph.reduced_redCons
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
hyp : reduced (cons e' p')
c : ¬w'' = u✝¹
p'' : EdgePath G u✝¹ w
red' : Reduction (cons e✝ (cons e' p')) p''
u✝ u' : V
p₁ : EdgePath G u✝¹ u✝
u w✝ : V
ph : EdgeBetween G u✝¹ w✝
pt : EdgePath G w✝ u
e : EdgeBetween G u u'
p₂ : EdgePath G u w
eqn : cons e✝ (cons e' p') = cons ph pt ++ cons e (cons (EdgeBetween.bar e) p₂)
tred : ¬reduced (cons e' p') := tail_reducible_of_split eqn
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Graph.cancelling_steps_redCons
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
hyp : reduced p
⊢ redCons (EdgeBetween.bar e) (redCons e p) = p
Tactic:
cases prepend_cases e p with
| inl h =>
    rw [h]
    apply redCons_cons_edge_eq
    simp [bar_bar]
| inr h =>
    let ⟨t, h₁, h₂⟩ := h
    rw[h₂, h₁]
    cases prepend_cases e.bar t with
    | inl h' =>
      assumption
    | inr h' =>
      let ⟨t', h₁', h₂'⟩ := h'
      rw [h₂', h₁']
      rw [h₁, h₁'] at hyp
      simp [bar_bar] at *
      have split :
                cons e.bar (cons e t') =
                  (nil v : EdgePath G v v) ++
                    cons e.bar (cons e.bar.bar t') := by
                  simp [nil_append]
      have :¬ reduced (cons e.bar (cons e t')) := by
        apply not_reduced_of_split split
      contradiction
Proof state after:
no goals
Theorem: Graph.cancelling_steps_redCons
Proof state before:
case inl
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
hyp : reduced p
h : redCons e p = cons e p
⊢ redCons (EdgeBetween.bar e) (redCons e p) = p
Tactic:
rw [h]
Proof state after:
case inl
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
hyp : reduced p
h : redCons e p = cons e p
⊢ redCons (EdgeBetween.bar e) (cons e p) = p
Theorem: Graph.cancelling_steps_redCons
Proof state before:
case inl
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
hyp : reduced p
h : redCons e p = cons e p
⊢ redCons (EdgeBetween.bar e) (cons e p) = p
Tactic:
apply redCons_cons_edge_eq
Proof state after:
case inl.h
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
hyp : reduced p
h : redCons e p = cons e p
⊢ e = EdgeBetween.bar (EdgeBetween.bar e)
Theorem: Graph.cancelling_steps_redCons
Proof state before:
case inl.h
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
hyp : reduced p
h : redCons e p = cons e p
⊢ e = EdgeBetween.bar (EdgeBetween.bar e)
Tactic:
simp [bar_bar]
Proof state after:
no goals
Theorem: Graph.cancelling_steps_redCons
Proof state before:
case inr
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
hyp : reduced p
h : ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
⊢ redCons (EdgeBetween.bar e) (redCons e p) = p
Tactic:
let ⟨t, h₁, h₂⟩ := h
Proof state after:
case inr
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
hyp : reduced p
h : ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
⊢ redCons (EdgeBetween.bar e) (redCons e p) = p