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)⁻¹
eqn : start :+ (a, b) = List.concat start (a, b)
⊢ start :+ (a, b) ≠ []
Tactic:
simp [eqn]
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)⁻¹
eqn : start :+ (a, b) = List.concat start (a, b)
nn : start :+ (a, b) ≠ []
⊢ List.getLast (start :+ (a, b)) nn = (a, !b)⁻¹
Tactic:
simp [inv_def, cancP, eqn]
Proof state after:
no goals
Theorem: FreeGroup.nextVertex_homotopic_concat
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
⊢ List.concat start letter ∼ start :+ letter
Tactic:
if nilP: start = [] then
  simp [nilP, nil_nextVertex]
else
  if cancP:start.getLast nilP = letter⁻¹
  then
    simp [cancP, nonnil_nextVertex_cancel, nilP]
    let (a, b) := letter
    apply Quot.sound
    let sp := split_drop start nilP
    rw [cancP] at sp
    let step' := @Step.not _ start.dropLast ([]) a !b
    simp [Bool.not_not] at step'
    have : List.dropLast start ++ [(a, !b), (a, b)] = 
      start.dropLast ++ [(a, !b)] ++ [(a, b)] := by simp
    rw [inv_def] at sp
    rw [this, sp] at step'
    exact step'
  else
    simp [cancP, nonnil_nextVertex_extend, nilP]
Proof state after:
no goals
Theorem: FreeGroup.nextVertex_homotopic_concat
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : start = []
⊢ List.concat start letter ∼ start :+ letter
Tactic:
simp [nilP, nil_nextVertex]
Proof state after:
no goals
Theorem: FreeGroup.nextVertex_homotopic_concat
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
⊢ List.concat start letter ∼ start :+ letter
Tactic:
if cancP:start.getLast nilP = letter⁻¹
then
  simp [cancP, nonnil_nextVertex_cancel, nilP]
  let (a, b) := letter
  apply Quot.sound
  let sp := split_drop start nilP
  rw [cancP] at sp
  let step' := @Step.not _ start.dropLast ([]) a !b
  simp [Bool.not_not] at step'
  have : List.dropLast start ++ [(a, !b), (a, b)] = 
    start.dropLast ++ [(a, !b)] ++ [(a, b)] := by simp
  rw [inv_def] at sp
  rw [this, sp] at step'
  exact step'
else
  simp [cancP, nonnil_nextVertex_extend, nilP]
Proof state after:
no goals
Theorem: FreeGroup.nextVertex_homotopic_concat
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
cancP : List.getLast start nilP = letter⁻¹
⊢ List.concat start letter ∼ start :+ letter
Tactic:
simp [cancP, nonnil_nextVertex_cancel, nilP]
Proof state after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
cancP : List.getLast start nilP = letter⁻¹
⊢ start ++ [letter] ∼ List.dropLast start
Theorem: FreeGroup.nextVertex_homotopic_concat
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
cancP : List.getLast start nilP = letter⁻¹
⊢ start ++ [letter] ∼ List.dropLast start
Tactic:
let (a, b) := letter
Proof state after:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
⊢ start ++ [(a, b)] ∼ List.dropLast start
Theorem: FreeGroup.nextVertex_homotopic_concat
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
⊢ start ++ [(a, b)] ∼ List.dropLast start
Tactic:
apply Quot.sound
Proof state after:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Theorem: FreeGroup.nextVertex_homotopic_concat
Proof state before:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Tactic:
let sp := split_drop start nilP
Proof state after:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Theorem: FreeGroup.nextVertex_homotopic_concat
Proof state before:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Tactic:
rw [cancP] at sp
Proof state after:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [(a, b)⁻¹] = start
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Theorem: FreeGroup.nextVertex_homotopic_concat
Proof state before:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [(a, b)⁻¹] = start
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Tactic:
let step' := @Step.not _ start.dropLast ([]) a !b
Proof state after:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [(a, b)⁻¹] = start
step' : Step (List.dropLast start ++ [(a, !b), (a, !!b)]) (List.dropLast start ++ []) := Step.not
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Theorem: FreeGroup.nextVertex_homotopic_concat
Proof state before:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [(a, b)⁻¹] = start
step' : Step (List.dropLast start ++ [(a, !b), (a, !!b)]) (List.dropLast start ++ []) := Step.not
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Tactic:
simp [Bool.not_not] at step'
Proof state after:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [(a, b)⁻¹] = start
step' : Step (List.dropLast start ++ [(a, !b), (a, b)]) (List.dropLast start)
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Theorem: FreeGroup.nextVertex_homotopic_concat
Proof state before:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [(a, b)⁻¹] = start
step' : Step (List.dropLast start ++ [(a, !b), (a, b)]) (List.dropLast start)
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Tactic:
have : List.dropLast start ++ [(a, !b), (a, b)] = 
  start.dropLast ++ [(a, !b)] ++ [(a, b)] := by simp
Proof state after:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [(a, b)⁻¹] = start
step' : Step (List.dropLast start ++ [(a, !b), (a, b)]) (List.dropLast start)
this : List.dropLast start ++ [(a, !b), (a, b)] = List.dropLast start ++ [(a, !b)] ++ [(a, b)]
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Theorem: FreeGroup.nextVertex_homotopic_concat
Proof state before:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [(a, b)⁻¹] = start
step' : Step (List.dropLast start ++ [(a, !b), (a, b)]) (List.dropLast start)
this : List.dropLast start ++ [(a, !b), (a, b)] = List.dropLast start ++ [(a, !b)] ++ [(a, b)]
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Tactic:
rw [inv_def] at sp
Proof state after:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [((a, b).1, !(a, b).2)] = start
step' : Step (List.dropLast start ++ [(a, !b), (a, b)]) (List.dropLast start)
this : List.dropLast start ++ [(a, !b), (a, b)] = List.dropLast start ++ [(a, !b)] ++ [(a, b)]
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Theorem: FreeGroup.nextVertex_homotopic_concat
Proof state before:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [((a, b).1, !(a, b).2)] = start
step' : Step (List.dropLast start ++ [(a, !b), (a, b)]) (List.dropLast start)
this : List.dropLast start ++ [(a, !b), (a, b)] = List.dropLast start ++ [(a, !b)] ++ [(a, b)]
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Tactic:
rw [this, sp] at step'
Proof state after:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [((a, b).1, !(a, b).2)] = start
step' : Step (start ++ [(a, b)]) (List.dropLast start)
this : List.dropLast start ++ [(a, !b), (a, b)] = List.dropLast start ++ [(a, !b)] ++ [(a, b)]
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Theorem: FreeGroup.nextVertex_homotopic_concat
Proof state before:
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [((a, b).1, !(a, b).2)] = start
step' : Step (start ++ [(a, b)]) (List.dropLast start)
this : List.dropLast start ++ [(a, !b), (a, b)] = List.dropLast start ++ [(a, !b)] ++ [(a, b)]
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
Tactic:
exact step'
Proof state after:
no goals
Theorem: FreeGroup.nextVertex_homotopic_concat
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [(a, b)⁻¹] = start
step' : Step (List.dropLast start ++ [(a, !b), (a, b)]) (List.dropLast start)
⊢ List.dropLast start ++ [(a, !b), (a, b)] = List.dropLast start ++ [(a, !b)] ++ [(a, b)]
Tactic:
simp
Proof state after:
no goals
Theorem: FreeGroup.nextVertex_homotopic_concat
Proof state before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
cancP : ¬List.getLast start nilP = letter⁻¹
⊢ List.concat start letter ∼ start :+ letter
Tactic:
simp [cancP, nonnil_nextVertex_extend, nilP]
Proof state after:
no goals
Theorem: FreeGroup.append_homotopic
Proof state before:
α : Type
inst✝ : DecidableEq α
L₁ L₂ L₃ : List (α × Bool)
⊢ L₁ ∼ L₂ → L₁ ++ L₃ ∼ L₂ ++ L₃
Tactic:
intro eqn
Proof state after:
α : Type
inst✝ : DecidableEq α
L₁ L₂ L₃ : List (α × Bool)
eqn : L₁ ∼ L₂
⊢ L₁ ++ L₃ ∼ L₂ ++ L₃
Theorem: FreeGroup.append_homotopic
Proof state before:
α : Type
inst✝ : DecidableEq α
L₁ L₂ L₃ : List (α × Bool)
eqn : L₁ ∼ L₂
⊢ L₁ ++ L₃ ∼ L₂ ++ L₃
Tactic:
show mk (L₁ ++ L₃) = mk (L₂ ++ L₃)
Proof state after:
α : Type
inst✝ : DecidableEq α
L₁ L₂ L₃ : List (α × Bool)
eqn : L₁ ∼ L₂
⊢ mk (L₁ ++ L₃) = mk (L₂ ++ L₃)
Theorem: FreeGroup.append_homotopic
Proof state before:
α : Type
inst✝ : DecidableEq α
L₁ L₂ L₃ : List (α × Bool)
eqn : L₁ ∼ L₂
⊢ mk (L₁ ++ L₃) = mk (L₂ ++ L₃)
Tactic:
rw [← mul_mk, ← mul_mk]
Proof state after:
α : Type
inst✝ : DecidableEq α
L₁ L₂ L₃ : List (α × Bool)
eqn : L₁ ∼ L₂
⊢ mk L₁ * mk L₃ = mk L₂ * mk L₃
Theorem: FreeGroup.append_homotopic
Proof state before:
α : Type
inst✝ : DecidableEq α
L₁ L₂ L₃ : List (α × Bool)
eqn : L₁ ∼ L₂
⊢ mk L₁ * mk L₃ = mk L₂ * mk L₃
Tactic:
rw [eqn]
Proof state after:
no goals
Theorem: FreeGroup.finalVertex_homotopic_append
Proof state before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
⊢ start ++ word ∼ finalVertex start word
Tactic:
match word with
| [] => simp [finalVertex]
| head ::tail => 
  simp [finalVertex, List.foldl_cons]
  let ih := finalVertex_homotopic_append (start :+ head) tail
  simp [finalVertex, List.foldl_cons] at ih
  let eqn := nextVertex_homotopic_concat start head
  show mk (start ++ head :: tail) = mk (List.foldl nextVertex (start :+ head) tail)
  rw [←ih]
  let eqn' := append_homotopic tail eqn
  simp [← eqn']
Proof state after:
no goals
Theorem: FreeGroup.finalVertex_homotopic_append
Proof state before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
⊢ start ++ [] ∼ finalVertex start []
Tactic:
simp [finalVertex]
Proof state after:
no goals
Theorem: FreeGroup.finalVertex_homotopic_append
Proof state before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
⊢ start ++ head :: tail ∼ finalVertex start (head :: tail)
Tactic:
simp [finalVertex, List.foldl_cons]
Proof state after:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
⊢ start ++ head :: tail ∼ List.foldl nextVertex (start :+ head) tail
Theorem: FreeGroup.finalVertex_homotopic_append
Proof state before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
⊢ start ++ head :: tail ∼ List.foldl nextVertex (start :+ head) tail
Tactic:
let ih := finalVertex_homotopic_append (start :+ head) tail
Proof state after:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ finalVertex (start :+ head) tail := finalVertex_homotopic_append (start :+ head) tail
⊢ start ++ head :: tail ∼ List.foldl nextVertex (start :+ head) tail
Theorem: FreeGroup.finalVertex_homotopic_append
Proof state before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ finalVertex (start :+ head) tail := finalVertex_homotopic_append (start :+ head) tail
⊢ start ++ head :: tail ∼ List.foldl nextVertex (start :+ head) tail
Tactic:
simp [finalVertex, List.foldl_cons] at ih
Proof state after:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
⊢ start ++ head :: tail ∼ List.foldl nextVertex (start :+ head) tail
Theorem: FreeGroup.finalVertex_homotopic_append
Proof state before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
⊢ start ++ head :: tail ∼ List.foldl nextVertex (start :+ head) tail
Tactic:
let eqn := nextVertex_homotopic_concat start head
Proof state after:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
eqn : List.concat start head ∼ start :+ head := nextVertex_homotopic_concat start head
⊢ start ++ head :: tail ∼ List.foldl nextVertex (start :+ head) tail
Theorem: FreeGroup.finalVertex_homotopic_append
Proof state before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
eqn : List.concat start head ∼ start :+ head := nextVertex_homotopic_concat start head
⊢ start ++ head :: tail ∼ List.foldl nextVertex (start :+ head) tail
Tactic:
show mk (start ++ head :: tail) = mk (List.foldl nextVertex (start :+ head) tail)
Proof state after:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
eqn : List.concat start head ∼ start :+ head := nextVertex_homotopic_concat start head
⊢ mk (start ++ head :: tail) = mk (List.foldl nextVertex (start :+ head) tail)
Theorem: FreeGroup.finalVertex_homotopic_append
Proof state before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
eqn : List.concat start head ∼ start :+ head := nextVertex_homotopic_concat start head
⊢ mk (start ++ head :: tail) = mk (List.foldl nextVertex (start :+ head) tail)
Tactic:
rw [←ih]
Proof state after:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
eqn : List.concat start head ∼ start :+ head := nextVertex_homotopic_concat start head
⊢ mk (start ++ head :: tail) = mk (start :+ head ++ tail)
Theorem: FreeGroup.finalVertex_homotopic_append
Proof state before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
eqn : List.concat start head ∼ start :+ head := nextVertex_homotopic_concat start head
⊢ mk (start ++ head :: tail) = mk (start :+ head ++ tail)
Tactic:
let eqn' := append_homotopic tail eqn
Proof state after:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
eqn : List.concat start head ∼ start :+ head := nextVertex_homotopic_concat start head
eqn' : List.concat start head ++ tail ∼ start :+ head ++ tail := append_homotopic tail eqn
⊢ mk (start ++ head :: tail) = mk (start :+ head ++ tail)
Theorem: FreeGroup.finalVertex_homotopic_append
Proof state before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
eqn : List.concat start head ∼ start :+ head := nextVertex_homotopic_concat start head
eqn' : List.concat start head ++ tail ∼ start :+ head ++ tail := append_homotopic tail eqn
⊢ mk (start ++ head :: tail) = mk (start :+ head ++ tail)
Tactic:
simp [← eqn']
Proof state after:
no goals
Theorem: FreeGroup.finalVertexOnFreeGroup_natural
Proof state before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
red : Reduced start
⊢ finalVertex start word = finalVertexOnFreeGroup start red (mk word)
Tactic:
rfl
Proof state after:
no goals
Theorem: FreeGroup.reducedWord_inverse
Proof state before:
α : Type
inst✝ : DecidableEq α
g : FreeGroup α
⊢ mk (reducedWord g) = g
Tactic:
apply Quot.ind (β := fun g ↦ mk (reducedWord g) = g )
Proof state after:
case mk
α : Type
inst✝ : DecidableEq α
g : FreeGroup α
⊢ ∀ (a : List (α × Bool)), mk (reducedWord (Quot.mk Step a)) = Quot.mk Step a
Theorem: FreeGroup.reducedWord_inverse
Proof state before:
case mk
α : Type
inst✝ : DecidableEq α
g : FreeGroup α
⊢ ∀ (a : List (α × Bool)), mk (reducedWord (Quot.mk Step a)) = Quot.mk Step a
Tactic:
intro word
Proof state after:
case mk
α : Type
inst✝ : DecidableEq α
g : FreeGroup α
word : List (α × Bool)
⊢ mk (reducedWord (Quot.mk Step word)) = Quot.mk Step word
Theorem: FreeGroup.reducedWord_inverse
Proof state before:
case mk
α : Type
inst✝ : DecidableEq α
g : FreeGroup α
word : List (α × Bool)
⊢ mk (reducedWord (Quot.mk Step word)) = Quot.mk Step word
Tactic:
simp [finalVertex_homotopic_append [], ←finalVertexOnFreeGroup_natural]
Proof state after:
case mk
α : Type
inst✝ : DecidableEq α
g : FreeGroup α
word : List (α × Bool)
⊢ mk (finalVertex [] word) = mk word
Theorem: FreeGroup.reducedWord_inverse
Proof state before:
case mk
α : Type
inst✝ : DecidableEq α
g : FreeGroup α
word : List (α × Bool)
⊢ mk (finalVertex [] word) = mk word
Tactic:
simp [←finalVertex_homotopic_append]
Proof state after:
no goals
Theorem: GroupLabelledGraph.pathLabel_append
Proof state before:
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
p' : Graph.EdgePath Γ v w
⊢ pathLabel 𝓖 (p ++ p') = pathLabel 𝓖 p * pathLabel 𝓖 p'
Tactic:
induction p <;> aesop (add norm simp [mul_assoc])
Proof state after:
no goals
Theorem: GroupLabelledGraph.pathLabel_concat
Proof state before:
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
e : Graph.EdgeBetween Γ v w
⊢ pathLabel 𝓖 (Graph.EdgePath.concat p e) = pathLabel 𝓖 p * 𝓖.label e
Tactic:
induction p <;> aesop (add norm simp [Graph.EdgePath.concat, mul_assoc])
Proof state after:
no goals
Theorem: GroupLabelledGraph.pathLabel_reverse
Proof state before:
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v : V
p : Graph.EdgePath Γ u v
⊢ pathLabel 𝓖 (Graph.EdgePath.reverse p) = (pathLabel 𝓖 p)⁻¹
Tactic:
induction p <;> aesop (add norm simp [Graph.EdgePath.reverse])
Proof state after:
no goals
Theorem: GroupLabelledGraph.pathLabel_reduction
Proof state before:
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝¹ v✝ w : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v : V
p✝ p'✝ : Graph.EdgePath Γ u v
u✝ u'✝ : V
e : Graph.EdgeBetween Γ u✝ u'✝
p : Graph.EdgePath Γ u u✝
p' : Graph.EdgePath Γ u✝ v
⊢ pathLabel 𝓖 (p ++ Graph.EdgePath.cons e (Graph.EdgePath.cons (Graph.EdgeBetween.bar e) p')) = pathLabel 𝓖 (p ++ p')
Tactic:
simp
Proof state after:
no goals
Theorem: GroupLabelledGraph.pathLabel_singletonPath
Proof state before:
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u v w : V
g h : G
𝓖 : GroupLabelledGraph Γ G
e : Graph.EdgeBetween Γ u v
⊢ pathLabel 𝓖 (Graph.singletonPath e) = 𝓖.label e
Tactic:
simp
Proof state after:
no goals
Theorem: GroupLabelledGraph.pathClassLabel_append
Proof state before:
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
⊢ ∀ (p : u ⟶ v) (p' : v ⟶ w), pathClassLabel 𝓖 (p ≫ p') = pathClassLabel 𝓖 p * pathClassLabel 𝓖 p'
Tactic:
apply Quot.ind
Proof state after:
case mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
⊢ ∀ (a : Graph.EdgePath Γ u v) (p' : v ⟶ w),
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction a ≫ p') =
      pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction a) * pathClassLabel 𝓖 p'
Theorem: GroupLabelledGraph.pathClassLabel_append
Proof state before:
case mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
⊢ ∀ (a : Graph.EdgePath Γ u v) (p' : v ⟶ w),
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction a ≫ p') =
      pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction a) * pathClassLabel 𝓖 p'
Tactic:
intro p
Proof state after:
case mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
⊢ ∀ (p' : v ⟶ w),
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p ≫ p') =
      pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p) * pathClassLabel 𝓖 p'