Yamaguchi Lean 4 Library
ReidemeisterSchreier/FreeGroup/PrefixParent.lean
ReidemeisterSchreier/FreeGroup/PrefixParent/Source

ReidemeisterSchreier/FreeGroup/PrefixParent.lean

1import Mathlib.GroupTheory.FreeGroup.Reduce
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ReidemeisterSchreier/FreeGroup/PrefixParent.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Free-group support
14Automorphisms, signed-letter words, prefix-parent operations, and generator equivalences for free groups.
15-/
17namespace ReidemeisterSchreier
19/-- A signed generator letter in the word model of a free group. -/
20abbrev SignedLetter (X : Type u) := X × Bool
22namespace SignedLetter
24/-- The inverse signed letter. -/
25def inv {X : Type u} (y : SignedLetter X) : SignedLetter X :=
26 (y.1, !y.2)
28@[simp] theorem inv_fst {X : Type u} (y : SignedLetter X) : y.inv.1 = y.1 := rfl
29@[simp] theorem inv_snd {X : Type u} (y : SignedLetter X) : y.inv.2 = !y.2 := rfl
30@[simp] theorem inv_inv {X : Type u} (y : SignedLetter X) : y.inv.inv = y := by
31 cases y
32 simp only [inv, Bool.not_not]
36namespace Internal.FreeGroupWord
38theorem FreeGroup.invRev_eq_getLast_append_dropLast {X : Type u}
39 (w : List (X × Bool)) (hw : w ≠ []) :
40 FreeGroup.invRev w =
41 [((w.getLast hw).1, ! (w.getLast hw).2)] ++ FreeGroup.invRev w.dropLast := by
42 refine (congrArg FreeGroup.invRev (List.dropLast_append_getLast hw)).symm.trans ?_
43 simp only [FreeGroup.invRev, List.map_append, List.map_dropLast, List.map_cons, List.map_nil,
44 List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append, List.cons_append]
46end Internal.FreeGroupWord
48/-- The last signed letter of the reduced word representing `g`, if it is nonempty. -/
49def FreeGroup.lastLetter? {X : Type u} [DecidableEq X] (g : FreeGroup X) :
50 Option (SignedLetter X) :=
51 (FreeGroup.toWord g).getLast?
53namespace Internal.FreeGroupWord
55theorem FreeGroup.lastLetter?_eq_some_iff {X : Type u} [DecidableEq X]
56 {g : FreeGroup X} {y : SignedLetter X} :
57 FreeGroup.lastLetter? g = some y ↔
58 ∃ hw : FreeGroup.toWord g ≠ [], (FreeGroup.toWord g).getLast hw = y := by
59 constructor
60 · intro h
61 have hy : y ∈ (FreeGroup.toWord g).getLast? := by
62 simpa [FreeGroup.lastLetter?, h]
63 rcases List.mem_getLast?_eq_getLast hy with ⟨hw, hyw⟩
64 exact ⟨hw, hyw.symm⟩
65 · rintro ⟨hw, hlast⟩
66 rw [FreeGroup.lastLetter?, List.getLast?_eq_getLast_of_ne_nil hw, hlast]
68theorem FreeGroup.toWord_mul_of_of_not_cancels {X : Type u} [DecidableEq X]
69 (t : FreeGroup X) (x : X)
70 (hcancel : ¬ ∃ hw : FreeGroup.toWord t ≠ [], (FreeGroup.toWord t).getLast hw = (x, false)) :
71 FreeGroup.toWord (t * FreeGroup.of x) = FreeGroup.toWord t ++ [(x, true)] := by
72 rw [FreeGroup.toWord_mul, FreeGroup.toWord_of]
73 have hred : FreeGroup.IsReduced (FreeGroup.toWord t ++ [(x, true)]) := by
74 refine List.IsChain.append (FreeGroup.isReduced_toWord (x := t)) ?_ ?_
75 · simp only [List.IsChain.singleton]
76 · intro a ha b hb hab
77 have hb' : (x, true) = b := by simpa using hb
78 cases hb'
79 rcases List.mem_getLast?_eq_getLast ha with ⟨hw, rfl⟩
80 have hne : (FreeGroup.toWord t).getLast hw ≠ (x, false) := by
81 intro hlast
82 exact hcancel ⟨hw, hlast⟩
83 dsimp at hab hne ⊢
84 cases h2 : ((FreeGroup.toWord t).getLast hw).2 with
85 | false =>
86 exfalso
87 apply hne
88 apply Prod.ext
89 · exact hab
90 · simpa using h2
91 | true => rfl
92 exact hred.reduce_eq
94theorem FreeGroup.mul_of_of_eq_mk_dropLast_of_cancels {X : Type u} [DecidableEq X]
95 (t : FreeGroup X) (x : X) (hw : FreeGroup.toWord t ≠ [])
96 (hlast : (FreeGroup.toWord t).getLast hw = (x, false)) :
97 t * FreeGroup.of x = FreeGroup.mk ((FreeGroup.toWord t).dropLast) := by
98 rw [← FreeGroup.mk_toWord (x := t)]
99 simp only [FreeGroup.toWord_mk, FreeGroup.reduce_toWord]
100 rw [FreeGroup.of, FreeGroup.mul_mk]
101 have ht :
102 FreeGroup.toWord t =
103 (FreeGroup.toWord t).dropLast ++ [(FreeGroup.toWord t).getLast hw] := by
104 simpa using (List.dropLast_append_getLast hw).symm
105 rw [ht, hlast]
106 simp only [List.append_assoc, List.cons_append, List.nil_append, ne_eq, List.cons_ne_self,
107 not_false_eq_true, List.dropLast_append_of_ne_nil, List.dropLast_singleton, List.append_nil]
108 exact Quot.sound (show FreeGroup.Red.Step
109 ((FreeGroup.toWord t).dropLast ++ (x, false) :: (x, true) :: [])
110 ((FreeGroup.toWord t).dropLast) from by
111 simpa using (show FreeGroup.Red.Step
112 ((FreeGroup.toWord t).dropLast ++ (x, false) :: (x, true) :: [])
113 ((FreeGroup.toWord t).dropLast ++ []) from by constructor))
115theorem FreeGroup.toWord_mul_of_of_cancels {X : Type u} [DecidableEq X]
116 (t : FreeGroup X) (x : X) (hw : FreeGroup.toWord t ≠ [])
117 (hlast : (FreeGroup.toWord t).getLast hw = (x, false)) :
118 FreeGroup.toWord (t * FreeGroup.of x) = (FreeGroup.toWord t).dropLast := by
119 rw [FreeGroup.mul_of_of_eq_mk_dropLast_of_cancels t x hw hlast, FreeGroup.toWord_mk]
120 have hred : FreeGroup.IsReduced ((FreeGroup.toWord t).dropLast) := by
121 exact (FreeGroup.isReduced_toWord (x := t)).dropLast
122 simpa using hred.reduce_eq
124/-- Appending a reduced signed letter to a reduced word stays reduced unless the last letter is
125its inverse. -/
126theorem FreeGroup.toWord_mul_mk_singleton_of_not_cancels {X : Type u} [DecidableEq X]
127 (t : FreeGroup X) (y : X × Bool)
128 (hcancel :
129 ¬ ∃ hw : FreeGroup.toWord t ≠ [],
130 (FreeGroup.toWord t).getLast hw = (y.1, !y.2)) :
131 FreeGroup.toWord (t * FreeGroup.mk [y]) = FreeGroup.toWord t ++ [y] := by
132 rw [FreeGroup.toWord_mul, FreeGroup.toWord_mk]
133 have hred : FreeGroup.IsReduced (FreeGroup.toWord t ++ [y]) := by
134 refine List.IsChain.append (FreeGroup.isReduced_toWord (x := t)) ?_ ?_
135 · simp only [List.IsChain.singleton]
136 · intro a ha b hb hab
137 have hb' : y = b := by simpa using hb
138 cases hb'
139 rcases List.mem_getLast?_eq_getLast ha with ⟨hw, rfl⟩
140 have hne : (FreeGroup.toWord t).getLast hw ≠ (y.1, !y.2) := by
141 intro hlast
142 exact hcancel ⟨hw, hlast⟩
143 dsimp at hab hne ⊢
144 cases h2 : ((FreeGroup.toWord t).getLast hw).2 with
145 | false =>
146 cases y with
147 | mk x b =>
148 cases b with
149 | false => rfl
150 | true =>
151 exfalso
152 apply hne
153 apply Prod.ext
154 · exact hab
155 · simpa using h2
156 | true =>
157 cases y with
158 | mk x b =>
159 cases b with
160 | false =>
161 exfalso
162 apply hne
163 apply Prod.ext
164 · exact hab
165 · simp only [h2, Bool.not_false]
166 | true => rfl
167 exact hred.reduce_eq
169/-- Cancelling a reduced signed letter on the right amounts to deleting the last letter in the
170word model. -/
171theorem FreeGroup.mul_mk_singleton_eq_mk_dropLast_of_cancels {X : Type u} [DecidableEq X]
172 (t : FreeGroup X) (y : X × Bool) (hw : FreeGroup.toWord t ≠ [])
173 (hlast : (FreeGroup.toWord t).getLast hw = (y.1, !y.2)) :
174 t * FreeGroup.mk [y] = FreeGroup.mk ((FreeGroup.toWord t).dropLast) := by
175 rw [← FreeGroup.mk_toWord (x := t)]
176 simp only [FreeGroup.toWord_mk, FreeGroup.reduce_toWord]
177 have ht :
178 FreeGroup.toWord t =
179 (FreeGroup.toWord t).dropLast ++ [(FreeGroup.toWord t).getLast hw] := by
180 simpa using (List.dropLast_append_getLast hw).symm
181 rw [ht, hlast]
182 simp only [FreeGroup.mul_mk, List.append_assoc, List.cons_append, List.nil_append, ne_eq,
183 List.cons_ne_self, not_false_eq_true, List.dropLast_append_of_ne_nil,
184 List.dropLast_singleton, List.append_nil]
185 exact Quot.sound
186 (show FreeGroup.Red.Step
187 ((FreeGroup.toWord t).dropLast ++ (y.1, !y.2) :: y :: [])
188 ((FreeGroup.toWord t).dropLast) from by
189 simpa using
190 (show FreeGroup.Red.Step
191 ((FreeGroup.toWord t).dropLast ++ (y.1, !y.2) :: y :: [])
192 ((FreeGroup.toWord t).dropLast ++ []) from
193 FreeGroup.Red.Step.not_rev))
195theorem FreeGroup.toWord_mul_mk_singleton_of_cancels {X : Type u} [DecidableEq X]
196 (t : FreeGroup X) (y : X × Bool) (hw : FreeGroup.toWord t ≠ [])
197 (hlast : (FreeGroup.toWord t).getLast hw = (y.1, !y.2)) :
198 FreeGroup.toWord (t * FreeGroup.mk [y]) = (FreeGroup.toWord t).dropLast := by
199 rw [FreeGroup.mul_mk_singleton_eq_mk_dropLast_of_cancels t y hw hlast, FreeGroup.toWord_mk]
200 have hred : FreeGroup.IsReduced ((FreeGroup.toWord t).dropLast) := by
201 exact (FreeGroup.isReduced_toWord (x := t)).dropLast
202 simpa using hred.reduce_eq
204/-- Unified signed-letter multiplication rule for reduced words. -/
205theorem FreeGroup.toWord_mul_singleton {X : Type u} [DecidableEq X]
206 (t : FreeGroup X) (y : SignedLetter X) :
207 FreeGroup.toWord (t * FreeGroup.mk [y]) =
208 if FreeGroup.lastLetter? t = some y.inv then
209 (FreeGroup.toWord t).dropLast
210 else
211 FreeGroup.toWord t ++ [y] := by
212 by_cases hlast? : FreeGroup.lastLetter? t = some y.inv
213 · rw [if_pos hlast?]
214 rcases (FreeGroup.lastLetter?_eq_some_iff (g := t) (y := y.inv)).1 hlast? with
215 ⟨hw, hlast⟩
216 simpa [SignedLetter.inv] using
217 FreeGroup.toWord_mul_mk_singleton_of_cancels t y hw hlast
218 · rw [if_neg hlast?]
219 have hcancel :
220 ¬ ∃ hw : FreeGroup.toWord t ≠ [],
221 (FreeGroup.toWord t).getLast hw = (y.1, !y.2) := by
222 intro h
223 exact hlast?
224 ((FreeGroup.lastLetter?_eq_some_iff (g := t) (y := y.inv)).2 (by
225 simpa [SignedLetter.inv] using h))
226 exact FreeGroup.toWord_mul_mk_singleton_of_not_cancels t y hcancel
228/-- Positive generators are the positive signed-letter specialization of
229`FreeGroup.toWord_mul_singleton`. -/
230theorem FreeGroup.toWord_mul_of {X : Type u} [DecidableEq X]
231 (t : FreeGroup X) (x : X) :
232 FreeGroup.toWord (t * FreeGroup.of x) =
233 if FreeGroup.lastLetter? t = some ((x, false) : SignedLetter X) then
234 (FreeGroup.toWord t).dropLast
235 else
236 FreeGroup.toWord t ++ [(x, true)] := by
237 simpa [FreeGroup.of, SignedLetter.inv] using
238 (FreeGroup.toWord_mul_singleton t ((x, true) : SignedLetter X))
240end Internal.FreeGroupWord
242/-- The predecessor of a reduced word, obtained by deleting its last letter. -/
243def FreeGroup.prefixParent {X : Type u} [DecidableEq X] (t : FreeGroup X) : FreeGroup X :=
244 FreeGroup.mk ((FreeGroup.toWord t).dropLast)
246namespace Internal.FreeGroupWord
248/-- Multiplication by a signed singleton either deletes the inverse last letter or appends the
249singleton to the reduced word. -/
250theorem FreeGroup.mul_mk_singleton_eq_ite_prefixParent {X : Type u} [DecidableEq X]
251 (t : FreeGroup X) (y : X × Bool) :
252 t * FreeGroup.mk [y] =
253 if _ : ∃ hw : FreeGroup.toWord t ≠ [],
254 (FreeGroup.toWord t).getLast hw = (y.1, !y.2)
255 then FreeGroup.prefixParent t
256 else FreeGroup.mk (FreeGroup.toWord t ++ [y]) := by
257 by_cases h : ∃ hw : FreeGroup.toWord t ≠ [],
258 (FreeGroup.toWord t).getLast hw = (y.1, !y.2)
259 · rcases h with ⟨hw, hlast⟩
260 rw [dif_pos ⟨hw, hlast⟩]
261 exact FreeGroup.mul_mk_singleton_eq_mk_dropLast_of_cancels t y hw hlast
262 · rw [dif_neg h]
263 calc
264 t * FreeGroup.mk [y] =
265 FreeGroup.mk (FreeGroup.toWord (t * FreeGroup.mk [y])) := by
266 exact (FreeGroup.mk_toWord (x := t * FreeGroup.mk [y])).symm
267 _ = FreeGroup.mk (FreeGroup.toWord t ++ [y]) := by
268 rw [FreeGroup.toWord_mul_mk_singleton_of_not_cancels t y h]
270@[simp] theorem FreeGroup.toWord_prefixParent {X : Type u} [DecidableEq X] (t : FreeGroup X) :
271 FreeGroup.toWord (FreeGroup.prefixParent t) = (FreeGroup.toWord t).dropLast := by
272 rw [FreeGroup.prefixParent, FreeGroup.toWord_mk]
273 have hred : FreeGroup.IsReduced ((FreeGroup.toWord t).dropLast) := by
274 exact (FreeGroup.isReduced_toWord (x := t)).dropLast
275 exact hred.reduce_eq
277theorem FreeGroup.toWord_length_prefixParent_lt {X : Type u} [DecidableEq X]
278 {t : FreeGroup X} (ht : t ≠ 1) :
279 (FreeGroup.toWord (FreeGroup.prefixParent t)).length < (FreeGroup.toWord t).length := by
280 rw [FreeGroup.toWord_prefixParent, List.length_dropLast]
281 have hnonempty : FreeGroup.toWord t ≠ [] := by
282 exact mt (FreeGroup.toWord_eq_nil_iff.mp) ht
283 have hlen : 0 < (FreeGroup.toWord t).length := List.length_pos_iff_ne_nil.mpr hnonempty
284 simpa using Nat.pred_lt (Nat.ne_of_gt hlen)
286theorem FreeGroup.length_prefixParent_eq_pred {X : Type u} [DecidableEq X]
287 (t : FreeGroup X) :
288 (FreeGroup.toWord (FreeGroup.prefixParent t)).length =
289 (FreeGroup.toWord t).length - 1 := by
290 rw [FreeGroup.toWord_prefixParent, List.length_dropLast]
292theorem FreeGroup.prefixParent_mul_of_of_last_pos {X : Type u} [DecidableEq X]
293 (t : FreeGroup X) (x : X) (hw : FreeGroup.toWord t ≠ [])
294 (hlast : (FreeGroup.toWord t).getLast hw = (x, true)) :
295 FreeGroup.prefixParent t * FreeGroup.of x = t := by
296 apply FreeGroup.toWord_injective
297 rw [FreeGroup.toWord_mul, FreeGroup.toWord_of]
298 have ht : FreeGroup.toWord t =
299 (FreeGroup.toWord t).dropLast ++ [(FreeGroup.toWord t).getLast hw] := by
300 simpa using (List.dropLast_append_getLast hw).symm
301 have hword : FreeGroup.toWord (FreeGroup.prefixParent t) ++ [(x, true)] = FreeGroup.toWord t := by
302 calc
303 FreeGroup.toWord (FreeGroup.prefixParent t) ++ [(x, true)]
304 = (FreeGroup.toWord t).dropLast ++ [(x, true)] := by rw [FreeGroup.toWord_prefixParent]
305 _ = FreeGroup.toWord t := by
306 have ht' := ht.symm
307 rw [hlast] at ht'
308 exact ht'
309 have hred : FreeGroup.IsReduced (FreeGroup.toWord (FreeGroup.prefixParent t) ++ [(x, true)]) := by
310 rw [hword]
311 exact FreeGroup.isReduced_toWord (x := t)
312 exact hred.reduce_eq.trans hword
314theorem FreeGroup.prefixParent_mul_mk_singleton_of_last {X : Type u} [DecidableEq X]
315 (t : FreeGroup X) (y : X × Bool) (hw : FreeGroup.toWord t ≠ [])
316 (hlast : (FreeGroup.toWord t).getLast hw = y) :
317 FreeGroup.prefixParent t * FreeGroup.mk [y] = t := by
318 apply FreeGroup.toWord_injective
319 rw [FreeGroup.toWord_mul, FreeGroup.toWord_prefixParent, FreeGroup.toWord_mk]
320 have ht :
321 FreeGroup.toWord t =
322 (FreeGroup.toWord t).dropLast ++ [(FreeGroup.toWord t).getLast hw] := by
323 simpa using (List.dropLast_append_getLast hw).symm
324 have hword : (FreeGroup.toWord t).dropLast ++ [y] = FreeGroup.toWord t := by
325 have ht' := ht.symm
326 rw [hlast] at ht'
327 exact ht'
328 have hred : FreeGroup.IsReduced ((FreeGroup.toWord t).dropLast ++ [y]) := by
329 rw [hword]
330 exact FreeGroup.isReduced_toWord (x := t)
331 exact hred.reduce_eq.trans hword
333theorem FreeGroup.prefixParent_mul_lastLetter {X : Type u} [DecidableEq X]
334 {t : FreeGroup X} {y : SignedLetter X}
335 (h : FreeGroup.lastLetter? t = some y) :
336 FreeGroup.prefixParent t * FreeGroup.mk [y] = t := by
337 rcases (FreeGroup.lastLetter?_eq_some_iff (g := t) (y := y)).1 h with
338 ⟨hw, hlast⟩
339 exact FreeGroup.prefixParent_mul_mk_singleton_of_last t y hw hlast
341end Internal.FreeGroupWord
343/-- The parent edge data obtained by deleting the last signed letter of a nontrivial word. -/
344structure FreeGroup.PrefixParentEdge {X : Type u} [DecidableEq X] (t : FreeGroup X) where
345 parent : FreeGroup X
346 letter : SignedLetter X
347 parent_eq : parent = FreeGroup.prefixParent t
348 rebuild : parent * FreeGroup.mk [letter] = t
350/-- A nontrivial reduced word has a canonical parent edge. -/
351def FreeGroup.prefixParentEdgeOfNeOne {X : Type u} [DecidableEq X]
352 {t : FreeGroup X} (ht : t ≠ 1) : FreeGroup.PrefixParentEdge t := by
353 have hw : FreeGroup.toWord t ≠ [] := by
354 exact mt (FreeGroup.toWord_eq_nil_iff.mp) ht
355 refine
356 { parent := FreeGroup.prefixParent t
357 letter := (FreeGroup.toWord t).getLast hw
358 parent_eq := rfl
359 rebuild := ?_ }
360 exact Internal.FreeGroupWord.FreeGroup.prefixParent_mul_mk_singleton_of_last t
361 ((FreeGroup.toWord t).getLast hw) hw rfl
363@[simp] theorem FreeGroup.prefixParentEdgeOfNeOne_parent {X : Type u} [DecidableEq X]
364 {t : FreeGroup X} (ht : t ≠ 1) :
365 (FreeGroup.prefixParentEdgeOfNeOne (X := X) ht).parent =
366 FreeGroup.prefixParent t :=
367 rfl
369theorem FreeGroup.prefixParentEdgeOfNeOne_lastLetter? {X : Type u} [DecidableEq X]
370 {t : FreeGroup X} (ht : t ≠ 1) :
371 FreeGroup.lastLetter? t =
372 some (FreeGroup.prefixParentEdgeOfNeOne (X := X) ht).letter := by
373 have hw : FreeGroup.toWord t ≠ [] := by
374 exact mt (FreeGroup.toWord_eq_nil_iff.mp) ht
375 simp only [lastLetter?, List.getLast?_eq_getLast_of_ne_nil hw, prefixParentEdgeOfNeOne]
377/-- Nontrivial words decompose as parent times their last signed letter. -/
378theorem FreeGroup.exists_prefixParent_mul_lastLetter_of_ne_one
379 {X : Type u} [DecidableEq X] {t : FreeGroup X} (ht : t ≠ 1) :
380 ∃ y : SignedLetter X,
381 FreeGroup.lastLetter? t = some y ∧
382 FreeGroup.prefixParent t * FreeGroup.mk [y] = t := by
383 have hw : FreeGroup.toWord t ≠ [] := by
384 exact mt (FreeGroup.toWord_eq_nil_iff.mp) ht
385 refine ⟨(FreeGroup.toWord t).getLast hw, ?_, ?_⟩
386 · rw [FreeGroup.lastLetter?, List.getLast?_eq_getLast_of_ne_nil hw]
387 · exact Internal.FreeGroupWord.FreeGroup.prefixParent_mul_mk_singleton_of_last t
388 ((FreeGroup.toWord t).getLast hw) hw rfl
390theorem FreeGroup.lastLetter_cases_of_ne_one {X : Type u} [DecidableEq X]
391 {t : FreeGroup X} (ht : t ≠ 1) :
392 ∃ x : X,
393 (∃ hw : FreeGroup.toWord t ≠ [],
394 (FreeGroup.toWord t).getLast hw = (x, true) ∧
395 FreeGroup.prefixParent t * FreeGroup.of x = t) ∨
396 (∃ hw : FreeGroup.toWord t ≠ [],
397 (FreeGroup.toWord t).getLast hw = (x, false) ∧
398 t * FreeGroup.of x = FreeGroup.prefixParent t) := by
399 have hw : FreeGroup.toWord t ≠ [] := by
400 exact mt (FreeGroup.toWord_eq_nil_iff.mp) ht
401 rcases hlast : (FreeGroup.toWord t).getLast hw with ⟨x, b⟩
402 cases b with
403 | false =>
404 refine ⟨x, Or.inr ⟨hw, hlast, ?_⟩⟩
405 simpa [FreeGroup.prefixParent] using
406 Internal.FreeGroupWord.FreeGroup.mul_of_of_eq_mk_dropLast_of_cancels t x hw hlast
407 | true =>
408 refine ⟨x, Or.inl ⟨hw, hlast, ?_⟩⟩
409 exact Internal.FreeGroupWord.FreeGroup.prefixParent_mul_of_of_last_pos t x hw hlast
411namespace Internal.FreeGroupWord
413theorem FreeGroup.mul_of_eq_prefixParent_of_cancels {X : Type u} [DecidableEq X]
414 (t : FreeGroup X) (x : X) (hw : FreeGroup.toWord t ≠ [])
415 (hlast : (FreeGroup.toWord t).getLast hw = (x, false)) :
416 t * FreeGroup.of x = FreeGroup.prefixParent t := by
417 simpa [FreeGroup.prefixParent] using
418 FreeGroup.mul_of_of_eq_mk_dropLast_of_cancels t x hw hlast
420end Internal.FreeGroupWord
422end ReidemeisterSchreier