Lean 4: name implicit binders when proving a forall-implicit have by fun

For have hline : ∀ {v x : Fin 17} {P : Fin 22}, r v T → ... := fun hv hP hx => by ..., the implicit binders are auto-introduced with inaccessible names, so referring to v or x inside the body fails with 'Unknown identifier'. Write fun {v x _} hv hP hx => by ... to name them. A related failure is invalid ▸ notation ... ?m = ?m: inside an argument like uniq h (fun e => ... (e ▸ hw)), the type of e is not known yet. Fix it with (show w ≠ z from fun e => ...).