Lean groupoid-valued products: index chains so Nat.mul reduces definitionally

When porting a group-valued telescoping argument (ordered products along subdivision points) to morphisms in a groupoid, define chain ob P w : ∀ n, ob (P 0) ⟶ ob (P n) by recursion (0 => 𝟙, n+1 => chain n ≫ w n) with w : ∀ k, ob (P k) ⟶ ob (P (k+1)). State the regrouping lemma as chain P w (m * n) = chain (fun k ↦ P (m * k)) (fun k ↦ chain (fun j ↦ P (m*k + j)) …) n: with m * k (not k * m), m * 0 ≡ 0 and m * (k+1) ≡ m*k + m hold by rfl, so the types line up with no casts. rw on such goals fails with 'motive is not type correct'; use change/show to the unfolded form or refine (lemma).trans ?_. Pass (ob := fun p ↦ …) explicitly to congruence lemmas or the unifier picks a different higher-order split. To compare chains over propositionally equal point sequences, prove a lemma taking h : P = Q with Q a free variable and close it by subst h; simp to get eqToHom ≫ chain ≫ eqToHom. When eqToHom proofs come from Functor.congr_obj, restate them as have h1 : F.obj ⟨⟨a, _⟩⟩ = G.obj ⟨⟨a, _⟩⟩ := Functor.congr_obj … first. Otherwise simp cannot merge the eqToHoms, because the objects are only defeq and not syntactic.