Zulip Chat Archive

Stream: maths

Topic: Equate Intersections


view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Ashvni Narayanan (Mar 24 2021 at 18:06):

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

view this post on Zulip 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 :-)

view this post on Zulip 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