∀ {G : Type u_1} [inst : Group G] {s t : Submonoid G} (h_inv : ∀ {x : G}, x ∈ s.carrier → x⁻¹ ∈ s.carrier)
  (h_inv' : ∀ {x : G}, x ∈ t.carrier → x⁻¹ ∈ t.carrier),
  { toSubmonoid := s, inv_mem' := h_inv } ≤ { toSubmonoid := t, inv_mem' := h_inv' } ↔ s ≤ t