feat(combinatorics/simple_graph/prod): add finset lemma and remove unecessary decidable_eq (#17461)

eric-wieser · eric-wieser · commit 2985fa3c31a2 · 2022-11-15T12:38:55.000Z
Now that `[fintype (G.neighbor_set x.1)] [fintype (H.neighbor_set x.2)]` alone implies `fintype ((G □ H).neighbor_set x)` without additional `decidable_eq` arguments, there is no real need to supply the latter argument to lemmas about `(G □ H).neighbor_finset`.

The new `simple_graph.box_prod_neighbor_finset` lemma unfortunately isn't true by refl, but the new fintype instance now at least has the right asymptotic complexity in computation.
diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean
@@ -788,6 +788,15 @@ lemma neighbor_finset_def : G.neighbor_finset v = (G.neighbor_set v).to_finset :
   w ∈ G.neighbor_finset v ↔ G.adj v w :=
 set.mem_to_finset
 
+@[simp] lemma not_mem_neighbor_finset_self : v ∉ G.neighbor_finset v :=
+(mem_neighbor_finset _ _ _).not.mpr $ G.loopless _
+
+lemma neighbor_finset_disjoint_singleton : disjoint (G.neighbor_finset v) {v} :=
+finset.disjoint_singleton_right.mpr $ not_mem_neighbor_finset_self _ _
+
+lemma singleton_disjoint_neighbor_finset : disjoint {v} (G.neighbor_finset v) :=
+finset.disjoint_singleton_left.mpr $ not_mem_neighbor_finset_self _ _
+
 /--
 `G.degree v` is the number of vertices adjacent to `v`.
 -/
diff --git a/src/combinatorics/simple_graph/prod.lean b/src/combinatorics/simple_graph/prod.lean
@@ -173,31 +173,36 @@ by { haveI := (nonempty_prod.1 h.nonempty).1, haveI := (nonempty_prod.1 h.nonemp
 @[simp] lemma box_prod_connected : (G □ H).connected ↔ G.connected ∧ H.connected :=
 ⟨λ h, ⟨h.of_box_prod_left, h.of_box_prod_right⟩, λ h, h.1.box_prod h.2⟩
 
-instance [decidable_eq α] [decidable_eq β] (x : α × β)
+instance box_prod_fintype_neighbor_set (x : α × β)
   [fintype (G.neighbor_set x.1)] [fintype (H.neighbor_set x.2)] :
   fintype ((G □ H).neighbor_set x) :=
+fintype.of_equiv
+  ((G.neighbor_finset x.1 ×ˢ {x.2}).disj_union ({x.1} ×ˢ H.neighbor_finset x.2)
+      $ finset.disjoint_product.mpr $ or.inl $ neighbor_finset_disjoint_singleton _ _)
+  ((equiv.refl _).subtype_equiv $ λ y, begin
+    simp_rw [finset.mem_disj_union, finset.mem_product, finset.mem_singleton,
+          mem_neighbor_finset, mem_neighbor_set, equiv.refl_apply, box_prod_adj],
+    simp only [eq_comm, and_comm],
+  end)
+
+lemma box_prod_neighbor_finset (x : α × β)
+  [fintype (G.neighbor_set x.1)] [fintype (H.neighbor_set x.2)] [fintype ((G □ H).neighbor_set x)] :
+  (G □ H).neighbor_finset x =
+    (G.neighbor_finset x.1 ×ˢ {x.2}).disj_union ({x.1} ×ˢ H.neighbor_finset x.2)
+      (finset.disjoint_product.mpr $ or.inl $ neighbor_finset_disjoint_singleton _ _) :=
 begin
-  rw box_prod_neighbor_set,
-  apply_instance,
+  -- swap out the fintype instance for the canonical one
+  letI : fintype ((G □ H).neighbor_set x) := simple_graph.box_prod_fintype_neighbor_set _,
+  refine eq.trans _ finset.attach_map_val,
+  convert (finset.map_map _ (function.embedding.subtype _) finset.univ),
 end
 
 lemma box_prod_degree (x : α × β)
-  [fintype (G.neighbor_set x.1)] [fintype (H.neighbor_set x.2)]
-  [fintype ((G □ H).neighbor_set x)] :
+  [fintype (G.neighbor_set x.1)] [fintype (H.neighbor_set x.2)] [fintype ((G □ H).neighbor_set x)] :
   (G □ H).degree x = G.degree x.1 + H.degree x.2 :=
 begin
-  classical,
-  simp_rw [← card_neighbor_set_eq_degree, box_prod_neighbor_set,
-    ← set.to_finset_card, set.to_finset_union],
-  convert finset.card_disjoint_union _;
-    simp only [set.to_finset_prod, finset.card_product, set.to_finset_card,
-      set.card_singleton, mul_one, one_mul],
-  { rw finset.disjoint_left,
-    rintro ⟨_,_⟩ hG hH,
-    simp only [finset.mem_product, set.mem_to_finset,
-      mem_neighbor_set, set.mem_singleton_iff] at hG hH,
-    obtain ⟨⟨q, rfl⟩, ⟨rfl, _⟩⟩ := ⟨hG, hH⟩,
-    exact (q.ne rfl).elim, },
+  rw [degree, degree, degree, box_prod_neighbor_finset, finset.card_disj_union],
+  simp_rw [finset.card_product, finset.card_singleton, mul_one, one_mul],
 end
 
 end simple_graph
diff --git a/src/data/finset/basic.lean b/src/data/finset/basic.lean
@@ -2165,7 +2165,7 @@ ext $ λ _, by simpa only [mem_map, exists_prop] using exists_eq_right
   s.map (equiv.cast h).to_embedding == s :=
 by { subst h, simp }
 
-theorem map_map {g : β ↪ γ} : (s.map f).map g = s.map (f.trans g) :=
+theorem map_map (f : α ↪ β) (g : β ↪ γ) (s : finset α) : (s.map f).map g = s.map (f.trans g) :=
 eq_of_veq $ by simp only [map_val, multiset.map_map]; refl
 
 lemma map_comm {β'} {f : β ↪ γ} {g : α ↪ β} {f' : α ↪ β'} {g' : β' ↪ γ}
