no goals
R : Type u_1
M : Type u_2
N : Type ?u.8223
G : Type ?u.8226
M' : Type ?u.8229
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
f : M →L[R] N
g : N →L[R] G
c : R
⊢ ContinuousLinearMap.id R M = 1 • toContinuousLinearMap LinearIsometry.id
simp