continuity? says rename_i

Stream: mathlib4

[Johan Commelin]

Please see https://github.com/leanprover-community/mathlib4/pull/6286/commits/834a33548266330033b07c9b32b812f0d6cf2c6d
The continuity? tactic somehow spits out a call to rename_i that is not needed. As a result, the unused variable linter complains, if you copy that line. But if you don't copy the line, then the says combinator is unhappy.

cc @Scott Morrison

[Scott Morrison]

This is output from aesop?

[Johan Commelin]

Hmm, probably, under the hood, yes. Since continuity? is probably implemented using aesop?.

[Adomas Baliuka]

It is aesop, yes.

[Jannis Limperg]

Removing this is on the todo list, but it's a bit tricky. More generally, I don't think it's realistic to assume that Aesop will in future reliably produce tactic scripts that satisfy all linters. Maybe the linters should be disabled in says?

[Adomas Baliuka]

I regularly have to delete lines (or fix indentation) from aesop? output to make the proof work in the first place, which seems weird (I would have thought aesop and aesop? do the same thing and the only difference is that aesop? prints it...)

[Jannis Limperg]

The first line being mis-indented should be fixed now (but I'm not sure whether mathlib uses the right version yet). If the proof doesn't work even after indentation fixes, that's a bug and I'd appreciate a report.