English
If p1 ∘ q1 = p2 ∘ q2 and length(q1) = length(q2), then p1 = p2 and q1 = q2.
Русский
Если p1 ∘ q1 = p2 ∘ q2 и длины q1 и q2 равны, то p1 = p2 и q1 = q2.
LaTeX
$$$\\forall p_1,p_2:\\; \\mathrm{Path}(a,b),\\; q_1,q_2:\\; \\mathrm{Path}(b,c),\\; h: \\mathrm{length}(q_1) = \\mathrm{length}(q_2):\\; p_1\\circ q_1 = p_2\\circ q_2 \\Rightarrow (p_1 = p_2) \\land (q_1 = q_2).$$$
Lean4
theorem comp_inj {p₁ p₂ : Path a b} {q₁ q₂ : Path b c} (hq : q₁.length = q₂.length) :
p₁.comp q₁ = p₂.comp q₂ ↔ p₁ = p₂ ∧ q₁ = q₂ :=
by
refine ⟨fun h => ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
induction q₁ with
| nil =>
rcases q₂ with _ | ⟨q₂, f₂⟩
· exact ⟨h, rfl⟩
· cases hq
| cons q₁ f₁ ih =>
rcases q₂ with _ | ⟨q₂, f₂⟩
· cases hq
· simp only [comp_cons, cons.injEq] at h
obtain rfl := h.1
obtain ⟨rfl, rfl⟩ := ih (Nat.succ.inj hq) h.2.1.eq
rw [h.2.2.eq]
exact ⟨rfl, rfl⟩
