feat: More clique lemmas (#8007)

Forward port leanprover-community/mathlib#19203

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -9,7 +9,7 @@ import Mathlib.Data.Rel
 import Mathlib.Data.Set.Finite
 import Mathlib.Data.Sym.Card
 
-#align_import combinatorics.simple_graph.basic from "leanprover-community/mathlib"@"c6ef6387ede9983aee397d442974e61f89dfd87b"
+#align_import combinatorics.simple_graph.basic from "leanprover-community/mathlib"@"3365b20c2ffa7c35e47e5209b89ba9abdddf3ffe"
 
 /-!
 # Simple graphs
@@ -578,12 +578,15 @@ variable {G G₁ G₂}
 
 @[simp] lemma disjoint_edgeSet : Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂ := by
   rw [Set.disjoint_iff, disjoint_iff_inf_le, ← edgeSet_inf, ← edgeSet_bot, ← Set.le_iff_subset,
-  OrderEmbedding.le_iff_le]
+    OrderEmbedding.le_iff_le]
+#align simple_graph.disjoint_edge_set SimpleGraph.disjoint_edgeSet
 
 @[simp] lemma edgeSet_eq_empty : G.edgeSet = ∅ ↔ G = ⊥ := by rw [← edgeSet_bot, edgeSet_inj]
+#align simple_graph.edge_set_eq_empty SimpleGraph.edgeSet_eq_empty
 
 @[simp] lemma edgeSet_nonempty : G.edgeSet.Nonempty ↔ G ≠ ⊥ := by
   rw [Set.nonempty_iff_ne_empty, edgeSet_eq_empty.ne]
+#align simple_graph.edge_set_nonempty SimpleGraph.edgeSet_nonempty
 
 /-- This lemma, combined with `edgeSet_sdiff` and `edgeSet_from_edgeSet`,
 allows proving `(G \ from_edgeSet s).edge_set = G.edgeSet \ s` by `simp`. -/
@@ -729,9 +732,11 @@ theorem fromEdgeSet_mono {s t : Set (Sym2 V)} (h : s ⊆ t) : fromEdgeSet s ≤
   conv_rhs => rw [← Set.diff_union_inter s {e : Sym2 V | e.IsDiag}]
   rw [← disjoint_edgeSet,  edgeSet_fromEdgeSet, Set.disjoint_union_right, and_iff_left]
   exact Set.disjoint_left.2 fun e he he' ↦ not_isDiag_of_mem_edgeSet _ he he'.2
+#align simple_graph.disjoint_from_edge_set SimpleGraph.disjoint_fromEdgeSet
 
 @[simp] lemma fromEdgeSet_disjoint : Disjoint (fromEdgeSet s) G ↔ Disjoint s G.edgeSet := by
   rw [disjoint_comm, disjoint_fromEdgeSet, disjoint_comm]
+#align simple_graph.from_edge_set_disjoint SimpleGraph.fromEdgeSet_disjoint
 
 instance [DecidableEq V] [Fintype s] : Fintype (fromEdgeSet s).edgeSet := by
   rw [edgeSet_fromEdgeSet s]
@@ -1028,6 +1033,9 @@ theorem mem_neighborSet (v w : V) : w ∈ G.neighborSet v ↔ G.Adj v w :=
   Iff.rfl
 #align simple_graph.mem_neighbor_set SimpleGraph.mem_neighborSet
 
+lemma not_mem_neighborSet_self : a ∉ G.neighborSet a := by simp
+#align simple_graph.not_mem_neighbor_set_self SimpleGraph.not_mem_neighborSet_self
+
 @[simp]
 theorem mem_incidenceSet (v w : V) : ⟦(v, w)⟧ ∈ G.incidenceSet v ↔ G.Adj v w := by
   simp [incidenceSet]
@@ -1197,8 +1205,10 @@ theorem deleteEdges_eq_sdiff_fromEdgeSet (s : Set (Sym2 V)) :
   exact ⟨fun h => ⟨h.1, not_and_of_not_left _ h.2⟩, fun h => ⟨h.1, not_and'.mp h.2 h.ne⟩⟩
 #align simple_graph.delete_edges_eq_sdiff_from_edge_set SimpleGraph.deleteEdges_eq_sdiff_fromEdgeSet
 
-@[simp] lemma deleteEdges_eq {s : Set (Sym2 V)} : G.deleteEdges s = G ↔ Disjoint G.edgeSet s := by
+@[simp]
+lemma deleteEdges_eq_self {s : Set (Sym2 V)} : G.deleteEdges s = G ↔ Disjoint G.edgeSet s := by
   rw [deleteEdges_eq_sdiff_fromEdgeSet, sdiff_eq_left, disjoint_fromEdgeSet]
+#align simple_graph.delete_edges_eq SimpleGraph.deleteEdges_eq_self
 
 theorem compl_eq_deleteEdges : Gᶜ = (⊤ : SimpleGraph V).deleteEdges G.edgeSet := by
   ext
@@ -1279,11 +1289,11 @@ variable {G}
 theorem deleteFar_iff :
     G.DeleteFar p r ↔ ∀ ⦃H : SimpleGraph _⦄ [DecidableRel H.Adj],
       H ≤ G → p H → r ≤ G.edgeFinset.card - H.edgeFinset.card := by
-  refine' ⟨fun h H _ hHG hH => _, fun h s hs hG => _⟩
+  refine ⟨fun h H _ hHG hH ↦ ?_, fun h s hs hG ↦ ?_⟩
   · have := h (sdiff_subset G.edgeFinset H.edgeFinset)
     simp only [deleteEdges_sdiff_eq_of_le _ hHG, edgeFinset_mono hHG, card_sdiff,
       card_le_of_subset, coe_sdiff, coe_edgeFinset, Nat.cast_sub] at this
-    convert this hH
+    exact this hH
   · classical
     simpa [card_sdiff hs, edgeFinset_deleteEdges, -Set.toFinset_card, Nat.cast_sub,
       card_le_of_subset hs] using h (G.deleteEdges_le s) hG
@@ -1352,6 +1362,10 @@ protected def map (f : V ↪ W) (G : SimpleGraph V) : SimpleGraph W where
     exact h.ne (f.injective h'.symm)
 #align simple_graph.map SimpleGraph.map
 
+instance instDecidableMapAdj {f : V ↪ W} {a b} [Decidable (Relation.Map G.Adj f f a b)] :
+    Decidable ((G.map f).Adj a b) := ‹Decidable (Relation.Map G.Adj f f a b)›
+#align simple_graph.decidable_map SimpleGraph.instDecidableMapAdj
+
 @[simp]
 theorem map_adj (f : V ↪ W) (G : SimpleGraph V) (u v : W) :
     (G.map f).Adj u v ↔ ∃ u' v' : V, G.Adj u' v' ∧ f u' = u ∧ f v' = v :=
@@ -1360,6 +1374,7 @@ theorem map_adj (f : V ↪ W) (G : SimpleGraph V) (u v : W) :
 
 lemma map_adj_apply {G : SimpleGraph V} {f : V ↪ W} {a b : V} :
     (G.map f).Adj (f a) (f b) ↔ G.Adj a b := by simp
+#align simple_graph.map_adj_apply SimpleGraph.map_adj_apply
 
 theorem map_monotone (f : V ↪ W) : Monotone (SimpleGraph.map f) := by
   rintro G G' h _ _ ⟨u, v, ha, rfl, rfl⟩
@@ -1368,12 +1383,11 @@ theorem map_monotone (f : V ↪ W) : Monotone (SimpleGraph.map f) := by
 
 @[simp] lemma map_id : G.map (Function.Embedding.refl _) = G :=
   SimpleGraph.ext _ _ $ Relation.map_id_id _
+#align simple_graph.map_id SimpleGraph.map_id
 
 @[simp] lemma map_map (f : V ↪ W) (g : W ↪ X) : (G.map f).map g = G.map (f.trans g) :=
   SimpleGraph.ext _ _ $ Relation.map_map _ _ _ _ _
-
-instance instDecidableMapAdj (f : V ↪ W) (G : SimpleGraph V)
-    [DecidableRel (Relation.Map G.Adj f f)] : DecidableRel (G.map f).Adj := ‹DecidableRel _›
+#align simple_graph.map_map SimpleGraph.map_map
 
 /-- Given a function, there is a contravariant induced map on graphs by pulling back the
 adjacency relation.
@@ -1390,9 +1404,11 @@ protected def comap (f : V → W) (G : SimpleGraph W) : SimpleGraph V where
     (G.comap f).Adj u v ↔ G.Adj (f u) (f v) := Iff.rfl
 
 @[simp] lemma comap_id {G : SimpleGraph V} : G.comap id = G := SimpleGraph.ext _ _ rfl
+#align simple_graph.comap_id SimpleGraph.comap_id
 
 @[simp] lemma comap_comap {G : SimpleGraph X} (f : V → W) (g : W → X) :
   (G.comap g).comap f = G.comap (g ∘ f) := rfl
+#align simple_graph.comap_comap SimpleGraph.comap_comap
 
 instance instDecidableComapAdj (f : V → W) (G : SimpleGraph W) [DecidableRel G.Adj] :
     DecidableRel (G.comap f).Adj := fun _ _ ↦ ‹DecidableRel G.Adj› _ _
@@ -1401,9 +1417,11 @@ lemma comap_symm (G : SimpleGraph V) (e : V ≃ W) :
     G.comap e.symm.toEmbedding = G.map e.toEmbedding := by
   ext; simp only [Equiv.apply_eq_iff_eq_symm_apply, comap_adj, map_adj, Equiv.toEmbedding_apply,
     exists_eq_right_right, exists_eq_right]
+#align simple_graph.comap_symm SimpleGraph.comap_symm
 
 lemma map_symm (G : SimpleGraph W) (e : V ≃ W) :
     G.map e.symm.toEmbedding = G.comap e.toEmbedding := by rw [← comap_symm, e.symm_symm]
+#align simple_graph.map_symm SimpleGraph.map_symm
 
 theorem comap_monotone (f : V ↪ W) : Monotone (SimpleGraph.comap f) := by
   intro G G' h _ _ ha
@@ -1459,15 +1477,18 @@ protected def _root_.Equiv.simpleGraph (e : V ≃ W) : SimpleGraph V ≃ SimpleG
   invFun := SimpleGraph.comap e
   left_inv _ := by simp
   right_inv _ := by simp
+#align equiv.simple_graph Equiv.simpleGraph
 
 @[simp] lemma _root_.Equiv.simpleGraph_refl : (Equiv.refl V).simpleGraph = Equiv.refl _ := by
   ext; rfl
 
 @[simp] lemma _root_.Equiv.simpleGraph_trans (e₁ : V ≃ W) (e₂ : W ≃ X) :
   (e₁.trans e₂).simpleGraph = e₁.simpleGraph.trans e₂.simpleGraph := rfl
+#align equiv.simple_graph_trans Equiv.simpleGraph_trans
 
 @[simp]
 lemma _root_.Equiv.symm_simpleGraph (e : V ≃ W) : e.simpleGraph.symm = e.symm.simpleGraph := rfl
+#align equiv.symm_simple_graph Equiv.symm_simpleGraph
 
 /-! ## Induced graphs -/
 
@@ -1858,10 +1879,10 @@ protected abbrev id : G →g G :=
   RelHom.id _
 #align simple_graph.hom.id SimpleGraph.Hom.id
 
-@[simp, norm_cast] lemma coe_id : ⇑(Hom.id : G →g G) = _root_.id := rfl
+@[simp, norm_cast] lemma coe_id : ⇑(Hom.id : G →g G) = id := rfl
+#align simple_graph.hom.coe_id SimpleGraph.Hom.coe_id
 
-instance [Subsingleton (V → W)] : Subsingleton (G →g H) :=
-  FunLike.coe_injective.subsingleton
+instance [Subsingleton (V → W)] : Subsingleton (G →g H) := FunLike.coe_injective.subsingleton
 
 instance [IsEmpty V] : Unique (G →g H) where
   default := ⟨isEmptyElim, fun {a} ↦ isEmptyElim a⟩
@@ -1953,8 +1974,10 @@ theorem coe_comp (f' : G' →g G'') (f : G →g G') : ⇑(f'.comp f) = f' ∘ f
 
 /-- The graph homomorphism from a smaller graph to a bigger one. -/
 def ofLe (h : G₁ ≤ G₂) : G₁ →g G₂ := ⟨id, @h⟩
+#align simple_graph.hom.of_le SimpleGraph.Hom.ofLe
 
 @[simp, norm_cast] lemma coe_ofLe (h : G₁ ≤ G₂) : ⇑(ofLe h) = id := rfl
+#align simple_graph.hom.coe_of_le SimpleGraph.Hom.coe_ofLe
 
 end Hom
 
@@ -1973,6 +1996,7 @@ abbrev toHom : G →g G' :=
 #align simple_graph.embedding.to_hom SimpleGraph.Embedding.toHom
 
 @[simp] lemma coe_toHom (f : G ↪g H) : ⇑f.toHom = f := rfl
+#align simple_graph.embedding.coe_to_hom SimpleGraph.Embedding.coe_toHom
 
 @[simp] theorem map_adj_iff {v w : V} : G'.Adj (f v) (f w) ↔ G.Adj v w :=
   f.map_rel_iff