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

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
⊢ Reduced start → Reduced (start :+ letter)
Tactic:
intro reduced_start
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
⊢ Reduced (start :+ letter)

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
⊢ Reduced (start :+ letter)
Tactic:
if nilP: start = [] 
then 
  simp [nil_nextVertex, nilP]
  apply reduced_singleton
else
  intro L' step
  let ⟨x, b, L₁, L₂, eqs⟩ := exists_of_step step
  let eq1 := eqs.1
  if cancP:start.getLast nilP = letter⁻¹ 
  then 
    simp [cancP, nilP, nonnil_nextVertex_cancel] at eq1
    have eq1' : start.dropLast.concat (start.getLast nilP) = 
        (L₁ ++ (x, b) :: (x, !b) :: L₂).concat (start.getLast nilP) :=
      by rw [eq1]
    simp [split_drop, nilP] at eq1'
    let L₂' := L₂ ++ [start.getLast nilP]
    apply reduced_start (L₁ ++ L₂')
    rw [eq1']
    apply Step.not
  else 
    simp [cancP, nilP, nonnil_nextVertex_extend] at eq1
    if endP : L₂ = [] 
    then
      simp [endP] at eq1
      rw [←List.concat_eq_append] at eq1
      have : L₁ ++ [(x, b), (x, !b)] = 
        (L₁ ++ [(x, b)]).concat (x, !b) := by simp
      rw [this] at eq1
      let eq1' := List.of_concat_eq_concat eq1
      let eq1'' := eq1'.1
      let sp := split_drop start nilP
      rw [← sp, ←List.concat_eq_append, ←List.concat_eq_append] at eq1''
      let eq1''' := eq1'.2
      let eq2' := List.of_concat_eq_concat eq1''
      let _eq2'' := eq2'.2
      rw [eq1''', _eq2''] at cancP
      simp [inv_def] at cancP
    else
      rw [← split_drop L₂ endP] at eq1
      rw [← List.cons_append, ← List.cons_append, 
        ← List.append_assoc, ← List.concat_eq_append,
        ← List.concat_eq_append] at eq1
      let eq1' := List.of_concat_eq_concat eq1
      let eq1'' := eq1'.1
      apply reduced_start (L₁ ++ L₂.dropLast)
      rw [eq1'']
      apply Step.not
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : start = []
⊢ Reduced (start :+ letter)
Tactic:
simp [nil_nextVertex, nilP]
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : start = []
⊢ Reduced [letter]

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : start = []
⊢ Reduced [letter]
Tactic:
apply reduced_singleton
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
⊢ Reduced (start :+ letter)
Tactic:
intro L' step
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
⊢ False
Tactic:
let ⟨x, b, L₁, L₂, eqs⟩ := exists_of_step step
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
⊢ False
Tactic:
let eq1 := eqs.1
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
eq1 : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ := eqs.left
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
eq1 : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ := eqs.left
⊢ False
Tactic:
if cancP:start.getLast nilP = letter⁻¹ 
then 
  simp [cancP, nilP, nonnil_nextVertex_cancel] at eq1
  have eq1' : start.dropLast.concat (start.getLast nilP) = 
      (L₁ ++ (x, b) :: (x, !b) :: L₂).concat (start.getLast nilP) :=
    by rw [eq1]
  simp [split_drop, nilP] at eq1'
  let L₂' := L₂ ++ [start.getLast nilP]
  apply reduced_start (L₁ ++ L₂')
  rw [eq1']
  apply Step.not
else 
  simp [cancP, nilP, nonnil_nextVertex_extend] at eq1
  if endP : L₂ = [] 
  then
    simp [endP] at eq1
    rw [←List.concat_eq_append] at eq1
    have : L₁ ++ [(x, b), (x, !b)] = 
      (L₁ ++ [(x, b)]).concat (x, !b) := by simp
    rw [this] at eq1
    let eq1' := List.of_concat_eq_concat eq1
    let eq1'' := eq1'.1
    let sp := split_drop start nilP
    rw [← sp, ←List.concat_eq_append, ←List.concat_eq_append] at eq1''
    let eq1''' := eq1'.2
    let eq2' := List.of_concat_eq_concat eq1''
    let _eq2'' := eq2'.2
    rw [eq1''', _eq2''] at cancP
    simp [inv_def] at cancP
  else
    rw [← split_drop L₂ endP] at eq1
    rw [← List.cons_append, ← List.cons_append, 
      ← List.append_assoc, ← List.concat_eq_append,
      ← List.concat_eq_append] at eq1
    let eq1' := List.of_concat_eq_concat eq1
    let eq1'' := eq1'.1
    apply reduced_start (L₁ ++ L₂.dropLast)
    rw [eq1'']
    apply Step.not
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
eq1 : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ := eqs.left
cancP : List.getLast start nilP = letter⁻¹
⊢ False
Tactic:
simp [cancP, nilP, nonnil_nextVertex_cancel] at eq1
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
⊢ False
Tactic:
have eq1' : start.dropLast.concat (start.getLast nilP) = 
    (L₁ ++ (x, b) :: (x, !b) :: L₂).concat (start.getLast nilP) :=
  by rw [eq1]
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' :
  List.concat (List.dropLast start) (List.getLast start nilP) =
    List.concat (L₁ ++ (x, b) :: (x, !b) :: L₂) (List.getLast start nilP)
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' :
  List.concat (List.dropLast start) (List.getLast start nilP) =
    List.concat (L₁ ++ (x, b) :: (x, !b) :: L₂) (List.getLast start nilP)
⊢ False
Tactic:
simp [split_drop, nilP] at eq1'
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])
⊢ False
Tactic:
let L₂' := L₂ ++ [start.getLast nilP]
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])
L₂' : List (α × Bool) := L₂ ++ [List.getLast start nilP]
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])
L₂' : List (α × Bool) := L₂ ++ [List.getLast start nilP]
⊢ False
Tactic:
apply reduced_start (L₁ ++ L₂')
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])
L₂' : List (α × Bool) := L₂ ++ [List.getLast start nilP]
⊢ Step start (L₁ ++ L₂')

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])
L₂' : List (α × Bool) := L₂ ++ [List.getLast start nilP]
⊢ Step start (L₁ ++ L₂')
Tactic:
rw [eq1']
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])
L₂' : List (α × Bool) := L₂ ++ [List.getLast start nilP]
⊢ Step (L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])) (L₁ ++ L₂')

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])
L₂' : List (α × Bool) := L₂ ++ [List.getLast start nilP]
⊢ Step (L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])) (L₁ ++ L₂')
Tactic:
apply Step.not
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
⊢ List.concat (List.dropLast start) (List.getLast start nilP) =
    List.concat (L₁ ++ (x, b) :: (x, !b) :: L₂) (List.getLast start nilP)
Tactic:
rw [eq1]
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
eq1 : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ := eqs.left
cancP : ¬List.getLast start nilP = letter⁻¹
⊢ False
Tactic:
simp [cancP, nilP, nonnil_nextVertex_extend] at eq1
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
eq1 : start ++ [letter] = L₁ ++ (x, b) :: (x, !b) :: L₂
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
eq1 : start ++ [letter] = L₁ ++ (x, b) :: (x, !b) :: L₂
⊢ False
Tactic:
if endP : L₂ = [] 
then
  simp [endP] at eq1
  rw [←List.concat_eq_append] at eq1
  have : L₁ ++ [(x, b), (x, !b)] = 
    (L₁ ++ [(x, b)]).concat (x, !b) := by simp
  rw [this] at eq1
  let eq1' := List.of_concat_eq_concat eq1
  let eq1'' := eq1'.1
  let sp := split_drop start nilP
  rw [← sp, ←List.concat_eq_append, ←List.concat_eq_append] at eq1''
  let eq1''' := eq1'.2
  let eq2' := List.of_concat_eq_concat eq1''
  let _eq2'' := eq2'.2
  rw [eq1''', _eq2''] at cancP
  simp [inv_def] at cancP
else
  rw [← split_drop L₂ endP] at eq1
  rw [← List.cons_append, ← List.cons_append, 
    ← List.append_assoc, ← List.concat_eq_append,
    ← List.concat_eq_append] at eq1
  let eq1' := List.of_concat_eq_concat eq1
  let eq1'' := eq1'.1
  apply reduced_start (L₁ ++ L₂.dropLast)
  rw [eq1'']
  apply Step.not
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
eq1 : start ++ [letter] = L₁ ++ (x, b) :: (x, !b) :: L₂
endP : L₂ = []
⊢ False
Tactic:
simp [endP] at eq1
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : start ++ [letter] = L₁ ++ [(x, b), (x, !b)]
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : start ++ [letter] = L₁ ++ [(x, b), (x, !b)]
⊢ False
Tactic:
rw [←List.concat_eq_append] at eq1
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = L₁ ++ [(x, b), (x, !b)]
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = L₁ ++ [(x, b), (x, !b)]
⊢ False
Tactic:
have : L₁ ++ [(x, b), (x, !b)] = 
  (L₁ ++ [(x, b)]).concat (x, !b) := by simp
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = L₁ ++ [(x, b), (x, !b)]
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = L₁ ++ [(x, b), (x, !b)]
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
⊢ False
Tactic:
rw [this] at eq1
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
⊢ False
Tactic:
let eq1' := List.of_concat_eq_concat eq1
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
eq1' : start = L₁ ++ [(x, b)] ∧ letter = (x, !b) := List.of_concat_eq_concat eq1
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
eq1' : start = L₁ ++ [(x, b)] ∧ letter = (x, !b) := List.of_concat_eq_concat eq1
⊢ False
Tactic:
let eq1'' := eq1'.1
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
eq1' : start = L₁ ++ [(x, b)] ∧ letter = (x, !b) := List.of_concat_eq_concat eq1
eq1'' : start = L₁ ++ [(x, b)] := eq1'.left
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
eq1' : start = L₁ ++ [(x, b)] ∧ letter = (x, !b) := List.of_concat_eq_concat eq1
eq1'' : start = L₁ ++ [(x, b)] := eq1'.left
⊢ False
Tactic:
let sp := split_drop start nilP
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
eq1' : start = L₁ ++ [(x, b)] ∧ letter = (x, !b) := List.of_concat_eq_concat eq1
eq1'' : start = L₁ ++ [(x, b)] := eq1'.left
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
eq1' : start = L₁ ++ [(x, b)] ∧ letter = (x, !b) := List.of_concat_eq_concat eq1
eq1'' : start = L₁ ++ [(x, b)] := eq1'.left
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ False
Tactic:
rw [← sp, ←List.concat_eq_append, ←List.concat_eq_append] at eq1''
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
eq1' : start = L₁ ++ [(x, b)] ∧ letter = (x, !b) := List.of_concat_eq_concat eq1
eq1'' : List.concat (List.dropLast start) (List.getLast start nilP) = List.concat L₁ (x, b)
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
eq1' : start = L₁ ++ [(x, b)] ∧ letter = (x, !b) := List.of_concat_eq_concat eq1
eq1'' : List.concat (List.dropLast start) (List.getLast start nilP) = List.concat L₁ (x, b)
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ False
Tactic:
let eq1''' := eq1'.2
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
eq1' : start = L₁ ++ [(x, b)] ∧ letter = (x, !b) := List.of_concat_eq_concat eq1
eq1'' : List.concat (List.dropLast start) (List.getLast start nilP) = List.concat L₁ (x, b)
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
eq1''' : letter = (x, !b) := eq1'.right
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
eq1' : start = L₁ ++ [(x, b)] ∧ letter = (x, !b) := List.of_concat_eq_concat eq1
eq1'' : List.concat (List.dropLast start) (List.getLast start nilP) = List.concat L₁ (x, b)
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
eq1''' : letter = (x, !b) := eq1'.right
⊢ False
Tactic:
let eq2' := List.of_concat_eq_concat eq1''
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
eq1' : start = L₁ ++ [(x, b)] ∧ letter = (x, !b) := List.of_concat_eq_concat eq1
eq1'' : List.concat (List.dropLast start) (List.getLast start nilP) = List.concat L₁ (x, b)
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
eq1''' : letter = (x, !b) := eq1'.right
eq2' : List.dropLast start = L₁ ∧ List.getLast start nilP = (x, b) := List.of_concat_eq_concat eq1''
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
eq1' : start = L₁ ++ [(x, b)] ∧ letter = (x, !b) := List.of_concat_eq_concat eq1
eq1'' : List.concat (List.dropLast start) (List.getLast start nilP) = List.concat L₁ (x, b)
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
eq1''' : letter = (x, !b) := eq1'.right
eq2' : List.dropLast start = L₁ ∧ List.getLast start nilP = (x, b) := List.of_concat_eq_concat eq1''
⊢ False
Tactic:
let _eq2'' := eq2'.2
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
eq1' : start = L₁ ++ [(x, b)] ∧ letter = (x, !b) := List.of_concat_eq_concat eq1
eq1'' : List.concat (List.dropLast start) (List.getLast start nilP) = List.concat L₁ (x, b)
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
eq1''' : letter = (x, !b) := eq1'.right
eq2' : List.dropLast start = L₁ ∧ List.getLast start nilP = (x, b) := List.of_concat_eq_concat eq1''
_eq2'' : List.getLast start nilP = (x, b) := eq2'.right
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
eq1' : start = L₁ ++ [(x, b)] ∧ letter = (x, !b) := List.of_concat_eq_concat eq1
eq1'' : List.concat (List.dropLast start) (List.getLast start nilP) = List.concat L₁ (x, b)
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
eq1''' : letter = (x, !b) := eq1'.right
eq2' : List.dropLast start = L₁ ∧ List.getLast start nilP = (x, b) := List.of_concat_eq_concat eq1''
_eq2'' : List.getLast start nilP = (x, b) := eq2'.right
⊢ False
Tactic:
rw [eq1''', _eq2''] at cancP
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬(x, b) = (x, !b)⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
eq1' : start = L₁ ++ [(x, b)] ∧ letter = (x, !b) := List.of_concat_eq_concat eq1
eq1'' : List.concat (List.dropLast start) (List.getLast start nilP) = List.concat L₁ (x, b)
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
eq1''' : letter = (x, !b) := eq1'.right
eq2' : List.dropLast start = L₁ ∧ List.getLast start nilP = (x, b) := List.of_concat_eq_concat eq1''
_eq2'' : List.getLast start nilP = (x, b) := eq2'.right
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬(x, b) = (x, !b)⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
eq1' : start = L₁ ++ [(x, b)] ∧ letter = (x, !b) := List.of_concat_eq_concat eq1
eq1'' : List.concat (List.dropLast start) (List.getLast start nilP) = List.concat L₁ (x, b)
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
eq1''' : letter = (x, !b) := eq1'.right
eq2' : List.dropLast start = L₁ ∧ List.getLast start nilP = (x, b) := List.of_concat_eq_concat eq1''
_eq2'' : List.getLast start nilP = (x, b) := eq2'.right
⊢ False
Tactic:
simp [inv_def] at cancP
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : L₂ = []
eq1 : List.concat start letter = L₁ ++ [(x, b), (x, !b)]
⊢ L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
eq1 : start ++ [letter] = L₁ ++ (x, b) :: (x, !b) :: L₂
endP : ¬L₂ = []
⊢ False
Tactic:
rw [← split_drop L₂ endP] at eq1
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : ¬L₂ = []
eq1 : start ++ [letter] = L₁ ++ (x, b) :: (x, !b) :: (List.dropLast L₂ ++ [List.getLast L₂ endP])
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : ¬L₂ = []
eq1 : start ++ [letter] = L₁ ++ (x, b) :: (x, !b) :: (List.dropLast L₂ ++ [List.getLast L₂ endP])
⊢ False
Tactic:
rw [← List.cons_append, ← List.cons_append, 
  ← List.append_assoc, ← List.concat_eq_append,
  ← List.concat_eq_append] at eq1
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : ¬L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂) (List.getLast L₂ endP)
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : ¬L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂) (List.getLast L₂ endP)
⊢ False
Tactic:
let eq1' := List.of_concat_eq_concat eq1
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : ¬L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂) (List.getLast L₂ endP)
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂ ∧ letter = List.getLast L₂ endP :=
  List.of_concat_eq_concat eq1
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : ¬L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂) (List.getLast L₂ endP)
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂ ∧ letter = List.getLast L₂ endP :=
  List.of_concat_eq_concat eq1
⊢ False
Tactic:
let eq1'' := eq1'.1
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : ¬L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂) (List.getLast L₂ endP)
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂ ∧ letter = List.getLast L₂ endP :=
  List.of_concat_eq_concat eq1
eq1'' : start = L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂ := eq1'.left
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : ¬L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂) (List.getLast L₂ endP)
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂ ∧ letter = List.getLast L₂ endP :=
  List.of_concat_eq_concat eq1
eq1'' : start = L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂ := eq1'.left
⊢ False
Tactic:
apply reduced_start (L₁ ++ L₂.dropLast)
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : ¬L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂) (List.getLast L₂ endP)
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂ ∧ letter = List.getLast L₂ endP :=
  List.of_concat_eq_concat eq1
eq1'' : start = L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂ := eq1'.left
⊢ Step start (L₁ ++ List.dropLast L₂)

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : ¬L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂) (List.getLast L₂ endP)
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂ ∧ letter = List.getLast L₂ endP :=
  List.of_concat_eq_concat eq1
eq1'' : start = L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂ := eq1'.left
⊢ Step start (L₁ ++ List.dropLast L₂)
Tactic:
rw [eq1'']
State after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : ¬L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂) (List.getLast L₂ endP)
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂ ∧ letter = List.getLast L₂ endP :=
  List.of_concat_eq_concat eq1
eq1'' : start = L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂ := eq1'.left
⊢ Step (L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂) (L₁ ++ List.dropLast L₂)

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : ¬List.getLast start nilP = letter⁻¹
endP : ¬L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂) (List.getLast L₂ endP)
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂ ∧ letter = List.getLast L₂ endP :=
  List.of_concat_eq_concat eq1
eq1'' : start = L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂ := eq1'.left
⊢ Step (L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂) (L₁ ++ List.dropLast L₂)
Tactic:
apply Step.not
State after:
no goals