English
For p, q, r paths, the two ways of associating concatenations are equal after a specific reparametrization.
Русский
Для путей p, q, r две формы склейки путей эквивалентны при заданной переparametrизации.
LaTeX
$$$$ (p \\star q) \\star r = (p \\star (q \\star r)).\\mathrm{reparam}\\Bigl( t \\mapsto \\langle \\mathrm{transAssocReparamAux}(t), \\mathrm{transAssocReparamAux\\_mem\\_I}(t) \\rangle \\Bigr). $$$$
Lean4
theorem trans_assoc_reparam {x₀ x₁ x₂ x₃ : X} (p : Path x₀ x₁) (q : Path x₁ x₂) (r : Path x₂ x₃) :
(p.trans q).trans r =
(p.trans (q.trans r)).reparam (fun t => ⟨transAssocReparamAux t, transAssocReparamAux_mem_I t⟩) (by fun_prop)
(Subtype.ext transAssocReparamAux_zero) (Subtype.ext transAssocReparamAux_one) :=
by
ext x
simp only [transAssocReparamAux, Path.trans_apply, Function.comp_apply, mul_ite, Path.coe_reparam]
-- TODO: why does split_ifs not reduce the ifs??????
split_ifs with h₁ h₂ h₃ h₄ h₅
· rfl
iterate 6 exfalso; linarith
· have h : 2 * (2 * (x : ℝ)) - 1 = 2 * (2 * (↑x + 1 / 4) - 1) := by linarith
simp [h]
iterate 6 exfalso; linarith
· congr
ring
