Zulip Chat Archive

Stream: new members

Topic: subgroup.subtype_mem


Yakov Pechersky (Sep 02 2022 at 20:13):

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 (Sep 02 2022 at 20:17):

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 (Sep 02 2022 at 20:17):

For example, library search is perfectly happy with

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

Last updated: Dec 20 2023 at 11:08 UTC