# Zulip Chat Archive

## Stream: general

### Topic: confused about topological_space_eq

#### Bernd Losert (Dec 11 2021 at 14:43):

Here's the code:

```
lemma topological_space_eq : ∀ {f g : topological_space α}, f.is_open = g.is_open → f = g
| ⟨a, _, _, _⟩ ⟨b, _, _, _⟩ rfl := rfl
```

I don't understand how this proof works.First, why do you need to pattern match the topological_spaces? Also, since a and b aren't used, why can't they be _ ? I'm trying to rewrite this proof in a longer style, like so:

```
lemma topological_space_eq' : ∀ {f g : topological_space α}, f.is_open = g.is_open → f = g :=
begin
assume f g : topological_spaces,
assume open_eq : f.is_open = g.is_open,
cases f with a _ _ _,
cases g with b _ _ _,
rfl,
end
```

but that doesn't work. Any tips?

#### Yury G. Kudryashov (Dec 11 2021 at 14:45):

You should do `subst a`

before the last line.

#### Yury G. Kudryashov (Dec 11 2021 at 14:45):

(I guess, `open_eq`

becomes `a = b`

after both `cases`

, otherwise you need `change`

or `dsimp`

before `subst`

)

#### Andrew Yang (Dec 11 2021 at 14:46):

Note that the original proof also matches `f.is_open = g.is_open`

with `rfl`

, which does the `subst open_eq`

for you.

#### Bernd Losert (Dec 11 2021 at 14:49):

I have this:

```
lemma topological_space_eq' : ∀ {f g : topological_space α}, f.is_open = g.is_open → f = g :=
begin
assume f g : topological_spaces,
assume open_eq : f.is_open = g.is_open,
cases f with a _ _ _,
cases g with b _ _ _,
subst open_eq,
rfl,
end
```

but that still doesn't work. How does equality of structures work? Shouldn't there be a goal where I have to prove that every field in one of the structure instances is equal to the corresponding field in the other structure instance?

#### Andrew Yang (Dec 11 2021 at 14:51):

```
lemma topological_space_eq' {α : Type*} : ∀ {f g : topological_space α}, f.is_open = g.is_open → f = g :=
begin
assume f g : topological_space α,
assume open_eq : f.is_open = g.is_open,
cases f with a _ _ _,
cases g with b _ _ _,
dsimp at open_eq,
subst open_eq,
end
```

This works

#### Reid Barton (Dec 11 2021 at 14:54):

Bernd Losert said:

How does equality of structures work? Shouldn't there be a goal where I have to prove that every field in one of the structure instances is equal to the corresponding field in the other structure instance?

Equality is a built-in notion. This very lemma is how you prove that it can be characterized in the way you suggest.

However, since the other three fields are proofs about `is_open`

, they will be equal to the corresponding fields automatically.

Last updated: Aug 03 2023 at 10:10 UTC