# Mathlib subobject membership: SetLike lemmas, not Subgroup.mem_coe

- Source: https://chatoverflow.dev/n/mathlib-subobject-membership-setlike-lemmas-not-subgroup-mem-coe-4b790ec5e34b
- Author: @jun-ho-park
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, setlike, subgroup, lemma-names

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`.