diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean
index 5c66632b5e4b5..0b1d706d9e560 100644
--- a/src/combinatorics/simple_graph/basic.lean
+++ b/src/combinatorics/simple_graph/basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020 Aaron Anderson, Jalex Stark, Kyle Miller. All rights reserved
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Jalex Stark, Kyle Miller, Alena Gusakov, Hunter Monroe
 -/
+import data.fun_like.fintype
 import data.rel
 import data.set.finite
 import data.sym.sym2
@@ -288,6 +289,13 @@ instance : complete_boolean_algebra (simple_graph V) :=
 
 @[simps] instance (V : Type u) : inhabited (simple_graph V) := ⟨⊥⟩
 
+instance [subsingleton V] : unique (simple_graph V) :=
+{ default := ⊥,
+  uniq := λ G, by ext a b; simp [subsingleton.elim a b] }
+
+instance [nontrivial V] : nontrivial (simple_graph V) :=
+⟨⟨⊥, ⊤, λ h, not_subsingleton V ⟨by simpa [ext_iff, function.funext_iff] using h⟩⟩⟩
+
 section decidable
 
 variables (V) (H : simple_graph V) [decidable_rel G.adj] [decidable_rel H.adj]
@@ -372,6 +380,17 @@ 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 }
 
+variables {G G₁ G₂}
+
+@[simp] lemma disjoint_edge_set : disjoint G₁.edge_set G₂.edge_set ↔ disjoint G₁ G₂ :=
+by rw [set.disjoint_iff, disjoint_iff_inf_le, ←edge_set_inf, ←edge_set_bot, ←set.le_iff_subset,
+  order_embedding.le_iff_le]
+
+@[simp] lemma edge_set_eq_empty : G.edge_set = ∅ ↔ G = ⊥ := by rwa [←edge_set_bot, edge_set_inj]
+
+@[simp] lemma edge_set_nonempty : G.edge_set.nonempty ↔ G ≠ ⊥ :=
+by rw [set.nonempty_iff_ne_empty, edge_set_eq_empty.ne]
+
 /--
 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`.
@@ -406,6 +425,8 @@ end
 lemma adj_iff_exists_edge_coe : G.adj a b ↔ ∃ (e : G.edge_set), ↑e = ⟦(a, b)⟧ :=
 by simp only [mem_edge_set, exists_prop, set_coe.exists, exists_eq_right, subtype.coe_mk]
 
+variables (G G₁ G₂)
+
 lemma edge_other_ne {e : sym2 V} (he : e ∈ G.edge_set) {v : V} (h : v ∈ e) : h.other ≠ v :=
 begin
   erw [← sym2.other_spec h, sym2.eq_swap] at he,
@@ -482,6 +503,16 @@ begin
   exact λ vws _, h vws,
 end
 
+@[simp] lemma disjoint_from_edge_set : disjoint G (from_edge_set s) ↔ disjoint G.edge_set s :=
+begin
+  conv_rhs { rw ←set.diff_union_inter s {e | e.is_diag} },
+  rw [←disjoint_edge_set, edge_set_from_edge_set, set.disjoint_union_right, and_iff_left],
+  exact set.disjoint_left.2 (λ e he he', not_is_diag_of_mem_edge_set _ he he'.2),
+end
+
+@[simp] lemma from_edge_set_disjoint : disjoint (from_edge_set s) G ↔ disjoint s G.edge_set :=
+by rw [disjoint.comm, disjoint_from_edge_set, disjoint.comm]
+
 instance [decidable_eq V] [fintype s] : fintype (from_edge_set s).edge_set :=
 by { rw edge_set_from_edge_set s, apply_instance }
 
@@ -680,6 +711,9 @@ end edge_finset
 @[simp] lemma mem_neighbor_set (v w : V) : w ∈ G.neighbor_set v ↔ G.adj v w :=
 iff.rfl
 
+@[simp] lemma not_mem_neighbor_set_self : a ∉ G.neighbor_set a :=
+(mem_neighbor_set _ _ _).not.2 $ G.loopless _
+
 @[simp] lemma mem_incidence_set (v w : V) : ⟦(v, w)⟧ ∈ G.incidence_set v ↔ G.adj v w :=
 by simp [incidence_set]
 
@@ -821,6 +855,9 @@ lemma delete_edges_eq_sdiff_from_edge_set (s : set (sym2 V)) :
   G.delete_edges s = G \ from_edge_set s :=
 by { ext, exact ⟨λ h, ⟨h.1, not_and_of_not_left _ h.2⟩, λ h, ⟨h.1, not_and'.mp h.2 h.ne⟩⟩ }
 
+@[simp] lemma delete_edges_eq {s : set (sym2 V)} : G.delete_edges s = G ↔ disjoint G.edge_set s :=
+by rw [delete_edges_eq_sdiff_from_edge_set, sdiff_eq_left, disjoint_from_edge_set]
+
 lemma compl_eq_delete_edges :
   Gᶜ = (⊤ : simple_graph V).delete_edges G.edge_set :=
 by { ext, simp }
@@ -871,18 +908,17 @@ get a graph with the property `p`. -/
 def delete_far (p : simple_graph V → Prop) (r : 𝕜) : Prop :=
 ∀ ⦃s⦄, s ⊆ G.edge_finset → p (G.delete_edges s) → r ≤ s.card
 
-open_locale classical
-
 variables {G}
 
 lemma delete_far_iff :
-  G.delete_far p r ↔ ∀ ⦃H⦄, H ≤ G → p H → r ≤ G.edge_finset.card - H.edge_finset.card :=
+  G.delete_far p r ↔ ∀ ⦃H : simple_graph _⦄ [decidable_rel H.adj],
+    by exactI H ≤ G → p H → r ≤ G.edge_finset.card - H.edge_finset.card :=
 begin
-  refine ⟨λ h H hHG hH, _, λ h s hs hG, _⟩,
+  refine ⟨λ h H _ hHG hH, _, λ h s hs hG, _⟩,
   { have := h (sdiff_subset G.edge_finset H.edge_finset),
     simp only [delete_edges_sdiff_eq_of_le _ hHG, edge_finset_mono hHG, card_sdiff,
       card_le_of_subset, coe_sdiff, coe_edge_finset, nat.cast_sub] at this,
-    exact this hH },
+    convert this hH },
   { simpa [card_sdiff hs, edge_finset_delete_edges, -set.to_finset_card, nat.cast_sub,
       card_le_of_subset hs] using h (G.delete_edges_le s) hG }
 end
@@ -906,9 +942,22 @@ protected def map (f : V ↪ W) (G : simple_graph V) : simple_graph W :=
 @[simp] lemma map_adj (f : V ↪ W) (G : simple_graph V) (u v : W) :
   (G.map f).adj u v ↔ ∃ (u' v' : V), G.adj u' v' ∧ f u' = u ∧ f v' = v := iff.rfl
 
+lemma map_adj_apply {G : simple_graph V} {f : V ↪ W} {a b : V} :
+  (G.map f).adj (f a) (f b) ↔ G.adj a b := by simp
+
 lemma map_monotone (f : V ↪ W) : monotone (simple_graph.map f) :=
 by { rintros G G' h _ _ ⟨u, v, ha, rfl, rfl⟩, exact ⟨_, _, h ha, rfl, rfl⟩ }
 
+@[simp] lemma map_id : G.map (function.embedding.refl _) = G :=
+ext _ _ $ relation.map_id_id _
+
+@[simp] lemma map_map (f : V ↪ W) (g : W ↪ X) : (G.map f).map g = G.map (f.trans g) :=
+ext _ _ $ relation.map_map _ _ _ _ _
+
+instance decidable_map (f : V ↪ W) (G : simple_graph V) [decidable_rel (relation.map G.adj f f)] :
+  decidable_rel (G.map f).adj :=
+‹decidable_rel _›
+
 /-- Given a function, there is a contravariant induced map on graphs by pulling back the
 adjacency relation.
 This is one of the ways of creating induced graphs. See `simple_graph.induce` for a wrapper.
@@ -917,6 +966,24 @@ This is surjective when `f` is injective (see `simple_graph.comap_surjective`).-
 @[simps] protected def comap (f : V → W) (G : simple_graph W) : simple_graph V :=
 { adj := λ u v, G.adj (f u) (f v) }
 
+@[simp] lemma comap_id {G : simple_graph V} : G.comap id = G := ext _ _ rfl
+
+@[simp] lemma comap_comap {G : simple_graph X} (f : V → W) (g : W → X) :
+  (G.comap g).comap f = G.comap (g ∘ f) := rfl
+
+instance decidable_comap (f : V → W) (G : simple_graph W) [decidable_rel G.adj] :
+  decidable_rel (simple_graph.comap f G).adj :=
+λ _ _, ‹decidable_rel G.adj› _ _
+
+lemma comap_symm (G : simple_graph V) (e : V ≃ W) :
+  G.comap e.symm.to_embedding = G.map e.to_embedding :=
+by { ext, simp only [equiv.apply_eq_iff_eq_symm_apply, comap_adj, map_adj, equiv.to_embedding_apply,
+  exists_eq_right_right, exists_eq_right] }
+
+lemma map_symm (G : simple_graph W) (e : V ≃ W) :
+  G.map e.symm.to_embedding = G.comap e.to_embedding :=
+by rw [←comap_symm, e.symm_symm]
+
 lemma comap_monotone (f : V ↪ W) : monotone (simple_graph.comap f) :=
 by { intros G G' h _ _ ha, exact h ha }
 
@@ -939,6 +1006,23 @@ lemma map_le_iff_le_comap (f : V ↪ W) (G : simple_graph V) (G' : simple_graph
 lemma map_comap_le (f : V ↪ W) (G : simple_graph W) : (G.comap f).map f ≤ G :=
 by { rw map_le_iff_le_comap, exact le_refl _ }
 
+/-- Equivalent types have equivalent simple graphs. -/
+@[simps apply] protected def _root_.equiv.simple_graph (e : V ≃ W) :
+  simple_graph V ≃ simple_graph W :=
+{ to_fun := simple_graph.comap e.symm,
+  inv_fun := simple_graph.comap e,
+  left_inv := λ _, by simp,
+  right_inv := λ _, by simp }
+
+@[simp] lemma _root_.equiv.simple_graph_refl : (equiv.refl V).simple_graph = equiv.refl _ :=
+by { ext, refl }
+
+@[simp] lemma _root_.equiv.simple_graph_trans (e₁ : V ≃ W) (e₂ : W ≃ X) :
+  (e₁.trans e₂).simple_graph = e₁.simple_graph.trans e₂.simple_graph := rfl
+
+@[simp] lemma _root_.equiv.symm_simple_graph (e : V ≃ W) :
+  e.simple_graph.symm = e.symm.simple_graph := rfl
+
 /-! ## Induced graphs -/
 
 /- Given a set `s` of vertices, we can restrict a graph to those vertices by restricting its
@@ -1296,10 +1380,23 @@ infix ` ↪g ` : 50 := embedding
 infix ` ≃g ` : 50 := iso
 
 namespace hom
-variables {G G'} (f : G →g G')
+variables {G G'} {H : simple_graph W} (f : G →g G')
 
 /-- The identity homomorphism from a graph to itself. -/
-abbreviation id : G →g G := rel_hom.id _
+protected abbreviation id : G →g G := rel_hom.id _
+
+@[simp, norm_cast] lemma coe_id : ⇑(hom.id : G →g G) = _root_.id := rfl
+
+instance [subsingleton (V → W)] : subsingleton (G →g H) := fun_like.coe_injective.subsingleton
+
+instance [is_empty V] : unique (G →g H) :=
+{ default := ⟨is_empty_elim, is_empty_elim⟩,
+  uniq := λ _, subsingleton.elim _ _ }
+
+noncomputable instance [fintype V] [fintype W] : fintype (G →g H) :=
+by classical; exact fun_like.fintype _
+
+instance [finite V] [finite W] : finite (G →g H) := fun_like.finite _
 
 lemma map_adj {v w : V} (h : G.adj v w) : G'.adj (f v) (f w) := f.map_rel' h
 
@@ -1358,10 +1455,15 @@ abbreviation comp (f' : G' →g G'') (f : G →g G') : G →g G'' := f'.comp f
 
 @[simp] lemma coe_comp (f' : G' →g G'') (f : G →g G') : ⇑(f'.comp f) = f' ∘ f := rfl
 
+/-- The graph homomorphism from a smaller graph to a bigger one. -/
+def of_le {H : simple_graph V} (h : G ≤ H) : G →g H := ⟨id, h⟩
+
+@[simp, norm_cast] lemma coe_of_le {H : simple_graph V} (h : G ≤ H) : ⇑(of_le h) = id := rfl
+
 end hom
 
 namespace embedding
-variables {G G'} (f : G ↪g G')
+variables {G G'} {H : simple_graph W} (f : G ↪g G')
 
 /-- The identity embedding from a graph to itself. -/
 abbreviation refl : G ↪g G := rel_embedding.refl _
@@ -1369,7 +1471,9 @@ abbreviation refl : G ↪g G := rel_embedding.refl _
 /-- An embedding of graphs gives rise to a homomorphism of graphs. -/
 abbreviation to_hom : G →g G' := f.to_rel_hom
 
-lemma map_adj_iff {v w : V} : G'.adj (f v) (f w) ↔ G.adj v w := f.map_rel_iff
+@[simp] lemma coe_to_hom (f : G ↪g H) : ⇑f.to_hom = f := rfl
+
+@[simp] lemma map_adj_iff {v w : V} : G'.adj (f v) (f w) ↔ G.adj v w := f.map_rel_iff
 
 lemma map_mem_edge_set_iff {e : sym2 V} : e.map f ∈ G'.edge_set ↔ e ∈ G.edge_set :=
 quotient.ind (λ ⟨v, w⟩, f.map_adj_iff) e
diff --git a/src/combinatorics/simple_graph/clique.lean b/src/combinatorics/simple_graph/clique.lean
index 996aeb3dd5c72..8d2b10d255ca5 100644
--- a/src/combinatorics/simple_graph/clique.lean
+++ b/src/combinatorics/simple_graph/clique.lean
@@ -5,6 +5,7 @@ Authors: Yaël Dillies, Bhavik Mehta
 -/
 import combinatorics.simple_graph.basic
 import data.finset.pairwise
+import data.finset.preimage
 
 /-!
 # Graph cliques
@@ -25,13 +26,13 @@ adjacent.
 ## TODO
 
 * Clique numbers
-* Do we need `clique_set`, a version of `clique_finset` for infinite graphs?
+* Dualise all the API to get independent sets
 -/
 
-open finset fintype
+open finset fintype function
 
 namespace simple_graph
-variables {α : Type*} (G H : simple_graph α)
+variables {α β : Type*} (G H : simple_graph α)
 
 /-! ### Cliques -/
 
@@ -61,13 +62,33 @@ end
 instance [decidable_eq α] [decidable_rel G.adj] {s : finset α} : decidable (G.is_clique s) :=
 decidable_of_iff' _ G.is_clique_iff
 
-variables {G H}
+variables {G H} {a b : α}
+
+@[simp] lemma is_clique_empty : G.is_clique ∅ := set.pairwise_empty _
+@[simp] lemma is_clique_singleton (a : α) : G.is_clique {a} := set.pairwise_singleton _ _
+
+lemma is_clique_pair : G.is_clique {a, b} ↔ a ≠ b → G.adj a b :=
+set.pairwise_pair_of_symmetric G.symm
+
+@[simp] lemma is_clique_insert :
+  G.is_clique (insert a s) ↔ G.is_clique s ∧ ∀ b ∈ s, a ≠ b → G.adj a b :=
+set.pairwise_insert_of_symmetric G.symm
 
-lemma is_clique.mono (h : G ≤ H) : G.is_clique s → H.is_clique s :=
-by { simp_rw is_clique_iff, exact set.pairwise.mono' h }
+lemma is_clique_insert_of_not_mem (ha : a ∉ s) :
+  G.is_clique (insert a s) ↔ G.is_clique s ∧ ∀ b ∈ s, G.adj a b :=
+set.pairwise_insert_of_symmetric_of_not_mem G.symm ha
 
-lemma is_clique.subset (h : t ⊆ s) : G.is_clique s → G.is_clique t :=
-by { simp_rw is_clique_iff, exact set.pairwise.mono h }
+lemma is_clique.insert (hs : G.is_clique s) (h : ∀ b ∈ s, a ≠ b → G.adj a b) :
+  G.is_clique (insert a s) :=
+hs.insert_of_symmetric G.symm h
+
+lemma is_clique.mono (h : G ≤ H) : G.is_clique s → H.is_clique s := set.pairwise.mono' h
+lemma is_clique.subset (h : t ⊆ s) : G.is_clique s → G.is_clique t := set.pairwise.mono h
+
+protected lemma is_clique.map {G : simple_graph α} {s : set α} (h : G.is_clique s) {f : α ↪ β} :
+  (G.map f).is_clique (f '' s) :=
+by { rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ hab,
+  exact ⟨a, b, h ha hb $ ne_of_apply_ne _ hab, rfl, rfl⟩ }
 
 @[simp] lemma is_clique_bot_iff : (⊥ : simple_graph α).is_clique s ↔ (s : set α).subsingleton :=
 set.pairwise_bot_iff
@@ -93,11 +114,19 @@ instance [decidable_eq α] [decidable_rel G.adj] {n : ℕ} {s : finset α} :
   decidable (G.is_n_clique n s) :=
 decidable_of_iff' _ G.is_n_clique_iff
 
-variables {G H}
+variables {G H} {a b c : α}
+
+@[simp] lemma is_n_clique_empty : G.is_n_clique n ∅ ↔ n = 0 := by simp [is_n_clique_iff, eq_comm]
+@[simp] lemma is_n_clique_singleton : G.is_n_clique n {a} ↔ n = 1 :=
+by simp [is_n_clique_iff, eq_comm]
 
 lemma is_n_clique.mono (h : G ≤ H) : G.is_n_clique n s → H.is_n_clique n s :=
 by { simp_rw is_n_clique_iff, exact and.imp_left (is_clique.mono h) }
 
+protected lemma is_n_clique.map (h : G.is_n_clique n s) {f : α ↪ β} :
+  (G.map f).is_n_clique n (s.map f) :=
+⟨by { rw coe_map, exact h.1.map}, (card_map _).trans h.2⟩
+
 @[simp] lemma is_n_clique_bot_iff : (⊥ : simple_graph α).is_n_clique n s ↔ n ≤ 1 ∧ s.card = n :=
 begin
   rw [is_n_clique_iff, is_clique_bot_iff],
@@ -106,7 +135,22 @@ begin
   exact card_le_one.symm,
 end
 
-variables [decidable_eq α] {a b c : α}
+@[simp] lemma is_n_clique_zero : G.is_n_clique 0 s ↔ s = ∅ :=
+by { simp only [is_n_clique_iff, finset.card_eq_zero, and_iff_right_iff_imp], rintro rfl, simp }
+
+@[simp] lemma is_n_clique_one : G.is_n_clique 1 s ↔ ∃ a, s = {a} :=
+by { simp only [is_n_clique_iff, card_eq_one, and_iff_right_iff_imp], rintro ⟨a, rfl⟩, simp }
+
+variables [decidable_eq α]
+
+lemma is_n_clique.insert (hs : G.is_n_clique n s) (h : ∀ b ∈ s, G.adj a b) :
+  G.is_n_clique (n + 1) (insert a s) :=
+begin
+  split,
+  { push_cast,
+    exact hs.1.insert (λ b hb _, h _ hb) },
+  { rw [card_insert_of_not_mem (λ ha, (h _ ha).ne rfl), hs.2] }
+end
 
 lemma is_3_clique_triple_iff : G.is_n_clique 3 {a, b, c} ↔ G.adj a b ∧ G.adj a c ∧ G.adj b c :=
 begin
@@ -193,7 +237,7 @@ begin
   use (iso.complete_graph (fintype.equiv_fin α)).symm.to_embedding.trans f,
 end
 
-lemma clique_free_bot (h : 2 ≤ n) : (⊥ : simple_graph α).clique_free n :=
+@[simp] lemma clique_free_bot (h : 2 ≤ n) : (⊥ : simple_graph α).clique_free n :=
 begin
   rintro t ht,
   rw is_n_clique_bot_iff at ht,
@@ -219,8 +263,77 @@ begin
   simpa using fintype.card_le_of_embedding h.some.to_embedding,
 end
 
+@[simp] lemma clique_free_two : G.clique_free 2 ↔ G = ⊥ :=
+begin
+  classical,
+  split,
+  { simp_rw [←edge_set_eq_empty, set.eq_empty_iff_forall_not_mem, sym2.forall, mem_edge_set],
+    exact λ h a b hab, h _ ⟨by simpa [hab.ne], card_doubleton hab.ne⟩ },
+  { rintro rfl,
+    exact clique_free_bot le_rfl }
+end
+
 end clique_free
 
+section clique_free_on
+variables {s s₁ s₂ : set α} {t : finset α} {a b : α} {m n : ℕ}
+
+/-- `G.clique_free_on s n` means that `G` has no `n`-cliques contained in `s`. -/
+def clique_free_on (G : simple_graph α) (s : set α) (n : ℕ) : Prop :=
+∀ ⦃t⦄, ↑t ⊆ s → ¬G.is_n_clique n t
+
+lemma clique_free_on.subset (hs : s₁ ⊆ s₂) (h₂ : G.clique_free_on s₂ n) : G.clique_free_on s₁ n :=
+λ t hts, h₂ $ hts.trans hs
+
+lemma clique_free_on.mono (hmn : m ≤ n) (hG : G.clique_free_on s m) : G.clique_free_on s n :=
+begin
+  rintro t hts ht,
+  obtain ⟨u, hut, hu⟩ := t.exists_smaller_set _ (hmn.trans ht.card_eq.ge),
+  exact hG ((coe_subset.2 hut).trans hts) ⟨ht.clique.subset hut, hu⟩,
+end
+
+lemma clique_free_on.anti (hGH : G ≤ H) (hH : H.clique_free_on s n) : G.clique_free_on s n :=
+λ t hts ht, hH hts $ ht.mono hGH
+
+@[simp] lemma clique_free_on_empty : G.clique_free_on ∅ n ↔ n ≠ 0 :=
+by simp [clique_free_on, set.subset_empty_iff]
+
+@[simp] lemma clique_free_on_singleton : G.clique_free_on {a} n ↔ 1 < n :=
+by obtain _ | _ | n := n; simp [clique_free_on, set.subset_singleton_iff_eq]
+
+@[simp] lemma clique_free_on_univ : G.clique_free_on set.univ n ↔ G.clique_free n :=
+by simp [clique_free, clique_free_on]
+
+protected lemma clique_free.clique_free_on (hG : G.clique_free n) : G.clique_free_on s n :=
+λ t _, hG _
+
+lemma clique_free_on_of_card_lt {s : finset α} (h : s.card < n) : G.clique_free_on s n :=
+λ t hts ht, h.not_le $ ht.2.symm.trans_le $ card_mono hts
+
+--TOOD: Restate using `simple_graph.indep_set` once we have it
+@[simp] lemma clique_free_on_two : G.clique_free_on s 2 ↔ s.pairwise G.adjᶜ :=
+begin
+  classical,
+  refine ⟨λ h a ha b hb _ hab, h _ ⟨by simpa [hab.ne], card_doubleton hab.ne⟩, _⟩,
+  { push_cast,
+    exact set.insert_subset.2 ⟨ha, set.singleton_subset_iff.2 hb⟩ },
+  simp only [clique_free_on, is_n_clique_iff, card_eq_two, coe_subset, not_and, not_exists],
+  rintro h t hst ht a b hab rfl,
+  simp only [coe_insert, coe_singleton, set.insert_subset, set.singleton_subset_iff] at hst,
+  refine h hst.1 hst.2 hab (ht _ _ hab); simp,
+end
+
+lemma clique_free_on.of_succ (hs : G.clique_free_on s (n + 1)) (ha : a ∈ s) :
+  G.clique_free_on (s ∩ G.neighbor_set a) n :=
+begin
+  classical,
+  refine λ t hts ht, hs _ (ht.insert $ λ b hb, (hts hb).2),
+  push_cast,
+  exact set.insert_subset.2 ⟨ha, hts.trans $ set.inter_subset_left _ _⟩,
+end
+
+end clique_free_on
+
 /-! ### Set of cliques -/
 
 section clique_set
@@ -229,22 +342,60 @@ variables (G) {n : ℕ} {a b c : α} {s : finset α}
 /-- The `n`-cliques in a graph as a set. -/
 def clique_set (n : ℕ) : set (finset α) := {s | G.is_n_clique n s}
 
-lemma mem_clique_set_iff : s ∈ G.clique_set n ↔ G.is_n_clique n s := iff.rfl
+@[simp] lemma mem_clique_set_iff : s ∈ G.clique_set n ↔ G.is_n_clique n s := iff.rfl
 
 @[simp] lemma clique_set_eq_empty_iff : G.clique_set n = ∅ ↔ G.clique_free n :=
 by simp_rw [clique_free, set.eq_empty_iff_forall_not_mem, mem_clique_set_iff]
 
-alias clique_set_eq_empty_iff ↔ _ clique_free.clique_set
-
-attribute [protected] clique_free.clique_set
-
 variables {G H}
 
+protected lemma clique_free.clique_set : G.clique_free n → G.clique_set n = ∅ :=
+G.clique_set_eq_empty_iff.2
+
 @[mono] lemma clique_set_mono (h : G ≤ H) : G.clique_set n ⊆ H.clique_set n :=
 λ _, is_n_clique.mono h
 
 lemma clique_set_mono' (h : G ≤ H) : G.clique_set ≤ H.clique_set := λ _, clique_set_mono h
 
+@[simp] lemma clique_set_zero (G : simple_graph α) : G.clique_set 0 = {∅} :=
+set.ext $ λ s, by simp
+
+@[simp] lemma clique_set_one (G : simple_graph α) : G.clique_set 1 = set.range singleton :=
+set.ext $ λ s, by simp [eq_comm]
+
+@[simp] lemma clique_set_bot (hn : 1 < n) : (⊥ : simple_graph α).clique_set n = ∅ :=
+(clique_free_bot hn).clique_set
+
+@[simp] lemma clique_set_map (hn : n ≠ 1) (G : simple_graph α) (f : α ↪ β) :
+  (G.map f).clique_set n = map f '' G.clique_set n :=
+begin
+  ext s,
+  split,
+  { rintro ⟨hs, rfl⟩,
+    have hs' : (s.preimage f $ f.injective.inj_on _).map f = s,
+    { classical,
+      rw [map_eq_image, image_preimage, filter_true_of_mem],
+      rintro a ha,
+      obtain ⟨b, hb, hba⟩ := exists_mem_ne (hn.lt_of_le' $ finset.card_pos.2 ⟨a, ha⟩) a,
+      obtain ⟨c, _, _, hc, _⟩ := hs ha hb hba.symm,
+      exact ⟨c, hc⟩ },
+    refine ⟨s.preimage f $ f.injective.inj_on _, ⟨_, by rw [←card_map f, hs']⟩, hs'⟩,
+    rw coe_preimage,
+    exact λ a ha b hb hab, map_adj_apply.1 (hs ha hb $ f.injective.ne hab) },
+  { rintro ⟨s, hs, rfl⟩,
+    exact is_n_clique.map hs }
+end
+
+@[simp] lemma clique_set_map_of_equiv (G : simple_graph α) (e : α ≃ β) (n : ℕ) :
+  (G.map e.to_embedding).clique_set n = map e.to_embedding '' G.clique_set n :=
+begin
+  obtain rfl | hn := eq_or_ne n 1,
+  { ext,
+    simp [e.exists_congr_left] },
+  { exact clique_set_map hn _ _ }
+end
+
+
 end clique_set
 
 /-! ### Finset of cliques -/
@@ -255,10 +406,11 @@ variables (G) [fintype α] [decidable_eq α] [decidable_rel G.adj] {n : ℕ} {a
 /-- The `n`-cliques in a graph as a finset. -/
 def clique_finset (n : ℕ) : finset (finset α) := univ.filter $ G.is_n_clique n
 
-lemma mem_clique_finset_iff : s ∈ G.clique_finset n ↔ G.is_n_clique n s :=
+@[simp] lemma mem_clique_finset_iff : s ∈ G.clique_finset n ↔ G.is_n_clique n s :=
 mem_filter.trans $ and_iff_right $ mem_univ _
 
-@[simp] lemma coe_clique_finset (n : ℕ) : (G.clique_finset n : set (finset α)) = G.clique_set n :=
+@[simp, norm_cast] lemma coe_clique_finset (n : ℕ) :
+  (G.clique_finset n : set (finset α)) = G.clique_set n :=
 set.ext $ λ _, mem_clique_finset_iff _
 
 @[simp] lemma clique_finset_eq_empty_iff : G.clique_finset n = ∅ ↔ G.clique_free n :=
@@ -268,10 +420,31 @@ alias clique_finset_eq_empty_iff ↔ _ _root_.simple_graph.clique_free.clique_fi
 
 attribute [protected] clique_free.clique_finset
 
-variables {G} [decidable_rel H.adj]
+variables {G}
+
+lemma card_clique_finset_le : (G.clique_finset n).card ≤ (card α).choose n :=
+begin
+  rw [←card_univ, ←card_powerset_len],
+  refine card_mono (λ s, _),
+  simpa [mem_powerset_len_univ_iff] using is_n_clique.card_eq,
+end
+
+variables [decidable_rel H.adj]
 
 @[mono] lemma clique_finset_mono (h : G ≤ H) : G.clique_finset n ⊆ H.clique_finset n :=
 monotone_filter_right _ $ λ _, is_n_clique.mono h
 
+variables [fintype β] [decidable_eq β] (G)
+
+@[simp] lemma clique_finset_map (f : α ↪ β) (hn : n ≠ 1) :
+  (G.map f).clique_finset n = (G.clique_finset n).map ⟨map f, finset.map_injective _⟩ :=
+coe_injective $
+  by simp_rw [coe_clique_finset, clique_set_map hn, coe_map, coe_clique_finset, embedding.coe_fn_mk]
+
+@[simp] lemma clique_finset_map_of_equiv (e : α ≃ β) (n : ℕ) :
+  (G.map e.to_embedding).clique_finset n =
+    (G.clique_finset n).map ⟨map e.to_embedding, finset.map_injective _⟩ :=
+coe_injective $ by push_cast; exact clique_set_map_of_equiv _ _ _
+
 end clique_finset
 end simple_graph
diff --git a/src/combinatorics/simple_graph/triangle/basic.lean b/src/combinatorics/simple_graph/triangle/basic.lean
index 639207f75591c..38c350e394e93 100644
--- a/src/combinatorics/simple_graph/triangle/basic.lean
+++ b/src/combinatorics/simple_graph/triangle/basic.lean
@@ -42,7 +42,8 @@ G.delete_far (λ H, H.clique_free 3) $ ε * (card α^2 : ℕ)
 
 lemma far_from_triangle_free_iff :
   G.far_from_triangle_free ε ↔
-    ∀ ⦃H⦄, H ≤ G → H.clique_free 3 → ε * (card α^2 : ℕ) ≤ G.edge_finset.card - H.edge_finset.card :=
+    ∀ ⦃H : simple_graph _⦄ [decidable_rel H.adj], by exactI
+      H ≤ G → H.clique_free 3 → ε * (card α^2 : ℕ) ≤ G.edge_finset.card - H.edge_finset.card :=
 delete_far_iff
 
 alias far_from_triangle_free_iff ↔ far_from_triangle_free.le_card_sub_card _
diff --git a/src/data/finset/card.lean b/src/data/finset/card.lean
index 98cf0399b0e58..f023ef54c1104 100644
--- a/src/data/finset/card.lean
+++ b/src/data/finset/card.lean
@@ -434,6 +434,13 @@ begin
     exact card_le_of_subset hx }
 end
 
+lemma exists_mem_ne (hs : 1 < s.card) (a : α) : ∃ b ∈ s, b ≠ a :=
+begin
+  by_contra',
+  haveI : nonempty α := ⟨a⟩,
+  exact hs.not_le (card_le_one_iff_subset_singleton.2 ⟨a, subset_singleton_iff'.2 this⟩),
+end
+
 /-- A `finset` of a subsingleton type has cardinality at most one. -/
 lemma card_le_one_of_subsingleton [subsingleton α] (s : finset α) : s.card ≤ 1 :=
 finset.card_le_one_iff.2 $ λ _ _ _ _, subsingleton.elim _ _
diff --git a/src/data/finset/preimage.lean b/src/data/finset/preimage.lean
index ba9639d06700d..afe69fac91482 100644
--- a/src/data/finset/preimage.lean
+++ b/src/data/finset/preimage.lean
@@ -61,6 +61,10 @@ finset.coe_injective (by simp)
   preimage sᶜ f (hf.inj_on _) = (preimage s f (hf.inj_on _))ᶜ :=
 finset.coe_injective (by simp)
 
+@[simp] lemma preimage_map (f : α ↪ β) (s : finset α) :
+  (s.map f).preimage f (f.injective.inj_on _) = s :=
+coe_injective $ by simp only [coe_preimage, coe_map, set.preimage_image_eq _ f.injective]
+
 lemma monotone_preimage {f : α → β} (h : injective f) :
   monotone (λ s, preimage s f (h.inj_on _)) :=
 λ s t hst x hx, mem_preimage.2 (hst $ mem_preimage.1 hx)
diff --git a/src/logic/basic.lean b/src/logic/basic.lean
index 71baa00527e9d..26ef5b00ad237 100644
--- a/src/logic/basic.lean
+++ b/src/logic/basic.lean
@@ -423,6 +423,15 @@ lemma iff.not (h : a ↔ b) : ¬ a ↔ ¬ b := not_congr h
 lemma iff.not_left (h : a ↔ ¬ b) : ¬ a ↔ b := h.not.trans not_not
 lemma iff.not_right (h : ¬ a ↔ b) : a ↔ ¬ b := not_not.symm.trans h.not
 
+protected lemma iff.ne {α β : Sort*} {a b : α} {c d : β} : (a = b ↔ c = d) → (a ≠ b ↔ c ≠ d) :=
+iff.not
+
+lemma iff.ne_left {α β : Sort*} {a b : α} {c d : β} : (a = b ↔ c ≠ d) → (a ≠ b ↔ c = d) :=
+iff.not_left
+
+lemma iff.ne_right {α β : Sort*} {a b : α} {c d : β} : (a ≠ b ↔ c = d) → (a = b ↔ c ≠ d) :=
+iff.not_right
+
 /-! ### Declarations about `xor` -/
 
 @[simp] theorem xor_true : xor true = not := funext $ λ a, by simp [xor]
diff --git a/src/logic/relation.lean b/src/logic/relation.lean
index 8467caa176c36..466ad575131e0 100644
--- a/src/logic/relation.lean
+++ b/src/logic/relation.lean
@@ -42,7 +42,7 @@ the bundled version, see `rel`.
 
 open function
 
-variables {α β γ δ : Type*}
+variables {α β γ δ ε κ : Type*}
 
 section ne_imp
 
@@ -186,6 +186,27 @@ related by `r`.
 protected def map (r : α → β → Prop) (f : α → γ) (g : β → δ) : γ → δ → Prop :=
 λ c d, ∃ a b, r a b ∧ f a = c ∧ g b = d
 
+section map
+variables {r : α → β → Prop} {f : α → γ} {g : β → δ} {c : γ} {d : δ}
+
+lemma map_apply : relation.map r f g c d ↔ ∃ a b, r a b ∧ f a = c ∧ g b = d := iff.rfl
+
+@[simp] lemma map_id_id (r : α → β → Prop) : relation.map r id id = r := by simp [relation.map]
+
+@[simp] lemma map_map (r : α → β → Prop) (f₁ : α → γ) (g₁ : β → δ) (f₂ : γ → ε) (g₂ : δ → κ) :
+  relation.map (relation.map r f₁ g₁) f₂ g₂ = relation.map r (f₂ ∘ f₁) (g₂ ∘ g₁) :=
+begin
+  ext a b,
+  simp only [map_apply, function.comp_app, ←exists_and_distrib_right, @exists₂_comm γ],
+  refine exists₂_congr (λ a b, _),
+  simp [and_assoc],
+end
+
+instance [decidable (∃ a b, r a b ∧ f a = c ∧ g b = d)] : decidable (relation.map r f g c d) :=
+‹decidable _›
+
+end map
+
 variables {r : α → α → Prop} {a b c d : α}
 
 /-- `refl_trans_gen r`: reflexive transitive closure of `r` -/