internlm/Lean-Github huggingface dataset:
Theorem: Graph.reduced_nil
Proof state before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u' : V
e : EdgeBetween G v u'
p₂ : EdgePath G v v
eqn : cons e (cons (EdgeBetween.bar e) p₂) = nil v
⊢ False
Tactic:
let leqn := congrArg EdgePath.toList eqn
Proof state after:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u' : V
e : EdgeBetween G v u'
p₂ : EdgePath G v v
eqn : cons e (cons (EdgeBetween.bar e) p₂) = nil v
leqn : toList (cons e (cons (EdgeBetween.bar e) p₂)) = toList (nil v) := congrArg toList eqn
⊢ False
Theorem: Graph.reduced_nil
Proof state before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u' : V
e : EdgeBetween G v u'
p₂ : EdgePath G v v
eqn : cons e (cons (EdgeBetween.bar e) p₂) = nil v
leqn : toList (cons e (cons (EdgeBetween.bar e) p₂)) = toList (nil v) := congrArg toList eqn
⊢ False
Tactic:
simp [cons_toList, nil_toList] at leqn
Proof state after:
no goals
Theorem: Graph.reduced_nil
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
w✝ : V
h : EdgeBetween G v w✝
t : EdgePath G w✝ u
eqn : cons h t ++ cons e (cons (EdgeBetween.bar e) p₂) = nil v
⊢ False
Tactic:
rw [cons_append] at eqn
Proof state after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
w✝ : V
h : EdgeBetween G v w✝
t : EdgePath G w✝ u
eqn : cons h (t ++ cons e (cons (EdgeBetween.bar e) p₂)) = nil v
⊢ False
Theorem: Graph.reduced_nil
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
w✝ : V
h : EdgeBetween G v w✝
t : EdgePath G w✝ u
eqn : cons h (t ++ cons e (cons (EdgeBetween.bar e) p₂)) = nil v
⊢ False
Tactic:
let leqn := congrArg EdgePath.toList eqn
Proof state after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
w✝ : V
h : EdgeBetween G v w✝
t : EdgePath G w✝ u
eqn : cons h (t ++ cons e (cons (EdgeBetween.bar e) p₂)) = nil v
leqn : toList (cons h (t ++ cons e (cons (EdgeBetween.bar e) p₂))) = toList (nil v) := congrArg toList eqn
⊢ False
Theorem: Graph.reduced_nil
Proof state before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
w✝ : V
h : EdgeBetween G v w✝
t : EdgePath G w✝ u
eqn : cons h (t ++ cons e (cons (EdgeBetween.bar e) p₂)) = nil v
leqn : toList (cons h (t ++ cons e (cons (EdgeBetween.bar e) p₂))) = toList (nil v) := congrArg toList eqn
⊢ False
Tactic:
simp [cons_toList, nil_toList, append_toList] at leqn
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
hyp : reduced p
⊢ reduced (redCons e p)
Tactic:
match p with
| nil _ =>
  simp [redCons_nil]
  apply reduced_singleton
| cons e' p' =>
  rename_i w' w''
  if c:w'' = u then
    cases c
    if c':e' = e.bar
      then
        simp [redCons_cons_edge_eq p' c']
        intro p'' red'
        let ⟨u, u', e, p₁, p₂, eqn⟩   := red'.property
        rw [←eqn, ← cons_append] at hyp
        let red := hyp <| cons e' p₁ ++ p₂
        apply red
        apply Reduction.step
      else
        simp [redCons_cons_edge_neq p' c']
        intro p'' red'
        let ⟨u, u', e, p₁, p₂, eqn⟩   := red'.property
        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 e''
          have : e' = e''.bar := by
            ext
            rw [EdgeBetween.bar_eq_bar]
            rw [← leqn.1, leqn.2.1]
          contradiction
        | cons ph pt =>
          symm at eqn
          let tred : ¬ reduced (cons e' p') :=
            tail_reducible_of_split eqn
          contradiction
  else
    simp [redCons_cons_vertex_neq e e' p' c]
    intro p'' red'
    let ⟨u, u', e, p₁, p₂, eqn⟩   := red'.property
    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
hyp : reduced (nil v)
⊢ reduced (redCons e (nil v))
Tactic:
simp [redCons_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 u v
p : EdgePath G v w
hyp : reduced (nil v)
⊢ reduced (cons e (nil v))
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
hyp : reduced (nil v)
⊢ reduced (cons e (nil v))
Tactic:
apply reduced_singleton
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')
⊢ reduced (redCons e (cons e' p'))
Tactic:
rename_i w' w''
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w' : V
e : EdgeBetween G u v
p : EdgePath G v w'
w w'' : V
e' : EdgeBetween G v w''
p' : EdgePath G w'' w
hyp : reduced (cons e' p')
⊢ reduced (redCons 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')
⊢ reduced (redCons e (cons e' p'))
Tactic:
if c:w'' = u then
  cases c
  if c':e' = e.bar
    then
      simp [redCons_cons_edge_eq p' c']
      intro p'' red'
      let ⟨u, u', e, p₁, p₂, eqn⟩   := red'.property
      rw [←eqn, ← cons_append] at hyp
      let red := hyp <| cons e' p₁ ++ p₂
      apply red
      apply Reduction.step
    else
      simp [redCons_cons_edge_neq p' c']
      intro p'' red'
      let ⟨u, u', e, p₁, p₂, eqn⟩   := red'.property
      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 e''
        have : e' = e''.bar := by
          ext
          rw [EdgeBetween.bar_eq_bar]
          rw [← leqn.1, leqn.2.1]
        contradiction
      | cons ph pt =>
        symm at eqn
        let tred : ¬ reduced (cons e' p') :=
          tail_reducible_of_split eqn
        contradiction
else
  simp [redCons_cons_vertex_neq e e' p' c]
  intro p'' red'
  let ⟨u, u', e, p₁, p₂, eqn⟩   := red'.property
  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
⊢ reduced (redCons e (cons e' p'))
Tactic:
cases c
Proof state after:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w' : V
e : EdgeBetween G u v
p : EdgePath G v w'
w : V
e' : EdgeBetween G v u
p' : EdgePath G u w
hyp : reduced (cons e' p')
⊢ reduced (redCons e (cons e' p'))
Theorem: Graph.reduced_redCons
Proof state before:
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w' : V
e : EdgeBetween G u v
p : EdgePath G v w'
w : V
e' : EdgeBetween G v u
p' : EdgePath G u w
hyp : reduced (cons e' p')
⊢ reduced (redCons e (cons e' p'))
Tactic:
if c':e' = e.bar
  then
    simp [redCons_cons_edge_eq p' c']
    intro p'' red'
    let ⟨u, u', e, p₁, p₂, eqn⟩   := red'.property
    rw [←eqn, ← cons_append] at hyp
    let red := hyp <| cons e' p₁ ++ p₂
    apply red
    apply Reduction.step
  else
    simp [redCons_cons_edge_neq p' c']
    intro p'' red'
    let ⟨u, u', e, p₁, p₂, eqn⟩   := red'.property
    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 e''
      have : e' = e''.bar := by
        ext
        rw [EdgeBetween.bar_eq_bar]
        rw [← leqn.1, leqn.2.1]
      contradiction
    | 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 : V
e' : EdgeBetween G v u
p' : EdgePath G u w
hyp : reduced (cons e' p')
c' : e' = EdgeBetween.bar e
⊢ reduced (redCons e (cons e' p'))
Tactic:
simp [redCons_cons_edge_eq p' c']
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w' : V
e : EdgeBetween G u v
p : EdgePath G v w'
w : V
e' : EdgeBetween G v u
p' : EdgePath G u w
hyp : reduced (cons e' p')
c' : e' = EdgeBetween.bar e
⊢ reduced 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 : V
e' : EdgeBetween G v u
p' : EdgePath G u w
hyp : reduced (cons e' p')
c' : e' = EdgeBetween.bar e
⊢ reduced 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 : 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 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 : 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 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 : 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 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₂) = 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 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₂) = p'
⊢ False
Tactic:
rw [←eqn, ← cons_append] at hyp
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v w' : V
e✝ : EdgeBetween G u✝ v
p : EdgePath G v w'
w : V
e' : EdgeBetween G v u✝
p' : EdgePath G u✝ w
c' : e' = EdgeBetween.bar e✝
p'' : EdgePath G u✝ w
red' : Reduction p' p''
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G u✝ u
p₂ : EdgePath G u w
hyp : reduced (cons e' p₁ ++ cons e (cons (EdgeBetween.bar e) p₂))
eqn : p₁ ++ cons e (cons (EdgeBetween.bar 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 : V
e' : EdgeBetween G v u✝
p' : EdgePath G u✝ w
c' : e' = EdgeBetween.bar e✝
p'' : EdgePath G u✝ w
red' : Reduction p' p''
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G u✝ u
p₂ : EdgePath G u w
hyp : reduced (cons e' p₁ ++ cons e (cons (EdgeBetween.bar e) p₂))
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = p'
⊢ False
Tactic:
let red := hyp <| cons e' 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 u✝ v
p : EdgePath G v w'
w : V
e' : EdgeBetween G v u✝
p' : EdgePath G u✝ w
c' : e' = EdgeBetween.bar e✝
p'' : EdgePath G u✝ w
red' : Reduction p' p''
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G u✝ u
p₂ : EdgePath G u w
hyp : reduced (cons e' p₁ ++ cons e (cons (EdgeBetween.bar e) p₂))
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = p'
red : ¬Reduction (cons e' p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (cons e' p₁ ++ p₂) := hyp (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 : V
e' : EdgeBetween G v u✝
p' : EdgePath G u✝ w
c' : e' = EdgeBetween.bar e✝
p'' : EdgePath G u✝ w
red' : Reduction p' p''
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G u✝ u
p₂ : EdgePath G u w
hyp : reduced (cons e' p₁ ++ cons e (cons (EdgeBetween.bar e) p₂))
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = p'
red : ¬Reduction (cons e' p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (cons e' p₁ ++ p₂) := hyp (cons e' 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 u✝ v
p : EdgePath G v w'
w : V
e' : EdgeBetween G v u✝
p' : EdgePath G u✝ w
c' : e' = EdgeBetween.bar e✝
p'' : EdgePath G u✝ w
red' : Reduction p' p''
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G u✝ u
p₂ : EdgePath G u w
hyp : reduced (cons e' p₁ ++ cons e (cons (EdgeBetween.bar e) p₂))
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = p'
red : ¬Reduction (cons e' p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (cons e' p₁ ++ p₂) := hyp (cons e' p₁ ++ p₂)
⊢ Reduction (cons e' p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (cons e' p₁ ++ 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 : V
e' : EdgeBetween G v u✝
p' : EdgePath G u✝ w
c' : e' = EdgeBetween.bar e✝
p'' : EdgePath G u✝ w
red' : Reduction p' p''
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G u✝ u
p₂ : EdgePath G u w
hyp : reduced (cons e' p₁ ++ cons e (cons (EdgeBetween.bar e) p₂))
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = p'
red : ¬Reduction (cons e' p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (cons e' p₁ ++ p₂) := hyp (cons e' p₁ ++ p₂)
⊢ Reduction (cons e' p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (cons e' p₁ ++ p₂)
Tactic:
apply Reduction.step
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
⊢ reduced (redCons e (cons e' p'))
Tactic:
simp [redCons_cons_edge_neq p' c']
Proof state after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w' : V
e : EdgeBetween G u v
p : EdgePath G v w'
w : V
e' : EdgeBetween G v u
p' : EdgePath G u w
hyp : reduced (cons e' p')
c' : ¬e' = EdgeBetween.bar e
⊢ 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 : V
e' : EdgeBetween G v u
p' : EdgePath G u w
hyp : reduced (cons e' p')
c' : ¬e' = EdgeBetween.bar e
⊢ 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 : 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''
⊢ 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''
⊢ 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 : 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
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 : 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
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 e''
  have : e' = e''.bar := by
    ext
    rw [EdgeBetween.bar_eq_bar]
    rw [← leqn.1, leqn.2.1]
  contradiction
| 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 : 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 : 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 : 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')
⊢ 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')
⊢ 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 : 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 : 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 : 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 : 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 : 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
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:
rename_i 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 : 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