internlm/Lean-Github huggingface dataset:
Theorem: FreeGroup.nextVertex_reduced
Proof 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
Proof 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
Theorem: FreeGroup.nextVertex_reduced
Proof 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
Proof state after:
no goals
Theorem: FreeGroup.nextVertex_reduced
Proof 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
Proof 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
Theorem: FreeGroup.nextVertex_reduced
Proof 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
Proof 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
Theorem: FreeGroup.nextVertex_reduced
Proof 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
Proof 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
Theorem: FreeGroup.nextVertex_reduced
Proof 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
Proof 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
Theorem: FreeGroup.nextVertex_reduced
Proof 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
Proof 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
Theorem: FreeGroup.nextVertex_reduced
Proof 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
Proof 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
Theorem: FreeGroup.nextVertex_reduced
Proof 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
Proof 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
Theorem: FreeGroup.nextVertex_reduced
Proof 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''
Proof 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
Theorem: FreeGroup.nextVertex_reduced
Proof 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
Proof 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
Theorem: FreeGroup.nextVertex_reduced
Proof 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''
Proof 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
Theorem: FreeGroup.nextVertex_reduced
Proof 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
Proof 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
Theorem: FreeGroup.nextVertex_reduced
Proof 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
Proof 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
Theorem: FreeGroup.nextVertex_reduced
Proof 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
Proof state after:
no goals
Theorem: FreeGroup.nextVertex_reduced
Proof 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
Proof state after:
no goals
Theorem: FreeGroup.nextVertex_reduced
Proof 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
Proof 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
Theorem: FreeGroup.nextVertex_reduced
Proof 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
Proof 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
Theorem: FreeGroup.nextVertex_reduced
Proof 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
Proof 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