## Stream: general

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