# Zulip Chat Archive

## Stream: maths

### Topic: Showing topological_space_eq "manually"

#### Golol (Oct 18 2020 at 16:27):

This is the definition of a topological space.

```
@[protect_proj] structure topological_space (α : Type u) :=
(is_open : set α → Prop)
(is_open_univ : is_open univ)
(is_open_inter : ∀s t, is_open s → is_open t → is_open (s ∩ t))
(is_open_sUnion : ∀s, (∀t∈s, is_open t) → is_open (⋃₀ s))
```

I want to show the following lemma

```
lemma topological_space_eq {X Y : topological_space α} : (X.is_open = Y.is_open) -> X = Y
```

by explicitly constructing a proof of X = Y, not just typing refl and letting lean do it.

To do this I want to show that `X.is_open_inter = Y.is_open_inter`

,` X.is_open_sUnion = Y.is_open_sUnion`

and `X.is_open_univ = Y.is_open_univ`

. Then I can apply `topological_space.mk`

and since I have proofs that all the arguments are equal, as well as that X is the result of applying the constructor, I should be able to get a proof (using eq.rec_on a bit).

My problem is that

```
lemma test {X Y : topological_space α} : (X.is_open = Y.is_open) -> X.is_open_univ = Y.is_open_univ
```

does not typecheck since lean says that the two types at the end are different.

How could I get around this?

#### Mario Carneiro (Oct 18 2020 at 16:35):

note that `refl`

is not a magic tool, it proves a very particular set of things. In particular, when `refl`

is the proof, the proof is literally `rfl`

, or `eq.refl _`

- there is no lower level proof

#### Mario Carneiro (Oct 18 2020 at 16:35):

In fact `refl`

will not prove this goal

#### Mario Carneiro (Oct 18 2020 at 16:37):

The proof of this theorem is actually `intro h; cases X; cases Y; cases h; refl`

, which should give you a hint as to how to proceed

#### Golol (Oct 18 2020 at 16:53):

Could you then explain how this proof works?

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

We start by using recursion on topological space to assume that f and g are outputs of the constructor for certain inputs. But what does the first rfl do, and why is it trivial to Lean that all the arguments are identical?

#### Mario Carneiro (Oct 18 2020 at 16:57):

that's the same proof as I just described, but written with the equation compiler

#### Mario Carneiro (Oct 18 2020 at 16:58):

the first two tuples are doing `cases X; cases Y`

and the `rfl`

on the left is doing `cases h`

, and the `rfl`

on the right is the finishing `refl`

#### Mario Carneiro (Oct 18 2020 at 16:59):

Once you have done cases on everything, all the props become definitionally equal by proof irrelevance

#### Golol (Oct 18 2020 at 19:57):

Thanks a lot, I did the tactics proof and looked at the proof term:

```
theorem topological_space_eq2 : ∀ (α : Type u) (X Y : topological_space α), X.is_open = Y.is_open → X = Y :=
λ (α : Type u) (X Y : topological_space α) (h : X.is_open = Y.is_open),
X.cases_on
(λ (X_is_open : set α → Prop) (X_is_open_univ : X_is_open univ)
(X_is_open_inter : ∀ (s t : set α), X_is_open s → X_is_open t → X_is_open (s ∩ t))
(X_is_open_sUnion : ∀ (s : set (set α)), (∀ (t : set α), t ∈ s → X_is_open t) → X_is_open (⋃₀ s))
(h :
{is_open := X_is_open,
is_open_univ := X_is_open_univ,
is_open_inter := X_is_open_inter,
is_open_sUnion := X_is_open_sUnion}.is_open =
Y.is_open),
Y.cases_on
(λ (Y_is_open : set α → Prop) (Y_is_open_univ : Y_is_open univ)
(Y_is_open_inter : ∀ (s t : set α), Y_is_open s → Y_is_open t → Y_is_open (s ∩ t))
(Y_is_open_sUnion :
∀ (s : set (set α)), (∀ (t : set α), t ∈ s → Y_is_open t) → Y_is_open (⋃₀ s))
(h :
{is_open := X_is_open,
is_open_univ := X_is_open_univ,
is_open_inter := X_is_open_inter,
is_open_sUnion := X_is_open_sUnion}.is_open =
{is_open := Y_is_open,
is_open_univ := Y_is_open_univ,
is_open_inter := Y_is_open_inter,
is_open_sUnion := Y_is_open_sUnion}.is_open),
h.dcases_on
(λ (a : Y_is_open = X_is_open),
eq.rec
(λ (Y_is_open_univ : X_is_open univ)
(Y_is_open_inter : ∀ (s t : set α), X_is_open s → X_is_open t → X_is_open (s ∩ t))
(Y_is_open_sUnion :
∀ (s : set (set α)), (∀ (t : set α), t ∈ s → X_is_open t) → X_is_open (⋃₀ s))
(h :
{is_open := X_is_open,
is_open_univ := X_is_open_univ,
is_open_inter := X_is_open_inter,
is_open_sUnion := X_is_open_sUnion}.is_open =
{is_open := X_is_open,
is_open_univ := Y_is_open_univ,
is_open_inter := Y_is_open_inter,
is_open_sUnion := Y_is_open_sUnion}.is_open)
(H_2 :
h ==
eq.refl
{is_open := X_is_open,
is_open_univ := X_is_open_univ,
is_open_inter := X_is_open_inter,
is_open_sUnion := X_is_open_sUnion}.is_open),
eq.refl
{is_open := X_is_open,
is_open_univ := X_is_open_univ,
is_open_inter := X_is_open_inter,
is_open_sUnion := X_is_open_sUnion})
a.symm
Y_is_open_univ
Y_is_open_inter
Y_is_open_sUnion
h)
(eq.refl
{is_open := Y_is_open,
is_open_univ := Y_is_open_univ,
is_open_inter := Y_is_open_inter,
is_open_sUnion := Y_is_open_sUnion}.is_open)
(heq.refl h))
h)
h
```

I basically spent all day trying to find this proof lol. There are surely shorter term-style proofs but now I see why tactics are important...

#### Mario Carneiro (Oct 18 2020 at 20:40):

There are surely shorter term-style proofs

well yes, the first proof you posted is term-style

#### Mario Carneiro (Oct 18 2020 at 20:47):

but here's a shorter term mode proof using only `rec_on`

s

```
lemma topological_space_eq' : ∀ {f g : topological_space α}, f.is_open = g.is_open → f = g :=
λ f, topological_space.cases_on f $ λ a a₁ a₂ a₃,
λ g, topological_space.cases_on g $ λ b b₁ b₂ b₃,
λ h : a = b, (eq.rec_on h $ λ _ _ _, rfl) b₁ b₂ b₃
```

Last updated: May 19 2021 at 00:40 UTC