## Stream: maths

### Topic: Equate Intersections

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

https://github.com/leanprover-community/mathlib/blob/765dfb9d5e7cb6a7bec5aab65c57c5c0a86a17cf/src/number_theory/L_functions.lean#L232

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