Source: FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/Relators/SourceTotal.lean

1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.SecondReduction.Relators.SourceCore

2

3/-

4PUBLIC_PAGE_SNAPSHOT

5generated_at: 2026-05-27T09:47:29+09:00

6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/SecondReduction/Relators/SourceTotal.lean

7translation_root: data/translation

8purpose: identifies the local data snapshot used to build pages/

9placement: after imports, never before imports

10-/

11/-!

12# Second compact zero-genus reduction

13

14The second explicit reduction step, with ordered target signatures, transport maps, source and target relator calculations, and quotient-basis comparison.

15-/

16

17namespace FenchelNielsen

18

19def SecondReductionCanonicalSecondBranchSourceTotalCase

20 {tailLen p q : ℕ}

21 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)

22 (hp : 2 ≤ p) (hq : 2 ≤ q)

23 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')

24 (htail : ∀ j, 2 ≤ tail j) : Prop :=

25 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩

26 let σ :=

27 secondReductionCanonicalSourceSignature

28 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

29 let τ :=

30 secondReductionTransportSignature (p := p) hq

31 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail

32 let φ :=

33 secondReductionCanonicalSourceFreeQuotientHom

34 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

35 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _

36 let e :=

37 secondReductionCanonicalSchreierBasisEquiv

38 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

39 let η :=

40 secondReductionCanonicalSchreierToTransportSecondBranchHom

41 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

42 let x : FuchsianGenerator σ :=

43 secondReductionCanonicalDistinguishedGenerator

44 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

45 ∀ k : Fin q,

46 η

47 (e.symm

48 (⟨(FreeGroup.of x) ^ k.val * totalRelation σ *

49 ((FreeGroup.of x) ^ k.val)⁻¹, by

50 change φ

51 ((FreeGroup.of x) ^ k.val * totalRelation σ *

52 ((FreeGroup.of x) ^ k.val)⁻¹) = 1

53 have hrφ : φ (totalRelation σ) = 1 :=

54 secondReductionCanonicalSourceFreeQuotientHom_respects_relators

55 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

56 (totalRelation σ) (Or.inr rfl)

57 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker)) ∈

58 Subgroup.normalClosure

59 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

60 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail)

61theorem secondReductionCanonicalSecondBranchSourceTotalCase_mem_normalClosure

62 {tailLen p q : ℕ}

63 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)

64 (hp : 2 ≤ p) (hq : 2 ≤ q)

65 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')

66 (htail : ∀ j, 2 ≤ tail j) :

67 SecondReductionCanonicalSecondBranchSourceTotalCase

68 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail := by

69 classical

70 dsimp [SecondReductionCanonicalSecondBranchSourceTotalCase]

71 intro k

72 letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩

73 let σ :=

74 secondReductionCanonicalSourceSignature

75 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

76 let τ :=

77 secondReductionTransportSignature (p := p) hq

78 m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail

79 let φ :=

80 secondReductionCanonicalSourceFreeQuotientHom

81 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

82 letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _

83 let e :=

84 secondReductionCanonicalSchreierBasisEquiv

85 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

86 let η :=

87 secondReductionCanonicalSchreierToTransportSecondBranchHom

88 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

89 let x : FuchsianGenerator σ :=

90 secondReductionCanonicalDistinguishedGenerator

91 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

92 let h0Gen : FuchsianGenerator σ :=

93 FuchsianGenerator.elliptic

94 (secondReductionCanonicalSourceZeroIndex

95 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)

96 let h1Gen : FuchsianGenerator σ :=

97 FuchsianGenerator.elliptic

98 (secondReductionCanonicalSourceOneIndex

99 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)

100 let y : FuchsianGenerator σ :=

101 FuchsianGenerator.elliptic

102 (secondReductionCanonicalSourceMiddleIndex

103 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨1, by omega⟩)

104 let midGen : Fin (p - 2) → FuchsianGenerator σ := fun r =>

105 FuchsianGenerator.elliptic

106 (secondReductionCanonicalSourceMiddleIndex

107 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail ⟨2 + r.val, by omega⟩)

108 let tailGen : Fin p → Fin tailLen → FuchsianGenerator σ := fun b j =>

109 FuchsianGenerator.elliptic

110 (secondReductionCanonicalSourceTailIndex

111 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j)

112 let z : φ.ker :=

113 ⟨(FreeGroup.of x) ^ k.val * totalRelation σ *

114 ((FreeGroup.of x) ^ k.val)⁻¹, by

115 change φ

116 ((FreeGroup.of x) ^ k.val * totalRelation σ *

117 ((FreeGroup.of x) ^ k.val)⁻¹) = 1

118 have hrφ : φ (totalRelation σ) = 1 :=

119 secondReductionCanonicalSourceFreeQuotientHom_respects_relators

120 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

121 (totalRelation σ) (Or.inr rfl)

122 simp only [Lean.Elab.WF.paramLet, map_mul, map_pow, hrφ, mul_one, map_inv, mul_inv_cancel]⟩

123 change η (e.symm z) ∈ Subgroup.normalClosure

124 (secondReductionCanonicalTransportBlockRelators (p := p) (q := q)

125 m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail)

126 by_cases hlast : k.val = q - 1

127 · let kLast : Fin q := ⟨q - 1, by omega⟩

128 let kZero : Fin q := ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hq⟩

129 let xk : FreeGroup (FuchsianGenerator σ) := (FreeGroup.of x) ^ (q - 1)

130 have hk : k = kLast := Fin.ext hlast

131 have hmiddleConj :

132 (List.ofFn (fun r : Fin (p - 2) =>

133 xk * FreeGroup.of (midGen r) * xk⁻¹)).prod =

134 xk * (List.ofFn (fun r : Fin (p - 2) =>

135 FreeGroup.of (midGen r))).prod * xk⁻¹ := by

136 simpa using

137 (ReidemeisterSchreier.Discrete.Presentations.conjugate_list_prod xk

138 (List.ofFn (fun r : Fin (p - 2) => FreeGroup.of (midGen r)))).symm

139 have htailConj :

140 (List.ofFn (fun b : Fin p =>

141 (List.ofFn (fun j : Fin tailLen =>

142 xk * FreeGroup.of (tailGen b j) * xk⁻¹)).prod)).prod =

143 xk *

144 (List.ofFn (fun b : Fin p =>

145 (List.ofFn (fun j : Fin tailLen =>

146 FreeGroup.of (tailGen b j))).prod)).prod *

147 xk⁻¹ := by

148 simpa using

149 ReidemeisterSchreier.Discrete.Presentations.nested_conjugate_list_prod xk

150 (fun b : Fin p => fun j : Fin tailLen => FreeGroup.of (tailGen b j))

151 have hsecondZeroCoe :

152 ((secondReductionCanonicalSecondEdgeKernelElement

153 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail kZero : φ.ker) :

154 FreeGroup (FuchsianGenerator σ)) =

155 FreeGroup.of y * xk⁻¹ := by

156 simpa [σ, φ, x, y, xk, kZero] using

157 secondReductionCanonicalSecondEdgeKernelElement_zero_coe

158 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

159 have hmiddleZeroVals :

160 (List.ofFn (fun r : Fin (p - 2) =>

161 ((secondReductionCanonicalMiddleRestZeroKernelElement

162 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r kLast : φ.ker) :

163 FreeGroup (FuchsianGenerator σ)))).prod =

164 (List.ofFn (fun r : Fin (p - 2) =>

165 xk * FreeGroup.of (midGen r) * xk⁻¹)).prod := by

166 apply congrArg List.prod

167 apply List.ofFn_inj.2

168 funext r

169 simpa [σ, φ, x, midGen, xk, kLast] using

170 secondReductionCanonicalMiddleRestZeroKernelElement_coe

171 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r kLast

172 have htailZeroVals :

173 (List.ofFn (fun b : Fin p =>

174 (((List.ofFn (fun j : Fin tailLen =>

175 secondReductionCanonicalTailZeroKernelElement

176 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j kLast)).prod :

177 φ.ker) : FreeGroup (FuchsianGenerator σ)))).prod =

178 (List.ofFn (fun b : Fin p =>

179 (List.ofFn (fun j : Fin tailLen =>

180 xk * FreeGroup.of (tailGen b j) * xk⁻¹)).prod)).prod := by

181 apply congrArg List.prod

182 apply List.ofFn_inj.2

183 funext b

184 change

185 (((List.ofFn (fun j : Fin tailLen =>

186 secondReductionCanonicalTailZeroKernelElement

187 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j kLast)).prod :

188 φ.ker) : FreeGroup (FuchsianGenerator σ)) =

189 (List.ofFn (fun j : Fin tailLen =>

190 xk * FreeGroup.of (tailGen b j) * xk⁻¹)).prod

191 rw [ReidemeisterSchreier.Discrete.Presentations.subgroup_list_prod_val]

192 apply congrArg List.prod

193 apply List.ofFn_inj.2

194 funext j

195 simpa [σ, φ, x, tailGen, xk, kLast] using

196 secondReductionCanonicalTailZeroKernelElement_coe

197 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j kLast

198 have hsecondZeroCoe0 :

199 ((secondReductionCanonicalSecondEdgeKernelElement

200 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail (0 : Fin q) :

201 φ.ker) : FreeGroup (FuchsianGenerator σ)) =

202 FreeGroup.of y * xk⁻¹ := by

203 simpa [kZero] using hsecondZeroCoe

204 have hmiddleZeroVals' :

205 (List.ofFn (Subtype.val ∘ fun r : Fin (p - 2) =>

206 secondReductionCanonicalMiddleRestZeroKernelElement

207 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r kLast)).prod =

208 (List.ofFn (fun r : Fin (p - 2) =>

209 xk * FreeGroup.of (midGen r) * xk⁻¹)).prod := by

210 simpa only [Function.comp_apply] using hmiddleZeroVals

211 have htailZeroVals' :

212 (List.ofFn (Subtype.val ∘ fun b : Fin p =>

213 (List.ofFn (fun j : Fin tailLen =>

214 secondReductionCanonicalTailZeroKernelElement

215 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j kLast)).prod)).prod =

216 (List.ofFn (fun b : Fin p =>

217 (List.ofFn (fun j : Fin tailLen =>

218 xk * FreeGroup.of (tailGen b j) * xk⁻¹)).prod)).prod := by

219 simpa only [Function.comp_apply] using htailZeroVals

220 have hkerEq :

221 z =

222 secondReductionCanonicalHeadZeroKernelElement

223 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail kLast *

224 secondReductionCanonicalHeadOneKernelElement

225 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail kLast *

226 secondReductionCanonicalFirstPowerKernel

227 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail *

228 secondReductionCanonicalSecondEdgeKernelElement

229 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail kZero *

230 (List.ofFn (fun r : Fin (p - 2) =>

231 secondReductionCanonicalMiddleRestZeroKernelElement

232 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r kLast)).prod *

233 (List.ofFn (fun b : Fin p =>

234 (List.ofFn (fun j : Fin tailLen =>

235 secondReductionCanonicalTailZeroKernelElement

236 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j kLast)).prod)).prod := by

237 apply Subtype.ext

238 change

239 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val * totalRelation σ *

240 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ =

241 (((secondReductionCanonicalHeadZeroKernelElement

242 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail kLast *

243 secondReductionCanonicalHeadOneKernelElement

244 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail kLast *

245 secondReductionCanonicalFirstPowerKernel

246 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail *

247 secondReductionCanonicalSecondEdgeKernelElement

248 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail kZero *

249 (List.ofFn (fun r : Fin (p - 2) =>

250 secondReductionCanonicalMiddleRestZeroKernelElement

251 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r kLast)).prod *

252 (List.ofFn (fun b : Fin p =>

253 (List.ofFn (fun j : Fin tailLen =>

254 secondReductionCanonicalTailZeroKernelElement

255 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j kLast)).prod)).prod : φ.ker) :

256 FreeGroup (FuchsianGenerator σ)))

257 rw [secondReductionCanonicalSource_totalRelation_eq

258 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail]

259 rw [hk]

260 simp only [secondReductionCanonicalDistinguishedGenerator, xWord, mul_assoc, Lean.Elab.WF.paramLet,

261 Fin.mk_zero', Subgroup.coe_mul, secondReductionCanonicalHeadZeroKernelElement_coe,

262 secondReductionCanonicalHeadOneKernelElement_coe, secondReductionCanonicalFirstPowerKernel_coe,

263 Subgroup.val_list_prod, List.map_ofFn, inv_mul_cancel_left, mul_right_inj, σ, x, kLast, kZero]

264 rw [hsecondZeroCoe0, hmiddleZeroVals', htailZeroVals']

265 rw [hmiddleConj, htailConj]

266 have hpow :

267 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ q =

268 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ (q - 1) *

269 FreeGroup.of x := by

270 have hq' : q = q - 1 + 1 := by omega

271 rw [hq', pow_succ]

272 have hnat : q - 1 + 1 - 1 = q - 1 := by omega

273 rw [hnat]

274 rw [hpow]

275 simp only [secondReductionCanonicalDistinguishedGenerator, conj_mul, x, y, xk, midGen, tailGen]

276 group

277 have hwrap :=

278 secondReductionCanonicalSchreierToTransportSecondBranch_wrapTotalRelator_image_eq_one

279 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

280 rw [hkerEq]

281 simp only [map_mul]

282 have hEq :

283 η ((MulEquiv.symm e)

284 (secondReductionCanonicalHeadZeroKernelElement

285 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail kLast)) *

286 η ((MulEquiv.symm e)

287 (secondReductionCanonicalHeadOneKernelElement

288 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail kLast)) *

289 η ((MulEquiv.symm e)

290 (secondReductionCanonicalFirstPowerKernel

291 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)) *

292 η ((MulEquiv.symm e)

293 (secondReductionCanonicalSecondEdgeKernelElement

294 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail kZero)) *

295 η ((MulEquiv.symm e)

296 (List.ofFn (fun r : Fin (p - 2) =>

297 secondReductionCanonicalMiddleRestZeroKernelElement

298 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r kLast)).prod) *

299 η ((MulEquiv.symm e)

300 (List.ofFn (fun b : Fin p =>

301 (List.ofFn (fun j : Fin tailLen =>

302 secondReductionCanonicalTailZeroKernelElement

303 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j kLast)).prod)).prod) =

304 1 := by

305 simpa [σ, e, η, kLast, kZero, Function.comp_def, map_list_prod, List.map_ofFn]

306 using hwrap

307 rw [hEq]

308 exact Subgroup.one_mem _

309 · let knw : Fin (q - 1) := ⟨k.val, by omega⟩

310 let k0 : Fin q := ⟨knw.val, by omega⟩

311 let k1 : Fin q := ⟨knw.val + 1, by omega⟩

312 let xk : FreeGroup (FuchsianGenerator σ) := (FreeGroup.of x) ^ k.val

313 have hk0 : k = k0 := by

314 ext

315 simp only [knw, k0]

316 have hmiddleConj :

317 (List.ofFn (fun r : Fin (p - 2) =>

318 xk * FreeGroup.of (midGen r) * xk⁻¹)).prod =

319 xk * (List.ofFn (fun r : Fin (p - 2) =>

320 FreeGroup.of (midGen r))).prod * xk⁻¹ := by

321 simpa using

322 (ReidemeisterSchreier.Discrete.Presentations.conjugate_list_prod xk

323 (List.ofFn (fun r : Fin (p - 2) => FreeGroup.of (midGen r)))).symm

324 have htailConj :

325 (List.ofFn (fun b : Fin p =>

326 (List.ofFn (fun j : Fin tailLen =>

327 xk * FreeGroup.of (tailGen b j) * xk⁻¹)).prod)).prod =

328 xk *

329 (List.ofFn (fun b : Fin p =>

330 (List.ofFn (fun j : Fin tailLen =>

331 FreeGroup.of (tailGen b j))).prod)).prod *

332 xk⁻¹ := by

333 simpa using

334 ReidemeisterSchreier.Discrete.Presentations.nested_conjugate_list_prod xk

335 (fun b : Fin p => fun j : Fin tailLen => FreeGroup.of (tailGen b j))

336 have hsecondSuccCoe :

337 ((secondReductionCanonicalSecondEdgeKernelElement

338 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail

339 ⟨k.val + 1, by omega⟩ : φ.ker) :

340 FreeGroup (FuchsianGenerator σ)) =

341 (FreeGroup.of x) ^ (k.val + 1) * FreeGroup.of y * xk⁻¹ := by

342 simpa [σ, φ, x, y, xk, knw] using

343 secondReductionCanonicalSecondEdgeKernelElement_succ_coe

344 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail knw

345 have hmiddleZeroVals :

346 (List.ofFn (Subtype.val ∘ fun r : Fin (p - 2) =>

347 secondReductionCanonicalMiddleRestZeroKernelElement

348 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r k)).prod =

349 (List.ofFn (fun r : Fin (p - 2) =>

350 xk * FreeGroup.of (midGen r) * xk⁻¹)).prod := by

351 apply congrArg List.prod

352 apply List.ofFn_inj.2

353 funext r

354 simpa [σ, φ, x, midGen, xk] using

355 secondReductionCanonicalMiddleRestZeroKernelElement_coe

356 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r k

357 have htailZeroVals :

358 (List.ofFn (Subtype.val ∘ fun b : Fin p =>

359 (List.ofFn (fun j : Fin tailLen =>

360 secondReductionCanonicalTailZeroKernelElement

361 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j k)).prod)).prod =

362 (List.ofFn (fun b : Fin p =>

363 (List.ofFn (fun j : Fin tailLen =>

364 xk * FreeGroup.of (tailGen b j) * xk⁻¹)).prod)).prod := by

365 apply congrArg List.prod

366 apply List.ofFn_inj.2

367 funext b

368 change

369 (((List.ofFn (fun j : Fin tailLen =>

370 secondReductionCanonicalTailZeroKernelElement

371 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j k)).prod :

372 φ.ker) : FreeGroup (FuchsianGenerator σ)) =

373 (List.ofFn (fun j : Fin tailLen =>

374 xk * FreeGroup.of (tailGen b j) * xk⁻¹)).prod

375 rw [ReidemeisterSchreier.Discrete.Presentations.subgroup_list_prod_val]

376 apply congrArg List.prod

377 apply List.ofFn_inj.2

378 funext j

379 simpa [σ, φ, x, tailGen, xk] using

380 secondReductionCanonicalTailZeroKernelElement_coe

381 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j k

382 have hkerEq :

383 z =

384 secondReductionCanonicalHeadZeroKernelElement

385 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k0 *

386 secondReductionCanonicalHeadOneKernelElement

387 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k0 *

388 secondReductionCanonicalSecondEdgeKernelElement

389 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k1 *

390 (List.ofFn (fun r : Fin (p - 2) =>

391 secondReductionCanonicalMiddleRestZeroKernelElement

392 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r k0)).prod *

393 (List.ofFn (fun b : Fin p =>

394 (List.ofFn (fun j : Fin tailLen =>

395 secondReductionCanonicalTailZeroKernelElement

396 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j k0)).prod)).prod := by

397 apply Subtype.ext

398 change

399 (FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val * totalRelation σ *

400 ((FreeGroup.of x : FreeGroup (FuchsianGenerator σ)) ^ k.val)⁻¹ =

401 (((secondReductionCanonicalHeadZeroKernelElement

402 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k0 *

403 secondReductionCanonicalHeadOneKernelElement

404 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k0 *

405 secondReductionCanonicalSecondEdgeKernelElement

406 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k1 *

407 (List.ofFn (fun r : Fin (p - 2) =>

408 secondReductionCanonicalMiddleRestZeroKernelElement

409 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r k0)).prod *

410 (List.ofFn (fun b : Fin p =>

411 (List.ofFn (fun j : Fin tailLen =>

412 secondReductionCanonicalTailZeroKernelElement

413 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j k0)).prod)).prod : φ.ker) :

414 FreeGroup (FuchsianGenerator σ)))

415 rw [secondReductionCanonicalSource_totalRelation_eq

416 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail]

417 rw [hk0]

418 simp only [secondReductionCanonicalDistinguishedGenerator, xWord, mul_assoc, Lean.Elab.WF.paramLet, Fin.eta,

419 Subgroup.coe_mul, secondReductionCanonicalHeadZeroKernelElement_coe,

420 secondReductionCanonicalHeadOneKernelElement_coe, Subgroup.val_list_prod, List.map_ofFn, inv_mul_cancel_left,

421 mul_right_inj, σ, x, k0, k1, knw]

422 rw [hsecondSuccCoe, hmiddleZeroVals, htailZeroVals]

423 rw [hmiddleConj, htailConj]

424 simp only [secondReductionCanonicalDistinguishedGenerator, conj_mul, x, y, xk, midGen, tailGen]

425 group

426 have hnonwrap :=

427 secondReductionCanonicalSchreierToTransportSecondBranch_nonwrapTotalRelator_image_eq_one

428 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail knw

429 rw [hkerEq]

430 simp only [map_mul]

431 have hEq :

432 η ((MulEquiv.symm e)

433 (secondReductionCanonicalHeadZeroKernelElement

434 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k0)) *

435 η ((MulEquiv.symm e)

436 (secondReductionCanonicalHeadOneKernelElement

437 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k0)) *

438 η ((MulEquiv.symm e)

439 (secondReductionCanonicalSecondEdgeKernelElement

440 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k1)) *

441 η ((MulEquiv.symm e)

442 (List.ofFn (fun r : Fin (p - 2) =>

443 secondReductionCanonicalMiddleRestZeroKernelElement

444 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r k0)).prod) *

445 η ((MulEquiv.symm e)

446 (List.ofFn (fun b : Fin p =>

447 (List.ofFn (fun j : Fin tailLen =>

448 secondReductionCanonicalTailZeroKernelElement

449 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j k0)).prod)).prod) =

450 1 := by

451 simpa [σ, e, η, knw, k0, k1, Function.comp_def, map_list_prod, List.map_ofFn]

452 using hnonwrap

453 rw [hEq]

454 exact Subgroup.one_mem _

455

456end FenchelNielsen