feat(*): add lemmas about sigma types (#15085)

* move `set.range_sigma_mk` to `data.set.sigma`;
* add `set.preimage_image_sigma_mk_of_ne`, `set.image_sigma_mk_preimage_sigma_map_subset`, and `set.image_sigma_mk_preimage_sigma_map`;
* add `function.injective.of_sigma_map` and `function.injective.sigma_map_iff`;
* don't use pattern matching in the definition of `prod.to_sigma`;
* add `filter.map_sigma_mk_comap`

Author: urkud

src/data/set/basic.lean

@@ -1993,15 +1993,6 @@ by simp [range_subset_iff, funext_iff, mem_singleton]
 lemma image_compl_preimage {f : α → β} {s : set β} : f '' ((f ⁻¹' s)ᶜ) = range f \ s :=
 by rw [compl_eq_univ_diff, image_diff_preimage, image_univ]
 
-@[simp] theorem range_sigma_mk {β : α → Type*} (a : α) :
-  range (sigma.mk a : β a → Σ a, β a) = sigma.fst ⁻¹' {a} :=
-begin
-  apply subset.antisymm,
-  { rintros _ ⟨b, rfl⟩, simp },
-  { rintros ⟨x, y⟩ (rfl|_),
-    exact mem_range_self y }
-end
-
 /-- Any map `f : ι → β` factors through a map `range_factorization f : ι → range f`. -/
 def range_factorization (f : ι → β) : ι → range f :=
 λ i, ⟨f i, mem_range_self i⟩

src/data/set/sigma.lean

@@ -13,7 +13,36 @@ This file defines `set.sigma`, the indexed sum of sets.
 
 namespace set
 variables {ι ι' : Type*} {α β : ι → Type*} {s s₁ s₂ : set ι} {t t₁ t₂ : Π i, set (α i)}
-  {u : set (Σ i, α i)} {x : Σ i, α i} {i : ι} {a : α i}
+  {u : set (Σ i, α i)} {x : Σ i, α i} {i j : ι} {a : α i}
+
+@[simp] theorem range_sigma_mk (i : ι) :
+  range (sigma.mk i : α i → sigma α) = sigma.fst ⁻¹' {i} :=
+begin
+  apply subset.antisymm,
+  { rintros _ ⟨b, rfl⟩, simp },
+  { rintros ⟨x, y⟩ (rfl|_),
+    exact mem_range_self y }
+end
+
+theorem preimage_image_sigma_mk_of_ne (h : i ≠ j) (s : set (α j)) :
+  sigma.mk i ⁻¹' (sigma.mk j '' s) = ∅ :=
+by { ext x, simp [h.symm] }
+
+lemma image_sigma_mk_preimage_sigma_map_subset {β : ι' → Type*} (f : ι → ι')
+  (g : Π i, α i → β (f i)) (i : ι) (s : set (β (f i))) :
+  sigma.mk i '' (g i ⁻¹' s) ⊆ sigma.map f g ⁻¹' (sigma.mk (f i) '' s) :=
+image_subset_iff.2 $ λ x hx, ⟨g i x, hx, rfl⟩
+
+lemma image_sigma_mk_preimage_sigma_map {β : ι' → Type*} {f : ι → ι'} (hf : function.injective f)
+  (g : Π i, α i → β (f i)) (i : ι) (s : set (β (f i))) :
+  sigma.mk i '' (g i ⁻¹' s) = sigma.map f g ⁻¹' (sigma.mk (f i) '' s) :=
+begin
+  refine (image_sigma_mk_preimage_sigma_map_subset f g i s).antisymm _,
+  rintro ⟨j, x⟩ ⟨y, hys, hxy⟩,
+  simp only [hf.eq_iff, sigma.map] at hxy,
+  rcases hxy with ⟨rfl, hxy⟩, rw [heq_iff_eq] at hxy, subst y,
+  exact ⟨x, hys, rfl⟩
+end
 
 /-- Indexed sum of sets. `s.sigma t` is the set of dependent pairs `⟨i, a⟩` such that `i ∈ s` and
 `a ∈ t i`.-/

src/data/sigma/basic.lean

@@ -97,21 +97,25 @@ lemma function.injective.sigma_map {f₁ : α₁ → α₂} {f₂ : Πa, β₁ a
 | ⟨i, x⟩ ⟨j, y⟩ h :=
 begin
   obtain rfl : i = j, from h₁ (sigma.mk.inj_iff.mp h).1,
-  obtain rfl : x = y, from h₂ i (eq_of_heq (sigma.mk.inj_iff.mp h).2),
+  obtain rfl : x = y, from h₂ i (sigma_mk_injective h),
   refl
 end
 
+lemma function.injective.of_sigma_map {f₁ : α₁ → α₂} {f₂ : Πa, β₁ a → β₂ (f₁ a)}
+  (h : function.injective (sigma.map f₁ f₂)) (a : α₁) : function.injective (f₂ a) :=
+λ x y hxy, sigma_mk_injective $ @h ⟨a, x⟩ ⟨a, y⟩ (sigma.ext rfl (heq_iff_eq.2 hxy))
+
+lemma function.injective.sigma_map_iff {f₁ : α₁ → α₂} {f₂ : Πa, β₁ a → β₂ (f₁ a)}
+  (h₁ : function.injective f₁) :
+  function.injective (sigma.map f₁ f₂) ↔ ∀ a, function.injective (f₂ a) :=
+⟨λ h, h.of_sigma_map, h₁.sigma_map⟩
+
 lemma function.surjective.sigma_map {f₁ : α₁ → α₂} {f₂ : Πa, β₁ a → β₂ (f₁ a)}
   (h₁ : function.surjective f₁) (h₂ : ∀ a, function.surjective (f₂ a)) :
   function.surjective (sigma.map f₁ f₂) :=
 begin
-  intros y,
-  cases y with j y,
-  cases h₁ j with i hi,
-  subst j,
-  cases h₂ i y with x hx,
-  subst y,
-  exact ⟨⟨i, x⟩, rfl⟩
+  simp only [function.surjective, sigma.forall, h₁.forall],
+  exact λ i, (h₂ _).forall.2 (λ x, ⟨⟨i, x⟩, rfl⟩)
 end
 
 /-- Interpret a function on `Σ x : α, β x` as a dependent function with two arguments.
@@ -137,17 +141,11 @@ lemma sigma.curry_uncurry {γ : Π a, β a → Type*} (f : Π x (y : β x), γ x
 rfl
 
 /-- Convert a product type to a Σ-type. -/
-@[simp]
-def prod.to_sigma {α β} : α × β → Σ _ : α, β
-| ⟨x,y⟩ := ⟨x,y⟩
+def prod.to_sigma {α β} (p : α × β) : Σ _ : α, β := ⟨p.1, p.2⟩
 
-@[simp]
-lemma prod.fst_to_sigma {α β} (x : α × β) : (prod.to_sigma x).fst = x.fst :=
-by cases x; refl
-
-@[simp]
-lemma prod.snd_to_sigma {α β} (x : α × β) : (prod.to_sigma x).snd = x.snd :=
-by cases x; refl
+@[simp] lemma prod.fst_to_sigma {α β} (x : α × β) : (prod.to_sigma x).fst = x.fst := rfl
+@[simp] lemma prod.snd_to_sigma {α β} (x : α × β) : (prod.to_sigma x).snd = x.snd := rfl
+@[simp] lemma prod.to_sigma_mk {α β} (x : α) (y : β) : (x, y).to_sigma = ⟨x, y⟩ := rfl
 
 -- we generate this manually as `@[derive has_reflect]` fails
 @[instance]

src/order/filter/bases.lean

@@ -777,6 +777,16 @@ lemma has_basis.coprod {ι ι' : Type*} {pa : ι → Prop} {sa : ι → set α}
 
 end two_types
 
+lemma map_sigma_mk_comap {π : α → Type*} {π' : β → Type*} {f : α → β}
+  (hf : function.injective f) (g : Π a, π a → π' (f a)) (a : α) (l : filter (π' (f a))) :
+  map (sigma.mk a) (comap (g a) l) = comap (sigma.map f g) (map (sigma.mk (f a)) l) :=
+begin
+  refine (((basis_sets _).comap _).map _).eq_of_same_basis _,
+  convert ((basis_sets _).map _).comap _,
+  ext1 s,
+  apply image_sigma_mk_preimage_sigma_map hf
+end
+
 end filter
 
 end sort