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