aligns without content?

Stream: mathlib4

[Heather Macbeth]

The mathport output in
https://github.com/leanprover-community/mathlib3port/blob/master/Mathbin/Algebra/Order/Monoid/Lemmas.lean
contains a lot of align statements in which the "before" and "after" names seem to be the same, such as

#align mul_le_mul_right' mul_le_mul_right'

Do these have any function? Can they be deleted?

[Jireh Loreaux]

I could be wrong, but I think this is the result of the discussion last week during meeting about mathport #aligning more statements. The idea being that it's easier to just delete the line if it's not necessary than to type most of it again.

[Heather Macbeth]

Thanks. So I should indeed delete them?

[Mario Carneiro]

you should delete them if you aren't planning a rename, yes