feat(data/set/finite): Add off_diag finitary instance and lemmas (#…

…16923)

Adds a `fintype` instance for `off_diag`, finite lemmas for it, and adds a related missing prod lemma.



Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>

src/data/fintype/basic.lean

@@ -693,6 +693,9 @@ lemma to_finset_prod (s : set α) (t : set β) [fintype s] [fintype t] [fintype
   (s ×ˢ t).to_finset = s.to_finset ×ˢ t.to_finset :=
 by { ext, simp }
 
+lemma to_finset_off_diag {s : set α} [decidable_eq α] [fintype s] [fintype s.off_diag] :
+s.off_diag.to_finset = s.to_finset.off_diag := finset.ext $ by simp
+
 /- TODO Without the coercion arrow (`↥`) there is an elaboration bug;
 it essentially infers `fintype.{v} (set.univ.{u} : set α)` with `v` and `u` distinct.
 Reported in leanprover-community/lean#672 -/

src/data/set/finite.lean

@@ -312,6 +312,9 @@ instance fintype_prod (s : set α) (t : set β) [fintype s] [fintype t] :
   fintype (s ×ˢ t : set (α × β)) :=
 fintype.of_finset (s.to_finset ×ˢ t.to_finset) $ by simp
 
+instance fintype_off_diag [decidable_eq α] (s : set α) [fintype s] : fintype s.off_diag :=
+fintype.of_finset s.to_finset.off_diag $ by simp
+
 /-- `image2 f s t` is `fintype` if `s` and `t` are. -/
 instance fintype_image2 [decidable_eq γ] (f : α → β → γ) (s : set α) (t : set β)
   [hs : fintype s] [ht : fintype t] : fintype (image2 f s t : set γ) :=
@@ -580,6 +583,9 @@ lemma finite.prod {s : set α} {t : set β} (hs : s.finite) (ht : t.finite) :
   (s ×ˢ t : set (α × β)).finite :=
 by { casesI hs, casesI ht, apply to_finite }
 
+lemma finite.off_diag {s : set α} (hs : s.finite) : s.off_diag.finite :=
+by { classical, casesI hs, apply set.to_finite }
+
 lemma finite.image2 (f : α → β → γ) {s : set α} {t : set β} (hs : s.finite) (ht : t.finite) :
   (image2 f s t).finite :=
 by { casesI hs, casesI ht, apply to_finite }
@@ -668,6 +674,12 @@ lemma finite.to_finset_insert' [decidable_eq α] {a : α} {s : set α} (hs : s.f
   (hs.insert a).to_finset = insert a hs.to_finset :=
 finite.to_finset_insert _
 
+lemma finite.to_finset_prod {s : set α} {t : set β} (hs : s.finite) (ht : t.finite) :
+hs.to_finset ×ˢ ht.to_finset = (hs.prod ht).to_finset := finset.ext $ by simp
+
+lemma finite.to_finset_off_diag {s : set α} [decidable_eq α] (hs : s.finite) :
+hs.off_diag.to_finset = hs.to_finset.off_diag := finset.ext $ by simp
+
 lemma finite.fin_embedding {s : set α} (h : s.finite) : ∃ (n : ℕ) (f : fin n ↪ α), range f = s :=
 ⟨_, (fintype.equiv_fin (h.to_finset : set α)).symm.as_embedding, by simp⟩