How to split union in universal statement

Stream: new members

[Shadman Sakib]

import tactic

open set

variables α I : Type*
variable  A : I → set α
variable  s : set α

-- BEGIN
open_locale classical

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=
begin
  ext,
  rw [mem_union_eq, mem_Inter],
  rw mem_Inter,
  split,
  { intros h i,
    cases h with xs xAi,
    { rw mem_union_eq,
      right,
      exact xs, },
    { rw mem_union_eq,
      left,
      exact xAi i, }, },
  { intros h,
    right,
    intro i,
    sorry,
  },
end
-- END

[Shadman Sakib]

Im trying to define the union at the universal statement h, but lean will not let me. How do I define the union with the variable i and split the hypothesis?

[Ruben Van de Velde]

Do you want to do have h' := h i,?

[Ruben Van de Velde]

Oh, you went down a wrong path before that

[Kevin Buzzard]

left and right are dangerous tactics :-)

[Shadman Sakib]

Which path should I have taken?

[Kevin Buzzard]

both paths lead the wrong way

[Shadman Sakib]

And your suggestion worked, thanks

[Shadman Sakib]

There is a way to do the proof without specifying left or right?

[Ruben Van de Velde]

No, but neither is correct in all cases. Do you know the pen-and-paper proof?

[Kevin Buzzard]

the problem is that you don't know which way to go yet. Do you know a maths proof of what you're trying to do?

[Shadman Sakib]

Well h says that for all x x in s or x in A i. So I would do cases on that then prove x in s with one case and x in A i with the other

[Ruben Van de Velde]

Indeed - do you know how to do a case split in lean?

[Kevin Buzzard]

but the statement you want to do a case split on depends on a variable i

[Shadman Sakib]

But I cant introduce a variable i, so I settled for choosing a path

[Shadman Sakib]

And no I thought cases h with ... was splitting?

[Kevin Buzzard]

yes, the problem is that you might want to go one way for some i, and the other way for other i. So it seems to me that you don't have a pen-and-paper proof yet.

[Shadman Sakib]

Well not really, I would go one way based on the case x in s or x in A i. Not depending on i

[Shadman Sakib]

Im a bit confused about what you mean sorry

[Heather Macbeth]

Shadman Sakib said:

I would go one way based on the case x in s or x in A i. Not depending on i

Read what you said ... it does depend on i! :)

[Ruben Van de Velde]

I can't figure out the proof @Kevin Buzzard has in mind either; I managed to finish using by_cases

[Shadman Sakib]

by_cases xs : x in s?