Zulip Chat Archive
Stream: triage
Topic: issue #2725: `push_hom` and `pull_hom` tactics
Random Issue Bot (Feb 14 2021 at 14:19):
Today I chose issue 2725 for discussion!
push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: feature-request, help wanted, meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Scott Morrison (Feb 14 2021 at 22:47):
I haven't thought about this in a while. But I'd certainly like to have something like this.
Scott Morrison (Feb 14 2021 at 22:48):
Indeed, in category theory proofs I can think of lots of related tools: push/pull for _functor, _eq_to_hom, ... I think all of them would just be named simp sets, and possibly rather light wrappers around them.
Eric Wieser (Feb 15 2021 at 05:30):
Is there a mechanism to say "use this simp set with every lemma reversed"?
Johan Commelin (Feb 15 2021 at 06:09):
On the other hand, since mathlib moved to bundled functions, I've had a lot less need for this type of tactics, because simp is now just a lot better at this.
Yury G. Kudryashov (Feb 15 2021 at 18:58):
simp is good as push_hom but sometimes (not often) I want pull_hom.
Random Issue Bot (Mar 17 2021 at 14:26):
Today I chose issue 2725 for discussion!
push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: feature-request, help wanted, meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Dec 07 2021 at 14:21):
Today I chose issue 2725 for discussion!
push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: help wanted, meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Anne Baanen (Dec 07 2021 at 15:39):
With #9888, the set of lemmas that have to be reversed should at least be smaller :)
Random Issue Bot (Jan 05 2022 at 14:15):
Today I chose issue 2725 for discussion!
push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: help wanted, meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jan 17 2022 at 14:18):
Today I chose issue 2725 for discussion!
push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: help wanted, meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (May 02 2022 at 14:20):
Today I chose issue 2725 for discussion!
push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: help wanted, meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (May 27 2023 at 14:07):
Today I chose issue 2725 for discussion!
push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: help-wanted, t-meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jul 23 2023 at 14:07):
Today I chose issue 2725 for discussion!
push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: help-wanted, t-meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jul 31 2023 at 14:07):
Today I chose issue 2725 for discussion!
push_hom and pull_hom tactics
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: help-wanted, t-meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC