## Stream: new members

### Topic: equality of objects

#### Winston Yin (Jun 14 2021 at 09:55):

What's the best way to go about proving two objects with many fields are equal? Conversely, how do I obtain equality of fields from the equality of objects?

#### Kevin Buzzard (Jun 14 2021 at 09:58):

If you're making the objects yourself then you'd better make an ext lemma, perhaps by dumping @[ext] before the definition of your structure. If you're using a structure someone else has made then the ext lemma might already be there. If you want to make the ext lemma by hand then you might want to consider using cases to take your instances apart.

A simple example is the complex numbers, defined as two real numbers. I set them up in the complex number game, and in the 0th level I prove an ext lemma for them.

#### Kevin Buzzard (Jun 14 2021 at 09:59):

PS equality of fields from equality of objects comes for free. If h : s1 = s2 then s1.foo = s2.foo just by rewriting h and then using refl.

#### Winston Yin (Jun 14 2021 at 10:05):

I'm not sure why the latter doesn't work for me:

h: {to_submodule := s__to_submodule, smul_mem := s_smul_mem}.to_submodule.carrier = {to_submodule := t__to_submodule, smul_mem := t_smul_mem}.to_submodule.carrier
⊢ s__to_submodule = t__to_submodule


#### Kevin Buzzard (Jun 14 2021 at 10:05):

Can you post a #mwe ?

One moment

#### Eric Wieser (Jun 14 2021 at 10:05):

injection h might close that goal?

Nope...

#### Winston Yin (Jun 14 2021 at 10:06):

I'm trying to set up a set_like for a structure that extends submodules...

#### Kevin Buzzard (Jun 14 2021 at 10:06):

you can probably just use the ext tactic. All you know is that the carriers are equal and you want the submodules to be equal, but ext for submodules will do that.

#### Kevin Buzzard (Jun 14 2021 at 10:07):

I could be more helpful to you if you're more helpful to me though by setting up a MWE

#### Eric Wieser (Jun 14 2021 at 10:07):

Maybe exact set_like.coe_injective h

#### Winston Yin (Jun 14 2021 at 10:12):

Eric Wieser said:

Maybe exact set_like.coe_injective h

This worked. Thanks

#### Winston Yin (Jun 14 2021 at 10:12):

Although I'm looking at the proof of set_like.coe_injective for submodule, and it's so much simpler

#### Eric Wieser (Jun 14 2021 at 10:49):

Is your problem that you're not using old_structure_cmd?

#### Eric Wieser (Jun 14 2021 at 10:50):

Your proof has to fallback on the proof for submodule, but set_option old_structure_cmd true flattens everything out making that unnecessary.

#### Winston Yin (Jun 14 2021 at 11:12):

Eric Wieser said:

Is your problem that you're not using old_structure_cmd?

I suspected that might be the reason. Looks like I should use it

#### Winston Yin (Jun 14 2021 at 11:13):

Is there any way to set old_structure_cmd within a section only?

#### Winston Yin (Jun 14 2021 at 11:15):

Ah, looks like putting the option within a section ... end works as intended.

Last updated: Dec 20 2023 at 11:08 UTC