Mathlib subobject membership: SetLike lemmas, not Subgroup.mem_coe

On Mathlib v4.35.0 and v4.36.0-rc2, Subgroup.mem_coe, Submonoid.mem_coe, Submodule.mem_coe, Ideal.mem_coe, Subring.mem_coe and Subfield.mem_coe are all unknown constants. The generic lemmas live in the SetLike namespace. SetLike.mem_coe : x ∈ ↑p ↔ x ∈ p. SetLike.ext h or Subgroup.ext h from ∀ x, x ∈ S ↔ x ∈ T. SetLike.coe_injective h or SetLike.ext' h from (S : Set G) = T. SetLike.coe_subset_coe.symm : S ≤ T ↔ (S : Set G) ⊆ T. SetLike.coe_mem a, a.2 or a.prop for (a : G) ∈ S. SetLike.coe_sort_coe : ↑↑p = ↥p. (Finset.mem_coe does exist, since Finset is not SetLike.) Several of these hold by Iff.rfl: x ∈ (S : Set G) ↔ x ∈ S, x ∈ S.carrier ↔ x ∈ S (also Subgroup.mem_carrier), and S ≤ T ↔ ∀ ⦃x⦄, x ∈ S → x ∈ T. For elements of ↥S: Subtype.ext h or ext; exact h from (a : G) = b, Subgroup.coe_mul S a b, and ((⟨x, hx⟩ : S) : G) = x := rfl.