useless equalities

Stream: general

[Damiano Testa]

In the process of porting a file, I think that one of the results is now redundant (presumably thanks to the new way in which coercions are handled). The result is an equality between two submodules.
To check that this result is no longer needed, I did

set_option pp.all true
#print possiblyUselessTheorem

and verified that the two explicit inputs to the corresponding Eq application are identical.

Does this justify removing the lemma? Could this lemma still be useful for something?

Thank!

[Anatole Dedecker]

You should double check that the statement indeed corresponds to the one in Lean 3, sometimes the statement written by mathport isn’t parsed in the same way so the statement becomes trivial. But if that is the case I think you can freely remove it.

[Damiano Testa]

the two statements are

@[norm_cast] lemma lie_ideal.coe_to_lie_subalgebra_to_submodule (I : lie_ideal R L) :
  ((I : lie_subalgebra R L) : submodule R L) = I := rfl

@[norm_cast]
theorem LieIdeal.coe_toLieSubalgebra_toSubmodule (I : LieIdeal R L) :
    ((I : LieSubalgebra R L) : Submodule R L) = I := rfl

They look pretty similar to me! Is this enough? I feel really uncomfortable about this, for some reason...

[Damiano Testa]

The double coercion is pretty printed as a double coercion in Lean3, but not in Lean4. In fact, in Lean 4 the output of the pp.all thing is exactly the same on the two sides of the equality.

[Damiano Testa]

(The only reason I picked up on this is because the norm_cast linter flagged it as badly shaped lemma, rhs can't start with coe ↑(lieIdealSubalgebra R L I).)

[Anne Baanen]

Double coercions are indeed implemented differently in Lean 4, so I agree that this is probably safe to remove. Doesn't the syntactic tautology linter check for this?

[Damiano Testa]

I did not even know that a syntactic tautology linter existed!

[Damiano Testa]

/- The `synTaut` linter reports:
THE FOLLOWING DECLARATIONS ARE SYNTACTIC TAUTOLOGIES.
This usually means that they are of the form `∀ a b ... z, e₁ = e₂` where `e₁` and `e₂` are identical expressions.
We call declarations of this form syntactic tautologies.
Such lemmas are (mostly) useless and sometimes introduced unintentionally when proving basic facts using `rfl`,
when elaboration results in a different term than the user intended. You should check that the declaration really
says what you think it does. -/
#check LieIdeal.coe_toLieSubalgebra_toSubmodule /- LHS equals RHS syntactically -/

[Damiano Testa]

Thanks Anne!

[Damiano Testa]

I fewer norm_cast problem to worry about!