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

State before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
⊢ start ++ word ∼ finalVertex start word
Tactic:
match word with
| [] => simp [finalVertex]
| head ::tail => 
  simp [finalVertex, List.foldl_cons]
  let ih := finalVertex_homotopic_append (start :+ head) tail
  simp [finalVertex, List.foldl_cons] at ih
  let eqn := nextVertex_homotopic_concat start head
  show mk (start ++ head :: tail) = mk (List.foldl nextVertex (start :+ head) tail)
  rw [←ih]
  let eqn' := append_homotopic tail eqn
  simp [← eqn']
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
⊢ start ++ [] ∼ finalVertex start []
Tactic:
simp [finalVertex]
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
⊢ start ++ head :: tail ∼ finalVertex start (head :: tail)
Tactic:
simp [finalVertex, List.foldl_cons]
State after:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
⊢ start ++ head :: tail ∼ List.foldl nextVertex (start :+ head) tail

State before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
⊢ start ++ head :: tail ∼ List.foldl nextVertex (start :+ head) tail
Tactic:
let ih := finalVertex_homotopic_append (start :+ head) tail
State after:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ finalVertex (start :+ head) tail := finalVertex_homotopic_append (start :+ head) tail
⊢ start ++ head :: tail ∼ List.foldl nextVertex (start :+ head) tail

State before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ finalVertex (start :+ head) tail := finalVertex_homotopic_append (start :+ head) tail
⊢ start ++ head :: tail ∼ List.foldl nextVertex (start :+ head) tail
Tactic:
simp [finalVertex, List.foldl_cons] at ih
State after:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
⊢ start ++ head :: tail ∼ List.foldl nextVertex (start :+ head) tail

State before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
⊢ start ++ head :: tail ∼ List.foldl nextVertex (start :+ head) tail
Tactic:
let eqn := nextVertex_homotopic_concat start head
State after:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
eqn : List.concat start head ∼ start :+ head := nextVertex_homotopic_concat start head
⊢ start ++ head :: tail ∼ List.foldl nextVertex (start :+ head) tail

State before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
eqn : List.concat start head ∼ start :+ head := nextVertex_homotopic_concat start head
⊢ start ++ head :: tail ∼ List.foldl nextVertex (start :+ head) tail
Tactic:
show mk (start ++ head :: tail) = mk (List.foldl nextVertex (start :+ head) tail)
State after:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
eqn : List.concat start head ∼ start :+ head := nextVertex_homotopic_concat start head
⊢ mk (start ++ head :: tail) = mk (List.foldl nextVertex (start :+ head) tail)

State before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
eqn : List.concat start head ∼ start :+ head := nextVertex_homotopic_concat start head
⊢ mk (start ++ head :: tail) = mk (List.foldl nextVertex (start :+ head) tail)
Tactic:
rw [←ih]
State after:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
eqn : List.concat start head ∼ start :+ head := nextVertex_homotopic_concat start head
⊢ mk (start ++ head :: tail) = mk (start :+ head ++ tail)

State before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
eqn : List.concat start head ∼ start :+ head := nextVertex_homotopic_concat start head
⊢ mk (start ++ head :: tail) = mk (start :+ head ++ tail)
Tactic:
let eqn' := append_homotopic tail eqn
State after:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
eqn : List.concat start head ∼ start :+ head := nextVertex_homotopic_concat start head
eqn' : List.concat start head ++ tail ∼ start :+ head ++ tail := append_homotopic tail eqn
⊢ mk (start ++ head :: tail) = mk (start :+ head ++ tail)

State before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
eqn : List.concat start head ∼ start :+ head := nextVertex_homotopic_concat start head
eqn' : List.concat start head ++ tail ∼ start :+ head ++ tail := append_homotopic tail eqn
⊢ mk (start ++ head :: tail) = mk (start :+ head ++ tail)
Tactic:
simp [← eqn']
State after:
no goals