set unions

Stream: new members

[Antoine Chambert-Loir]

I am not particularly happy of having written these lines, in either version. Does anybody see how to shorten it ?

import data.set.basic
import data.set.lattice

variables ι α: Type*


lemma Union_union_distrib' {ι} {α} (s : ι → set α) (J₁ J₂ : set ι) :
  (⋃ (j : ↥(J₁ ∪ J₂)), s ↑j) = (⋃ (j : ↥J₁), s ↑j) ∪ (⋃ (j : ↥J₂), s ↑j) :=
begin

  apply set.ext, intro x,
  split,

  { intro hx,
    obtain ⟨j, hxj⟩ := set.mem_Union.1 hx,
    have z : ↑j ∈ J₁ ∨ ↑j ∈ J₂,
          { apply (set.mem_union ↑j J₁ J₂).1,  exact subtype.mem j, },
    apply or.elim z,
    { intro hj, apply set.mem_union_left,
      apply set.mem_Union.2,
      use ↑j, exact hj, exact hxj, },
    { intro hj, apply set.mem_union_right,
      apply set.mem_Union.2,
      use ↑j, exact hj, exact hxj, },  },

  { intro hx,
    apply or.elim hx,
    { intro hx1, obtain ⟨j, hxj  ⟩ := set.mem_Union.1 hx1,
      apply set.mem_Union.2, use j, apply set.mem_union_left,
      exact subtype.mem j, exact hxj, },
    { intro hx1, obtain ⟨j, hxj  ⟩ := set.mem_Union.1 hx1,
      apply set.mem_Union.2, use j, apply set.mem_union_right,
      exact subtype.mem j, exact hxj, }, },
end


lemma Union_union_distrib'' {ι} {α} (s : ι → set α) (J₁ J₂ : set ι) :
  (⋃ (j : ↥(J₁ ∪ J₂)), s ↑j) = (⋃ (j : ↥J₁), s ↑j) ∪ (⋃ (j : ↥J₂), s ↑j) :=
begin
  apply set.subset.antisymm_iff.2 ,  split,

  apply set.Union_subset, intro i,
  have z : ↑i ∈ J₁ ∨ ↑i ∈ J₂,
          { apply (set.mem_union ↑i J₁ J₂).1,  exact subtype.mem i, },
  apply or.elim z,
  { intro hi, apply set.subset_union_of_subset_left  ,
      apply set.subset_Union (set.restrict s J₁) ⟨i, hi⟩, },
  { intro hi, apply set.subset_union_of_subset_right  ,
      apply set.subset_Union (set.restrict s J₂) ⟨i, hi⟩, },


  apply set.union_subset,
  { apply set.Union_subset, intro i,
    exact set.subset_Union (set.restrict s (J₁ ∪ J₂))
      ⟨i, (set.mem_union ↑i J₁ J₂).2 (or.intro_left _ (subtype.mem i))⟩, },
  { apply set.Union_subset, intro i,
    exact set.subset_Union (set.restrict s (J₁ ∪ J₂))
      ⟨i, (set.mem_union ↑i J₁ J₂).2 (or.intro_right _ (subtype.mem i))⟩, },
end

[Adam Topaz]

Here it is golfed to a reasonable state:

import data.set.basic
import data.set.lattice

variables ι α: Type*

import data.set.basic
import data.set.lattice

variables ι α: Type*

lemma Union_union_distrib' {ι} {α} (s : ι → set α) (J₁ J₂ : set ι) :
  (⋃ (j : (J₁ ∪ J₂)), s j) = (⋃ (j : J₁), s j) ∪ (⋃ (j : J₂), s j) :=
begin
  ext x,
  split,
  { rintro ⟨S, ⟨⟨j, (hj|hj)⟩, rfl⟩, hx⟩,
    { exact or.inl ⟨_, ⟨⟨j, hj⟩, rfl⟩, hx⟩ },
    { exact or.inr ⟨_, ⟨⟨j, hj⟩, rfl⟩, hx⟩ } },
  { rintro (⟨_, ⟨⟨⟨j, hj⟩, rfl⟩, hx⟩⟩ | ⟨_, ⟨⟨⟨j, hj⟩, rfl⟩, hx⟩⟩),
    { exact ⟨_, ⟨⟨j, or.inl hj⟩, rfl⟩, hx⟩ },
    { exact ⟨_, ⟨⟨j, or.inr hj⟩, rfl⟩, hx⟩ } }
end

tactic#rintro is amazing!

[Adam Topaz]

Note also that explicitly denoting the coercions is not necessary.

[Eric Wieser]

Do we have docs#set.Union_subtype? If we had ⋃ i : s, f I = ⋃ i ∈ s, f i then you could just apply docs#set.Union_or after docs#set.mem_union

[Eric Wieser]

Ah, it's docs#set.bUnion_eq_Union in reverse

[Sebastien Gouezel]

What about

theorem set.bUnion_eq_Union' (s : set ι) (t : ι → set α) :
  (⋃ x ∈ s, t x) = (⋃ x : s, t x) :=
supr_subtype'

lemma Union_union_distrib' {ι} {α} (s : ι → set α) (J₁ J₂ : set ι) :
  (⋃ (j : (J₁ ∪ J₂)), s j) = (⋃ (j : J₁), s j) ∪ (⋃ (j : J₂), s j) :=
by rw [← set.bUnion_eq_Union', ← set.bUnion_eq_Union', ← set.bUnion_eq_Union', set.bUnion_union]

But mainly, this indicates that what you are doing is not really idiomatic: instead of using Unions over subtypes, it is more usual to use a Union with the condition that the point belongs to a subset (called bUnion in our naming conventions). I.e., if you replace your lemma with

lemma Union_union_distrib' {ι} {α} (s : ι → set α) (J₁ J₂ : set ι) :
  (⋃ (j ∈ (J₁ ∪ J₂)), s j) = (⋃ (j ∈ J₁), s j) ∪ (⋃ (j ∈ J₂), s j) :=

then this is just bUnion_union.