feat(data/set/prod): add lemmas about set.pi (#16828)

Author: urkud

src/data/set/basic.lean

@@ -888,6 +888,11 @@ ssubset_singleton_iff.1 hs
 
 /-! ### Disjointness -/
 
+protected theorem disjoint_iff : disjoint s t ↔ s ∩ t ⊆ ∅ := iff.rfl
+
+theorem disjoint_iff_inter_eq_empty : disjoint s t ↔ s ∩ t = ∅ :=
+disjoint_iff
+
 lemma _root_.disjoint.inter_eq : disjoint s t → s ∩ t = ∅ := disjoint.eq_bot
 
 lemma disjoint_left : disjoint s t ↔ ∀ ⦃a⦄, a ∈ s → a ∉ t := forall_congr $ λ _, not_and

src/data/set/lattice.lean

@@ -1579,11 +1579,6 @@ end disjoint
 
 namespace set
 
-protected theorem disjoint_iff : disjoint s t ↔ s ∩ t ⊆ ∅ := iff.rfl
-
-theorem disjoint_iff_inter_eq_empty : disjoint s t ↔ s ∩ t = ∅ :=
-disjoint_iff
-
 lemma not_disjoint_iff : ¬disjoint s t ↔ ∃ x, x ∈ s ∧ x ∈ t :=
 not_forall.trans $ exists_congr $ λ x, not_not
 

src/data/set/prod.lean

@@ -430,20 +430,19 @@ lemma pi_eq_empty_iff : s.pi t = ∅ ↔ ∃ i, is_empty (α i) ∨ i ∈ s ∧
 begin
   rw [← not_nonempty_iff_eq_empty, pi_nonempty_iff],
   push_neg,
-  refine exists_congr (λ i, ⟨λ h, (is_empty_or_nonempty (α i)).imp_right _, _⟩),
-  { rintro ⟨x⟩,
-    exact ⟨(h x).1, by simp [eq_empty_iff_forall_not_mem, h]⟩ },
-  { rintro (h | h) x,
-    { exact h.elim' x },
-    { simp [h] } }
+  refine exists_congr (λ i, _),
+  casesI is_empty_or_nonempty (α i); simp [*, forall_and_distrib, eq_empty_iff_forall_not_mem],
 end
 
-lemma univ_pi_eq_empty_iff : pi univ t = ∅ ↔ ∃ i, t i = ∅ :=
+@[simp] lemma univ_pi_eq_empty_iff : pi univ t = ∅ ↔ ∃ i, t i = ∅ :=
 by simp [← not_nonempty_iff_eq_empty, univ_pi_nonempty_iff]
 
 @[simp] lemma univ_pi_empty [h : nonempty ι] : pi univ (λ i, ∅ : Π i, set (α i)) = ∅ :=
 univ_pi_eq_empty_iff.2 $ h.elim $ λ x, ⟨x, rfl⟩
 
+@[simp] lemma disjoint_univ_pi : disjoint (pi univ t₁) (pi univ t₂) ↔ ∃ i, disjoint (t₁ i) (t₂ i) :=
+by simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, univ_pi_eq_empty_iff]
+
 @[simp] lemma range_dcomp (f : Π i, α i → β i) :
   range (λ (g : Π i, α i), (λ i, f i (g i))) = pi univ (λ i, range (f i)) :=
 begin
@@ -525,6 +524,18 @@ lemma eval_image_pi (hs : i ∈ s) (ht : (s.pi t).nonempty) : eval i '' s.pi t =
   (λ f : Π i, α i, f i) '' pi univ t = t i :=
 eval_image_pi (mem_univ i) ht
 
+lemma pi_subset_pi_iff : pi s t₁ ⊆ pi s t₂ ↔ (∀ i ∈ s, t₁ i ⊆ t₂ i) ∨ pi s t₁ = ∅ :=
+begin
+  refine ⟨λ h, or_iff_not_imp_right.2 _, λ h, h.elim pi_mono (λ h', h'.symm ▸ empty_subset _)⟩,
+  rw [← ne.def, ne_empty_iff_nonempty],
+  intros hne i hi,
+  simpa only [eval_image_pi hi hne, eval_image_pi hi (hne.mono h)]
+    using image_subset (λ f : Π i, α i, f i) h
+end
+
+lemma univ_pi_subset_univ_pi_iff : pi univ t₁ ⊆ pi univ t₂ ↔ (∀ i, t₁ i ⊆ t₂ i) ∨ ∃ i, t₁ i = ∅ :=
+by simp [pi_subset_pi_iff]
+
 lemma eval_preimage [decidable_eq ι] {s : set (α i)} :
   eval i ⁻¹' s = pi univ (update (λ i, univ) i s) :=
 by { ext x, simp [@forall_update_iff _ (λ i, set (α i)) _ _ _ _ (λ i' y, x i' ∈ y)] }