feat(analysis/normed_space/linear_isometry): trans_one, one_trans…

…, `refl_mul`, `mul_refl` (#12016)

Add variants of the `linear_isometry_equiv.trans_refl` and
`linear_isometry_equiv.refl_trans` `simp` lemmas where `refl` is given
as `1`.  (`one_def` isn't a `simp` lemma in either direction, since
either `refl` or `1` could be the appropriate simplest form depending
on the context, but it seems clear these expressions involving `trans`
with `1` are still appropriate to simplify.)

Also add corresponding `refl_mul` and `mul_refl`.

src/analysis/normed_space/linear_isometry.lean

@@ -442,6 +442,19 @@ lemma one_def : (1 : E ≃ₗᵢ[R] E) = refl _ _ := rfl
 lemma mul_def (e e' : E ≃ₗᵢ[R] E) : (e * e' : E ≃ₗᵢ[R] E) = e'.trans e := rfl
 lemma inv_def (e : E ≃ₗᵢ[R] E) : (e⁻¹ : E ≃ₗᵢ[R] E) = e.symm := rfl
 
+/-! Lemmas about mixing the group structure with definitions. Because we have multiple ways to
+express `linear_isometry_equiv.refl`, `linear_isometry_equiv.symm`, and
+`linear_isometry_equiv.trans`, we want simp lemmas for every combination.
+The assumption made here is that if you're using the group structure, you want to preserve it
+after simp.
+
+This copies the approach used by the lemmas near `equiv.perm.trans_one`. -/
+
+@[simp] lemma trans_one : e.trans (1 : E₂ ≃ₗᵢ[R₂] E₂) = e := trans_refl _
+@[simp] lemma one_trans : (1 : E ≃ₗᵢ[R] E).trans e = e := refl_trans _
+@[simp] lemma refl_mul (e : E ≃ₗᵢ[R] E) : (refl _ _) * e = e := trans_refl _
+@[simp] lemma mul_refl (e : E ≃ₗᵢ[R] E) : e * (refl _ _) = e := refl_trans _
+
 include σ₂₁
 
 /-- Reinterpret a `linear_isometry_equiv` as a `continuous_linear_equiv`. -/