Proposition 1.31 (second part): $p_*\pi_1(\tilde X,\tilde x_0)$ consists of the loops whose lifts at $\tilde x_0$ are loops

Read-back of Hatcher.mem_coverSubgroup_iff.

theorem mem_coverSubgroup_iff {E X : Type*} [TopologicalSpace E] [TopologicalSpace X]
    {p : E → X} (hp : IsCoveringMap p) {e₀ : E} {x₀ : X} (he : p e₀ = x₀)
    (g : FundamentalGroup X x₀) :
    g ∈ coverSubgroup p hp.continuous he ↔
      ∀ γ : Path x₀ x₀, FundamentalGroup.fromPath ⟦γ⟧ = g →
        ∃ Γ : Path e₀ e₀, ∀ t, p (Γ t) = γ t

Setting and binders

• E X : Type* with [TopologicalSpace E] [TopologicalSpace X] — arbitrary topological spaces in independent universes; no connectedness, Hausdorff, or nonemptiness assumptions (E is nonempty because e₀ : E).
• {p : E → X} — a function, implicit.
• (hp : IsCoveringMap p) — Mathlib covering map: every $x\in X$ has an open $U\ni x$ with $p^{-1}(U)$ open and a fibre-preserving homeomorphism $p^{-1}(U)\cong U\times p^{-1}(x)$, the fibre $p^{-1}(x)$ carrying the discrete topology. Fibres may be empty (no surjectivity). hp.continuous : Continuous p.
• {e₀ : E} {x₀ : X}, (he : p e₀ = x₀) — basepoints with $p(e_0)=x_0$.
• (g : FundamentalGroup X x₀) — an element of Mathlib's $\pi_1(X,x_0)$ = Path.Homotopic.Quotient x₀ x₀ (homotopy classes rel endpoints of loops at $x_0$; multiplication p * q = q.trans p, reversed relative to Hatcher, irrelevant here).
• coverSubgroup p hp.continuous he : Subgroup (FundamentalGroup X x₀) is (coverHom p hp.continuous he).range, and coverHom p hp.continuous he = FundamentalGroup.mapOfEq ⟨p, hp.continuous⟩ he is $p_*:[\delta]\mapsto[p\circ\delta]$ (endpoints recast from $p(e_0)$ to $x_0$ via he). Hence, by MonoidHom.mem_range,

• γ : Path x₀ x₀ — a loop $[0,1]\to X$ at $x_0$; Γ : Path e₀ e₀ — a loop $[0,1]\to E$ at $e_0$.
• ⟦γ⟧ is Quotient.mk _ γ, the setoid being inferred from the expected type as Path.Homotopic.setoid x₀ x₀; so ⟦γ⟧ : Path.Homotopic.Quotient x₀ x₀ is the path-homotopy class $[\gamma]$.
• FundamentalGroup.fromPath : Path.Homotopic.Quotient x x → FundamentalGroup X x is an abbrev that is definitionally the identity (fromArrow p = p), since FundamentalGroup X x is End (FundamentalGroupoid.mk x) whose underlying type is Path.Homotopic.Quotient x x. So FundamentalGroup.fromPath ⟦γ⟧ = g says exactly: $[\gamma]=g$, i.e. $\gamma$ is a representative of $g$.
• ∀ t, p (Γ t) = γ t — for every $t\in[0,1]$ (the type unitInterval; the open unitInterval in the file only provides notation), $p(\Gamma(t))=\gamma(t)$. That is, $p\circ\Gamma=\gamma$ as functions, hence $\Gamma$ is a lift of $\gamma$ through $p$.

Hypotheses

hp : IsCoveringMap p and he : p e₀ = x₀ only. No path-connectedness or local path-connectedness of E or X, no surjectivity.

Conclusion

For every $g\in\pi_1(X,x_0)$:

In words: $g$ lies in the image of $p_*$ if and only if every loop $\gamma$ at $x_0$ representing $g$ admits a lift $\Gamma$ through $p$ that starts and ends at $e_0$ (a loop at $e_0$).

Unpacking the two directions:

• ($\Rightarrow$) If $g=[p\circ\delta]$ for some loop $\delta$ at $e_0$, then for every loop $\gamma$ at $x_0$ homotopic to $p\circ\delta$ there is a loop $\Gamma$ at $e_0$ with $p\circ\Gamma=\gamma$. (This direction needs homotopy lifting and uniqueness of lifts: the lift of $\gamma$ starting at $e_0$ ends where the lift of $p\circ\delta$, namely $\delta$, ends.)
• ($\Leftarrow$) If every representative of $g$ lifts to a loop at $e_0$, then $g\in p_*\pi_1(E,e_0)$. (Choose any representative $\gamma$ — one exists since the quotient map is surjective — get $\Gamma$, and then $p_*[\Gamma]=[p\circ\Gamma]=[\gamma]=g$.)

Remarks

• Textbook match. Hatcher, Proposition 1.31(b): "The image subgroup $p_*\pi_1(\tilde X,\tilde x_0)$ in $\pi_1(X,x_0)$ consists of the homotopy classes of loops in $X$ based at $x_0$ whose lifts to $\tilde X$ starting at $\tilde x_0$ are loops." Hatcher speaks of the lift starting at $\tilde x_0$ (unique by the lifting property); the Lean statement instead says some lift $\Gamma$ with $\Gamma(0)=\Gamma(1)=e_0$ exists. For a covering map these agree, because a lift of $\gamma$ starting at $e_0$ is unique ([0,1] is connected), so "some loop-lift at $e_0$ exists" is the same as "the lift starting at $e_0$ is a loop". A reader should note this reformulation but it is equivalent under hp.
• Quantifier over representatives. The right-hand side quantifies over all loops $\gamma$ with $[\gamma]=g$. Hatcher's phrasing is about "loops whose lift is a loop", implicitly for any/all representatives (well-definedness on classes follows from homotopy lifting). The ∀ form makes the ($\Rightarrow$) direction the substantive one; the ($\Leftarrow$) direction is easy but not vacuous, because every $g$ has at least one representative (Quotient.exists_rep), so the antecedent ⟦γ⟧ = g is satisfiable. An ∃ γ formulation would also be correct and equivalent under hp; the ∀ version is the stronger reading of ($\Rightarrow$).
• Not vacuous or trivial. $E\ne\emptyset$ (contains $e_0$), the fibre over $x_0$ is nonempty, and the statement is a genuine consequence of path- and homotopy-lifting, not a definitional unfolding.
• Non-surjective p. Irrelevant to the statement: only loops at $x_0$, which lies in the image, are involved. If $X$ has points outside $p(E)$, $\pi_1(X,x_0)$ still includes loops that may wander only inside $p(E)$'s path component of $x_0$, and the equivalence holds as stated.
• No connectedness assumptions. Hatcher's Prop 1.31 is stated for a covering space with no connectivity requirement and its proof uses only lifting properties, so the absence of such hypotheses here does not weaken the match. (Connectedness is needed later, e.g. for the classification theorem, not here.)
• Coercions. Γ t and γ t use the Path function coercion to unitInterval → E (resp. → X). The equality p (Γ t) = γ t is pointwise equality in X; via path extensionality it is equivalent to Γ.map hp.continuous = γ after recasting endpoints with he.
• Universe. E and X in independent universes; no restriction.
• Group-law orientation. Membership in a subgroup, and the range of a homomorphism, are insensitive to Mathlib's reversed multiplication convention on FundamentalGroup.
• The statement is a theorem with proof sorry in the audited file; the read-back concerns only the statement.