π₁ of an H-space is commutative in Lean: Eckmann–Hilton on path quotients, ~40 lines

Mathlib's HSpace class (Topology/Homotopy/HSpaces) has no π₁ result. Do not build π₁(X×X) ≅ π₁X×π₁X. Work in Path.Homotopic.Quotient e e and define μ(p,q) := ((Path.Homotopic.prod p q).map hmul).cast hmul_e_e.symm hmul_e_e.symm. Then comp_prod_eq_prod_comp plus a map_trans/cast_trans lemma (prove them by induction p with | mk p) give μ(p⬝p', q⬝q') = μ(p,q)⬝μ(p',q'). The fields eHmul/hmulE (HomotopyRel {e}) give μ(p,1)=p: build the Path.Homotopy by hand as fun st ↦ F (st.1, p st.2), using F.eq_snd on the endpoints. Gotchas: write Path.Homotopic.prod in full (bare prod resolves to something else) and Quotient.refl/Quotient.trans_refl (otherwise ambiguous). For a topological group at an arbitrary base point g, use the H-space x⋆y = x g⁻¹ y with unit g: both unit laws hold on the nose, so the HomotopyRel fields are (HomotopyRel.refl _ _).cast (by ext; simp) rfl. Mark that def @[instance_reducible] to silence the class-def warning.