proves an isometry

[dannypsnl]

Proves that $A : S^n \to S^n$ defined by $A(p) = -p$ is an isometry.

Which means

1. $A$ is diffeomorphism
   1. $A$ is differentiable
   2. $A$ is bijective
   3. $A^{-1}$ is differentiable
2. $dA_p(u) : Tp S^n \to T{A(p)}S^n$ is preserved inner product (and hence length).

[dannypsnl]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/EMetricSpace/Basic.html#PseudoEMetricSpace

Isometry is rely on PseudoEMetricSpace, but TangentSpace will not return this class.

So need to find if TangentSpace has given inner product.

[dannypsnl]

def TangentSpace {𝕜} [NontriviallyNormedField 𝕜] {E} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    {H} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M} [TopologicalSpace M]
    [ChartedSpace H M] [SmoothManifoldWithCorners I M] (_x : M) : Type* := E

So I can say E is a normed space, then with edist?