linter.fugue.inductionWith

induction / fun_induction carry their cases in with | name => …, checked for exhaustiveness — a forgotten constructor is an error at the induction, not a goal that survives to the end of the proof. Never bare case name => blocks after the tactic.