## 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):

PS

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.

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 }


to

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.

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: May 14 2021 at 14:20 UTC