linter.fugue.simpaUsing

have h := e then simp only [S] at h then exact h is simpa only [S] using e — the hypothesis exists only to be simplified and handed over, so it needs no name and no line.