problem with simp normal form for linear_isometry_equiv

Stream: general

[Scott Morrison]

We seem to have a problem back in mathlib3 about simp normal form for turning a linear_isometry_equiv into a linear_map:

import analysis.normed_space.linear_isometry

variables {E F : Type*} [seminormed_add_comm_group E] [seminormed_add_comm_group F]
variables {R S : Type*} [semiring R] [semiring S] [module R E]
  [module S F] {σ₁₂ : R →+* S} {σ₂₁ : S →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂]

include σ₂₁

example (e : E ≃ₛₗᵢ[σ₁₂] F) : (e.to_linear_equiv : E →ₛₗ[σ₁₂] F) = e.to_linear_map := by simp -- fails!

Would someone be willing to look into this for me?

@Yury G. Kudryashov, @Frédéric Dupuis, @Heather Macbeth are listed as the authors of linear_isometry.lean, so I'll ping them here. :-)

[Scott Morrison]

Relatedly, it's curious that:

-- We have a coercion from linear equivalences to linear maps:
example (e : E ≃ₛₗ[σ₁₂] F) : E →ₛₗ[σ₁₂] F := e -- succeeds

-- But no corresponding coercion from linear isometry equivalences to linear isometries?
example (e : E ≃ₛₗᵢ[σ₁₂] F) : E →ₛₗᵢ[σ₁₂] F := e -- fails

and perhaps that (and deciding the simp normal form, and implementing it) could be fixed at the same time?

[Eric Wieser]

I'm pretty sure this is the problem I warned about with adding coercions based on semilinear_map_class

[Eric Wieser]

Which is that now we have a coercion from every morphism to every other morphism, and no lemmas to cut that coercion in two (for example, showing that coercing an alg_hom to a monoid_hom is the same as coercing via a ring hom)

[Yury G. Kudryashov]

I suggest that we add simp lemmas as needed for now, then after the port we try !4#2202 or some other way to automate the process.

[Eric Wieser]

I'd preface that with "In mathlib3, ...". If the port tells us that we're missing a simp lemma here but mathlib3 didn't, then something else has gone wrong.

[Scott Morrison]

Anyone want to add this simp lemma to mathlib3? I only indirectly ran into this problem while porting (trying to fix a timeout by making something irreducible, and then backporting the irreducible to mathlib3 to check it was sane uncovered this problem).