Theorem: FreeGroup.homotopy_lifting_endpoints (Lectures/WordProblem/FreeGroup.lean)

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
⊢ Reduced start → start :+ (a, b) :+ (a, !b) = start
Tactic:
intro reduced_start
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
⊢ start :+ (a, b) :+ (a, !b) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
⊢ start :+ (a, b) :+ (a, !b) = start
Tactic:
if nilP: start = [] then
  simp [nilP, nextVertex, inv_def]
else 
  if cancP:start.getLast nilP = (a, b)⁻¹ 
  then 
    simp [cancP, nonnil_nextVertex_cancel, nilP]
    if nil' : start.dropLast = [] 
    then
      simp [nilP, nil', nil_nextVertex]
      let sp := split_drop start nilP
      rw [←sp, nil']
      simp
      simp [inv_def] at cancP
      rw [cancP]
    else
      if cancP':start.dropLast.getLast nil'  = (a, !b)⁻¹ 
      then
        let sp := split_drop start nilP
        let sp' := split_drop start.dropLast nil'
        rw [←sp', cancP', cancP] at sp
        simp [inv_def' a !b] at sp
        let L' := start.dropLast.dropLast
        have : 
          List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ (a, b) :: (a, !b) :: [] := by simp [inv_def]
        rw [this] at sp
        have step : Step start (L' ++ []) := by
          rw [← sp]
          show Step (L' ++ (a, b) :: (a, !b) :: []) (L' ++ [])
          apply Step.not
        apply False.elim
        apply reduced_start
        exact step
      else
        let res := 
          nonnil_nextVertex_extend start.dropLast nil' (a, !b) cancP'    
        rw [res]
        let sp := split_drop start nilP
        rw [cancP] at sp
        simp [inv_def] at cancP
        simp [inv_def] at sp 
        simp [sp]
  else
    have eqn : start :+ (a, b) = start.concat (a, b) := by 
      simp [nonnil_nextVertex_extend, cancP, nilP]
    have nn : start :+ (a, b) ≠ [] := by 
      simp [eqn]
    let cnc := 
      nonnil_nextVertex_cancel (start :+ (a, b)) nn (a, !b)
      (by 
        simp [inv_def, cancP, eqn]) 
    rw [cnc, eqn]
    simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : start = []
⊢ start :+ (a, b) :+ (a, !b) = start
Tactic:
simp [nilP, nextVertex, inv_def]
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
⊢ start :+ (a, b) :+ (a, !b) = start
Tactic:
if cancP:start.getLast nilP = (a, b)⁻¹ 
then 
  simp [cancP, nonnil_nextVertex_cancel, nilP]
  if nil' : start.dropLast = [] 
  then
    simp [nilP, nil', nil_nextVertex]
    let sp := split_drop start nilP
    rw [←sp, nil']
    simp
    simp [inv_def] at cancP
    rw [cancP]
  else
    if cancP':start.dropLast.getLast nil'  = (a, !b)⁻¹ 
    then
      let sp := split_drop start nilP
      let sp' := split_drop start.dropLast nil'
      rw [←sp', cancP', cancP] at sp
      simp [inv_def' a !b] at sp
      let L' := start.dropLast.dropLast
      have : 
        List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ (a, b) :: (a, !b) :: [] := by simp [inv_def]
      rw [this] at sp
      have step : Step start (L' ++ []) := by
        rw [← sp]
        show Step (L' ++ (a, b) :: (a, !b) :: []) (L' ++ [])
        apply Step.not
      apply False.elim
      apply reduced_start
      exact step
    else
      let res := 
        nonnil_nextVertex_extend start.dropLast nil' (a, !b) cancP'    
      rw [res]
      let sp := split_drop start nilP
      rw [cancP] at sp
      simp [inv_def] at cancP
      simp [inv_def] at sp 
      simp [sp]
else
  have eqn : start :+ (a, b) = start.concat (a, b) := by 
    simp [nonnil_nextVertex_extend, cancP, nilP]
  have nn : start :+ (a, b) ≠ [] := by 
    simp [eqn]
  let cnc := 
    nonnil_nextVertex_cancel (start :+ (a, b)) nn (a, !b)
    (by 
      simp [inv_def, cancP, eqn]) 
  rw [cnc, eqn]
  simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
⊢ start :+ (a, b) :+ (a, !b) = start
Tactic:
simp [cancP, nonnil_nextVertex_cancel, nilP]
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
⊢ List.dropLast start :+ (a, !b) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
if nil' : start.dropLast = [] 
then
  simp [nilP, nil', nil_nextVertex]
  let sp := split_drop start nilP
  rw [←sp, nil']
  simp
  simp [inv_def] at cancP
  rw [cancP]
else
  if cancP':start.dropLast.getLast nil'  = (a, !b)⁻¹ 
  then
    let sp := split_drop start nilP
    let sp' := split_drop start.dropLast nil'
    rw [←sp', cancP', cancP] at sp
    simp [inv_def' a !b] at sp
    let L' := start.dropLast.dropLast
    have : 
      List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ (a, b) :: (a, !b) :: [] := by simp [inv_def]
    rw [this] at sp
    have step : Step start (L' ++ []) := by
      rw [← sp]
      show Step (L' ++ (a, b) :: (a, !b) :: []) (L' ++ [])
      apply Step.not
    apply False.elim
    apply reduced_start
    exact step
  else
    let res := 
      nonnil_nextVertex_extend start.dropLast nil' (a, !b) cancP'    
    rw [res]
    let sp := split_drop start nilP
    rw [cancP] at sp
    simp [inv_def] at cancP
    simp [inv_def] at sp 
    simp [sp]
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : List.dropLast start = []
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
simp [nilP, nil', nil_nextVertex]
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : List.dropLast start = []
⊢ [(a, !b)] = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : List.dropLast start = []
⊢ [(a, !b)] = start
Tactic:
let sp := split_drop start nilP
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : List.dropLast start = []
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ [(a, !b)] = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : List.dropLast start = []
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ [(a, !b)] = start
Tactic:
rw [←sp, nil']
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : List.dropLast start = []
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ [(a, !b)] = [] ++ [List.getLast start nilP]

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : List.dropLast start = []
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ [(a, !b)] = [] ++ [List.getLast start nilP]
Tactic:
simp
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : List.dropLast start = []
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ (a, !b) = List.getLast start nilP

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : List.dropLast start = []
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ (a, !b) = List.getLast start nilP
Tactic:
simp [inv_def] at cancP
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, !b)
nil' : List.dropLast start = []
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ (a, !b) = List.getLast start nilP

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, !b)
nil' : List.dropLast start = []
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ (a, !b) = List.getLast start nilP
Tactic:
rw [cancP]
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
if cancP':start.dropLast.getLast nil'  = (a, !b)⁻¹ 
then
  let sp := split_drop start nilP
  let sp' := split_drop start.dropLast nil'
  rw [←sp', cancP', cancP] at sp
  simp [inv_def' a !b] at sp
  let L' := start.dropLast.dropLast
  have : 
    List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ (a, b) :: (a, !b) :: [] := by simp [inv_def]
  rw [this] at sp
  have step : Step start (L' ++ []) := by
    rw [← sp]
    show Step (L' ++ (a, b) :: (a, !b) :: []) (L' ++ [])
    apply Step.not
  apply False.elim
  apply reduced_start
  exact step
else
  let res := 
    nonnil_nextVertex_extend start.dropLast nil' (a, !b) cancP'    
  rw [res]
  let sp := split_drop start nilP
  rw [cancP] at sp
  simp [inv_def] at cancP
  simp [inv_def] at sp 
  simp [sp]
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
let sp := split_drop start nilP
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ List.dropLast start :+ (a, !b) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
let sp' := split_drop start.dropLast nil'
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
⊢ List.dropLast start :+ (a, !b) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
rw [←sp', cancP', cancP] at sp
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp : List.dropLast (List.dropLast start) ++ [(a, !b)⁻¹] ++ [(a, b)⁻¹] = start
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
⊢ List.dropLast start :+ (a, !b) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp : List.dropLast (List.dropLast start) ++ [(a, !b)⁻¹] ++ [(a, b)⁻¹] = start
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
simp [inv_def' a !b] at sp
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
sp : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = start
⊢ List.dropLast start :+ (a, !b) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
sp : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = start
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
let L' := start.dropLast.dropLast
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
sp : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = start
L' : List (α × Bool) := List.dropLast (List.dropLast start)
⊢ List.dropLast start :+ (a, !b) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
sp : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = start
L' : List (α × Bool) := List.dropLast (List.dropLast start)
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
have : 
  List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ (a, b) :: (a, !b) :: [] := by simp [inv_def]
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
sp : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = start
L' : List (α × Bool) := List.dropLast (List.dropLast start)
this : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ [(a, b), (a, !b)]
⊢ List.dropLast start :+ (a, !b) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
sp : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = start
L' : List (α × Bool) := List.dropLast (List.dropLast start)
this : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ [(a, b), (a, !b)]
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
rw [this] at sp
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
L' : List (α × Bool) := List.dropLast (List.dropLast start)
sp : L' ++ [(a, b), (a, !b)] = start
this : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ [(a, b), (a, !b)]
⊢ List.dropLast start :+ (a, !b) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
L' : List (α × Bool) := List.dropLast (List.dropLast start)
sp : L' ++ [(a, b), (a, !b)] = start
this : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ [(a, b), (a, !b)]
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
have step : Step start (L' ++ []) := by
  rw [← sp]
  show Step (L' ++ (a, b) :: (a, !b) :: []) (L' ++ [])
  apply Step.not
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
L' : List (α × Bool) := List.dropLast (List.dropLast start)
sp : L' ++ [(a, b), (a, !b)] = start
this : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ [(a, b), (a, !b)]
step : Step start (L' ++ [])
⊢ List.dropLast start :+ (a, !b) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
L' : List (α × Bool) := List.dropLast (List.dropLast start)
sp : L' ++ [(a, b), (a, !b)] = start
this : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ [(a, b), (a, !b)]
step : Step start (L' ++ [])
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
apply False.elim
State after:
case h
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
L' : List (α × Bool) := List.dropLast (List.dropLast start)
sp : L' ++ [(a, b), (a, !b)] = start
this : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ [(a, b), (a, !b)]
step : Step start (L' ++ [])
⊢ False

State before:
case h
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
L' : List (α × Bool) := List.dropLast (List.dropLast start)
sp : L' ++ [(a, b), (a, !b)] = start
this : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ [(a, b), (a, !b)]
step : Step start (L' ++ [])
⊢ False
Tactic:
apply reduced_start
State after:
case h.a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
L' : List (α × Bool) := List.dropLast (List.dropLast start)
sp : L' ++ [(a, b), (a, !b)] = start
this : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ [(a, b), (a, !b)]
step : Step start (L' ++ [])
⊢ Step start ?h.L'

case h.L'
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
L' : List (α × Bool) := List.dropLast (List.dropLast start)
sp : L' ++ [(a, b), (a, !b)] = start
this : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ [(a, b), (a, !b)]
step : Step start (L' ++ [])
⊢ List (α × Bool)

State before:
case h.a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
L' : List (α × Bool) := List.dropLast (List.dropLast start)
sp : L' ++ [(a, b), (a, !b)] = start
this : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ [(a, b), (a, !b)]
step : Step start (L' ++ [])
⊢ Step start ?h.L'

case h.L'
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
L' : List (α × Bool) := List.dropLast (List.dropLast start)
sp : L' ++ [(a, b), (a, !b)] = start
this : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ [(a, b), (a, !b)]
step : Step start (L' ++ [])
⊢ List (α × Bool)
Tactic:
exact step
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
sp : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = start
L' : List (α × Bool) := List.dropLast (List.dropLast start)
⊢ List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ [(a, b), (a, !b)]
Tactic:
simp [inv_def]
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
L' : List (α × Bool) := List.dropLast (List.dropLast start)
sp : L' ++ [(a, b), (a, !b)] = start
this : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ [(a, b), (a, !b)]
⊢ Step start (L' ++ [])
Tactic:
rw [← sp]
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
L' : List (α × Bool) := List.dropLast (List.dropLast start)
sp : L' ++ [(a, b), (a, !b)] = start
this : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ [(a, b), (a, !b)]
⊢ Step (L' ++ [(a, b), (a, !b)]) (L' ++ [])

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
L' : List (α × Bool) := List.dropLast (List.dropLast start)
sp : L' ++ [(a, b), (a, !b)] = start
this : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ [(a, b), (a, !b)]
⊢ Step (L' ++ [(a, b), (a, !b)]) (L' ++ [])
Tactic:
apply Step.not
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : ¬List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
let res := 
  nonnil_nextVertex_extend start.dropLast nil' (a, !b) cancP'
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : ¬List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
res : List.dropLast start :+ (a, !b) = List.concat (List.dropLast start) (a, !b) :=
  nonnil_nextVertex_extend (List.dropLast start) nil' (a, !b) cancP'
⊢ List.dropLast start :+ (a, !b) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : ¬List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
res : List.dropLast start :+ (a, !b) = List.concat (List.dropLast start) (a, !b) :=
  nonnil_nextVertex_extend (List.dropLast start) nil' (a, !b) cancP'
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
rw [res]
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : ¬List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
res : List.dropLast start :+ (a, !b) = List.concat (List.dropLast start) (a, !b) :=
  nonnil_nextVertex_extend (List.dropLast start) nil' (a, !b) cancP'
⊢ List.concat (List.dropLast start) (a, !b) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : ¬List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
res : List.dropLast start :+ (a, !b) = List.concat (List.dropLast start) (a, !b) :=
  nonnil_nextVertex_extend (List.dropLast start) nil' (a, !b) cancP'
⊢ List.concat (List.dropLast start) (a, !b) = start
Tactic:
let sp := split_drop start nilP
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : ¬List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
res : List.dropLast start :+ (a, !b) = List.concat (List.dropLast start) (a, !b) :=
  nonnil_nextVertex_extend (List.dropLast start) nil' (a, !b) cancP'
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ List.concat (List.dropLast start) (a, !b) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : ¬List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
res : List.dropLast start :+ (a, !b) = List.concat (List.dropLast start) (a, !b) :=
  nonnil_nextVertex_extend (List.dropLast start) nil' (a, !b) cancP'
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ List.concat (List.dropLast start) (a, !b) = start
Tactic:
rw [cancP] at sp
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : ¬List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
res : List.dropLast start :+ (a, !b) = List.concat (List.dropLast start) (a, !b) :=
  nonnil_nextVertex_extend (List.dropLast start) nil' (a, !b) cancP'
sp : List.dropLast start ++ [(a, b)⁻¹] = start
⊢ List.concat (List.dropLast start) (a, !b) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : ¬List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
res : List.dropLast start :+ (a, !b) = List.concat (List.dropLast start) (a, !b) :=
  nonnil_nextVertex_extend (List.dropLast start) nil' (a, !b) cancP'
sp : List.dropLast start ++ [(a, b)⁻¹] = start
⊢ List.concat (List.dropLast start) (a, !b) = start
Tactic:
simp [inv_def] at cancP
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, !b)
nil' : ¬List.dropLast start = []
cancP' : ¬List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
res : List.dropLast start :+ (a, !b) = List.concat (List.dropLast start) (a, !b) :=
  nonnil_nextVertex_extend (List.dropLast start) nil' (a, !b) cancP'
sp : List.dropLast start ++ [(a, b)⁻¹] = start
⊢ List.concat (List.dropLast start) (a, !b) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, !b)
nil' : ¬List.dropLast start = []
cancP' : ¬List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
res : List.dropLast start :+ (a, !b) = List.concat (List.dropLast start) (a, !b) :=
  nonnil_nextVertex_extend (List.dropLast start) nil' (a, !b) cancP'
sp : List.dropLast start ++ [(a, b)⁻¹] = start
⊢ List.concat (List.dropLast start) (a, !b) = start
Tactic:
simp [inv_def] at sp
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, !b)
nil' : ¬List.dropLast start = []
cancP' : ¬List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
res : List.dropLast start :+ (a, !b) = List.concat (List.dropLast start) (a, !b) :=
  nonnil_nextVertex_extend (List.dropLast start) nil' (a, !b) cancP'
sp : List.dropLast start ++ [(a, !b)] = start
⊢ List.concat (List.dropLast start) (a, !b) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, !b)
nil' : ¬List.dropLast start = []
cancP' : ¬List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
res : List.dropLast start :+ (a, !b) = List.concat (List.dropLast start) (a, !b) :=
  nonnil_nextVertex_extend (List.dropLast start) nil' (a, !b) cancP'
sp : List.dropLast start ++ [(a, !b)] = start
⊢ List.concat (List.dropLast start) (a, !b) = start
Tactic:
simp [sp]
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : ¬List.getLast start nilP = (a, b)⁻¹
⊢ start :+ (a, b) :+ (a, !b) = start
Tactic:
have eqn : start :+ (a, b) = start.concat (a, b) := by 
  simp [nonnil_nextVertex_extend, cancP, nilP]
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : ¬List.getLast start nilP = (a, b)⁻¹
eqn : start :+ (a, b) = List.concat start (a, b)
⊢ start :+ (a, b) :+ (a, !b) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : ¬List.getLast start nilP = (a, b)⁻¹
eqn : start :+ (a, b) = List.concat start (a, b)
⊢ start :+ (a, b) :+ (a, !b) = start
Tactic:
have nn : start :+ (a, b) ≠ [] := by 
  simp [eqn]
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : ¬List.getLast start nilP = (a, b)⁻¹
eqn : start :+ (a, b) = List.concat start (a, b)
nn : start :+ (a, b) ≠ []
⊢ start :+ (a, b) :+ (a, !b) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : ¬List.getLast start nilP = (a, b)⁻¹
eqn : start :+ (a, b) = List.concat start (a, b)
nn : start :+ (a, b) ≠ []
⊢ start :+ (a, b) :+ (a, !b) = start
Tactic:
let cnc := 
  nonnil_nextVertex_cancel (start :+ (a, b)) nn (a, !b)
  (by 
    simp [inv_def, cancP, eqn])
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : ¬List.getLast start nilP = (a, b)⁻¹
eqn : start :+ (a, b) = List.concat start (a, b)
nn : start :+ (a, b) ≠ []
cnc : start :+ (a, b) :+ (a, !b) = List.dropLast (start :+ (a, b)) :=
  nonnil_nextVertex_cancel (start :+ (a, b)) nn (a, !b)
    (of_eq_true
      ((congr
            (congrArg Eq
              (((fun {α} as as_1 e_as =>
                      Eq.rec (motive := fun as_2 e_as =>
                        ∀ (a : as ≠ []), List.getLast as a = List.getLast as_2 (e_as ▸ a))
                        (fun a => Eq.refl (List.getLast as a)) e_as)
                    (start :+ (a, b)) (start ++ [(a, b)]) (eqn.trans (List.concat_eq_append start (a, b))) nn).trans
                (List.getLast_append start (eqn.trans (List.concat_eq_append start (a, b)) ▸ nn))))
            (congrArg (Prod.mk a) (Bool.not_not b))).trans
        (eq_self (a, b))))
⊢ start :+ (a, b) :+ (a, !b) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : ¬List.getLast start nilP = (a, b)⁻¹
eqn : start :+ (a, b) = List.concat start (a, b)
nn : start :+ (a, b) ≠ []
cnc : start :+ (a, b) :+ (a, !b) = List.dropLast (start :+ (a, b)) :=
  nonnil_nextVertex_cancel (start :+ (a, b)) nn (a, !b)
    (of_eq_true
      ((congr
            (congrArg Eq
              (((fun {α} as as_1 e_as =>
                      Eq.rec (motive := fun as_2 e_as =>
                        ∀ (a : as ≠ []), List.getLast as a = List.getLast as_2 (e_as ▸ a))
                        (fun a => Eq.refl (List.getLast as a)) e_as)
                    (start :+ (a, b)) (start ++ [(a, b)]) (eqn.trans (List.concat_eq_append start (a, b))) nn).trans
                (List.getLast_append start (eqn.trans (List.concat_eq_append start (a, b)) ▸ nn))))
            (congrArg (Prod.mk a) (Bool.not_not b))).trans
        (eq_self (a, b))))
⊢ start :+ (a, b) :+ (a, !b) = start
Tactic:
rw [cnc, eqn]
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : ¬List.getLast start nilP = (a, b)⁻¹
eqn : start :+ (a, b) = List.concat start (a, b)
nn : start :+ (a, b) ≠ []
cnc : start :+ (a, b) :+ (a, !b) = List.dropLast (start :+ (a, b)) :=
  nonnil_nextVertex_cancel (start :+ (a, b)) nn (a, !b)
    (of_eq_true
      ((congr
            (congrArg Eq
              (((fun {α} as as_1 e_as =>
                      Eq.rec (motive := fun as_2 e_as =>
                        ∀ (a : as ≠ []), List.getLast as a = List.getLast as_2 (e_as ▸ a))
                        (fun a => Eq.refl (List.getLast as a)) e_as)
                    (start :+ (a, b)) (start ++ [(a, b)]) (eqn.trans (List.concat_eq_append start (a, b))) nn).trans
                (List.getLast_append start (eqn.trans (List.concat_eq_append start (a, b)) ▸ nn))))
            (congrArg (Prod.mk a) (Bool.not_not b))).trans
        (eq_self (a, b))))
⊢ List.dropLast (List.concat start (a, b)) = start

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : ¬List.getLast start nilP = (a, b)⁻¹
eqn : start :+ (a, b) = List.concat start (a, b)
nn : start :+ (a, b) ≠ []
cnc : start :+ (a, b) :+ (a, !b) = List.dropLast (start :+ (a, b)) :=
  nonnil_nextVertex_cancel (start :+ (a, b)) nn (a, !b)
    (of_eq_true
      ((congr
            (congrArg Eq
              (((fun {α} as as_1 e_as =>
                      Eq.rec (motive := fun as_2 e_as =>
                        ∀ (a : as ≠ []), List.getLast as a = List.getLast as_2 (e_as ▸ a))
                        (fun a => Eq.refl (List.getLast as a)) e_as)
                    (start :+ (a, b)) (start ++ [(a, b)]) (eqn.trans (List.concat_eq_append start (a, b))) nn).trans
                (List.getLast_append start (eqn.trans (List.concat_eq_append start (a, b)) ▸ nn))))
            (congrArg (Prod.mk a) (Bool.not_not b))).trans
        (eq_self (a, b))))
⊢ List.dropLast (List.concat start (a, b)) = start
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : ¬List.getLast start nilP = (a, b)⁻¹
⊢ start :+ (a, b) = List.concat start (a, b)
Tactic:
simp [nonnil_nextVertex_extend, cancP, nilP]
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : ¬List.getLast start nilP = (a, b)⁻¹
eqn : start :+ (a, b) = List.concat start (a, b)
⊢ start :+ (a, b) ≠ []
Tactic:
simp [eqn]
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : ¬List.getLast start nilP = (a, b)⁻¹
eqn : start :+ (a, b) = List.concat start (a, b)
nn : start :+ (a, b) ≠ []
⊢ List.getLast (start :+ (a, b)) nn = (a, !b)⁻¹
Tactic:
simp [inv_def, cancP, eqn]
State after:
no goals