feat(combinatorics/simple_graph/*): some more from_edge_set and `ed…

…ge_set` lemmas (#17723)

Co-authored-by: Kyle Miller <kmill31415@gmail.com>



Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

src/combinatorics/simple_graph/basic.lean

@@ -73,7 +73,9 @@ finitely many vertices.
   in order to start learning what the combinatorics hierarchy should
   look like.
 -/
-open finset
+
+open finset function
+
 universes u v w
 
 /--
@@ -270,19 +272,66 @@ def neighbor_set (v : V) : set V := set_of (G.adj v)
 instance neighbor_set.mem_decidable (v : V) [decidable_rel G.adj] :
   decidable_pred (∈ G.neighbor_set v) := by { unfold neighbor_set, apply_instance }
 
+section edge_set
+variables {G₁ G₂ : simple_graph V}
+
 /--
 The edges of G consist of the unordered pairs of vertices related by
 `G.adj`.
 
 The way `edge_set` is defined is such that `mem_edge_set` is proved by `refl`.
 (That is, `⟦(v, w)⟧ ∈ G.edge_set` is definitionally equal to `G.adj v w`.)
 -/
-def edge_set : set (sym2 V) := sym2.from_rel G.symm
+def edge_set : simple_graph V ↪o set (sym2 V) :=
+order_embedding.of_map_le_iff (λ G, sym2.from_rel G.symm) $
+  λ G G', ⟨λ h a b, @h ⟦(a, b)⟧, λ h e, sym2.ind @h e⟩
 
 @[simp] lemma mem_edge_set : ⟦(v, w)⟧ ∈ G.edge_set ↔ G.adj v w := iff.rfl
 
-lemma edge_set_mono {G G' : simple_graph V} (h : G ≤ G') : G.edge_set ⊆ G'.edge_set :=
-λ e, sym2.ind (λ v w, @h v w) e
+lemma not_is_diag_of_mem_edge_set : e ∈ G.edge_set → ¬ e.is_diag := sym2.ind (λ v w, adj.ne) e
+
+@[simp] lemma edge_set_inj : G₁.edge_set = G₂.edge_set ↔ G₁ = G₂ :=
+(edge_set : simple_graph V ↪o set (sym2 V)).eq_iff_eq
+
+@[simp] lemma edge_set_subset_edge_set : G₁.edge_set ⊆ G₂.edge_set ↔ G₁ ≤ G₂ :=
+(edge_set : simple_graph V ↪o set (sym2 V)).le_iff_le
+
+@[simp] lemma edge_set_ssubset_edge_set : G₁.edge_set ⊂ G₂.edge_set ↔ G₁ < G₂ :=
+(edge_set : simple_graph V ↪o set (sym2 V)).lt_iff_lt
+
+lemma edge_set_injective : injective (edge_set : simple_graph V → set (sym2 V)) :=
+edge_set.injective
+
+alias edge_set_subset_edge_set ↔ _ edge_set_mono
+alias edge_set_ssubset_edge_set ↔ _ edge_set_strict_mono
+
+attribute [mono] edge_set_mono edge_set_strict_mono
+
+variables (G₁ G₂)
+
+@[simp] lemma edge_set_bot : (⊥ : simple_graph V).edge_set = ∅ := sym2.from_rel_bot
+
+@[simp] lemma edge_set_sup : (G₁ ⊔ G₂).edge_set = G₁.edge_set ∪ G₂.edge_set :=
+by { ext ⟨x, y⟩, refl }
+
+@[simp] lemma edge_set_inf : (G₁ ⊓ G₂).edge_set = G₁.edge_set ∩ G₂.edge_set :=
+by { ext ⟨x, y⟩, refl }
+
+@[simp] lemma edge_set_sdiff : (G₁ \ G₂).edge_set = G₁.edge_set \ G₂.edge_set :=
+by { ext ⟨x, y⟩, refl }
+
+/--
+This lemma, combined with `edge_set_sdiff` and `edge_set_from_edge_set`,
+allows proving `(G \ from_edge_set s).edge_set = G.edge_set \ s` by `simp`.
+-/
+@[simp] lemma edge_set_sdiff_sdiff_is_diag (G : simple_graph V) (s : set (sym2 V)) :
+  G.edge_set \ (s \ {e | e.is_diag}) = G.edge_set \ s :=
+begin
+  ext e,
+  simp only [set.mem_diff, set.mem_set_of_eq, not_and, not_not, and.congr_right_iff],
+  intro h,
+  simp only [G.not_is_diag_of_mem_edge_set h, imp_false],
+end
 
 /--
 Two vertices are adjacent iff there is an edge between them. The
@@ -314,9 +363,26 @@ end
 instance decidable_mem_edge_set [decidable_rel G.adj] :
   decidable_pred (∈ G.edge_set) := sym2.from_rel.decidable_pred _
 
-instance edges_fintype [decidable_eq V] [fintype V] [decidable_rel G.adj] :
+instance fintype_edge_set [decidable_eq V] [fintype V] [decidable_rel G.adj] :
   fintype G.edge_set := subtype.fintype _
 
+instance fintype_edge_set_bot : fintype (⊥ : simple_graph V).edge_set :=
+by { rw edge_set_bot, apply_instance }
+
+instance fintype_edge_set_sup [decidable_eq V] [fintype G₁.edge_set] [fintype G₂.edge_set] :
+  fintype (G₁ ⊔ G₂).edge_set :=
+by { rw edge_set_sup, apply_instance }
+
+instance fintype_edge_set_inf [decidable_eq V] [fintype G₁.edge_set] [fintype G₂.edge_set] :
+  fintype (G₁ ⊓ G₂).edge_set :=
+by { rw edge_set_inf, exact set.fintype_inter _ _ }
+
+instance fintype_edge_set_sdiff [decidable_eq V] [fintype G₁.edge_set] [fintype G₂.edge_set] :
+  fintype (G₁ \ G₂).edge_set :=
+by { rw edge_set_sdiff, exact set.fintype_diff _ _  }
+
+end edge_set
+
 section from_edge_set
 
 variable (s : set (sym2 V))
@@ -332,7 +398,7 @@ def from_edge_set : simple_graph V :=
 
 -- Note: we need to make sure `from_edge_set_adj` and this lemma are confluent.
 -- In particular, both yield `⟦(u, v)⟧ ∈ (from_edge_set s).edge_set` ==> `⟦(v, w)⟧ ∈ s ∧ v ≠ w`.
-@[simp] lemma edge_set_from_edge_set : (from_edge_set s).edge_set = {e ∈ s | ¬ e.is_diag} :=
+@[simp] lemma edge_set_from_edge_set : (from_edge_set s).edge_set = s \ {e | e.is_diag} :=
 by { ext e, exact sym2.ind (by simp) e }
 
 @[simp] lemma from_edge_set_edge_set : from_edge_set G.edge_set = G :=
@@ -344,6 +410,26 @@ by { ext v w, simp only [from_edge_set_adj, set.mem_empty_iff_false, false_and,
 @[simp] lemma from_edge_set_univ : from_edge_set (set.univ : set (sym2 V)) = ⊤ :=
 by { ext v w, simp only [from_edge_set_adj, set.mem_univ, true_and, top_adj] }
 
+@[simp] lemma from_edge_set_inf (s t : set (sym2 V)) :
+  from_edge_set s ⊓ from_edge_set t = from_edge_set (s ∩ t) :=
+by { ext v w, simp only [from_edge_set_adj, set.mem_inter_iff, ne.def, inf_adj], tauto, }
+
+@[simp] lemma from_edge_set_sup (s t : set (sym2 V)) :
+  from_edge_set s ⊔ from_edge_set t = from_edge_set (s ∪ t) :=
+by { ext v w, simp [set.mem_union, or_and_distrib_right], }
+
+@[simp] lemma from_edge_set_sdiff (s t : set (sym2 V)) :
+  from_edge_set s \ from_edge_set t = from_edge_set (s \ t) :=
+by { ext v w, split; simp { contextual := tt }, }
+
+@[mono]
+lemma from_edge_set_mono {s t : set (sym2 V)} (h : s ⊆ t) : from_edge_set s ≤ from_edge_set t :=
+begin
+  rintro v w,
+  simp only [from_edge_set_adj, ne.def, not_false_iff, and_true, and_imp] {contextual := tt},
+  exact λ vws _, h vws,
+end
+
 instance [decidable_eq V] [fintype s] : fintype (from_edge_set s).edge_set :=
 by { rw edge_set_from_edge_set s, apply_instance }
 
@@ -487,30 +573,54 @@ end
 instance decidable_mem_incidence_set [decidable_eq V] [decidable_rel G.adj] (v : V) :
   decidable_pred (∈ G.incidence_set v) := λ e, and.decidable
 
+section edge_finset
+variables {G₁ G₂ : simple_graph V} [fintype G.edge_set] [fintype G₁.edge_set] [fintype G₂.edge_set]
+
 /--
 The `edge_set` of the graph as a `finset`.
 -/
-@[reducible] def edge_finset [fintype G.edge_set] : finset (sym2 V) :=
-set.to_finset G.edge_set
-
-@[simp] lemma mem_edge_finset [fintype G.edge_set] (e : sym2 V) :
-  e ∈ G.edge_finset ↔ e ∈ G.edge_set :=
-set.mem_to_finset
+@[reducible] def edge_finset : finset (sym2 V) := set.to_finset G.edge_set
 
-@[simp, norm_cast] lemma coe_edge_finset [fintype G.edge_set] :
-  (G.edge_finset : set (sym2 V)) = G.edge_set :=
+@[simp, norm_cast] lemma coe_edge_finset : (G.edge_finset : set (sym2 V)) = G.edge_set :=
 set.coe_to_finset _
 
-lemma edge_finset_mono {G G' : simple_graph V} [fintype G.edge_set] [fintype G'.edge_set] :
-  G ≤ G' → G.edge_finset ⊆ G'.edge_finset :=
-by { simp_rw [←coe_subset, coe_edge_finset], exact edge_set_mono }
+variables {G}
+
+@[simp] lemma mem_edge_finset : e ∈ G.edge_finset ↔ e ∈ G.edge_set := set.mem_to_finset
+
+lemma not_is_diag_of_mem_edge_finset : e ∈ G.edge_finset → ¬ e.is_diag :=
+not_is_diag_of_mem_edge_set _ ∘ mem_edge_finset.1
+
+@[simp] lemma edge_finset_inj : G₁.edge_finset = G₂.edge_finset ↔ G₁ = G₂ := by simp [edge_finset]
+
+@[simp] lemma edge_finset_subset_edge_finset : G₁.edge_finset ⊆ G₂.edge_finset ↔ G₁ ≤ G₂ :=
+by simp [edge_finset]
+
+@[simp] lemma edge_finset_ssubset_edge_finset : G₁.edge_finset ⊂ G₂.edge_finset ↔ G₁ < G₂ :=
+by simp [edge_finset]
+
+alias edge_finset_subset_edge_finset ↔ _ edge_finset_mono
+alias edge_finset_ssubset_edge_finset ↔ _ edge_finset_strict_mono
+
+attribute [mono] edge_finset_mono edge_finset_strict_mono
+
+@[simp] lemma edge_finset_bot : (⊥ : simple_graph V).edge_finset = ∅ := by simp [edge_finset]
+
+@[simp] lemma edge_finset_sup : (G₁ ⊔ G₂).edge_finset = G₁.edge_finset ∪ G₂.edge_finset :=
+by simp [edge_finset]
+
+@[simp] lemma edge_finset_inf : (G₁ ⊓ G₂).edge_finset = G₁.edge_finset ∩ G₂.edge_finset :=
+by simp [edge_finset]
+
+@[simp] lemma edge_finset_sdiff : (G₁ \ G₂).edge_finset = G₁.edge_finset \ G₂.edge_finset :=
+by simp [edge_finset]
+
+lemma edge_finset_card : G.edge_finset.card = fintype.card G.edge_set := set.to_finset_card _
 
-lemma edge_finset_card [fintype G.edge_set] : G.edge_finset.card = fintype.card G.edge_set :=
-set.to_finset_card _
+@[simp] lemma edge_set_univ_card : (univ : finset G.edge_set).card = G.edge_finset.card :=
+fintype.card_of_subtype G.edge_finset $ λ _, mem_edge_finset
 
-@[simp] lemma edge_set_univ_card [fintype G.edge_set] :
-  (univ : finset G.edge_set).card = G.edge_finset.card :=
-fintype.card_of_subtype G.edge_finset (mem_edge_finset _)
+end edge_finset
 
 @[simp] lemma mem_neighbor_set (v w : V) : w ∈ G.neighbor_set v ↔ G.adj v w :=
 iff.rfl

src/combinatorics/simple_graph/connectivity.lean

@@ -1651,22 +1651,25 @@ section bridge_edges
 are no longer reachable from one another. -/
 def is_bridge (G : simple_graph V) (e : sym2 V) : Prop :=
 e ∈ G.edge_set ∧
-sym2.lift ⟨λ v w, ¬ (G.delete_edges {e}).reachable v w, by simp [reachable_comm]⟩ e
+sym2.lift ⟨λ v w, ¬ (G \ from_edge_set {e}).reachable v w, by simp [reachable_comm]⟩ e
 
 lemma is_bridge_iff {u v : V} :
-  G.is_bridge ⟦(u, v)⟧ ↔ G.adj u v ∧ ¬ (G.delete_edges {⟦(u, v)⟧}).reachable u v := iff.rfl
+  G.is_bridge ⟦(u, v)⟧ ↔ G.adj u v ∧ ¬ (G \ from_edge_set {⟦(u, v)⟧}).reachable u v := iff.rfl
 
 lemma reachable_delete_edges_iff_exists_walk {v w : V} :
-  (G.delete_edges {⟦(v, w)⟧}).reachable v w ↔ ∃ (p : G.walk v w), ¬ ⟦(v, w)⟧ ∈ p.edges :=
+  (G \ from_edge_set {⟦(v, w)⟧}).reachable v w ↔ ∃ (p : G.walk v w), ¬ ⟦(v, w)⟧ ∈ p.edges :=
 begin
   split,
   { rintro ⟨p⟩,
-    use p.map (hom.map_spanning_subgraphs (G.delete_edges_le _)),
+    use p.map (hom.map_spanning_subgraphs (by simp)),
     simp_rw [walk.edges_map, list.mem_map, hom.map_spanning_subgraphs_apply, sym2.map_id', id.def],
     rintro ⟨e, h, rfl⟩,
     simpa using p.edges_subset_edge_set h, },
   { rintro ⟨p, h⟩,
-    exact ⟨p.to_delete_edge _ h⟩, },
+    refine ⟨p.transfer _ (λ e ep, _)⟩,
+    simp only [edge_set_sdiff, edge_set_from_edge_set, edge_set_sdiff_sdiff_is_diag,
+               set.mem_diff, set.mem_singleton_iff],
+    exact ⟨p.edges_subset_edge_set ep, λ h', h (h' ▸ ep)⟩,  },
 end
 
 lemma is_bridge_iff_adj_and_forall_walk_mem_edges {v w : V} :
@@ -1709,7 +1712,7 @@ begin
 end
 
 lemma adj_and_reachable_delete_edges_iff_exists_cycle {v w : V} :
-  G.adj v w ∧ (G.delete_edges {⟦(v, w)⟧}).reachable v w ↔
+  G.adj v w ∧ (G \ from_edge_set {⟦(v, w)⟧}).reachable v w ↔
   ∃ (u : V) (p : G.walk u u), p.is_cycle ∧ ⟦(v, w)⟧ ∈ p.edges :=
 begin
   classical,

src/data/fintype/basic.lean

@@ -482,23 +482,23 @@ by simp only [finset.ssubset_def, to_finset_subset, ssubset_def]
   disjoint s.to_finset t.to_finset ↔ disjoint s t :=
 by simp only [←disjoint_coe, coe_to_finset]
 
-lemma to_finset_inter {α : Type*} [decidable_eq α] (s t : set α) [fintype (s ∩ t : set α)]
+@[simp] lemma to_finset_inter {α : Type*} [decidable_eq α] (s t : set α) [fintype (s ∩ t : set α)]
   [fintype s] [fintype t] : (s ∩ t).to_finset = s.to_finset ∩ t.to_finset :=
 by { ext, simp }
 
-lemma to_finset_union {α : Type*} [decidable_eq α] (s t : set α) [fintype (s ∪ t : set α)]
+@[simp] lemma to_finset_union {α : Type*} [decidable_eq α] (s t : set α) [fintype (s ∪ t : set α)]
   [fintype s] [fintype t] : (s ∪ t).to_finset = s.to_finset ∪ t.to_finset :=
 by { ext, simp }
 
-lemma to_finset_diff {α : Type*} [decidable_eq α] (s t : set α) [fintype s] [fintype t]
+@[simp] lemma to_finset_diff {α : Type*} [decidable_eq α] (s t : set α) [fintype s] [fintype t]
   [fintype (s \ t : set α)] : (s \ t).to_finset = s.to_finset \ t.to_finset :=
 by { ext, simp }
 
 lemma to_finset_ne_eq_erase {α : Type*} [decidable_eq α] [fintype α] (a : α)
   [fintype {x : α | x ≠ a}] : {x : α | x ≠ a}.to_finset = finset.univ.erase a :=
 by { ext, simp }
 
-theorem to_finset_compl [decidable_eq α] [fintype α] (s : set α) [fintype s] [fintype ↥sᶜ] :
+@[simp] theorem to_finset_compl [decidable_eq α] [fintype α] (s : set α) [fintype s] [fintype ↥sᶜ] :
   (sᶜ).to_finset = s.to_finsetᶜ :=
 by { ext, simp }