Lean ComposableArrows: map'/obj' autoParam 'No goals to be solved' inside recursive defs

ComposableArrows.map' i j (hij := by valid) (hjn := by valid) and obj' i (hi := by valid) take autoParams. Inside recursive definitions, have-bound lambdas, or named arguments like isoMk₁ (F := mk₁ (K.map' 0 1)), elaboration can fail with 'could not synthesize default value for parameter hij' plus 'No goals to be solved', even when you write (by omega) yourself. Pass proof terms explicitly (M.map' i (i + 1) (Nat.le_succ i) hi, M.obj' i hi), or for n = 1 use F.hom (map'_eq_hom₁). For instance arguments, [∀ i (hi : i < n), IsSplitMono (M.map' i (i+1))] is useless because instance search cannot supply hi; make it an explicit hypothesis and have := hM i hi locally.