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

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
⊢ List.concat start letter ∼ start :+ letter
Tactic:
if nilP: start = [] then
  simp [nilP, nil_nextVertex]
else
  if cancP:start.getLast nilP = letter⁻¹
  then
    simp [cancP, nonnil_nextVertex_cancel, nilP]
    let (a, b) := letter
    apply Quot.sound
    let sp := split_drop start nilP
    rw [cancP] at sp
    let step' := @Step.not _ start.dropLast ([]) a !b
    simp [Bool.not_not] at step'
    have : List.dropLast start ++ [(a, !b), (a, b)] = 
      start.dropLast ++ [(a, !b)] ++ [(a, b)] := by simp
    rw [inv_def] at sp
    rw [this, sp] at step'
    exact step'
  else
    simp [cancP, nonnil_nextVertex_extend, nilP]
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : start = []
⊢ List.concat start letter ∼ start :+ letter
Tactic:
simp [nilP, nil_nextVertex]
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
⊢ List.concat start letter ∼ start :+ letter
Tactic:
if cancP:start.getLast nilP = letter⁻¹
then
  simp [cancP, nonnil_nextVertex_cancel, nilP]
  let (a, b) := letter
  apply Quot.sound
  let sp := split_drop start nilP
  rw [cancP] at sp
  let step' := @Step.not _ start.dropLast ([]) a !b
  simp [Bool.not_not] at step'
  have : List.dropLast start ++ [(a, !b), (a, b)] = 
    start.dropLast ++ [(a, !b)] ++ [(a, b)] := by simp
  rw [inv_def] at sp
  rw [this, sp] at step'
  exact step'
else
  simp [cancP, nonnil_nextVertex_extend, nilP]
State after:
no goals

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

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

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
⊢ start ++ [(a, b)] ∼ List.dropLast start
Tactic:
apply Quot.sound
State after:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
⊢ Step (start ++ [(a, b)]) (List.dropLast start)

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

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

State before:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [(a, b)⁻¹] = start
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Tactic:
let step' := @Step.not _ start.dropLast ([]) a !b
State after:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [(a, b)⁻¹] = start
step' : Step (List.dropLast start ++ [(a, !b), (a, !!b)]) (List.dropLast start ++ []) := Step.not
⊢ Step (start ++ [(a, b)]) (List.dropLast start)

State before:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [(a, b)⁻¹] = start
step' : Step (List.dropLast start ++ [(a, !b), (a, !!b)]) (List.dropLast start ++ []) := Step.not
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Tactic:
simp [Bool.not_not] at step'
State after:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [(a, b)⁻¹] = start
step' : Step (List.dropLast start ++ [(a, !b), (a, b)]) (List.dropLast start)
⊢ Step (start ++ [(a, b)]) (List.dropLast start)

State before:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [(a, b)⁻¹] = start
step' : Step (List.dropLast start ++ [(a, !b), (a, b)]) (List.dropLast start)
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Tactic:
have : List.dropLast start ++ [(a, !b), (a, b)] = 
  start.dropLast ++ [(a, !b)] ++ [(a, b)] := by simp
State after:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [(a, b)⁻¹] = start
step' : Step (List.dropLast start ++ [(a, !b), (a, b)]) (List.dropLast start)
this : List.dropLast start ++ [(a, !b), (a, b)] = List.dropLast start ++ [(a, !b)] ++ [(a, b)]
⊢ Step (start ++ [(a, b)]) (List.dropLast start)

State before:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [(a, b)⁻¹] = start
step' : Step (List.dropLast start ++ [(a, !b), (a, b)]) (List.dropLast start)
this : List.dropLast start ++ [(a, !b), (a, b)] = List.dropLast start ++ [(a, !b)] ++ [(a, b)]
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Tactic:
rw [inv_def] at sp
State after:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [((a, b).1, !(a, b).2)] = start
step' : Step (List.dropLast start ++ [(a, !b), (a, b)]) (List.dropLast start)
this : List.dropLast start ++ [(a, !b), (a, b)] = List.dropLast start ++ [(a, !b)] ++ [(a, b)]
⊢ Step (start ++ [(a, b)]) (List.dropLast start)

State before:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [((a, b).1, !(a, b).2)] = start
step' : Step (List.dropLast start ++ [(a, !b), (a, b)]) (List.dropLast start)
this : List.dropLast start ++ [(a, !b), (a, b)] = List.dropLast start ++ [(a, !b)] ++ [(a, b)]
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Tactic:
rw [this, sp] at step'
State after:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [((a, b).1, !(a, b).2)] = start
step' : Step (start ++ [(a, b)]) (List.dropLast start)
this : List.dropLast start ++ [(a, !b), (a, b)] = List.dropLast start ++ [(a, !b)] ++ [(a, b)]
⊢ Step (start ++ [(a, b)]) (List.dropLast start)

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

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

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