Note: I have pushed an update to the lean toolchain because this PR was on a buggy version of the toolchain. WARNING: checking out old commits of this PR using v4.2.0-rc2 or v4.2.0-rc3 can cause lake clean to delete your mathlib folder! If you need to do so, make sure to delete lakefile.olean manually before running any lake commands.

I'm not sure what the value of such a PR is. On one hand, you make the proofs less likely to break due to the addition of a lemma in the simp set. On the other hand, proofs now refer explicitly to more lemmas that are susceptible to change in ways that a fancy tactic call wouldn't have noticed.

I am sympathetic to this argument. However, I think most maintainers are on the side of "nonterminal simps are bad". I have gotten reviews before telling me to remove nonterminal simps. The point of this PR is to make way for #7496 so that reviewers hopefully don't have to do this as often.

I will revert the things you suggest and also make the style PR more lax so that they don't conflict.

Not sure what this error means.

Error: ./././Mathlib/Algebra/FreeAlgebra.lean:577:2: error: Failed to parse tactic output: simp only [AlgHom.ext_iff, AlgHom.coe_id, id_eq, AlgHom.coe_comp, Subalgebra.coe_val, Function.comp_apply] at
of_id 

What I currently have is

  simp? [AlgHom.ext_iff] at of_id says
    simp only [AlgHom.ext_iff, AlgHom.coe_id, id_eq, AlgHom.coe_comp, Subalgebra.coe_val,
      Function.comp_apply] at of_id

Annoyingly, my file builds this just fine in the IDE, but CI is saying it's broken. If I delete what's after the says

  simp? [AlgHom.ext_iff] at of_id says

Then the IDE gives the suggestion, but also the same error as CI.

  simp? [AlgHom.ext_iff] at of_id

Is fine, but not what I am trying to do.

You should be able to reproduce the additional testing that says does in CI using lake build -KCI Mathlib.X.Y.Z. Or put set_option says.verify true in the failing files.

I've improved the error message in CI in #9061.

I merged master, and then looked at the first two errors: both were resolved by replacing the current RHS with what says is now suggesting.

I'll hand it back over to you to look at the remainder?

Thanks!

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Check all files imported