weird linter warning

Stream: mathlib4

[David Loeffler]

I just made a PR to split up Analysis/Calculus/FDeriv/Basic.lean (#25207), since the file is perilously close to the 1500-line limit and one of my under-review PR's would push it over.

For some reason the file-split PR is failing CI with a linter warning in some completely unrelated code:

Running linter on specified module: Mathlib
-- Found 1 error in 252888 declarations (plus 546163 automatically generated ones) in Mathlib with 15 linters
/- The `unusedHavesSuffices` linter reports:
THE FOLLOWING DECLARATIONS HAVE INEFFECTUAL TERM MODE HAVE/SUFFICES BLOCKS. In the case of `have` this is a term of the form `have h := foo, bar` where `bar` does not refer to `foo`. Such statements have no effect on the generated proof, and can just be replaced by `bar`, in addition to being ineffectual, they may make unnecessary assumptions in proofs appear as if they are used. For `suffices` this is a term of the form `suffices h : foo, proof_of_goal, proof_of_foo` where `proof_of_goal` does not refer to `foo`. Such statements have no effect on the generated proof, and can just be replaced by `proof_of_goal`, in addition to being ineffectual, they may make unnecessary assumptions in proofs appear as if they are used. -/
-- Mathlib.Analysis.Complex.Angle
Error: /home/lean/actions-runner/_work/mathlib4/mathlib4/Mathlib/Analysis/Complex/Angle.lean:33:1: error: @Complex.angle_eq_abs_arg unnecessary have this : ‖y‖ ≠
  0

Of course it is trivial to fix this, and I have pushed a one-line fix to that PR, but I am puzzled why I am seeing this build failure as part of CI for a completely unrelated PR – did some failing code somehow get merged into master, or does my PR somehow randomly perturb stuff downstream (maybe changing which simp lemmas get used) that exposes the error somehow?

[Yaël Dillies]

Probably what happened is that some simp call was using the unnecessary hypothesis previously, and is not using it after your change because it perturbed the discr tree for simp lemmas

[David Loeffler]

Fair enough! I am surprised that splitting one big file into several smaller ones would have that effect, but the workings of the simplifier are a mystery to me

[Kevin Buzzard]

If you want to chase this up further I guess you could squeeze the simp before and after and see if you get different answers.

[David Loeffler]

TBH I just want to stop the long-file-linter blocking me from getting my modular forms PR's reviewed; I'm not particularly motivated to chase it up any more than necessary.