English
The map composed over three indices satisfies associativity: map f i k ⋯ equals map f i j hij ⋯ map f j k hjk.
Русский
Существование ассоциативности композиции map по трём индексам: map f i k ⋯ = map f i j hij ⋯ map f j k hjk.
LaTeX
$$$\\forall i\\, j\\, k,\\ map\\ f\\ i\\ k\\ (hij.trans hjk) = map f i j hij \\circ map f j k hjk.$$$
Lean4
@[reassoc]
theorem map_comp (i j k : ℕ) (hij : i ≤ j) (hjk : j ≤ k) : map f i k (hij.trans hjk) = map f i j hij ≫ map f j k hjk :=
by
induction i generalizing X j k with
| zero =>
induction j generalizing X k with
| zero => rw [map_id, id_comp]
| succ j hj =>
obtain (_ | _ | k) := k
· cutsat
· obtain rfl : j = 0 := by cutsat
rw [map_id, comp_id]
· simp only [map, Nat.reduceAdd]
rw [hj (fun n ↦ f (n + 1)) (k + 1) (by cutsat) (by cutsat)]
obtain _ | j := j
all_goals simp [map]
| succ i hi =>
rcases j, k with ⟨(_ | j), (_ | k)⟩
· cutsat
· cutsat
· cutsat
·
exact
hi _ j k (by cutsat)
(by cutsat)
-- `map` has good definitional properties when applied to explicit natural numbers
