Equate Intersections

Stream: maths

[Ashvni Narayanan]

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]

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]

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

[Kevin Buzzard]

You might find life easier if you didn't have two things called h and two things called g :-)

[Kevin Buzzard]

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