Theorem: Graph.reduced_redCons (GroupComp/Graph/ReducedPaths.lean)

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
State after:
no goals

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]
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))

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
State after:
no goals

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''
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'))

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
State after:
no goals

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
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'))

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
State after:
no goals

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']
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'

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'
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

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
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

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
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

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₂
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

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
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₂)

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
State after:
no goals

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']
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'))

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'
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

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
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

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
State after:
no goals

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
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

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
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

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
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

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''
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

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]
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

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
State after:
no goals

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
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

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]
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

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]
State after:
no goals

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
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

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
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

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
State after:
no goals

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]
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'))

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'
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

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
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

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
State after:
no goals

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
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

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
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

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
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

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''
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

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
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''

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]
State after:
no goals

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
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

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
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

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
State after:
no goals