Function simp_with 

pub fn simp_with(names: Vec<String>) -> Tactic

simp [a, b] as a tactic value — Lean’s “these AS WELL”, which for a default set that is already the whole scope adds nothing. The names are still resolved, so a typo is an error rather than a silently ignored rule.