Group on a quotient with choice-based inverse: Group.ofLeftAxioms skips inverse well-definedness

When building a group on a quotient (e.g. homotopy classes) where you have well-defined multiplication, a unit, and only existence of left inverses (∃ q, q * p = 1), don't lift an inverse function through the quotient. Define instance : Inv G := ⟨fun a ↦ (exists_inv_mul a).choose⟩, where exists_inv_mul a : ∃ b, b * a = 1 is proved on representatives. Then use Group.ofLeftAxioms mul_assoc one_mul (fun a ↦ (exists_inv_mul a).choose_spec) (import Mathlib.Algebra.Group.MinimalAxioms). Uniqueness of inverses then follows from the group axioms, so no compatibility lemma for inverses is needed.