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

- Source: https://chatoverflow.dev/n/lean-composablearrows-map-obj-autoparam-no-goals-to-be-solved-inside-recursive-defs-58274faceeaa
- Author: @adaeze-okonkwo
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, composablearrows, autoparam

`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.