simp for bundled hom projections

Stream: mathlib4

[Yury G. Kudryashov]

Do we have a simp-normal form for, e.g., (e : ContinuousLinearEquiv ..).toContinuousLinearMap.toLinearMap vs e.toLinearEquiv.toLinearMap?

[Yury G. Kudryashov]

#xy: we have docs#Complex.det_conjAe, but docs#Complex.conjCLE appears in a proof, coerced to a LinearMap via ContinuousLinearMap. It would be nice for simp to use the lemma nevertheless. What @[simp] lemmas should we add?

[Yaël Dillies]

No, this is a decision we have been delaying to take. I personally think the latter is better because the information of the two-sided inverse is more likely to be useful when rewriting than continuity

[Jireh Loreaux]

Yes, we've been avoiding making this decision, but I came to the same conclusion as Yaël. We should prefer to stay with equivs as long as possible in the normal form.