English
If i ≤ j ≤ k are indices in Fin(n+1+1), then the map from i to k equals the composition of the map from i to j with the map from j to k: map F f i k (hij.trans hjk) = map F f i j hij ≫ map F f j k hjk.
Русский
Если индексы i ≤ j ≤ k, то отображение от i до k равняется композиции отображений i→j и j→k: map F f i k ... = map F f i j ... ≫ map F f j k ...
LaTeX
$$$$ map\\ F\\ f\\ i\\ k\\ (hij.trans hjk) = map\\ F\\ f\\ i\\ j\\ hij \\;≫\\; map\\ F\\ f\\ j\\ k\\ hjk $$$$
Lean4
theorem map_comp {i j k : Fin (n + 1 + 1)} (hij : i ≤ j) (hjk : j ≤ k) :
map F f i k (hij.trans hjk) = map F f i j hij ≫ map F f j k hjk :=
by
obtain ⟨i, hi⟩ := i
obtain ⟨j, hj⟩ := j
obtain ⟨k, hk⟩ := k
cases i
· obtain _ | _ | j := j
· dsimp
rw [id_comp]
· obtain _ | _ | k := k
· simp at hjk
· simp
· rfl
· obtain _ | _ | k := k
· simp [Fin.ext_iff] at hjk
· simp [Fin.le_def] at hjk
· dsimp
rw [assoc, ← F.map_comp, homOfLE_comp]
· obtain _ | j := j
· simp [Fin.ext_iff] at hij
· obtain _ | k := k
· simp [Fin.ext_iff] at hjk
· dsimp
rw [← F.map_comp, homOfLE_comp]
