From 3d401e0bb3b0295605d8083d5683efd6dbbea2eb Mon Sep 17 00:00:00 2001
From: Gio <102917377+gio256@users.noreply.github.com>
Date: Fri, 22 Nov 2024 18:29:55 +0000
Subject: [PATCH] feat(AlgebraicTopology/SimplicialSet): Add auxiliary ext
 lemma for paths (#19349)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

We implement the generalization of the path extensionality lemmas suggested by @joelriou in #19057. Two paths of the same nonzero length can be identified by constructing an identification between each of their arrows.

Co-Authored-By: [Joël Riou](https://github.com/joelriou)
---
 Mathlib/AlgebraicTopology/SimplicialSet/Path.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/Path.lean b/Mathlib/AlgebraicTopology/SimplicialSet/Path.lean
index 696d2c7aa9498..047e74c18ff93 100644
--- a/Mathlib/AlgebraicTopology/SimplicialSet/Path.lean
+++ b/Mathlib/AlgebraicTopology/SimplicialSet/Path.lean
@@ -73,4 +73,16 @@ lemma spine_map_subinterval {n : ℕ} (j l : ℕ) (hjl : j + l ≤ n) (Δ : X _[
   · simp only [spine_arrow, Path.interval, ← FunctorToTypes.map_comp_apply, ← op_comp,
       mkOfSucc_subinterval_eq]
 
+/-- Two paths of the same nonzero length are equal if all of their arrows are equal. -/
+@[ext]
+lemma Path.ext' {n : ℕ} {f g : Path X (n + 1)}
+    (h : ∀ i : Fin (n + 1), f.arrow i = g.arrow i) :
+    f = g := by
+  ext j
+  · rcases Fin.eq_castSucc_or_eq_last j with ⟨k, hk⟩ | hl
+    · rw [hk, ← f.arrow_src k, ← g.arrow_src k, h]
+    · simp only [hl, ← Fin.succ_last]
+      rw [← f.arrow_tgt (Fin.last n), ← g.arrow_tgt (Fin.last n), h]
+  · exact h j
+
 end SSet