prove instance equality

Stream: Is there code for X?

[Miguel Marco]

I am writing Lean files that try to follow what we cover in a general topology course. I define topological spaces as a class that contains a family of subsets (the open sets) and proofs for the properties that a topology should satisfy.

In some exercises, we must prove that two topologies over the same type are equal, but I am stuck trying to do so.

What is the way to prove that two instances of a class are equal?

[Kevin Buzzard]

You shouldn't have two non-equal instances of a class full stop. But if by "instance" you just mean "term" then maybe ext is the tactic you're looking for

[Kyle Miller]

(A class is a structure whose terms are allowed to have the instance attribute. If an "instance" is an instance-tagged term of a class, then Kevin is saying the fact that one should never have non-equal instances with the same type. It's perfectly fine working with different topologies on the same type, so long as you don't make them both instances.)

[Kyle Miller]

For ext to work, you need to register an ext lemma (an extensionality lemma). Usually you can put @[ext] on your structure/class to auto-generate one.

[Kyle Miller]

It looks like mathlib's TopologicalSpace defines its own ext lemma and registers it with @[ext]: https://github.com/leanprover-community/mathlib4/blob/6c1021b515a78ff4a8f628aa8720dbd22d2570a8/Mathlib/Topology/Basic.lean#L113