confused about topological_space_eq

Stream: general

[Bernd Losert]

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]

You should do subst a before the last line.

[Yury G. Kudryashov]

(I guess, open_eq becomes a = b after both cases, otherwise you need change or dsimp before subst)

[Andrew Yang]

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]

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]

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]

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.