∀ {G : Type u_1} [inst : Group G] {S : Type u_4} {H K : S} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G]
  [inst_3 : Preorder S] [inst_4 : IsConcreteLE S G] {L : S} (hHK : H ≤ K) (hKL : K ≤ L) (x : ↥H),
  (SubgroupClass.inclusion hKL) ((SubgroupClass.inclusion hHK) x) = (SubgroupClass.inclusion ⋯) x