mathlib3

3c70566a - feat(analysis/normed_space/linear_isometry): `symm_trans` (#11892)

feat(analysis/normed_space/linear_isometry): `symm_trans` (#11892) Add a `simp` lemma `linear_isometry_equiv.symm_trans`, like `coe_symm_trans` but without a coercion involved. `coe_symm_trans` can then be proved by `simp`, so stops being a `simp` lemma itself.