Redundant variable declaration

Stream: mathlib4

[Martin Dvořák]

There are places in Mathlib where the same variable is declared twice. For example here:
https://github.com/leanprover-community/mathlib4/blob/cc016b6463c62bb4ae5ddb751734ee4d41a6f811/Mathlib/Algebra/Group/Basic.lean#L255

First, the variables a and b are declared for the section:

variable [InvolutiveInv G] {a b : G}

Then a theorem repeats the same arguments:

theorem inv_inj {a b : G} : a⁻¹ = b⁻¹ ↔ a = b

Are we going to going to remove these redundant variable declarations in an organized/automated manner, or should I just create a cleanup PR (chore) whenever I stumble across such a declaration?

[Eric Wieser]

The duplicates in the theorem often aren't redundant, sometimes they change the order of the variables to something more desirable (yours is not an example of this)

[Eric Wieser]

The one in the variable line can be removed safely, but probably it's used by another lemma

[Martin Dvořák]

Most theorems use the "global" ones in this section. I wanted to remove them from here:

theorem inv_inj {a b : G}

[Martin Dvořák]

What is the general recommendation? When I notice an undesirably redundancy, should I create a PR to remove it?

[Eric Wieser]

I would say leave it be, unless it annoys you enough to write a linter to prevent it happening in future

[Martin Dvořák]

I don't have skills to write a linter. I only have skills to manually remove it when I see it.

[Eric Wieser]

The problem with these redundancies is that there are two directions they can be resolved, and deciding is a game of bike-shedding

[Martin Dvořák]

I am not going to make a general policy, but I think I can safely say that whenever both global and local declaration exist and the global declaration is actually used => remove the local declaration.

[Eric Wieser]

If one lemma uses the global declaration and the other 10 in the section use local declarations, are you sure that approach makes sense?

[Martin Dvořák]

Don't we want to use global declarations in precisely these situations?
(when the same local declaration repeats many times)

[Eric Wieser]

What if you have a section like:

variable {X : Type*} {a b : X}
theorem t1 (a b : X) : a = b := sorry
theorem t2 {a b : X} : a = b := sorry
theorem t3 [DecidableEq X] {a b : X} : a = b := sorry
theorem t4 : a = b := sorry

[Eric Wieser]

What would your proposed fix be?

[Martin Dvořák]

As I said, I don't have ambitions to make a general policy about that.
However, my gut feeling says that all local {a b : X} should be removed.

[Eric Wieser]

That changes the type of t3, breaks consistency between t2 and t1, and results in a larger patch

[Martin Dvořák]

I see your point; I am just saying what my gut feeling is.