# Zulip Chat Archive

## Stream: maths

### Topic: Equate Intersections

#### Ashvni Narayanan (Mar 24 2021 at 16:02):

I have proved that the intersection of finitely many clopens are clopen, and I have another set, which Lean infers as a possibly infinite intersection of clopens, which is actually the same as the previous set, hence is clopen. I am having trouble in showing that both the sets (given in `g`

and the goal) are indeed the same. This essentially involves splitting up elements of `↥(↑t ∩ Uᶜ)`

, however, that is problematic. When I try to use `set.mem_inter_iff`

, I get the error : ```
rewrite tactic failed, motive is not type correct
λ (_a : Prop), h ↑i _ = h ↑i _
```

.

I have no idea as to how to proceed, any help is appreciated, thank you!

#### Kevin Buzzard (Mar 24 2021 at 18:01):

It seems to me that if you can change `⋂ (i : H) (i_1 : i ∈ t) (i_1 : i ∈ Uᶜ), ...`

to `⋂ (i : H) (i_1 : i ∈ t \cap Uᶜ), ...`

then your life would be much easier :-) I'm fiddling with this now.

#### Ashvni Narayanan (Mar 24 2021 at 18:06):

I just managed to complete the proof! I found a way out :)

#### Kevin Buzzard (Mar 24 2021 at 18:06):

You might find life easier if you didn't have two things called `h`

and two things called `g`

:-)

#### Kevin Buzzard (Mar 24 2021 at 19:19):

```
example (X Y : Type) (s t : set X) (F : X → set Y) :
(⋂ (x : X) (h1 : x ∈ s) (h2 : x ∈ t), F x) = ⋂ (x : X) (h : x ∈ s ∩ t), F x :=
begin
ext y,
simp,
end
```

by the way

Last updated: May 09 2021 at 10:11 UTC