∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {S T : AddSubgroup M} (h : S ≤ T),
  QuotientAddGroup.quotientQuotientIsometryEquivQuotient h =
    { toEquiv := (QuotientAddGroup.quotientQuotientEquivQuotient S T h).toEquiv, isometry_toFun := ⋯ }