∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] {S : Type u_2} [inst_2 : SetLike S M₀] [inst_3 : MulMemClass S M₀]
  [inst_4 : ZeroMemClass S M₀] (s : S) [IsLeftCancelMulZero M₀], IsLeftCancelMulZero ↥s