feat(analysis/normed_space/linear_isometry): add congr_arg and congr_…

…fun (#11428)

Two trivial lemmas that are missing from this bundled morphism but present on most others.

Turns out I didn't actually need these in the branch I created them in, but we should have them anyway.

src/analysis/normed_space/linear_isometry.lean

@@ -68,6 +68,11 @@ linear_map.coe_injective.comp to_linear_map_injective
 @[ext] lemma ext {f g : E →ₛₗᵢ[σ₁₂] E₂} (h : ∀ x, f x = g x) : f = g :=
 coe_fn_injective $ funext h
 
+protected lemma congr_arg {f : E →ₛₗᵢ[σ₁₂] E₂} : Π {x x' : E}, x = x' → f x = f x'
+| _ _ rfl := rfl
+
+protected lemma congr_fun {f g : E →ₛₗᵢ[σ₁₂] E₂} (h : f = g) (x : E) : f x = g x := h ▸ rfl
+
 @[simp] lemma map_zero : f 0 = 0 := f.to_linear_map.map_zero
 
 @[simp] lemma map_add (x y : E) : f (x + y) = f x + f y := f.to_linear_map.map_add x y