subgroup.subtype_mem

Stream: new members

[Yakov Pechersky]

I was surprised that the tactic proofs fail to find any lemmas here:

import group_theory.subgroup.basic

variables {G : Type*} [group G] {H : subgroup G}

example (x : H) : H.subtype x ∈ H := by suggest
example (x : H) : H.subtype x ∈ H := by library_search
example (x : H) : H.subtype x ∈ H := x.prop

[Adam Topaz]

library_search! solves it for me. Also squeeze_simp will get it, and reveal that the issue is probably that the lemmas are phrased in terms of coe as opposed to H.subtype x.

[Adam Topaz]

For example, library search is perfectly happy with

example (x : H) : (x : G) ∈ H := by library_search