Top homology of a closed simply connected $n$-manifold maps isomorphically to $H_n(M, M\setminus\{p\})$

Let $M$ be a closed (compact Hausdorff) topological $n$-manifold which is simply connected, and let $p\in M$. Then the natural map from the top homology group to the local homology group at $p$,

is an isomorphism. This is the fundamental-class theorem for closed orientable manifolds (Hatcher, Theorem 3.26(a)): for a closed connected $R$-orientable $n$-manifold the map $H_n(M;R)\to H_n(M\,|\,x;R)\cong R$ is an isomorphism for every $x\in M$, so that $H_n(M;\mathbb Z)\cong\mathbb Z$ is generated by a fundamental class restricting to a generator of every local homology group. A simply connected manifold is connected and orientable (Hatcher, Proposition 3.25: $M$ is orientable if $\pi_1(M)$ has no subgroup of index two), which is why simple connectivity appears as the hypothesis; Mathlib has no notion of orientability. In the mission the statement is applied to a homotopy $4$-sphere and, through the long exact sequence of the pair $(M,M\setminus\{p\})$, gives $H_4(M\setminus\{p\})=0$ and $H_3(M\setminus\{p\})\cong H_3(M)$.

Formalization Note The pair is given by the inclusion Subtype.val : {x : M // x ≠ p} → M, the map is SP4Homology.toRel n, and the conclusion is Mathlib's IsIso in ModuleCat ℤ. The manifold hypothesis is a topological atlas ChartedSpace (EuclideanSpace ℝ (Fin n)) M with T2Space M and CompactSpace M; the statement holds for all $n\ge0$.