Zulip Chat Archive

Stream: general

Topic: trouble with function as set

Marcus Klaas (Dec 01 2018 at 23:12):

Hi! Is this a proper channel for asking (elementary) questions?

Marcus Klaas (Dec 01 2018 at 23:12):

I'm stuck trying to prove the following trivial statement:

def func_as_set {α β} (f : α → β) : set (α × β) := { x | x.2 = f(x.1) }

example {α β} (a : α) (f : α → β) : (a, f a) ∈ func_as_set f := sorry

Marcus Klaas (Dec 01 2018 at 23:13):

Refl and Simp tactics don't seem to work, unfortunately

Chris Hughes (Dec 01 2018 at 23:17):

Did you try rfl?

Marcus Klaas (Dec 01 2018 at 23:18):

I don't think so. I will do it now.

Chris Hughes (Dec 01 2018 at 23:18):

refl works for any reflexive relation, and I guess the elaborator looks for a proof that ∈ is reflexive. rfl is only for equality.

Marcus Klaas (Dec 01 2018 at 23:19):

omg that worked. Thanks for the elaboration too. Very useful to know!!

Kevin Buzzard (Dec 01 2018 at 23:31):

Hi! Is this a proper channel for asking (elementary) questions?

Here is fine, although most of the elementary questions get asked in #new members . There are no hard and fast rules though.

Marcus Klaas (Dec 01 2018 at 23:36):

Cool, thanks

Marcus Klaas (Dec 01 2018 at 23:38):

In that case, I have another trivial follow up ;-) How does one go from a hypothesis in this form

x ∈{ y | P y }

P x

Kevin Buzzard (Dec 01 2018 at 23:39):

Again isn't that rfl?

Chris Hughes (Dec 01 2018 at 23:40):

rw set.mem_set_of_eq also works. That lemma does not have a good name.

Marcus Klaas (Dec 01 2018 at 23:40):

but you can't use that when it's a hypothesis, right?

Chris Hughes (Dec 01 2018 at 23:40):

rw _ at h

Marcus Klaas (Dec 01 2018 at 23:40):

right - trying now

Kevin Buzzard (Dec 01 2018 at 23:40):

Are you in tactic mode or term mode?

Chris Hughes (Dec 01 2018 at 23:40):

if h is your hypothesis.

Marcus Klaas (Dec 01 2018 at 23:41):

tactic mode

Kenny Lau (Dec 01 2018 at 23:41):

you can just change it

Kenny Lau (Dec 01 2018 at 23:41):

or pretend that it's already in that form

Kenny Lau (Dec 01 2018 at 23:41):

depending on what you're trying to do

Kevin Buzzard (Dec 01 2018 at 23:41):

You could do change P x at h as well

Marcus Klaas (Dec 01 2018 at 23:41):

oooh, that's useful
thanks folks!

Kevin Buzzard (Dec 01 2018 at 23:41):

Because the two terms are definitionally equal you might not even need to change it

Marcus Klaas (Dec 01 2018 at 23:46):

@Kevin Buzzard my proposition is an equality in this case. i need it for a rewrite. doesnt seem to work without an explicit change

Marcus Klaas (Dec 01 2018 at 23:46):

with the change, it does! :-)

Kevin Buzzard (Dec 01 2018 at 23:47):

Post some working code?

Kevin Buzzard (Dec 01 2018 at 23:47):

But yes, rw needs things to be unravelled explicitly.

Last updated: Dec 20 2023 at 11:08 UTC