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₂
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
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
eq1'' : start = L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂ := 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) :: 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)
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
eq1'' : start = L₁ ++ (x, b) :: (x, !b) :: List.dropLast L₂ := eq1'.left
⊢ Step start (L₁ ++ List.dropLast L₂)
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)
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'']
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
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₂)
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)
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
Proof state after:
no goals
Theorem: FreeGroup.homotopy_lifting_endpoints
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
⊢ Reduced start → start :+ (a, b) :+ (a, !b) = start
Tactic:
intro reduced_start
Proof state after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
⊢ 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
⊢ start :+ (a, b) :+ (a, !b) = start
Tactic:
if nilP: start = [] then
  simp [nilP, nextVertex, inv_def]
else 
  if cancP:start.getLast nilP = (a, b)⁻¹ 
  then 
    simp [cancP, nonnil_nextVertex_cancel, nilP]
    if nil' : start.dropLast = [] 
    then
      simp [nilP, nil', nil_nextVertex]
      let sp := split_drop start nilP
      rw [←sp, nil']
      simp
      simp [inv_def] at cancP
      rw [cancP]
    else
      if cancP':start.dropLast.getLast nil'  = (a, !b)⁻¹ 
      then
        let sp := split_drop start nilP
        let sp' := split_drop start.dropLast nil'
        rw [←sp', cancP', cancP] at sp
        simp [inv_def' a !b] at sp
        let L' := start.dropLast.dropLast
        have : 
          List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ (a, b) :: (a, !b) :: [] := by simp [inv_def]
        rw [this] at sp
        have step : Step start (L' ++ []) := by
          rw [← sp]
          show Step (L' ++ (a, b) :: (a, !b) :: []) (L' ++ [])
          apply Step.not
        apply False.elim
        apply reduced_start
        exact step
      else
        let res := 
          nonnil_nextVertex_extend start.dropLast nil' (a, !b) cancP'    
        rw [res]
        let sp := split_drop start nilP
        rw [cancP] at sp
        simp [inv_def] at cancP
        simp [inv_def] at sp 
        simp [sp]
  else
    have eqn : start :+ (a, b) = start.concat (a, b) := by 
      simp [nonnil_nextVertex_extend, cancP, nilP]
    have nn : start :+ (a, b) ≠ [] := by 
      simp [eqn]
    let cnc := 
      nonnil_nextVertex_cancel (start :+ (a, b)) nn (a, !b)
      (by 
        simp [inv_def, cancP, eqn]) 
    rw [cnc, eqn]
    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 = []
⊢ start :+ (a, b) :+ (a, !b) = start
Tactic:
simp [nilP, nextVertex, 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 = []
⊢ start :+ (a, b) :+ (a, !b) = start
Tactic:
if cancP:start.getLast nilP = (a, b)⁻¹ 
then 
  simp [cancP, nonnil_nextVertex_cancel, nilP]
  if nil' : start.dropLast = [] 
  then
    simp [nilP, nil', nil_nextVertex]
    let sp := split_drop start nilP
    rw [←sp, nil']
    simp
    simp [inv_def] at cancP
    rw [cancP]
  else
    if cancP':start.dropLast.getLast nil'  = (a, !b)⁻¹ 
    then
      let sp := split_drop start nilP
      let sp' := split_drop start.dropLast nil'
      rw [←sp', cancP', cancP] at sp
      simp [inv_def' a !b] at sp
      let L' := start.dropLast.dropLast
      have : 
        List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ (a, b) :: (a, !b) :: [] := by simp [inv_def]
      rw [this] at sp
      have step : Step start (L' ++ []) := by
        rw [← sp]
        show Step (L' ++ (a, b) :: (a, !b) :: []) (L' ++ [])
        apply Step.not
      apply False.elim
      apply reduced_start
      exact step
    else
      let res := 
        nonnil_nextVertex_extend start.dropLast nil' (a, !b) cancP'    
      rw [res]
      let sp := split_drop start nilP
      rw [cancP] at sp
      simp [inv_def] at cancP
      simp [inv_def] at sp 
      simp [sp]
else
  have eqn : start :+ (a, b) = start.concat (a, b) := by 
    simp [nonnil_nextVertex_extend, cancP, nilP]
  have nn : start :+ (a, b) ≠ [] := by 
    simp [eqn]
  let cnc := 
    nonnil_nextVertex_cancel (start :+ (a, b)) nn (a, !b)
    (by 
      simp [inv_def, cancP, eqn]) 
  rw [cnc, eqn]
  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) :+ (a, !b) = start
Tactic:
simp [cancP, nonnil_nextVertex_cancel, 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)⁻¹
⊢ 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)⁻¹
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
if nil' : start.dropLast = [] 
then
  simp [nilP, nil', nil_nextVertex]
  let sp := split_drop start nilP
  rw [←sp, nil']
  simp
  simp [inv_def] at cancP
  rw [cancP]
else
  if cancP':start.dropLast.getLast nil'  = (a, !b)⁻¹ 
  then
    let sp := split_drop start nilP
    let sp' := split_drop start.dropLast nil'
    rw [←sp', cancP', cancP] at sp
    simp [inv_def' a !b] at sp
    let L' := start.dropLast.dropLast
    have : 
      List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ (a, b) :: (a, !b) :: [] := by simp [inv_def]
    rw [this] at sp
    have step : Step start (L' ++ []) := by
      rw [← sp]
      show Step (L' ++ (a, b) :: (a, !b) :: []) (L' ++ [])
      apply Step.not
    apply False.elim
    apply reduced_start
    exact step
  else
    let res := 
      nonnil_nextVertex_extend start.dropLast nil' (a, !b) cancP'    
    rw [res]
    let sp := split_drop start nilP
    rw [cancP] at sp
    simp [inv_def] at cancP
    simp [inv_def] at sp 
    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)⁻¹
nil' : List.dropLast start = []
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
simp [nilP, nil', nil_nextVertex]
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 = []
⊢ [(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 = []
⊢ [(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 = []
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ [(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 = []
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ [(a, !b)] = start
Tactic:
rw [←sp, nil']
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 = []
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ [(a, !b)] = [] ++ [List.getLast start nilP]
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 = []
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ [(a, !b)] = [] ++ [List.getLast start nilP]
Tactic:
simp
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 = []
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ (a, !b) = List.getLast start nilP
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 = []
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ (a, !b) = List.getLast start nilP
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 = []
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ (a, !b) = List.getLast start nilP
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 = []
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ (a, !b) = List.getLast start nilP
Tactic:
rw [cancP]
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 = []
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
if cancP':start.dropLast.getLast nil'  = (a, !b)⁻¹ 
then
  let sp := split_drop start nilP
  let sp' := split_drop start.dropLast nil'
  rw [←sp', cancP', cancP] at sp
  simp [inv_def' a !b] at sp
  let L' := start.dropLast.dropLast
  have : 
    List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ (a, b) :: (a, !b) :: [] := by simp [inv_def]
  rw [this] at sp
  have step : Step start (L' ++ []) := by
    rw [← sp]
    show Step (L' ++ (a, b) :: (a, !b) :: []) (L' ++ [])
    apply Step.not
  apply False.elim
  apply reduced_start
  exact step
else
  let res := 
    nonnil_nextVertex_extend start.dropLast nil' (a, !b) cancP'    
  rw [res]
  let sp := split_drop start nilP
  rw [cancP] at sp
  simp [inv_def] at cancP
  simp [inv_def] at sp 
  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)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
⊢ 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)⁻¹
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ 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 start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
let sp' := split_drop start.dropLast nil'
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 start ++ [List.getLast start nilP] = start := split_drop start nilP
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
⊢ 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 start ++ [List.getLast start nilP] = start := split_drop start nilP
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
rw [←sp', cancP', 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)⁻¹
sp : List.dropLast (List.dropLast start) ++ [(a, !b)⁻¹] ++ [(a, b)⁻¹] = start
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
⊢ 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) ++ [(a, !b)⁻¹] ++ [(a, b)⁻¹] = start
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
simp [inv_def' a !b] 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'
sp : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = start
⊢ 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'
sp : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = start
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
let L' := start.dropLast.dropLast
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'
sp : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = start
L' : List (α × Bool) := List.dropLast (List.dropLast start)
⊢ 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'
sp : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = start
L' : List (α × Bool) := List.dropLast (List.dropLast start)
⊢ List.dropLast start :+ (a, !b) = start
Tactic:
have : 
  List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ (a, b) :: (a, !b) :: [] := by simp [inv_def]
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'
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