refactor(set_theory/cardinal): split up mk_Union_le_mk_sigma, add mk_Union_eq_mk_sigma; add equiv congruence for subtype

Author: johoelzl

src/data/equiv/basic.lean

@@ -507,6 +507,13 @@ def pi_equiv_subtype_sigma (ι : Type*) (π : ι → Type*) :
   assume ⟨f, hf⟩, subtype.eq $ funext $ assume i, sigma.eq (hf i).symm $
     eq_of_heq $ rec_heq_of_heq _ $ rec_heq_of_heq _ $ heq.refl _⟩
 
+def subtype_congr {α : Type*} {p q : α → Prop} (h : p = q) : subtype p ≃ subtype q :=
+⟨subtype.map id $ by rw [h]; exact assume h, id, subtype.map id $ by rw [h]; exact assume h, id,
+  assume ⟨a, h⟩, rfl, assume ⟨a, h⟩, rfl,⟩
+
+def set_congr {α : Type*} {s t : set α} (h : s = t) : s ≃ t :=
+subtype_congr h
+
 end
 
 section

src/data/set/lattice.lean

@@ -664,24 +664,34 @@ end disjoint
 theorem set.disjoint_diff {a b : set α} : disjoint a (b \ a) :=
 disjoint_iff.2 (inter_diff_self _ _)
 
-section
-open set
-set_option eqn_compiler.zeta true
+namespace set
+variables (t : α → set β)
 
-noncomputable def set.bUnion_eq_sigma_of_disjoint {α β} {s : set α} {t : α → set β}
-  (h : pairwise_on s (disjoint on t)) : (⋃i∈s, t i) ≃ (Σi:s, t i.val) :=
-let f : (Σi:s, t i.val) → (⋃i∈s, t i) := λ⟨⟨a, ha⟩, ⟨b, hb⟩⟩, ⟨b, mem_bUnion ha hb⟩ in
-have injective f,
-  from assume ⟨⟨a₁, ha₁⟩, ⟨b₁, hb₁⟩⟩ ⟨⟨a₂, ha₂⟩, ⟨b₂, hb₂⟩⟩ eq,
+def sigma_to_Union (x : Σi, t i) : (⋃i, t i) := ⟨x.2, mem_Union.2 ⟨x.1, x.2.2⟩⟩
+
+lemma surjective_sigma_to_Union : surjective (sigma_to_Union t)
+| ⟨b, hb⟩ := have ∃a, b ∈ t a, by simpa using hb, let ⟨a, hb⟩ := this in ⟨⟨a, ⟨b, hb⟩⟩, rfl⟩
+
+lemma injective_sigma_to_Union (h : ∀i j, i ≠ j → disjoint (t i) (t j)) :
+  injective (sigma_to_Union t)
+| ⟨a₁, ⟨b₁, h₁⟩⟩ ⟨a₂, ⟨b₂, h₂⟩⟩ eq :=
   have b_eq : b₁ = b₂, from congr_arg subtype.val eq,
   have a_eq : a₁ = a₂, from classical.by_contradiction $ assume ne,
-    have b₁ ∈ t a₁ ∩ t a₂, from ⟨hb₁, b_eq.symm ▸ hb₂⟩,
-    h _ ha₁ _ ha₂ ne this,
-  sigma.eq (subtype.eq a_eq) (subtype.eq $ by subst b_eq; subst a_eq),
-have surjective f,
-  from assume ⟨b, hb⟩,
-  have ∃a∈s, b ∈ t a, by simpa using hb,
-  let ⟨a, ha, hb⟩ := this in ⟨⟨⟨a, ha⟩, ⟨b, hb⟩⟩, rfl⟩,
-(equiv.of_bijective ⟨‹injective f›, ‹surjective f›⟩).symm
+    have b₁ ∈ t a₁ ∩ t a₂, from ⟨h₁, b_eq.symm ▸ h₂⟩,
+    h _ _ ne this,
+  sigma.eq a_eq $ subtype.eq $ by subst b_eq; subst a_eq
 
-end
+lemma bijective_sigma_to_Union (h : ∀i j, i ≠ j → disjoint (t i) (t j)) :
+  bijective (sigma_to_Union t) :=
+⟨injective_sigma_to_Union t h, surjective_sigma_to_Union t⟩
+
+noncomputable def Union_eq_sigma_of_disjoint {t : α → set β}
+  (h : ∀i j, i ≠ j → disjoint (t i) (t j)) : (⋃i, t i) ≃ (Σi, t i) :=
+(equiv.of_bijective $ bijective_sigma_to_Union t h).symm
+
+noncomputable def bUnion_eq_sigma_of_disjoint {s : set α} {t : α → set β}
+  (h : pairwise_on s (disjoint on t)) : (⋃i∈s, t i) ≃ (Σi:s, t i.val) :=
+equiv.trans (equiv.set_congr (bUnion_eq_Union _ _)) $ Union_eq_sigma_of_disjoint $
+  assume ⟨i, hi⟩ ⟨j, hj⟩ ne, h _ hi _ hj $ assume eq, ne $ subtype.eq eq
+
+end set

src/set_theory/cardinal.lean

@@ -699,16 +699,18 @@ mk_le_of_surjective surjective_onto_image
 theorem mk_range_le {α β : Type u} {f : α → β} {s : set α} : mk (range f) ≤ mk α :=
 mk_le_of_surjective surjective_onto_range
 
-theorem mk_eq_of_injective {α β : Type u} {f : α → β} {s : set α} (hf : injective f) : mk (f '' s) = mk s :=
+theorem mk_eq_of_injective {α β : Type u} {f : α → β} {s : set α} (hf : injective f) :
+  mk (f '' s) = mk s :=
 quotient.sound ⟨(equiv.set.image f s hf).symm⟩
 
 theorem mk_Union_le_sum_mk {α ι : Type u} {f : ι → set α} : mk (⋃ i, f i) ≤ sum (λ i, mk (f i)) :=
-calc  mk (⋃ i, f i)
-    ≤ mk (Σ i, f i) :
-        let f : (Σ i, f i) → (⋃ i, f i) := λ ⟨i, x, hx⟩, ⟨x, mem_Union.2 ⟨i, hx⟩⟩ in
-        have surjective f := λ ⟨x, hx⟩, let ⟨i, hi⟩ := mem_Union.1 hx in ⟨⟨i, x, hi⟩, rfl⟩,
-        mk_le_of_surjective this
-... = sum (λ i, mk (f i)) : (sum_mk _).symm
+calc mk (⋃ i, f i) ≤ mk (Σ i, f i) : mk_le_of_surjective (set.surjective_sigma_to_Union f)
+  ... = sum (λ i, mk (f i)) : (sum_mk _).symm
+
+theorem mk_Union_eq_sum_mk {α ι : Type u} {f : ι → set α} (h : ∀i j, i ≠ j → disjoint (f i) (f j)) :
+  mk (⋃ i, f i) = sum (λ i, mk (f i)) :=
+calc mk (⋃ i, f i) = mk (Σi, f i) : quot.sound ⟨set.Union_eq_sigma_of_disjoint h⟩
+  ... = sum (λi, mk (f i)) : (sum_mk _).symm
 
 @[simp] lemma finset_card {α : Type u} {s : finset α} : ↑(finset.card s) = mk (↑s : set α) :=
 by rw [fintype_card, nat_cast_inj, fintype.card_coe]