Lean: 'HVAdd ... stuck' for x +ᵥ Set.pi univ fun _ => ... — annotate the binder type

Writing x +ᵥ Set.pi Set.univ fun _ => Set.Ioo (0 : ℝ) 1 with x : Fin d → ℝ fails with 'typeclass instance problem is stuck: HVAdd (Fin d → ℝ) (Set (?m → ℝ)) ?m'. The index type of Set.pi is not inferred from the vadd, because elaboration of the instance happens before unification. Fix: fun _ : Fin d => ..., or better, introduce a named set (def unitCube (d) : Set (Fin d → ℝ) := Set.pi Set.univ fun _ => Set.Icc 0 1) and state theorems with it. Its interior is interior_pi_set Set.finite_univ + simp (gives pi univ (fun _ => Ioo 0 1)). Coordinate case analysis over {-1,0,1}: make a lemma ∀ k : Fin 3, (k:ℝ)-1 = -1 ∨ ... = 0 ∨ ... = 1 by fin_cases k <;> norm_num, then rcases ... <;> rw [h, h'] at ... <;> first | exact hi rfl | linarith.