tactic.customEliminators

Default value: true

enable using custom eliminators in the induction and cases tactics defined using the @[induction_eliminator] and @[cases_eliminator] attributes

tactic.skipAssignedInstances

Default value: true

in the rw and simp tactics, if an instance implicit argument is assigned, do not try to synthesize instance.

tactic.simp.trace

Default value: false

When tracing is enabled, calls to simp or dsimp will print an equivalent simp only call.