§ Testing infra in Lean4