diff --git a/OLD_README.md b/OLD_README.md
new file mode 100644
index 0000000000000..53d8c3defebf5
--- /dev/null
+++ b/OLD_README.md
@@ -0,0 +1,115 @@
+# Lean 3's mathlib
+
+> [!WARNING]  
+> Lean 3 and Mathlib 3 are no longer actively maintained.
+> It is strongly recommended that you use [mathlib4](https://github.com/leanprover-community/mathlib4) for Lean 4 instead.
+
+![](https://github.com/leanprover-community/mathlib/workflows/continuous%20integration/badge.svg?branch=master)
+[![Bors enabled](https://bors.tech/images/badge_small.svg)](https://app.bors.tech/repositories/24316)
+[![project chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://leanprover.zulipchat.com)
+[![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-ready--to--code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/leanprover-community/mathlib)
+
+[Mathlib](https://leanprover-community.github.io) is a user maintained library for the [Lean 3 theorem prover](https://github.com/leanprover-community/lean).
+It contains both programming infrastructure and mathematics,
+as well as tactics that use the former and allow to develop the latter.
+
+## Installation
+
+You can find detailed instructions to install Lean 3, mathlib 3, and supporting tools on [our website](https://leanprover-community.github.io/lean3/get_started.html).
+
+## Experimenting
+
+Got everything installed? Why not start with the [tutorial project](https://leanprover-community.github.io/lean3/install/project.html)?
+
+For more pointers, see [Learning Lean](https://leanprover-community.github.io/lean3/learn.html).
+
+## Documentation
+
+Besides the installation guides above and [Lean's general
+documentation](https://leanprover.github.io/lean3/documentation/), the documentation
+of mathlib consists of:
+
+- [The mathlib docs](https://leanprover-community.github.io/mathlib_docs): documentation [generated
+  automatically](https://github.com/leanprover-community/doc-gen) from the source `.lean` files.
+  In addition to the pages generated for each file in the library, the docs also include pages on:
+  - [tactics](https://leanprover-community.github.io/mathlib_docs/tactics.html),
+  - [commands](https://leanprover-community.github.io/mathlib_docs/commands.html),
+  - [hole commands](https://leanprover-community.github.io/mathlib_docs/hole_commands.html), and
+  - [attributes](https://leanprover-community.github.io/mathlib_docs/attributes.html).
+- A description of [currently covered theories](https://leanprover-community.github.io/theories.html),
+  as well as an [overview](https://leanprover-community.github.io/lean3/mathlib-overview.html) for mathematicians.
+- A couple of [tutorial Lean files](docs/tutorial/)
+- Some [extra Lean documentation](https://leanprover-community.github.io/lean3/learn.html) not specific to mathlib (see "Miscellaneous topics")
+- Documentation for people who would like to [contribute to mathlib3](https://leanprover-community.github.io/lean3/contribute/index.html)
+
+Much of the discussion surrounding mathlib occurs in a
+[Zulip chat room](https://leanprover.zulipchat.com/). Since this
+chatroom is only visible to registered users, we provide an
+[openly accessible archive](https://leanprover-community.github.io/archive/)
+of the public discussions. This is useful for quick reference; for a
+better browsing interface, and to participate in the discussions, we strongly
+suggest joining the chat. Questions from users at all levels of expertise are
+welcomed.
+
+## Contributing
+
+> [!WARNING]  
+> Contributions are no longer accepted to mathlib 3; contribute to mathlib 4 instead!
+
+The complete documentation for contributing to ``mathlib`` is located
+[on the community guide contribute to mathlib](https://leanprover-community.github.io/lean3/contribute/index.html)
+
+The process is different from other projects where one should not fork the repository.
+Instead write permission for non-master branches should be requested on [Zulip](https://leanprover.zulipchat.com)
+by introducing yourself, providing your GitHub handle and what contribution you are planning on doing.
+
+### Guidelines
+
+Mathlib has the following guidelines and conventions that must be followed
+
+ - The [style guide](https://leanprover-community.github.io/lean3/contribute/style.html)
+ - A guide on the [naming convention](https://leanprover-community.github.io/lean3/contribute/naming.html)
+ - The [documentation style](https://leanprover-community.github.io/lean3/contribute/doc.html)
+ - The [commit naming conventions](https://github.com/leanprover-community/lean/blob/master/doc/commit_convention.md)
+
+Note: the title of a PR should follow the commit naming convention.
+
+### Using ``leanproject`` to contribute
+
+Running the ``leanproject get -b mathlib:shiny_lemma`` command will create a new worktree ``mathlib_shiny_lemma``
+with a local branch called ``shiny_lemma`` which has a copy of mathlib to work on.
+
+``leanproject build`` will check that nothing broke.
+Be warned that this will take some time if a fundamental file was changed.
+
+## Maintainers:
+
+* Anne Baanen (@Vierkantor): algebra, number theory, tactics
+* Reid Barton (@rwbarton): category theory, topology
+* Riccardo Brasca (@riccardobrasca): algebra, number theory, algebraic geometry, category theory
+* Mario Carneiro (@digama0): lean formalization, tactics, type theory, proof engineering
+* Bryan Gin-ge Chen (@bryangingechen): documentation, infrastructure
+* Johan Commelin (@jcommelin): algebra, number theory, category theory, algebraic geometry
+* Rémy Degenne (@RemyDegenne): probability, measure theory, analysis
+* Floris van Doorn (@fpvandoorn): measure theory, model theory, tactics
+* Frédéric Dupuis (@dupuisf): linear algebra, functional analysis
+* Gabriel Ebner (@gebner): tactics, infrastructure, core, formal languages
+* Sébastien Gouëzel (@sgouezel): topology, calculus, geometry, analysis, measure theory
+* Markus Himmel (@TwoFX): category theory
+* Chris Hughes (@ChrisHughes24): algebra
+* Yury G. Kudryashov (@urkud): analysis, topology, measure theory
+* Robert Y. Lewis (@robertylewis): tactics, documentation
+* Heather Macbeth (@hrmacbeth): geometry, analysis
+* Patrick Massot (@patrickmassot): documentation, topology, geometry
+* Bhavik Mehta (@b-mehta): category theory, combinatorics
+* Kyle Miller (@kmill): combinatorics, documentation
+* Scott Morrison (@semorrison): category theory, tactics
+* Oliver Nash (@ocfnash): algebra, geometry, topology
+* Adam Topaz (@adamtopaz): algebra, category theory, algebraic geometry
+* Eric Wieser (@eric-wieser): algebra, infrastructure
+
+## Emeritus maintainers:
+
+* Jeremy Avigad (@avigad): analysis
+* Johannes Hölzl (@johoelzl): measure theory, topology
+* Simon Hudon (@cipher1024): tactics
diff --git a/README.md b/README.md
index 88b3c18f3ccbe..f850c525cc3b0 100644
--- a/README.md
+++ b/README.md
@@ -1,108 +1,7 @@
-# Lean mathlib
+# Lean 3's mathlib
 
-![](https://github.com/leanprover-community/mathlib/workflows/continuous%20integration/badge.svg?branch=master)
-[![Bors enabled](https://bors.tech/images/badge_small.svg)](https://app.bors.tech/repositories/24316)
-[![project chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://leanprover.zulipchat.com)
-[![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-ready--to--code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/leanprover-community/mathlib)
+> [!WARNING]  
+> Lean 3 and Mathlib 3 are no longer actively maintained.
+> It is strongly recommended that you use [mathlib4](https://github.com/leanprover-community/mathlib4) for Lean 4 instead.
 
-[Mathlib](https://leanprover-community.github.io) is a user maintained library for the [Lean theorem prover](https://leanprover.github.io).
-It contains both programming infrastructure and mathematics,
-as well as tactics that use the former and allow to develop the latter.
-
-## Installation
-
-You can find detailed instructions to install Lean, mathlib, and supporting tools on [our website](https://leanprover-community.github.io/get_started.html).
-
-## Experimenting
-
-Got everything installed? Why not start with the [tutorial project](https://leanprover-community.github.io/install/project.html)?
-
-For more pointers, see [Learning Lean](https://leanprover-community.github.io/learn.html).
-
-## Documentation
-
-Besides the installation guides above and [Lean's general
-documentation](https://leanprover.github.io/documentation/), the documentation
-of mathlib consists of:
-
-- [The mathlib docs](https://leanprover-community.github.io/mathlib_docs): documentation [generated
-  automatically](https://github.com/leanprover-community/doc-gen) from the source `.lean` files.
-  In addition to the pages generated for each file in the library, the docs also include pages on:
-  - [tactics](https://leanprover-community.github.io/mathlib_docs/tactics.html),
-  - [commands](https://leanprover-community.github.io/mathlib_docs/commands.html),
-  - [hole commands](https://leanprover-community.github.io/mathlib_docs/hole_commands.html), and
-  - [attributes](https://leanprover-community.github.io/mathlib_docs/attributes.html).
-- A description of [currently covered theories](https://leanprover-community.github.io/theories.html),
-  as well as an [overview](https://leanprover-community.github.io/mathlib-overview.html) for mathematicians.
-- A couple of [tutorial Lean files](docs/tutorial/)
-- Some [extra Lean documentation](https://leanprover-community.github.io/learn.html) not specific to mathlib (see "Miscellaneous topics")
-- Documentation for people who would like to [contribute to mathlib](https://leanprover-community.github.io/contribute/index.html)
-
-Much of the discussion surrounding mathlib occurs in a
-[Zulip chat room](https://leanprover.zulipchat.com/). Since this
-chatroom is only visible to registered users, we provide an
-[openly accessible archive](https://leanprover-community.github.io/archive/)
-of the public discussions. This is useful for quick reference; for a
-better browsing interface, and to participate in the discussions, we strongly
-suggest joining the chat. Questions from users at all levels of expertise are
-welcomed.
-
-## Contributing
-
-The complete documentation for contributing to ``mathlib`` is located
-[on the community guide contribute to mathlib](https://leanprover-community.github.io/contribute/index.html)
-
-The process is different from other projects where one should not fork the repository.
-Instead write permission for non-master branches should be requested on [Zulip](https://leanprover.zulipchat.com)
-by introducing yourself, providing your GitHub handle and what contribution you are planning on doing.
-
-### Guidelines
-
-Mathlib has the following guidelines and conventions that must be followed
-
- - The [style guide](https://leanprover-community.github.io/contribute/style.html)
- - A guide on the [naming convention](https://leanprover-community.github.io/contribute/naming.html)
- - The [documentation style](https://leanprover-community.github.io/contribute/doc.html)
- - The [commit naming conventions](https://github.com/leanprover-community/lean/blob/master/doc/commit_convention.md)
-
-Note: the title of a PR should follow the commit naming convention.
-
-### Using ``leanproject`` to contribute
-
-Running the ``leanproject get -b mathlib:shiny_lemma`` command will create a new worktree ``mathlib_shiny_lemma``
-with a local branch called ``shiny_lemma`` which has a copy of mathlib to work on.
-
-``leanproject build`` will check that nothing broke.
-Be warned that this will take some time if a fundamental file was changed.
-
-## Maintainers:
-
-* Anne Baanen (@Vierkantor): algebra, number theory, tactics
-* Reid Barton (@rwbarton): category theory, topology
-* Riccardo Brasca (@riccardobrasca): algebra, number theory, algebraic geometry, category theory
-* Mario Carneiro (@digama0): lean formalization, tactics, type theory, proof engineering
-* Bryan Gin-ge Chen (@bryangingechen): documentation, infrastructure
-* Johan Commelin (@jcommelin): algebra, number theory, category theory, algebraic geometry
-* Rémy Degenne (@RemyDegenne): probability, measure theory, analysis
-* Floris van Doorn (@fpvandoorn): measure theory, model theory, tactics
-* Frédéric Dupuis (@dupuisf): linear algebra, functional analysis
-* Gabriel Ebner (@gebner): tactics, infrastructure, core, formal languages
-* Sébastien Gouëzel (@sgouezel): topology, calculus, geometry, analysis, measure theory
-* Markus Himmel (@TwoFX): category theory
-* Chris Hughes (@ChrisHughes24): algebra
-* Yury G. Kudryashov (@urkud): analysis, topology, measure theory
-* Robert Y. Lewis (@robertylewis): tactics, documentation
-* Heather Macbeth (@hrmacbeth): geometry, analysis
-* Patrick Massot (@patrickmassot): documentation, topology, geometry
-* Bhavik Mehta (@b-mehta): category theory, combinatorics
-* Kyle Miller (@kmill): combinatorics, documentation
-* Scott Morrison (@semorrison): category theory, tactics
-* Oliver Nash (@ocfnash): algebra, geometry, topology
-* Adam Topaz (@adamtopaz): algebra, category theory, algebraic geometry
-* Eric Wieser (@eric-wieser): algebra, infrastructure
-
-## Emeritus maintainers:
-
-* Jeremy Avigad (@avigad): analysis
-* Johannes Hölzl (@johoelzl): measure theory, topology
-* Simon Hudon (@cipher1024): tactics
+(If you need to read the old `README.md`, please see `OLD_README.md`.)
diff --git a/src/algebra/big_operators/basic.lean b/src/algebra/big_operators/basic.lean
index 85ce482038a50..ac6250a471925 100644
--- a/src/algebra/big_operators/basic.lean
+++ b/src/algebra/big_operators/basic.lean
@@ -106,6 +106,9 @@ variables {s s₁ s₂ : finset α} {a : α} {f g : α → β}
 @[to_additive] lemma prod_eq_multiset_prod [comm_monoid β] (s : finset α) (f : α → β) :
   ∏ x in s, f x = (s.1.map f).prod := rfl
 
+@[simp, to_additive] lemma prod_map_val [comm_monoid β] (s : finset α) (f : α → β) :
+  (s.1.map f).prod = ∏ a in s, f a := rfl
+
 @[to_additive]
 theorem prod_eq_fold [comm_monoid β] (s : finset α) (f : α → β) :
   ∏ x in s, f x = s.fold (*) 1 f :=
@@ -1418,16 +1421,19 @@ begin
   apply sum_congr rfl h₁
 end
 
+lemma nat_cast_card_filter [add_comm_monoid_with_one β] (p) [decidable_pred p] (s : finset α) :
+  ((filter p s).card : β) = ∑ a in s, if p a then 1 else 0 :=
+by simp only [add_zero, sum_const, nsmul_eq_mul, eq_self_iff_true, sum_const_zero, sum_ite,
+  nsmul_one]
+
+lemma card_filter (p) [decidable_pred p] (s : finset α) :
+  (filter p s).card = ∑ a in s, ite (p a) 1 0 :=
+nat_cast_card_filter _ _
+
 @[simp]
-lemma sum_boole {s : finset α} {p : α → Prop} [non_assoc_semiring β] {hp : decidable_pred p} :
-  (∑ x in s, if p x then (1 : β) else (0 : β)) = (s.filter p).card :=
-by simp only [add_zero,
- mul_one,
- finset.sum_const,
- nsmul_eq_mul,
- eq_self_iff_true,
- finset.sum_const_zero,
- finset.sum_ite]
+lemma sum_boole {s : finset α} {p : α → Prop} [add_comm_monoid_with_one β] {hp : decidable_pred p} :
+  (∑ x in s, if p x then 1 else 0 : β) = (s.filter p).card :=
+(nat_cast_card_filter _ _).symm
 
 lemma _root_.commute.sum_right [non_unital_non_assoc_semiring β] (s : finset α)
   (f : α → β) (b : β) (h : ∀ i ∈ s, commute b (f i)) :
diff --git a/src/algebra/big_operators/order.lean b/src/algebra/big_operators/order.lean
index 2573be61bcdb6..cda6b956aaa63 100644
--- a/src/algebra/big_operators/order.lean
+++ b/src/algebra/big_operators/order.lean
@@ -174,7 +174,7 @@ lemma prod_le_pow_card (s : finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s,
 begin
   refine (multiset.prod_le_pow_card (s.val.map f) n _).trans _,
   { simpa using h },
-  { simpa }
+  { simp }
 end
 
 @[to_additive card_nsmul_le_sum]
diff --git a/src/analysis/normed/group/pointwise.lean b/src/analysis/normed/group/pointwise.lean
index 672dd575ae904..340dc562045b2 100644
--- a/src/analysis/normed/group/pointwise.lean
+++ b/src/analysis/normed/group/pointwise.lean
@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel, Yaël Dillies
 -/
 import analysis.normed.group.basic
 import topology.metric_space.hausdorff_distance
+import topology.metric_space.isometric_smul
 
 /-!
 # Properties of pointwise addition of sets in normed groups
@@ -24,6 +25,7 @@ variables {E : Type*}
 section seminormed_group
 variables [seminormed_group E] {ε δ : ℝ} {s t : set E} {x y : E}
 
+-- note: we can't use `lipschitz_on_with.bounded_image2` here without adding `[isometric_smul E E]`
 @[to_additive] lemma metric.bounded.mul (hs : bounded s) (ht : bounded t) : bounded (s * t) :=
 begin
   obtain ⟨Rs, hRs⟩ : ∃ R, ∀ x ∈ s, ‖x‖ ≤ R := hs.exists_norm_le',
@@ -33,6 +35,10 @@ begin
   exact norm_mul_le_of_le (hRs x hx) (hRt y hy),
 end
 
+@[to_additive] lemma metric.bounded.of_mul (hst : bounded (s * t)) :
+  bounded s ∨ bounded t :=
+antilipschitz_with.bounded_of_image2_left _ (λ x, (isometry_mul_right x).antilipschitz) hst
+
 @[to_additive] lemma metric.bounded.inv : bounded s → bounded s⁻¹ :=
 by { simp_rw [bounded_iff_forall_norm_le', ←image_inv, ball_image_iff, norm_inv'], exact id }
 
@@ -55,6 +61,13 @@ eq_of_forall_le_iff $ λ r, by simp_rw [le_inf_edist, ←image_inv, ball_image_i
 lemma inf_edist_inv_inv (x : E) (s : set E) : inf_edist x⁻¹ s⁻¹ = inf_edist x s :=
 by rw [inf_edist_inv, inv_inv]
 
+@[to_additive] lemma ediam_mul_le (x y : set E) :
+  emetric.diam (x * y) ≤ emetric.diam x + emetric.diam y :=
+(lipschitz_on_with.ediam_image2_le (*) _ _
+    (λ _ _, (isometry_mul_right _).lipschitz.lipschitz_on_with _)
+    (λ _ _, (isometry_mul_left _).lipschitz.lipschitz_on_with _)).trans_eq $
+  by simp only [ennreal.coe_one, one_mul]
+
 end emetric
 
 variables (ε δ s t x y)
diff --git a/src/analysis/normed/order/upper_lower.lean b/src/analysis/normed/order/upper_lower.lean
index c834d2d671ddc..a081b70aa9623 100644
--- a/src/analysis/normed/order/upper_lower.lean
+++ b/src/analysis/normed/order/upper_lower.lean
@@ -23,10 +23,11 @@ are measurable.
 -/
 
 open function metric set
+open_locale pointwise
 
 variables {α ι : Type*}
 
-section metric_space
+section normed_ordered_group
 variables [normed_ordered_group α] {s : set α}
 
 @[to_additive is_upper_set.thickening]
@@ -49,12 +50,22 @@ protected lemma is_lower_set.cthickening' (hs : is_lower_set s) (ε : ℝ) :
   is_lower_set (cthickening ε s) :=
 by { rw cthickening_eq_Inter_thickening'', exact is_lower_set_Inter₂ (λ δ hδ, hs.thickening' _) }
 
-end metric_space
+@[to_additive upper_closure_interior_subset]
+lemma upper_closure_interior_subset' (s : set α) :
+  (upper_closure (interior s) : set α) ⊆ interior (upper_closure s) :=
+upper_closure_min (interior_mono subset_upper_closure) (upper_closure s).upper.interior
+
+@[to_additive lower_closure_interior_subset]
+lemma lower_closure_interior_subset' (s : set α) :
+  (upper_closure (interior s) : set α) ⊆ interior (upper_closure s) :=
+upper_closure_min (interior_mono subset_upper_closure) (upper_closure s).upper.interior
+
+end normed_ordered_group
 
 /-! ### `ℝⁿ` -/
 
 section finite
-variables [finite ι] {s : set (ι → ℝ)} {x y : ι → ℝ} {δ : ℝ}
+variables [finite ι] {s : set (ι → ℝ)} {x y : ι → ℝ}
 
 lemma is_upper_set.mem_interior_of_forall_lt (hs : is_upper_set s) (hx : x ∈ closure s)
   (h : ∀ i, x i < y i) :
@@ -99,7 +110,78 @@ end
 end finite
 
 section fintype
-variables [fintype ι] {s : set (ι → ℝ)} {x y : ι → ℝ} {δ : ℝ}
+variables [fintype ι] {s t : set (ι → ℝ)} {a₁ a₂ b₁ b₂ x y : ι → ℝ} {δ : ℝ}
+
+-- TODO: Generalise those lemmas so that they also apply to `ℝ` and `euclidean_space ι ℝ`
+lemma dist_inf_sup (x y : ι → ℝ) : dist (x ⊓ y) (x ⊔ y) = dist x y :=
+begin
+  refine congr_arg coe (finset.sup_congr rfl $ λ i _, _),
+  simp only [real.nndist_eq', sup_eq_max, inf_eq_min, max_sub_min_eq_abs, pi.inf_apply,
+    pi.sup_apply, real.nnabs_of_nonneg, abs_nonneg, real.to_nnreal_abs],
+end
+
+lemma dist_mono_left : monotone_on (λ x, dist x y) (Ici y) :=
+begin
+  refine λ y₁ hy₁ y₂ hy₂ hy, nnreal.coe_le_coe.2 (finset.sup_mono_fun $ λ i _, _),
+  rw [real.nndist_eq, real.nnabs_of_nonneg (sub_nonneg_of_le (‹y ≤ _› i : y i ≤ y₁ i)),
+    real.nndist_eq, real.nnabs_of_nonneg (sub_nonneg_of_le (‹y ≤ _› i : y i ≤ y₂ i))],
+  exact real.to_nnreal_mono (sub_le_sub_right (hy _) _),
+end
+
+lemma dist_mono_right : monotone_on (dist x) (Ici x) :=
+by simpa only [dist_comm] using dist_mono_left
+
+lemma dist_anti_left : antitone_on (λ x, dist x y) (Iic y) :=
+begin
+  refine λ y₁ hy₁ y₂ hy₂ hy, nnreal.coe_le_coe.2 (finset.sup_mono_fun $ λ i _, _),
+  rw [real.nndist_eq', real.nnabs_of_nonneg (sub_nonneg_of_le (‹_ ≤ y› i : y₂ i ≤ y i)),
+    real.nndist_eq', real.nnabs_of_nonneg (sub_nonneg_of_le (‹_ ≤ y› i : y₁ i ≤ y i))],
+  exact real.to_nnreal_mono (sub_le_sub_left (hy _) _),
+end
+
+lemma dist_anti_right : antitone_on (dist x) (Iic x) :=
+by simpa only [dist_comm] using dist_anti_left
+
+lemma dist_le_dist_of_le (ha : a₂ ≤ a₁) (h₁ : a₁ ≤ b₁) (hb : b₁ ≤ b₂) : dist a₁ b₁ ≤ dist a₂ b₂ :=
+(dist_mono_right h₁ (h₁.trans hb) hb).trans $
+  dist_anti_left (ha.trans $ h₁.trans hb) (h₁.trans hb) ha
+
+protected lemma metric.bounded.bdd_below : bounded s → bdd_below s :=
+begin
+  rintro ⟨r, hr⟩,
+  obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty,
+  { exact bdd_below_empty },
+  { exact ⟨x - const _ r, λ y hy i, sub_le_comm.1
+      (abs_sub_le_iff.1 $ (dist_le_pi_dist _ _ _).trans $ hr _ hx _ hy).1⟩ }
+end
+
+protected lemma metric.bounded.bdd_above : bounded s → bdd_above s :=
+begin
+  rintro ⟨r, hr⟩,
+  obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty,
+  { exact bdd_above_empty },
+  { exact ⟨x + const _ r, λ y hy i, sub_le_iff_le_add'.1 $
+      (abs_sub_le_iff.1 $ (dist_le_pi_dist _ _ _).trans $ hr _ hx _ hy).2⟩ }
+end
+
+protected lemma bdd_below.bounded : bdd_below s → bdd_above s → bounded s :=
+begin
+  rintro ⟨a, ha⟩ ⟨b, hb⟩,
+  refine ⟨dist a b, λ x hx y hy, _⟩,
+  rw ←dist_inf_sup,
+  exact dist_le_dist_of_le (le_inf (ha hx) $ ha hy) inf_le_sup (sup_le (hb hx) $ hb hy),
+end
+
+protected lemma bdd_above.bounded : bdd_above s → bdd_below s → bounded s := flip bdd_below.bounded
+
+lemma bounded_iff_bdd_below_bdd_above : bounded s ↔ bdd_below s ∧ bdd_above s :=
+⟨λ h, ⟨h.bdd_below, h.bdd_above⟩, λ h, h.1.bounded h.2⟩
+
+lemma bdd_below.bounded_inter (hs : bdd_below s) (ht : bdd_above t) : bounded (s ∩ t) :=
+(hs.mono $ inter_subset_left _ _).bounded $ ht.mono $ inter_subset_right _ _
+
+lemma bdd_above.bounded_inter (hs : bdd_above s) (ht : bdd_below t) : bounded (s ∩ t) :=
+(hs.mono $ inter_subset_left _ _).bounded $ ht.mono $ inter_subset_right _ _
 
 lemma is_upper_set.exists_subset_ball (hs : is_upper_set s) (hx : x ∈ closure s) (hδ : 0 < δ) :
   ∃ y, closed_ball y (δ/4) ⊆ closed_ball x δ ∧ closed_ball y (δ/4) ⊆ interior s :=
@@ -140,3 +222,74 @@ begin
 end
 
 end fintype
+
+section finite
+variables [finite ι] {s t : set (ι → ℝ)} {a₁ a₂ b₁ b₂ x y : ι → ℝ} {δ : ℝ}
+
+lemma is_antichain.interior_eq_empty [nonempty ι] (hs : is_antichain (≤) s) : interior s = ∅ :=
+begin
+  casesI nonempty_fintype ι,
+  refine eq_empty_of_forall_not_mem (λ x hx, _),
+  have hx' := interior_subset hx,
+  rw [mem_interior_iff_mem_nhds, metric.mem_nhds_iff] at hx,
+  obtain ⟨ε, hε, hx⟩ := hx,
+  refine hs.not_lt hx' (hx _) (lt_add_of_pos_right _ (by positivity : 0 < const ι (ε / 2))),
+  simpa [const, @pi_norm_const ι ℝ _ _ _ (ε / 2), abs_of_nonneg hε.lt.le],
+end
+
+/-!
+#### Note
+
+The closure and frontier of an antichain might not be antichains. Take for example the union
+of the open segments from `(0, 2)` to `(1, 1)` and from `(2, 1)` to `(3, 0)`. `(1, 1)` and `(2, 1)`
+are comparable and both in the closure/frontier.
+-/
+
+protected lemma is_closed.upper_closure (hs : is_closed s) (hs' : bdd_below s) :
+  is_closed (upper_closure s : set (ι → ℝ)) :=
+begin
+  casesI nonempty_fintype ι,
+  refine is_seq_closed.is_closed (λ f x hf hx, _),
+  choose g hg hgf using hf,
+  obtain ⟨a, ha⟩ := hx.bdd_above_range,
+  obtain ⟨b, hb, φ, hφ, hbf⟩ := tendsto_subseq_of_bounded (hs'.bounded_inter
+    bdd_above_Iic) (λ n, ⟨hg n, (hgf _).trans $  ha $ mem_range_self _⟩),
+  exact ⟨b, closure_minimal (inter_subset_left _ _) hs hb,
+    le_of_tendsto_of_tendsto' hbf (hx.comp hφ.tendsto_at_top) $ λ _, hgf _⟩,
+end
+
+protected lemma is_closed.lower_closure (hs : is_closed s) (hs' : bdd_above s) :
+  is_closed (lower_closure s : set (ι → ℝ)) :=
+begin
+  casesI nonempty_fintype ι,
+  refine is_seq_closed.is_closed (λ f x hf hx, _),
+  choose g hg hfg using hf,
+  haveI : bounded_ge_nhds_class ℝ := by apply_instance,
+  obtain ⟨a, ha⟩ := hx.bdd_below_range,
+  obtain ⟨b, hb, φ, hφ, hbf⟩ := tendsto_subseq_of_bounded (hs'.bounded_inter
+    bdd_below_Ici) (λ n, ⟨hg n, (ha $ mem_range_self _).trans $ hfg _⟩),
+  exact ⟨b, closure_minimal (inter_subset_left _ _) hs hb,
+    le_of_tendsto_of_tendsto' (hx.comp hφ.tendsto_at_top) hbf $ λ _, hfg _⟩,
+end
+
+protected lemma is_clopen.upper_closure (hs : is_clopen s) (hs' : bdd_below s) :
+  is_clopen (upper_closure s : set (ι → ℝ)) :=
+⟨hs.1.upper_closure, hs.2.upper_closure hs'⟩
+
+protected lemma is_clopen.lower_closure (hs : is_clopen s) (hs' : bdd_above s) :
+  is_clopen (lower_closure s : set (ι → ℝ)) :=
+⟨hs.1.lower_closure, hs.2.lower_closure hs'⟩
+
+lemma closure_upper_closure_comm (hs : bdd_below s) :
+  closure (upper_closure s : set (ι → ℝ)) = upper_closure (closure s) :=
+(closure_minimal (upper_closure_anti subset_closure) $
+  is_closed_closure.upper_closure hs.closure).antisymm $
+    upper_closure_min (closure_mono subset_upper_closure) (upper_closure s).upper.closure
+
+lemma closure_lower_closure_comm (hs : bdd_above s) :
+  closure (lower_closure s : set (ι → ℝ)) = lower_closure (closure s) :=
+(closure_minimal (lower_closure_mono subset_closure) $
+  is_closed_closure.lower_closure hs.closure).antisymm $
+    lower_closure_min (closure_mono subset_lower_closure) (lower_closure s).lower.closure
+
+end finite
diff --git a/src/combinatorics/set_family/ahlswede_zhang.lean b/src/combinatorics/set_family/ahlswede_zhang.lean
new file mode 100644
index 0000000000000..276084c473ce1
--- /dev/null
+++ b/src/combinatorics/set_family/ahlswede_zhang.lean
@@ -0,0 +1,264 @@
+/-
+Copyright (c) 2023 Yaël Dillies, Vladimir Ivanov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, Vladimir Ivanov
+-/
+import data.finset.sups
+
+/-!
+# The Ahlswede-Zhang identity
+
+This file proves the Ahlswede-Zhang identity, which is a nontrivial relation between the size of the
+"truncated unions"  of a set family. It sharpens the Lubell-Yamamoto-Meshalkin inequality
+`finset.sum_card_slice_div_choose_le_one`, by making explicit the correction term.
+
+For a set family `𝒜`, the Ahlswede-Zhang identity states that the sum of
+`|⋂ B ∈ 𝒜, B ⊆ A, B|/(|A| * n.choose |A|)` is exactly `1`.
+
+## Main declarations
+
+* `finset.truncated_sup`: `s.truncated_sup a` is the supremum of all `b ≤ a` in `𝒜` if there are
+  some, or `⊤` if there are none.
+* `finset.truncated_inf` `s.truncated_inf a` is the infimum of all `b ≥ a` in `𝒜` if there are
+  some, or `⊥` if there are none.
+
+## References
+
+* [R. Ahlswede, Z. Zhang, *An identity in combinatorial extremal theory*](https://doi.org/10.1016/0001-8708(90)90023-G)
+* [D. T. Tru, *An AZ-style identity and Bollobás deficiency*](https://doi.org/10.1016/j.jcta.2007.03.005)
+-/
+
+open_locale finset_family
+
+namespace finset
+variables {α β : Type*}
+
+/-! ### Truncated supremum, truncated infimum -/
+
+section semilattice_sup
+variables [semilattice_sup α] [order_top α] [@decidable_rel α (≤)]
+  [semilattice_sup β] [bounded_order β] [@decidable_rel β (≤)] {s t : finset α} {a b : α}
+
+private lemma sup_aux : a ∈ lower_closure (s : set α) → (s.filter $ λ b, a ≤ b).nonempty :=
+λ ⟨b, hb, hab⟩, ⟨b, mem_filter.2 ⟨hb, hab⟩⟩
+
+/-- The infimum of the elements of `s` less than `a` if there are some, otherwise `⊤`. -/
+def truncated_sup (s : finset α) (a : α) : α :=
+if h : a ∈ lower_closure (s : set α) then (s.filter $ λ b, a ≤ b).sup' (sup_aux h) id else ⊤
+
+lemma truncated_sup_of_mem (h : a ∈ lower_closure (s : set α)) :
+  truncated_sup s a = (s.filter $ λ b, a ≤ b).sup' (sup_aux h) id := dif_pos h
+
+lemma truncated_sup_of_not_mem (h : a ∉ lower_closure (s : set α)) : truncated_sup s a = ⊤ :=
+dif_neg h
+
+@[simp] lemma truncated_sup_empty (a : α) : truncated_sup ∅ a = ⊤ :=
+truncated_sup_of_not_mem $ by simp
+
+lemma le_truncated_sup : a ≤ truncated_sup s a :=
+begin
+  rw truncated_sup,
+  split_ifs,
+  { obtain ⟨ℬ, hb, h⟩ := h,
+    exact h.trans (le_sup' _ $ mem_filter.2 ⟨hb, h⟩) },
+  { exact le_top }
+end
+
+lemma map_truncated_sup (e : α ≃o β) (s : finset α) (a : α) :
+  e (truncated_sup s a) = truncated_sup (s.map e.to_equiv.to_embedding) (e a) :=
+begin
+  have : e a ∈ lower_closure (s.map e.to_equiv.to_embedding : set β)
+    ↔ a ∈ lower_closure (s : set α),
+  { simp },
+  simp_rw [truncated_sup, apply_dite e, map_finset_sup', map_top, this],
+  congr' with h,
+  simp only [filter_map, function.comp, equiv.coe_to_embedding, rel_iso.coe_fn_to_equiv,
+    order_iso.le_iff_le, id.def],
+  rw sup'_map, -- TODO: Why can't `simp` use `finset.sup'_map`?
+  simp only [equiv.coe_to_embedding, rel_iso.coe_fn_to_equiv],
+end
+
+variables [decidable_eq α]
+
+private lemma lower_aux :
+  a ∈ lower_closure (↑(s ∪ t) : set α) ↔
+    a ∈ lower_closure (s : set α) ∨ a ∈ lower_closure (t : set α) :=
+by rw [coe_union, lower_closure_union, lower_set.mem_sup_iff]
+
+lemma truncated_sup_union (hs : a ∈ lower_closure (s : set α))
+  (ht : a ∈ lower_closure (t : set α)) :
+  truncated_sup (s ∪ t) a = truncated_sup s a ⊔ truncated_sup t a :=
+by simpa only [truncated_sup_of_mem, hs, ht, lower_aux.2 (or.inl hs), filter_union]
+  using sup'_union _ _ _
+
+lemma truncated_sup_union_left (hs : a ∈ lower_closure (s : set α))
+  (ht : a ∉ lower_closure (t : set α)) :
+  truncated_sup (s ∪ t) a = truncated_sup s a :=
+begin
+  simp only [mem_lower_closure, mem_coe, exists_prop, not_exists, not_and] at ht,
+  simp only [truncated_sup_of_mem, hs, filter_union, filter_false_of_mem ht, union_empty,
+    lower_aux.2 (or.inl hs), ht],
+end
+
+lemma truncated_sup_union_right (hs : a ∉ lower_closure (s : set α))
+  (ht : a ∈ lower_closure (t : set α)) :
+  truncated_sup (s ∪ t) a = truncated_sup t a :=
+by rw [union_comm, truncated_sup_union_left ht hs]
+
+lemma truncated_sup_union_of_not_mem (hs : a ∉ lower_closure (s : set α))
+  (ht : a ∉ lower_closure (t : set α)) :
+  truncated_sup (s ∪ t) a = ⊤ :=
+truncated_sup_of_not_mem $ λ h, (lower_aux.1 h).elim hs ht
+
+end semilattice_sup
+
+section semilattice_inf
+variables [semilattice_inf α] [bounded_order α] [@decidable_rel α (≤)]
+  [semilattice_inf β] [bounded_order β] [@decidable_rel β (≤)] {s t : finset α} {a : α}
+
+private lemma inf_aux : a ∈ upper_closure (s : set α) → (s.filter $ λ b, b ≤ a).nonempty :=
+λ ⟨b, hb, hab⟩, ⟨b, mem_filter.2 ⟨hb, hab⟩⟩
+
+/-- The infimum of the elements of `s` less than `a` if there are some, otherwise `⊥`. -/
+def truncated_inf (s : finset α) (a : α) : α :=
+if h : a ∈ upper_closure (s : set α) then (s.filter $ λ b, b ≤ a).inf' (inf_aux h) id else ⊥
+
+lemma truncated_inf_of_mem (h : a ∈ upper_closure (s : set α)) :
+  truncated_inf s a = (s.filter $ λ b, b ≤ a).inf' (inf_aux h) id := dif_pos h
+
+lemma truncated_inf_of_not_mem (h : a ∉ upper_closure (s : set α)) : truncated_inf s a = ⊥ :=
+dif_neg h
+
+lemma truncated_inf_le (s : finset α) (a : α) : truncated_inf s a ≤ a :=
+begin
+  unfold truncated_inf,
+  split_ifs,
+  { obtain ⟨ℬ, hb, h⟩ := h,
+    exact (inf'_le _ $ mem_filter.2 ⟨hb, h⟩).trans h },
+  { exact bot_le }
+end
+
+@[simp] lemma truncated_inf_empty (a : α) : truncated_inf ∅ a = ⊥ :=
+truncated_inf_of_not_mem $ by simp
+
+lemma map_truncated_inf (e : α ≃o β) (s : finset α) (a : α) :
+  e (truncated_inf s a) = truncated_inf (s.map e.to_equiv.to_embedding) (e a) :=
+begin
+  have : e a ∈ upper_closure (s.map e.to_equiv.to_embedding : set β)
+    ↔ a ∈ upper_closure (s : set α),
+  { simp },
+  simp_rw [truncated_inf, apply_dite e, map_finset_inf', map_bot, this],
+  congr' with h,
+  simp only [filter_map, function.comp, equiv.coe_to_embedding, rel_iso.coe_fn_to_equiv,
+    order_iso.le_iff_le, id.def],
+  rw inf'_map, -- TODO: Why can't `simp` use `finset.inf'_map`?
+  simp only [equiv.coe_to_embedding, rel_iso.coe_fn_to_equiv],
+end
+
+variables [decidable_eq α]
+
+private lemma upper_aux :
+  a ∈ upper_closure (↑(s ∪ t) : set α) ↔
+    a ∈ upper_closure (s : set α) ∨ a ∈ upper_closure (t : set α) :=
+by rw [coe_union, upper_closure_union, upper_set.mem_inf_iff]
+
+lemma truncated_inf_union (hs : a ∈ upper_closure (s : set α))
+  (ht : a ∈ upper_closure (t : set α)) :
+  truncated_inf (s ∪ t) a = truncated_inf s a ⊓ truncated_inf t a :=
+by simpa only [truncated_inf_of_mem, hs, ht, upper_aux.2 (or.inl hs), filter_union]
+  using inf'_union _ _ _
+
+lemma truncated_inf_union_left (hs : a ∈ upper_closure (s : set α))
+  (ht : a ∉ upper_closure (t : set α)) :
+  truncated_inf (s ∪ t) a = truncated_inf s a :=
+begin
+  simp only [mem_upper_closure, mem_coe, exists_prop, not_exists, not_and] at ht,
+  simp only [truncated_inf_of_mem, hs, filter_union, filter_false_of_mem ht, union_empty,
+    upper_aux.2 (or.inl hs), ht],
+end
+
+lemma truncated_inf_union_right (hs : a ∉ upper_closure (s : set α))
+  (ht : a ∈ upper_closure (t : set α)) :
+  truncated_inf (s ∪ t) a = truncated_inf t a :=
+by rw [union_comm, truncated_inf_union_left ht hs]
+
+lemma truncated_inf_union_of_not_mem (hs : a ∉ upper_closure (s : set α))
+  (ht : a ∉ upper_closure (t : set α)) :
+  truncated_inf (s ∪ t) a = ⊥ :=
+truncated_inf_of_not_mem $ by { rw [coe_union, upper_closure_union], exact λ h, h.elim hs ht }
+
+end semilattice_inf
+
+section distrib_lattice
+variables [distrib_lattice α] [bounded_order α] [decidable_eq α] [@decidable_rel α (≤)]
+  {s t : finset α} {a : α}
+
+private lemma infs_aux
+ : a ∈ lower_closure (↑(s ⊼ t) : set α) ↔ a ∈ lower_closure (s : set α) ⊓ lower_closure t :=
+by rw [coe_infs, lower_closure_infs, lower_set.mem_inf_iff]
+
+private lemma sups_aux :
+  a ∈ upper_closure (↑(s ⊻ t) : set α) ↔ a ∈ upper_closure (s : set α) ⊔ upper_closure t :=
+by rw [coe_sups, upper_closure_sups, upper_set.mem_sup_iff]
+
+lemma truncated_sup_infs (hs : a ∈ lower_closure (s : set α)) (ht : a ∈ lower_closure (t : set α)) :
+  truncated_sup (s ⊼ t) a = truncated_sup s a ⊓ truncated_sup t a :=
+begin
+  simp only [truncated_sup_of_mem, hs, ht, infs_aux.2 ⟨hs, ht⟩, sup'_inf_sup', filter_infs_ge],
+  simp_rw ←image_inf_product,
+  rw sup'_image,
+  refl,
+end
+
+lemma truncated_inf_sups (hs : a ∈ upper_closure (s : set α)) (ht : a ∈ upper_closure (t : set α)) :
+  truncated_inf (s ⊻ t) a = truncated_inf s a ⊔ truncated_inf t a :=
+begin
+  simp only [truncated_inf_of_mem, hs, ht, sups_aux.2 ⟨hs, ht⟩, inf'_sup_inf', filter_sups_le],
+  simp_rw ←image_sup_product,
+  rw inf'_image,
+  refl,
+end
+
+lemma truncated_sup_infs_of_not_mem (ha : a ∉ lower_closure (s : set α) ⊓ lower_closure t) :
+  truncated_sup (s ⊼ t) a = ⊤ :=
+truncated_sup_of_not_mem $ by rwa [coe_infs, lower_closure_infs]
+
+lemma truncated_inf_sups_of_not_mem (ha : a ∉ upper_closure (s : set α) ⊔ upper_closure t) :
+  truncated_inf (s ⊻ t) a = ⊥ :=
+truncated_inf_of_not_mem $ by rwa [coe_sups, upper_closure_sups]
+
+end distrib_lattice
+
+section boolean_algebra
+variables [boolean_algebra α] [@decidable_rel α (≤)] {s : finset α} {a : α}
+
+@[simp] lemma compl_truncated_sup (s : finset α) (a : α) :
+  (truncated_sup s a)ᶜ = truncated_inf (s.map ⟨compl, compl_injective⟩) aᶜ :=
+map_truncated_sup (order_iso.compl α) _ _
+
+@[simp] lemma compl_truncated_inf (s : finset α) (a : α) :
+  (truncated_inf s a)ᶜ = truncated_sup (s.map ⟨compl, compl_injective⟩) aᶜ :=
+map_truncated_inf (order_iso.compl α) _ _
+
+end boolean_algebra
+
+variables [decidable_eq α] [fintype α]
+
+lemma card_truncated_sup_union_add_card_truncated_sup_infs (𝒜 ℬ : finset (finset α))
+  (s : finset α) :
+  (truncated_sup (𝒜 ∪ ℬ) s).card + (truncated_sup (𝒜 ⊼ ℬ) s).card =
+    (truncated_sup 𝒜 s).card + (truncated_sup ℬ s).card :=
+begin
+  by_cases h𝒜 : s ∈ lower_closure (𝒜 : set $ finset α);
+    by_cases hℬ : s ∈ lower_closure (ℬ : set $ finset α),
+  { rw [truncated_sup_union h𝒜 hℬ, truncated_sup_infs h𝒜 hℬ],
+    exact card_union_add_card_inter _ _ },
+  { rw [truncated_sup_union_left h𝒜 hℬ, truncated_sup_of_not_mem hℬ,
+      truncated_sup_infs_of_not_mem (λ h, hℬ h.2)] },
+  { rw [truncated_sup_union_right h𝒜 hℬ, truncated_sup_of_not_mem h𝒜,
+      truncated_sup_infs_of_not_mem (λ h, h𝒜 h.1), add_comm] },
+  { rw [truncated_sup_of_not_mem h𝒜, truncated_sup_of_not_mem hℬ,
+      truncated_sup_union_of_not_mem h𝒜 hℬ, truncated_sup_infs_of_not_mem (λ h, h𝒜 h.1)] }
+end
+
+end finset
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..ae354aa222531 100644
--- a/src/data/finset/card.lean
+++ b/src/data/finset/card.lean
@@ -42,6 +42,7 @@ variables {s t : finset α} {a b : α}
 def card (s : finset α) : ℕ := s.1.card
 
 lemma card_def (s : finset α) : s.card = s.1.card := rfl
+@[simp] lemma card_val (s : finset α) : s.1.card = s.card := rfl
 
 @[simp] lemma card_mk {m nodup} : (⟨m, nodup⟩ : finset α).card = m.card := rfl
 
@@ -434,6 +435,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/image.lean b/src/data/finset/image.lean
index e41fa0925240e..74a678a27cabc 100644
--- a/src/data/finset/image.lean
+++ b/src/data/finset/image.lean
@@ -127,6 +127,22 @@ lemma filter_map {p : β → Prop} [decidable_pred p] :
   (s.map f).filter p = (s.filter (p ∘ f)).map f :=
 eq_of_veq (map_filter _ _ _)
 
+lemma map_filter' (p : α → Prop) [decidable_pred p] (f : α ↪ β) (s : finset α)
+  [decidable_pred (λ b, ∃ a, p a ∧ f a = b)] :
+  (s.filter p).map f = (s.map f).filter (λ b, ∃ a, p a ∧ f a = b) :=
+by simp [(∘), filter_map, f.injective.eq_iff]
+
+lemma filter_attach' [decidable_eq α] (s : finset α) (p : s → Prop) [decidable_pred p] :
+  s.attach.filter p =
+    (s.filter $ λ x, ∃ h, p ⟨x, h⟩).attach.map ⟨subtype.map id $ filter_subset _ _,
+      subtype.map_injective _ injective_id⟩ :=
+eq_of_veq $ multiset.filter_attach' _ _
+
+@[simp] lemma filter_attach (p : α → Prop) [decidable_pred p]  (s : finset α) :
+  (s.attach.filter (λ x, p ↑x)) =
+    (s.filter p).attach.map ((embedding.refl _).subtype_map mem_of_mem_filter) :=
+eq_of_veq $ multiset.filter_attach _ _
+
 lemma map_filter {f : α ≃ β} {p : α → Prop} [decidable_pred p] :
   (s.filter p).map f.to_embedding = (s.map f.to_embedding).filter (p ∘ f.symm) :=
 by simp only [filter_map, function.comp, equiv.to_embedding_apply, equiv.symm_apply_apply]
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/data/finset/sups.lean b/src/data/finset/sups.lean
index 0c2c69a056427..b94a8777cedc4 100644
--- a/src/data/finset/sups.lean
+++ b/src/data/finset/sups.lean
@@ -36,6 +36,20 @@ We define the following notation in locale `finset_family`:
 open function
 open_locale set_family
 
+-- TODO: Is there a better spot for those two instances?
+namespace finset
+variables {α : Type*} [preorder α] {s t : set α} {a : α}
+
+instance decidable_pred_mem_upper_closure (s : finset α) [@decidable_rel α (≤)] :
+  decidable_pred (∈ upper_closure (s : set α)) :=
+λ _, finset.decidable_dexists_finset
+
+instance decidable_pred_mem_lower_closure (s : finset α) [@decidable_rel α (≤)] :
+  decidable_pred (∈ lower_closure (s : set α)) :=
+λ _, finset.decidable_dexists_finset
+
+end finset
+
 variables {α : Type*} [decidable_eq α]
 
 namespace finset
@@ -116,6 +130,21 @@ lemma sups_right_comm : (s ⊻ t) ⊻ u = (s ⊻ u) ⊻ t := image₂_right_comm
 lemma sups_sups_sups_comm : (s ⊻ t) ⊻ (u ⊻ v) = (s ⊻ u) ⊻ (t ⊻ v) :=
 image₂_image₂_image₂_comm sup_sup_sup_comm
 
+variables [@decidable_rel α (≤)]
+
+lemma filter_sups_le (s t : finset α) (a : α) :
+  (s ⊻ t).filter (λ b, b ≤ a) = s.filter (λ b, b ≤ a) ⊻ t.filter (λ b, b ≤ a) :=
+begin
+  ext b,
+  simp only [mem_filter, mem_sups],
+  split,
+  { rintro ⟨⟨b, hb, c, hc, rfl⟩, ha⟩,
+    rw sup_le_iff at ha,
+    exact ⟨_, ⟨hb, ha.1⟩, _, ⟨hc, ha.2⟩, rfl⟩ },
+  { rintro ⟨b, hb, c, hc, _, rfl⟩,
+    exact ⟨⟨_, hb.1, _, hc.1, rfl⟩, sup_le hb.2 hc.2⟩ }
+end
+
 end sups
 
 section infs
@@ -195,6 +224,21 @@ lemma infs_right_comm : (s ⊼ t) ⊼ u = (s ⊼ u) ⊼ t := image₂_right_comm
 lemma infs_infs_infs_comm : (s ⊼ t) ⊼ (u ⊼ v) = (s ⊼ u) ⊼ (t ⊼ v) :=
 image₂_image₂_image₂_comm inf_inf_inf_comm
 
+variables [@decidable_rel α (≤)]
+
+lemma filter_infs_ge (s t : finset α) (a : α) :
+  (s ⊼ t).filter (λ b, a ≤ b) = s.filter (λ b, a ≤ b) ⊼ t.filter (λ b, a ≤ b) :=
+begin
+  ext b,
+  simp only [mem_filter, mem_infs],
+  split,
+  { rintro ⟨⟨b, hb, c, hc, rfl⟩, ha⟩,
+    rw le_inf_iff at ha,
+    exact ⟨_, ⟨hb, ha.1⟩, _, ⟨hc, ha.2⟩, rfl⟩ },
+  { rintro ⟨b, hb, c, hc, _, rfl⟩,
+    exact ⟨⟨_, hb.1, _, hc.1, rfl⟩, le_inf hb.2 hc.2⟩ }
+end
+
 end infs
 
 open_locale finset_family
diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean
index 939c431e6d038..ce40ca44d44af 100644
--- a/src/data/list/basic.lean
+++ b/src/data/list/basic.lean
@@ -2716,6 +2716,8 @@ end split_at_on
   with the same elements but in the type `{x // x ∈ l}`. -/
 def attach (l : list α) : list {x // x ∈ l} := pmap subtype.mk l (λ a, id)
 
+@[simp] lemma attach_nil : ([] : list α).attach = [] := rfl
+
 theorem sizeof_lt_sizeof_of_mem [has_sizeof α] {x : α} {l : list α} (hx : x ∈ l) :
   sizeof x < sizeof l :=
 begin
@@ -3250,12 +3252,35 @@ theorem map_filter (f : β → α) (l : list β) :
   filter p (map f l) = map f (filter (p ∘ f) l) :=
 by rw [← filter_map_eq_map, filter_filter_map, filter_map_filter]; refl
 
+lemma map_filter' {f : α → β} (hf : injective f) (l : list α)
+  [decidable_pred (λ b, ∃ a, p a ∧ f a = b)] :
+  (l.filter p).map f = (l.map f).filter (λ b, ∃ a, p a ∧ f a = b) :=
+by simp [(∘), map_filter, hf.eq_iff]
+
+lemma filter_attach' (l : list α) (p : {a // a ∈ l} → Prop) [decidable_eq α] [decidable_pred p] :
+  l.attach.filter p = (l.filter $ λ x, ∃ h, p ⟨x, h⟩).attach.map
+    (subtype.map id $ λ x hx, let ⟨h, _⟩ := of_mem_filter hx in h) :=
+begin
+  classical,
+  refine map_injective_iff.2 subtype.coe_injective _,
+  simp [(∘), map_filter' _ subtype.coe_injective],
+end
+
+@[simp] lemma filter_attach (l : list α) (p : α → Prop) [decidable_pred p] :
+  l.attach.filter (λ x, p ↑x) = (l.filter p).attach.map (subtype.map id $ λ _, mem_of_mem_filter) :=
+map_injective_iff.2 subtype.coe_injective $ by
+  simp_rw [map_map, (∘), subtype.map, subtype.coe_mk, id.def, ←map_filter, attach_map_coe]
+
 @[simp] theorem filter_filter (q) [decidable_pred q] : ∀ l,
   filter p (filter q l) = filter (λ a, p a ∧ q a) l
 | [] := rfl
 | (a :: l) := by by_cases hp : p a; by_cases hq : q a; simp only [hp, hq, filter, if_true, if_false,
     true_and, false_and, filter_filter l, eq_self_iff_true]
 
+lemma filter_comm (q) [decidable_pred q] (l : list α) :
+  filter p (filter q l) = filter q (filter p l) :=
+by simp [and_comm]
+
 @[simp] lemma filter_true {h : decidable_pred (λ a : α, true)} (l : list α) :
   @filter α (λ _, true) h l = l :=
 by convert filter_eq_self.2 (λ _ _, trivial)
diff --git a/src/data/list/count.lean b/src/data/list/count.lean
index 5660878757f14..25d72187efa05 100644
--- a/src/data/list/count.lean
+++ b/src/data/list/count.lean
@@ -84,6 +84,9 @@ by simp only [countp_eq_length_filter, filter_filter]
 | [] := rfl
 | (a::l) := by rw [map_cons, countp_cons, countp_cons, countp_map]
 
+@[simp] lemma countp_attach (l : list α) : l.attach.countp (λ a, p ↑a) = l.countp p :=
+by rw [←countp_map, attach_map_coe]
+
 variables {p q}
 
 lemma countp_mono_left (h : ∀ x ∈ l, p x → q x) : countp p l ≤ countp q l :=
@@ -197,6 +200,9 @@ lemma count_bind {α β} [decidable_eq β] (l : list α) (f : α → list β) (x
   count x (l.bind f) = sum (map (count x ∘ f) l) :=
 by rw [list.bind, count_join, map_map]
 
+@[simp] lemma count_attach (a : {x // x ∈ l}) : l.attach.count a = l.count a :=
+eq.trans (countp_congr $ λ _ _, subtype.ext_iff) $ countp_attach _ _
+
 @[simp] lemma count_map_of_injective {α β} [decidable_eq α] [decidable_eq β]
   (l : list α) (f : α → β) (hf : function.injective f) (x : α) :
   count (f x) (map f l) = count x l :=
diff --git a/src/data/list/perm.lean b/src/data/list/perm.lean
index 8c1667485d02c..22c3396410970 100644
--- a/src/data/list/perm.lean
+++ b/src/data/list/perm.lean
@@ -396,7 +396,7 @@ theorem subperm.countp_le (p : α → Prop) [decidable_pred p]
 | ⟨l, p', s⟩ := p'.countp_eq p ▸ s.countp_le p
 
 theorem perm.countp_congr (s : l₁ ~ l₂) {p p' : α → Prop} [decidable_pred p] [decidable_pred p']
-  (hp : ∀ x ∈ l₁, p x = p' x) : l₁.countp p = l₂.countp p' :=
+  (hp : ∀ x ∈ l₁, p x ↔ p' x) : l₁.countp p = l₂.countp p' :=
 begin
   rw ← s.countp_eq p',
   clear s,
diff --git a/src/data/multiset/basic.lean b/src/data/multiset/basic.lean
index f58ff719fad96..99873f8d0abe7 100644
--- a/src/data/multiset/basic.lean
+++ b/src/data/multiset/basic.lean
@@ -16,7 +16,7 @@ These are implemented as the quotient of a list by permutations.
 We define the global infix notation `::ₘ` for `multiset.cons`.
 -/
 
-open list subtype nat
+open function list nat subtype
 
 variables {α : Type*} {β : Type*} {γ : Type*}
 
@@ -1543,6 +1543,10 @@ le_antisymm (le_inter
   filter p (filter q s) = filter (λ a, p a ∧ q a) s :=
 quot.induction_on s $ λ l, congr_arg coe $ filter_filter p q l
 
+lemma filter_comm (q) [decidable_pred q] (s : multiset α) :
+  filter p (filter q s) = filter q (filter p s) :=
+by simp [and_comm]
+
 theorem filter_add_filter (q) [decidable_pred q] (s : multiset α) :
   filter p s + filter q s = filter (λ a, p a ∨ q a) s + filter (λ a, p a ∧ q a) s :=
 multiset.induction_on s rfl $ λ a s IH,
@@ -1556,6 +1560,11 @@ theorem map_filter (f : β → α) (s : multiset β) :
   filter p (map f s) = map f (filter (p ∘ f) s) :=
 quot.induction_on s (λ l, by simp [map_filter])
 
+lemma map_filter' {f : α → β} (hf : injective f) (s : multiset α)
+  [decidable_pred (λ b, ∃ a, p a ∧ f a = b)] :
+  (s.filter p).map f = (s.map f).filter (λ b, ∃ a, p a ∧ f a = b) :=
+by simp [(∘), map_filter, hf.eq_iff]
+
 /-! ### Simultaneously filter and map elements of a multiset -/
 
 /-- `filter_map f s` is a combination filter/map operation on `s`.
@@ -1704,6 +1713,18 @@ begin
       card_singleton, add_comm] },
 end
 
+@[simp] lemma countp_attach (s : multiset α) : s.attach.countp (λ a, p ↑a) = s.countp p :=
+quotient.induction_on s $ λ l, begin
+  simp only [quot_mk_to_coe, coe_countp],
+  rw [quot_mk_to_coe, coe_attach, coe_countp],
+  exact list.countp_attach _ _,
+end
+
+@[simp] lemma filter_attach (m : multiset α) (p : α → Prop) [decidable_pred p] :
+  (m.attach.filter (λ x, p ↑x)) =
+    (m.filter p).attach.map (subtype.map id $ λ _, multiset.mem_of_mem_filter) :=
+quotient.induction_on m $ λ l, congr_arg coe (list.filter_attach l p)
+
 variable {p}
 
 theorem countp_pos {s} : 0 < countp p s ↔ ∃ a ∈ s, p a :=
@@ -1720,7 +1741,7 @@ countp_pos.2 ⟨_, h, pa⟩
 
 theorem countp_congr {s s' : multiset α} (hs : s = s')
   {p p' : α → Prop} [decidable_pred p] [decidable_pred p']
-  (hp : ∀ x ∈ s, p x = p' x) : s.countp p = s'.countp p' :=
+  (hp : ∀ x ∈ s, p x ↔ p' x) : s.countp p = s'.countp p' :=
 quot.induction_on₂ s s' (λ l l' hs hp, begin
   simp only [quot_mk_to_coe'', coe_eq_coe] at hs,
   exact hs.countp_congr hp,
@@ -1731,7 +1752,7 @@ end
 /-! ### Multiplicity of an element -/
 
 section
-variable [decidable_eq α]
+variables [decidable_eq α] {s : multiset α}
 
 /-- `count a s` is the multiplicity of `a` in `s`. -/
 def count (a : α) : multiset α → ℕ := countp (eq a)
@@ -1778,6 +1799,9 @@ def count_add_monoid_hom (a : α) : multiset α →+ ℕ := countp_add_monoid_ho
 @[simp] theorem count_nsmul (a : α) (n s) : count a (n • s) = n * count a s :=
 by induction n; simp [*, succ_nsmul', succ_mul, zero_nsmul]
 
+@[simp] lemma count_attach (a : {x // x ∈ s}) : s.attach.count a = s.count a :=
+eq.trans (countp_congr rfl $ λ _ _, subtype.ext_iff) $ countp_attach _ _
+
 theorem count_pos {a : α} {s : multiset α} : 0 < count a s ↔ a ∈ s :=
 by simp [count, countp_pos]
 
@@ -1901,13 +1925,6 @@ begin
     contradiction }
 end
 
-@[simp]
-lemma attach_count_eq_count_coe (m : multiset α) (a) : m.attach.count a = m.count (a : α) :=
-calc m.attach.count a
-    = (m.attach.map (coe : _ → α)).count (a : α) :
-  (multiset.count_map_eq_count' _ _ subtype.coe_injective _).symm
-... = m.count (a : α) : congr_arg _ m.attach_map_coe
-
 lemma filter_eq' (s : multiset α) (b : α) : s.filter (= b) = replicate (count b s) b :=
 quotient.induction_on s $ λ l, congr_arg coe $ filter_eq' l b
 
@@ -2174,6 +2191,19 @@ theorem map_injective {f : α → β} (hf : function.injective f) :
   function.injective (multiset.map f) :=
 assume x y, (map_eq_map hf).1
 
+lemma filter_attach' (s : multiset α) (p : {a // a ∈ s} → Prop) [decidable_eq α]
+  [decidable_pred p] :
+  s.attach.filter p =
+    (s.filter $ λ x, ∃ h, p ⟨x, h⟩).attach.map (subtype.map id $ λ x hx,
+      let ⟨h, _⟩ := of_mem_filter hx in h) :=
+begin
+  classical,
+  refine multiset.map_injective subtype.coe_injective _,
+  simp only [function.comp, map_filter' _ subtype.coe_injective, subtype.exists, coe_mk,
+    exists_and_distrib_right, exists_eq_right, attach_map_coe, map_map, map_coe, id.def],
+  rw attach_map_coe,
+end
+
 end map
 
 section quot
diff --git a/src/data/multiset/lattice.lean b/src/data/multiset/lattice.lean
index 7b279882080d6..5e575d279b753 100644
--- a/src/data/multiset/lattice.lean
+++ b/src/data/multiset/lattice.lean
@@ -39,7 +39,7 @@ sup_bot_eq
 @[simp] lemma sup_add (s₁ s₂ : multiset α) : (s₁ + s₂).sup = s₁.sup ⊔ s₂.sup :=
 eq.trans (by simp [sup]) (fold_add _ _ _ _ _)
 
-lemma sup_le {s : multiset α} {a : α} : s.sup ≤ a ↔ (∀b ∈ s, b ≤ a) :=
+@[simp] lemma sup_le {s : multiset α} {a : α} : s.sup ≤ a ↔ (∀b ∈ s, b ≤ a) :=
 multiset.induction_on s (by simp)
   (by simp [or_imp_distrib, forall_and_distrib] {contextual := tt})
 
diff --git a/src/data/real/nnreal.lean b/src/data/real/nnreal.lean
index cca419cf48609..47dba7306a2d2 100644
--- a/src/data/real/nnreal.lean
+++ b/src/data/real/nnreal.lean
@@ -822,6 +822,8 @@ lemma nnabs_coe (x : ℝ≥0) : nnabs x = x := by simp
 lemma coe_to_nnreal_le (x : ℝ) : (to_nnreal x : ℝ) ≤ |x| :=
 max_le (le_abs_self _) (abs_nonneg _)
 
+@[simp] lemma to_nnreal_abs (x : ℝ) : |x|.to_nnreal = x.nnabs := nnreal.coe_injective $ by simp
+
 lemma cast_nat_abs_eq_nnabs_cast (n : ℤ) :
   (n.nat_abs : ℝ≥0) = nnabs n :=
 by { ext, rw [nnreal.coe_nat_cast, int.cast_nat_abs, real.coe_nnabs] }
diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
index 9ac1590fab649..065bb077cb029 100644
--- a/src/data/set/basic.lean
+++ b/src/data/set/basic.lean
@@ -1906,3 +1906,6 @@ lemma subset_right_of_subset_union (h : s ⊆ t ∪ u) (hab : disjoint s t) : s
 hab.left_le_of_le_sup_left h
 
 end disjoint
+
+@[simp] lemma Prop.compl_singleton (p : Prop) : ({p}ᶜ : set Prop) = {¬ p} :=
+ext $ λ q, by simpa [@iff.comm q] using not_iff
diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean
index f86cca6bfa443..c073dce02f496 100644
--- a/src/data/set/finite.lean
+++ b/src/data/set/finite.lean
@@ -927,8 +927,7 @@ eq.trans (by congr) empty_card
 
 theorem card_fintype_insert_of_not_mem {a : α} (s : set α) [fintype s] (h : a ∉ s) :
   @fintype.card _ (fintype_insert_of_not_mem s h) = fintype.card s + 1 :=
-by rw [fintype_insert_of_not_mem, fintype.card_of_finset];
-   simp [finset.card, to_finset]; refl
+by simp [fintype_insert_of_not_mem, fintype.card_of_finset]
 
 @[simp] theorem card_insert {a : α} (s : set α)
   [fintype s] (h : a ∉ s) {d : fintype.{u} (insert a s : set α)} :
diff --git a/src/data/set/image.lean b/src/data/set/image.lean
index 4e942d43a7266..9b00e12e92842 100644
--- a/src/data/set/image.lean
+++ b/src/data/set/image.lean
@@ -71,6 +71,9 @@ theorem subset_preimage_univ {s : set α} : s ⊆ f ⁻¹' univ := subset_univ _
 @[simp] theorem preimage_diff (f : α → β) (s t : set β) :
   f ⁻¹' (s \ t) = f ⁻¹' s \ f ⁻¹' t := rfl
 
+@[simp] lemma preimage_symm_diff (f : α → β) (s t : set β) :
+  f ⁻¹' (s ∆ t) = (f ⁻¹' s) ∆ (f ⁻¹' t) := rfl
+
 @[simp] theorem preimage_ite (f : α → β) (s t₁ t₂ : set β) :
   f ⁻¹' (s.ite t₁ t₂) = (f ⁻¹' s).ite (f ⁻¹' t₁) (f ⁻¹' t₂) :=
 rfl
@@ -120,6 +123,10 @@ lemma nonempty_of_nonempty_preimage {s : set β} {f : α → β} (hf : (f ⁻¹'
   s.nonempty :=
 let ⟨x, hx⟩ := hf in ⟨f x, hx⟩
 
+@[simp] lemma preimage_singleton_true (p : α → Prop) : p ⁻¹' {true} = {a | p a} := by { ext, simp }
+@[simp] lemma preimage_singleton_false (p : α → Prop) : p ⁻¹' {false} = {a | ¬ p a} :=
+by { ext, simp }
+
 lemma preimage_subtype_coe_eq_compl {α : Type*} {s u v : set α} (hsuv : s ⊆ u ∪ v)
   (H : s ∩ (u ∩ v) = ∅) : (coe : s → α) ⁻¹' u = (coe ⁻¹' v)ᶜ :=
 begin
@@ -1003,6 +1010,9 @@ lemma left_inverse.preimage_preimage {g : β → α} (h : left_inverse g f) (s :
   f ⁻¹' (g ⁻¹' s) = s :=
 by rw [← preimage_comp, h.comp_eq_id, preimage_id]
 
+protected lemma involutive.preimage {f : α → α} (hf : involutive f) : involutive (preimage f) :=
+hf.right_inverse.preimage_preimage
+
 end function
 
 namespace equiv_like
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` -/
diff --git a/src/measure_theory/measurable_space.lean b/src/measure_theory/measurable_space.lean
index 98a586b1589a6..74b43d1b7bce7 100644
--- a/src/measure_theory/measurable_space.lean
+++ b/src/measure_theory/measurable_space.lean
@@ -7,6 +7,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 import data.prod.tprod
 import group_theory.coset
 import logic.equiv.fin
+import logic.lemmas
 import measure_theory.measurable_space_def
 import order.filter.small_sets
 import order.liminf_limsup
@@ -136,6 +137,12 @@ lemma le_map_comap : m ≤ (m.comap g).map g := (gc_comap_map g).le_u_l _
 
 end functors
 
+@[simp] lemma map_const {m} (b : β) : measurable_space.map (λ a : α, b) m = ⊤ :=
+eq_top_iff.2 $ by { rintro s hs, by_cases b ∈ s; change measurable_set (preimage _ _); simp [*] }
+
+@[simp] lemma comap_const {m} (b : β) : measurable_space.comap (λ a : α, b) m = ⊥ :=
+eq_bot_iff.2 $ by { rintro _ ⟨s, -, rfl⟩, by_cases b ∈ s; simp [*] }
+
 lemma comap_generate_from {f : α → β} {s : set (set β)} :
   (generate_from s).comap f = generate_from (preimage f '' s) :=
 le_antisymm
@@ -291,6 +298,7 @@ section constructions
 instance : measurable_space empty := ⊤
 instance : measurable_space punit := ⊤ -- this also works for `unit`
 instance : measurable_space bool := ⊤
+instance Prop.measurable_space : measurable_space Prop := ⊤
 instance : measurable_space ℕ := ⊤
 instance : measurable_space ℤ := ⊤
 instance : measurable_space ℚ := ⊤
@@ -298,6 +306,7 @@ instance : measurable_space ℚ := ⊤
 instance : measurable_singleton_class empty := ⟨λ _, trivial⟩
 instance : measurable_singleton_class punit := ⟨λ _, trivial⟩
 instance : measurable_singleton_class bool := ⟨λ _, trivial⟩
+instance Prop.measurable_singleton_class : measurable_singleton_class Prop := ⟨λ _, trivial⟩
 instance : measurable_singleton_class ℕ := ⟨λ _, trivial⟩
 instance : measurable_singleton_class ℤ := ⟨λ _, trivial⟩
 instance : measurable_singleton_class ℚ := ⟨λ _, trivial⟩
@@ -340,6 +349,15 @@ begin
   exact h,
 end
 
+lemma measurable_to_prop {f : α → Prop} (h : measurable_set (f⁻¹' {true})) : measurable f :=
+begin
+  refine measurable_to_countable' (λ x, _),
+  by_cases hx : x,
+  { simpa [hx] using h },
+  { simpa only [hx, ←preimage_compl, Prop.compl_singleton, not_true, preimage_singleton_false]
+      using h.compl }
+end
+
 lemma measurable_find_greatest' {p : α → ℕ → Prop} [∀ x, decidable_pred (p x)]
   {N : ℕ} (hN : ∀ k ≤ N, measurable_set {x | nat.find_greatest (p x) N = k}) :
   measurable (λ x, nat.find_greatest (p x) N) :=
@@ -860,8 +878,38 @@ end sum
 instance {α} {β : α → Type*} [m : Πa, measurable_space (β a)] : measurable_space (sigma β) :=
 ⨅a, (m a).map (sigma.mk a)
 
+section prop
+variables {p : α → Prop}
+
+variables [measurable_space α]
+
+@[simp] lemma measurable_set_set_of : measurable_set {a | p a} ↔ measurable p :=
+⟨λ h, measurable_to_prop $ by simpa only [preimage_singleton_true], λ h,
+  by simpa using h (measurable_set_singleton true)⟩
+
+@[simp] lemma measurable_mem : measurable (∈ s) ↔ measurable_set s := measurable_set_set_of.symm
+
+alias measurable_set_set_of ↔ _ measurable.set_of
+alias measurable_mem ↔ _ measurable_set.mem
+
+end prop
 end constructions
 
+namespace measurable_space
+
+/-- The sigma-algebra generated by a single set `s` is `{∅, s, sᶜ, univ}`. -/
+@[simp] lemma generate_from_singleton (s : set α) :
+  generate_from {s} = measurable_space.comap (∈ s) ⊤ :=
+begin
+  classical,
+  letI : measurable_space α := generate_from {s},
+  refine le_antisymm (generate_from_le $ λ t ht, ⟨{true}, trivial, by simp [ht.symm]⟩) _,
+  rintro _ ⟨u, -, rfl⟩,
+  exact (show measurable_set s, from generate_measurable.basic _ $ mem_singleton s).mem trivial,
+end
+
+end measurable_space
+
 /-- A map `f : α → β` is called a *measurable embedding* if it is injective, measurable, and sends
 measurable sets to measurable sets. The latter assumption can be replaced with “`f` has measurable
 inverse `g : range f → α`”, see `measurable_embedding.measurable_range_splitting`,
@@ -1052,6 +1100,9 @@ e.to_equiv.image_eq_preimage s
   measurable_set (e '' s) ↔ measurable_set s :=
 by rw [image_eq_preimage, measurable_set_preimage]
 
+@[simp] lemma map_eq (e : α ≃ᵐ β) : measurable_space.map e ‹_› = ‹_› :=
+e.measurable.le_map.antisymm' $ λ s, e.measurable_set_preimage.1
+
 /-- A measurable equivalence is a measurable embedding. -/
 protected lemma measurable_embedding (e : α ≃ᵐ β) : measurable_embedding e :=
 { injective := e.injective,
@@ -1277,12 +1328,41 @@ def sum_compl {s : set α} [decidable_pred s] (hs : measurable_set s) : s ⊕ (s
   measurable_to_fun := by {apply measurable.sum_elim; exact measurable_subtype_coe},
   measurable_inv_fun :=  measurable.dite measurable_inl measurable_inr hs }
 
+/-- Convert a measurable involutive function `f` to a measurable permutation with
+`to_fun = inv_fun = f`. See also `function.involutive.to_perm`. -/
+@[simps to_equiv] def of_involutive (f : α → α) (hf : involutive f) (hf' : measurable f) : α ≃ᵐ α :=
+{ measurable_to_fun := hf',
+  measurable_inv_fun := hf',
+  ..hf.to_perm _ }
+
+@[simp] lemma of_involutive_apply (f : α → α) (hf : involutive f) (hf' : measurable f) (a : α) :
+  of_involutive f hf hf' a = f a := rfl
+
+@[simp] lemma of_involutive_symm (f : α → α) (hf : involutive f) (hf' : measurable f) :
+  (of_involutive f hf hf').symm = of_involutive f hf hf' := rfl
+
 end measurable_equiv
 
 namespace measurable_embedding
 
 variables [measurable_space α] [measurable_space β] [measurable_space γ] {f : α → β} {g : β → α}
 
+@[simp] lemma comap_eq (hf : measurable_embedding f) : measurable_space.comap f ‹_› = ‹_› :=
+hf.measurable.comap_le.antisymm $ λ s h,
+  ⟨_, hf.measurable_set_image' h, hf.injective.preimage_image _⟩
+
+lemma iff_comap_eq :
+  measurable_embedding f ↔
+    injective f ∧ measurable_space.comap f ‹_› = ‹_› ∧ measurable_set (range f) :=
+⟨λ hf, ⟨hf.injective, hf.comap_eq, hf.measurable_set_range⟩, λ hf,
+  { injective := hf.1,
+    measurable := by { rw ←hf.2.1, exact comap_measurable f },
+    measurable_set_image' := begin
+      rw ←hf.2.1,
+      rintro _ ⟨s, hs, rfl⟩,
+      simpa only [image_preimage_eq_inter_range] using hs.inter hf.2.2,
+    end }⟩
+
 /-- A set is equivalent to its image under a function `f` as measurable spaces,
   if `f` is a measurable embedding -/
 noncomputable def equiv_image (s : set α) (hf : measurable_embedding f) :
@@ -1377,6 +1457,19 @@ end
 
 end measurable_embedding
 
+lemma measurable_space.comap_compl {m' : measurable_space β} [boolean_algebra β]
+  (h : measurable (compl : β → β)) (f : α → β) :
+  measurable_space.comap (λ a, (f a)ᶜ) infer_instance = measurable_space.comap f infer_instance :=
+begin
+  rw ←measurable_space.comap_comp,
+  congr',
+  exact (measurable_equiv.of_involutive _ compl_involutive h).measurable_embedding.comap_eq,
+end
+
+@[simp] lemma measurable_space.comap_not (p : α → Prop) :
+  measurable_space.comap (λ a, ¬ p a) infer_instance = measurable_space.comap p infer_instance :=
+measurable_space.comap_compl (λ _ _, trivial) _
+
 section countably_generated
 
 namespace measurable_space
diff --git a/src/measure_theory/measurable_space_def.lean b/src/measure_theory/measurable_space_def.lean
index 642af17ecd600..6fb980dffc3f7 100644
--- a/src/measure_theory/measurable_space_def.lean
+++ b/src/measure_theory/measurable_space_def.lean
@@ -196,7 +196,7 @@ by { cases i, exacts [h₂, h₁] }
   measurable_set (disjointed f n) :=
 disjointed_rec (λ t i ht, measurable_set.diff ht $ h _) (h n)
 
-@[simp] lemma measurable_set.const (p : Prop) : measurable_set {a : α | p} :=
+lemma measurable_set.const (p : Prop) : measurable_set {a : α | p} :=
 by { by_cases p; simp [h, measurable_set.empty]; apply measurable_set.univ }
 
 /-- Every set has a measurable superset. Declare this as local instance as needed. -/
@@ -377,10 +377,10 @@ begin
   { exact measurable_set_generate_from ht, },
 end
 
-@[simp] lemma generate_from_singleton_empty : generate_from {∅} = (⊥ : measurable_space α) :=
+lemma generate_from_singleton_empty : generate_from {∅} = (⊥ : measurable_space α) :=
 by { rw [eq_bot_iff, generate_from_le_iff], simp, }
 
-@[simp] lemma generate_from_singleton_univ : generate_from {set.univ} = (⊥ : measurable_space α) :=
+lemma generate_from_singleton_univ : generate_from {set.univ} = (⊥ : measurable_space α) :=
 by { rw [eq_bot_iff, generate_from_le_iff], simp, }
 
 lemma measurable_set_bot_iff {s : set α} : @measurable_set α ⊥ s ↔ (s = ∅ ∨ s = univ) :=
diff --git a/src/measure_theory/order/upper_lower.lean b/src/measure_theory/order/upper_lower.lean
new file mode 100644
index 0000000000000..d6bc49a4cfffa
--- /dev/null
+++ b/src/measure_theory/order/upper_lower.lean
@@ -0,0 +1,131 @@
+/-
+Copyright (c) 2022 Yaël Dillies, Kexing Ying. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, Kexing Ying
+-/
+import analysis.normed.order.upper_lower
+import logic.lemmas
+import measure_theory.covering.besicovitch_vector_space
+
+/-!
+# Order-connected sets are null-measurable
+
+This file proves that order-connected sets in `ℝⁿ` under the pointwise order are null-measurable.
+Recall that `x ≤ y` iff `∀ i, x i ≤ y i`, and `s` is order-connected iff
+`∀ x y ∈ s, ∀ z, x ≤ z → z ≤ y → z ∈ s`.
+
+## Main declarations
+
+* `set.ord_connected.null_frontier`: The frontier of an order-connected set in `ℝⁿ` has measure `0`.
+
+## Notes
+
+We prove null-measurability in `ℝⁿ` with the `∞`-metric, but this transfers directly to `ℝⁿ` with
+the Euclidean metric because they have the same measurable sets.
+
+Null-measurability can't be strengthened to measurability because any antichain (and in particular
+any subset of the antidiagonal `{(x, y) | x + y = 0}`) is order-connected.
+
+## TODO
+
+Generalize so that it also applies to `ℝ × ℝ`, for example.
+-/
+
+open filter measure_theory metric set
+open_locale topology
+
+variables {ι : Type*} [fintype ι] {s : set (ι → ℝ)} {x y : ι → ℝ} {δ : ℝ}
+
+/-- If we can fit a small ball inside a set `s` intersected with any neighborhood of `x`, then the
+density of `s` near `x` is not `0`. Along with `aux₁`, this proves that `x` is a Lebesgue point of
+`s`. This will be used to prove that the frontier of an order-connected set is null. -/
+private lemma aux₀
+  (h : ∀ δ, 0 < δ → ∃ y, closed_ball y (δ/4) ⊆ closed_ball x δ ∧ closed_ball y (δ/4) ⊆ interior s) :
+  ¬ tendsto (λ r, volume (closure s ∩ closed_ball x r) / volume (closed_ball x r)) (𝓝[>] 0)
+    (𝓝 0) :=
+begin
+  choose f hf₀ hf₁ using h,
+  intros H,
+  obtain ⟨ε, hε, hε', hε₀⟩ := exists_seq_strict_anti_tendsto_nhds_within (0 : ℝ),
+  refine not_eventually.2 (frequently_of_forall $ λ _, lt_irrefl $
+    ennreal.of_real $ 4⁻¹ ^ fintype.card ι)
+   ((tendsto.eventually_lt (H.comp hε₀) tendsto_const_nhds _).mono $ λ n, lt_of_le_of_lt _),
+  swap,
+  refine (ennreal.div_le_div_right (volume.mono $ subset_inter
+    ((hf₁ _ $ hε' n).trans interior_subset_closure) $ hf₀ _ $ hε' n) _).trans_eq' _,
+  dsimp,
+  have := hε' n,
+  rw [real.volume_pi_closed_ball, real.volume_pi_closed_ball, ←ennreal.of_real_div_of_pos, ←div_pow,
+    mul_div_mul_left _ _ (two_ne_zero' ℝ), div_right_comm, div_self, one_div],
+  all_goals { positivity },
+end
+
+/-- If we can fit a small ball inside a set `sᶜ` intersected with any neighborhood of `x`, then the
+density of `s` near `x` is not `1`. Along with `aux₀`, this proves that `x` is a Lebesgue point of
+`s`. This will be used to prove that the frontier of an order-connected set is null. -/
+private lemma aux₁
+  (h : ∀ δ, 0 < δ →
+    ∃ y, closed_ball y (δ/4) ⊆ closed_ball x δ ∧ closed_ball y (δ/4) ⊆ interior sᶜ) :
+  ¬ tendsto (λ r, volume (closure s ∩ closed_ball x r) / volume (closed_ball x r)) (𝓝[>] 0)
+    (𝓝 1) :=
+begin
+  choose f hf₀ hf₁ using h,
+  intros H,
+  obtain ⟨ε, hε, hε', hε₀⟩ := exists_seq_strict_anti_tendsto_nhds_within (0 : ℝ),
+  refine not_eventually.2 (frequently_of_forall $ λ _, lt_irrefl $
+    1 - ennreal.of_real (4⁻¹ ^ fintype.card ι))
+    ((tendsto.eventually_lt tendsto_const_nhds (H.comp hε₀) $
+    ennreal.sub_lt_self ennreal.one_ne_top one_ne_zero _).mono $ λ n, lt_of_le_of_lt' _),
+  swap,
+  refine (ennreal.div_le_div_right (volume.mono _) _).trans_eq _,
+  { exact closed_ball x (ε n) \ closed_ball (f (ε n) $ hε' n) (ε n / 4) },
+  { rw diff_eq_compl_inter,
+    refine inter_subset_inter_left _ _,
+    rw [subset_compl_comm, ←interior_compl],
+    exact hf₁ _ _ },
+  dsimp,
+  have := hε' n,
+  rw [measure_diff (hf₀ _ _) _ ((real.volume_pi_closed_ball _ _).trans_ne ennreal.of_real_ne_top),
+    real.volume_pi_closed_ball, real.volume_pi_closed_ball,  ennreal.sub_div (λ _ _, _),
+    ennreal.div_self _ ennreal.of_real_ne_top, ←ennreal.of_real_div_of_pos, ←div_pow,
+    mul_div_mul_left _ _ (two_ne_zero' ℝ), div_right_comm, div_self, one_div],
+  all_goals { positivity <|> measurability },
+end
+
+lemma is_upper_set.null_frontier (hs : is_upper_set s) : volume (frontier s) = 0 :=
+begin
+  refine eq_bot_mono (volume.mono $ λ x hx, _)
+    (besicovitch.ae_tendsto_measure_inter_div_of_measurable_set _ is_closed_closure.measurable_set),
+  { exact s },
+  by_cases x ∈ closure s; simp [h],
+  { exact aux₁ (λ _, hs.compl.exists_subset_ball $ frontier_subset_closure $
+      by rwa frontier_compl) },
+  { exact aux₀ (λ _, hs.exists_subset_ball $ frontier_subset_closure hx) }
+end
+
+lemma is_lower_set.null_frontier (hs : is_lower_set s) : volume (frontier s) = 0 :=
+begin
+  refine eq_bot_mono (volume.mono $ λ x hx, _)
+    (besicovitch.ae_tendsto_measure_inter_div_of_measurable_set _ is_closed_closure.measurable_set),
+  { exact s },
+  by_cases x ∈ closure s; simp [h],
+  { exact aux₁ (λ _, hs.compl.exists_subset_ball $ frontier_subset_closure $
+      by rwa frontier_compl) },
+  { exact aux₀ (λ _, hs.exists_subset_ball $ frontier_subset_closure hx) }
+end
+
+lemma set.ord_connected.null_frontier (hs : s.ord_connected) : volume (frontier s) = 0 :=
+begin
+  rw ← hs.upper_closure_inter_lower_closure,
+  refine le_bot_iff.1 ((volume.mono $ (frontier_inter_subset _ _).trans $ union_subset_union
+    (inter_subset_left _ _) $ inter_subset_right _ _).trans $ (measure_union_le _ _).trans_eq _),
+  rw [(upper_set.upper _).null_frontier, (lower_set.lower _).null_frontier, zero_add, bot_eq_zero],
+end
+
+protected lemma set.ord_connected.null_measurable_set (hs : s.ord_connected) :
+  null_measurable_set s :=
+null_measurable_set_of_null_frontier hs.null_frontier
+
+lemma is_antichain.volume_eq_zero [nonempty ι] (hs : is_antichain (≤) s) : volume s = 0 :=
+le_bot_iff.1 $ (volume.mono $ by { rw [←closure_diff_interior, hs.interior_eq_empty, diff_empty],
+  exact subset_closure }).trans_eq hs.ord_connected.null_frontier
diff --git a/src/number_theory/kummer_dedekind.lean b/src/number_theory/kummer_dedekind.lean
index 28af342219f88..381da69360e7e 100644
--- a/src/number_theory/kummer_dedekind.lean
+++ b/src/number_theory/kummer_dedekind.lean
@@ -294,7 +294,7 @@ begin
   rw [multiset.count_map_eq_count' (λ f,
       ((normalized_factors_map_equiv_normalized_factors_min_poly_mk hI hI' hx hx').symm f
         : ideal S)),
-      multiset.attach_count_eq_count_coe],
+      multiset.count_attach],
   { exact subtype.coe_injective.comp (equiv.injective _) },
   { exact (normalized_factors_map_equiv_normalized_factors_min_poly_mk hI hI' hx hx' _).prop},
   { exact irreducible_of_normalized_factor _
diff --git a/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean b/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean
index 171dcc9523d6f..293f6f86796bb 100644
--- a/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean
+++ b/src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean
@@ -114,13 +114,14 @@ lemma gauss_lemma {p : ℕ} [fact p.prime] {a : ℤ} (hp : p ≠ 2) (ha0 : (a :
     (λ x : ℕ, p / 2 < (a * x : zmod p).val)).card :=
 begin
   haveI hp' : fact (p % 2 = 1) := ⟨nat.prime.mod_two_eq_one_iff_ne_two.mpr hp⟩,
+  haveI : fact (2 < p) := ⟨hp.lt_of_le' (fact.out p.prime).two_le⟩,
   have : (legendre_sym p a : zmod p) = (((-1)^((Ico 1 (p / 2).succ).filter
     (λ x : ℕ, p / 2 < (a * x : zmod p).val)).card : ℤ) : zmod p) :=
     by { rw [legendre_sym.eq_pow, gauss_lemma_aux p ha0]; simp },
   cases legendre_sym.eq_one_or_neg_one p ha0;
   cases neg_one_pow_eq_or ℤ ((Ico 1 (p / 2).succ).filter
     (λ x : ℕ, p / 2 < (a * x : zmod p).val)).card;
-  simp [*, ne_neg_self p one_ne_zero, (ne_neg_self p one_ne_zero).symm] at *
+  simp only [*, neg_one_ne_one, neg_one_ne_one.symm, algebra_map.coe_one, int.cast_neg] at *,
 end
 
 private lemma eisenstein_lemma_aux₁ (p : ℕ) [fact p.prime] [hp2 : fact (p % 2 = 1)]
diff --git a/src/order/bounds/basic.lean b/src/order/bounds/basic.lean
index 6add0bb14d555..ab986bd7f2fd4 100644
--- a/src/order/bounds/basic.lean
+++ b/src/order/bounds/basic.lean
@@ -62,6 +62,8 @@ def is_glb (s : set α) : α → Prop := is_greatest (lower_bounds s)
 
 lemma mem_upper_bounds : a ∈ upper_bounds s ↔ ∀ x ∈ s, x ≤ a := iff.rfl
 lemma mem_lower_bounds : a ∈ lower_bounds s ↔ ∀ x ∈ s, a ≤ x := iff.rfl
+lemma mem_upper_bounds_iff_subset_Iic : a ∈ upper_bounds s ↔ s ⊆ Iic a := iff.rfl
+lemma mem_lower_bounds_iff_subset_Ici : a ∈ lower_bounds s ↔ s ⊆ Ici a := iff.rfl
 
 lemma bdd_above_def : bdd_above s ↔ ∃ x, ∀ y ∈ s, y ≤ x := iff.rfl
 lemma bdd_below_def : bdd_below s ↔ ∃ x, ∀ y ∈ s, x ≤ y := iff.rfl
diff --git a/src/order/filter/pi.lean b/src/order/filter/pi.lean
index d069ed0dcd512..1d9167060ab6f 100644
--- a/src/order/filter/pi.lean
+++ b/src/order/filter/pi.lean
@@ -28,6 +28,7 @@ open_locale classical filter
 namespace filter
 
 variables {ι : Type*} {α : ι → Type*} {f f₁ f₂ : Π i, filter (α i)} {s : Π i, set (α i)}
+  {p : Π i, α i → Prop}
 
 section pi
 
@@ -93,6 +94,14 @@ end
   I.pi s ∈ pi f ↔ ∀ i ∈ I, s i ∈ f i :=
 ⟨λ h i hi, mem_of_pi_mem_pi h hi, pi_mem_pi hI⟩
 
+lemma eventually.eval_pi {i : ι} (hf : ∀ᶠ (x : α i) in f i, p i x) :
+  ∀ᶠ (x : Π (i : ι), α i) in pi f, p i (x i) :=
+(tendsto_eval_pi _ _).eventually hf
+
+lemma eventually_pi [finite ι] (hf : ∀ i, ∀ᶠ x in f i, p i x) :
+  ∀ᶠ (x : Π i, α i) in pi f, ∀ i, p i (x i) :=
+eventually_all.2 $ λ i, (hf _).eval_pi
+
 lemma has_basis_pi {ι' : ι → Type} {s : Π i, ι' i → set (α i)} {p : Π i, ι' i → Prop}
   (h : ∀ i, (f i).has_basis (p i) (s i)) :
   (pi f).has_basis (λ If : set ι × Π i, ι' i, If.1.finite ∧ ∀ i ∈ If.1, p i (If.2 i))
diff --git a/src/probability/independence/basic.lean b/src/probability/independence/basic.lean
index 7223f9b23c01e..03218d5783112 100644
--- a/src/probability/independence/basic.lean
+++ b/src/probability/independence/basic.lean
@@ -64,7 +64,7 @@ when defining `μ` in the example above, the measurable space used is the last o
 Part A, Chapter 4.
 -/
 
-open measure_theory measurable_space
+open measure_theory measurable_space set
 open_locale big_operators measure_theory ennreal
 
 namespace probability_theory
@@ -577,7 +577,8 @@ We prove the following equivalences on `indep_set`, for measurable sets `s, t`.
 * `indep_set s t μ ↔ indep_sets {s} {t} μ`.
 -/
 
-variables {s t : set Ω} (S T : set (set Ω))
+variables {s t : set Ω} (S T : set (set Ω)) {π : ι → set (set Ω)} {f : ι → set Ω}
+  {m0 : measurable_space Ω} {μ : measure Ω}
 
 lemma indep_set_iff_indep_sets_singleton {m0 : measurable_space Ω}
   (hs_meas : measurable_set s) (ht_meas : measurable_set t)
@@ -624,6 +625,40 @@ lemma indep_iff_forall_indep_set (m₁ m₂ : measurable_space Ω) {m0 : measura
   λ h s t hs ht, h s t hs ht s t (measurable_set_generate_from (set.mem_singleton s))
     (measurable_set_generate_from (set.mem_singleton t))⟩
 
+lemma Indep_sets.meas_Inter [fintype ι] (h : Indep_sets π μ) (hf : ∀ i, f i ∈ π i) :
+  μ (⋂ i, f i) = ∏ i, μ (f i) :=
+by simp [← h _ (λ i _, hf _)]
+
+lemma Indep_comap_mem_iff : Indep (λ i, measurable_space.comap (∈ f i) ⊤) μ ↔ Indep_set f μ :=
+by { simp_rw ←generate_from_singleton, refl }
+
+alias Indep_comap_mem_iff ↔ _ Indep_set.Indep_comap_mem
+
+lemma Indep_sets_singleton_iff :
+  Indep_sets (λ i, {f i}) μ ↔ ∀ t, μ (⋂ i ∈ t, f i) = ∏ i in t, μ (f i) :=
+forall_congr $ λ t,
+  ⟨λ h, h $ λ _ _, mem_singleton _,
+  λ h f hf, begin
+    refine eq.trans _ (h.trans $ finset.prod_congr rfl $ λ i hi, congr_arg _ $ (hf i hi).symm),
+    rw Inter₂_congr hf,
+  end⟩
+
+variables [is_probability_measure μ]
+
+lemma Indep_set_iff_Indep_sets_singleton (hf : ∀ i, measurable_set (f i)) :
+  Indep_set f μ ↔ Indep_sets (λ i, {f i}) μ :=
+⟨Indep.Indep_sets $ λ _, rfl, Indep_sets.Indep _
+  (λ i, generate_from_le $ by { rintro t (rfl : t = _), exact hf _}) _
+    (λ _, is_pi_system.singleton _) $ λ _, rfl⟩
+
+lemma Indep_set_iff_measure_Inter_eq_prod (hf : ∀ i, measurable_set (f i)) :
+  Indep_set f μ ↔ ∀ s, μ (⋂ i ∈ s, f i) = ∏ i in s, μ (f i) :=
+(Indep_set_iff_Indep_sets_singleton hf).trans Indep_sets_singleton_iff
+
+lemma Indep_sets.Indep_set_of_mem (hfπ : ∀ i, f i ∈ π i) (hf : ∀ i, measurable_set (f i))
+  (hπ : Indep_sets π μ) : Indep_set f μ :=
+(Indep_set_iff_measure_Inter_eq_prod hf).2 $ λ t, hπ _ $ λ i _, hfπ _
+
 end indep_set
 
 section indep_fun
diff --git a/src/topology/algebra/order/liminf_limsup.lean b/src/topology/algebra/order/liminf_limsup.lean
index c16bae4dda725..74946971a14e3 100644
--- a/src/topology/algebra/order/liminf_limsup.lean
+++ b/src/topology/algebra/order/liminf_limsup.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
+Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov, Yaël Dillies
 -/
 import algebra.big_operators.intervals
 import algebra.big_operators.order
@@ -16,68 +16,152 @@ import topology.order.basic
 
 > THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
 > Any changes to this file require a corresponding PR to mathlib4.
+
+## Main declarations
+
+* `bounded_le_nhds_class`: Typeclass stating that neighborhoods are eventually bounded above.
+* `bounded_ge_nhds_class`: Typeclass stating that neighborhoods are eventually bounded below.
+
+## Implementation notes
+
+The same lemmas are true in `ℝ`, `ℝ × ℝ`, `ι → ℝ`, `euclidean_space ι ℝ`. To avoid code
+duplication, we provide an ad hoc axiomatisation of the properties we need.
 -/
 
 open filter topological_space
 open_locale topology classical
 
 universes u v
-variables {α : Type u} {β : Type v}
+variables {ι α β R S : Type*} {π : ι → Type*}
 
-section liminf_limsup
+/-- Ad hoc typeclass stating that neighborhoods are eventually bounded above. -/
+class bounded_le_nhds_class (α : Type*) [preorder α] [topological_space α] : Prop :=
+(is_bounded_le_nhds (a : α) : (𝓝 a).is_bounded (≤))
+
+/-- Ad hoc typeclass stating that neighborhoods are eventually bounded below. -/
+class bounded_ge_nhds_class (α : Type*) [preorder α] [topological_space α] : Prop :=
+(is_bounded_ge_nhds (a : α) : (𝓝 a).is_bounded (≥))
+
+section preorder
+variables [preorder α] [preorder β] [topological_space α] [topological_space β]
 
-section order_closed_topology
-variables [semilattice_sup α] [topological_space α] [order_topology α]
+section bounded_le_nhds_class
+variables [bounded_le_nhds_class α] [bounded_le_nhds_class β] {f : filter ι} {u : ι → α} {a : α}
 
 lemma is_bounded_le_nhds (a : α) : (𝓝 a).is_bounded (≤) :=
-(is_top_or_exists_gt a).elim (λ h, ⟨a, eventually_of_forall h⟩) (λ ⟨b, hb⟩, ⟨b, ge_mem_nhds hb⟩)
+bounded_le_nhds_class.is_bounded_le_nhds _
 
-lemma filter.tendsto.is_bounded_under_le {f : filter β} {u : β → α} {a : α}
-  (h : tendsto u f (𝓝 a)) : f.is_bounded_under (≤) u :=
+lemma filter.tendsto.is_bounded_under_le (h : tendsto u f (𝓝 a)) :
+  f.is_bounded_under (≤) u :=
 (is_bounded_le_nhds a).mono h
 
-lemma filter.tendsto.bdd_above_range_of_cofinite {u : β → α} {a : α}
+lemma filter.tendsto.bdd_above_range_of_cofinite [is_directed α (≤)]
   (h : tendsto u cofinite (𝓝 a)) : bdd_above (set.range u) :=
 h.is_bounded_under_le.bdd_above_range_of_cofinite
 
-lemma filter.tendsto.bdd_above_range {u : ℕ → α} {a : α}
-  (h : tendsto u at_top (𝓝 a)) : bdd_above (set.range u) :=
+lemma filter.tendsto.bdd_above_range [is_directed α (≤)] {u : ℕ → α} (h : tendsto u at_top (𝓝 a)) :
+  bdd_above (set.range u) :=
 h.is_bounded_under_le.bdd_above_range
 
 lemma is_cobounded_ge_nhds (a : α) : (𝓝 a).is_cobounded (≥) :=
 (is_bounded_le_nhds a).is_cobounded_flip
 
-lemma filter.tendsto.is_cobounded_under_ge {f : filter β} {u : β → α} {a : α}
-  [ne_bot f] (h : tendsto u f (𝓝 a)) : f.is_cobounded_under (≥) u :=
+lemma filter.tendsto.is_cobounded_under_ge [ne_bot f] (h : tendsto u f (𝓝 a)) :
+  f.is_cobounded_under (≥) u :=
 h.is_bounded_under_le.is_cobounded_flip
 
-end order_closed_topology
+instance : bounded_ge_nhds_class αᵒᵈ := ⟨@is_bounded_le_nhds α _ _ _⟩
+
+instance : bounded_le_nhds_class (α × β) :=
+begin
+  refine ⟨λ x, _⟩,
+  obtain ⟨a, ha⟩ := is_bounded_le_nhds x.1,
+  obtain ⟨b, hb⟩ := is_bounded_le_nhds x.2,
+  rw [←@prod.mk.eta _ _ x, nhds_prod_eq],
+  exact ⟨(a, b), ha.prod_mk hb⟩,
+end
+
+instance [finite ι] [Π i, preorder (π i)] [Π i, topological_space (π i)]
+  [Π i, bounded_le_nhds_class (π i)] : bounded_le_nhds_class (Π i, π i) :=
+begin
+  refine ⟨λ x, _⟩,
+  rw nhds_pi,
+  choose f hf using λ i, is_bounded_le_nhds (x i),
+  exact ⟨f, eventually_pi hf⟩,
+end
+
+end bounded_le_nhds_class
 
-section order_closed_topology
-variables [semilattice_inf α] [topological_space α] [order_topology α]
+section bounded_ge_nhds_class
+variables [bounded_ge_nhds_class α] [bounded_ge_nhds_class β] {f : filter ι} {u : ι → α} {a : α}
 
-lemma is_bounded_ge_nhds (a : α) : (𝓝 a).is_bounded (≥) := @is_bounded_le_nhds αᵒᵈ _ _ _ a
+lemma is_bounded_ge_nhds (a : α) : (𝓝 a).is_bounded (≥) :=
+bounded_ge_nhds_class.is_bounded_ge_nhds _
 
-lemma filter.tendsto.is_bounded_under_ge {f : filter β} {u : β → α} {a : α}
-  (h : tendsto u f (𝓝 a)) : f.is_bounded_under (≥) u :=
+lemma filter.tendsto.is_bounded_under_ge (h : tendsto u f (𝓝 a)) :
+  f.is_bounded_under (≥) u :=
 (is_bounded_ge_nhds a).mono h
 
-lemma filter.tendsto.bdd_below_range_of_cofinite {u : β → α} {a : α}
+lemma filter.tendsto.bdd_below_range_of_cofinite [is_directed α (≥)]
   (h : tendsto u cofinite (𝓝 a)) : bdd_below (set.range u) :=
 h.is_bounded_under_ge.bdd_below_range_of_cofinite
 
-lemma filter.tendsto.bdd_below_range {u : ℕ → α} {a : α}
-  (h : tendsto u at_top (𝓝 a)) : bdd_below (set.range u) :=
+lemma filter.tendsto.bdd_below_range [is_directed α (≥)] {u : ℕ → α} (h : tendsto u at_top (𝓝 a)) :
+  bdd_below (set.range u) :=
 h.is_bounded_under_ge.bdd_below_range
 
 lemma is_cobounded_le_nhds (a : α) : (𝓝 a).is_cobounded (≤) :=
 (is_bounded_ge_nhds a).is_cobounded_flip
 
-lemma filter.tendsto.is_cobounded_under_le {f : filter β} {u : β → α} {a : α}
-  [ne_bot f] (h : tendsto u f (𝓝 a)) : f.is_cobounded_under (≤) u :=
+lemma filter.tendsto.is_cobounded_under_le [ne_bot f] (h : tendsto u f (𝓝 a)) :
+  f.is_cobounded_under (≤) u :=
 h.is_bounded_under_ge.is_cobounded_flip
 
-end order_closed_topology
+instance : bounded_le_nhds_class αᵒᵈ := ⟨@is_bounded_ge_nhds α _ _ _⟩
+
+instance : bounded_ge_nhds_class (α × β) :=
+begin
+  refine ⟨λ x, _⟩,
+  obtain ⟨a, ha⟩ := is_bounded_ge_nhds x.1,
+  obtain ⟨b, hb⟩ := is_bounded_ge_nhds x.2,
+  rw [←@prod.mk.eta _ _ x, nhds_prod_eq],
+  exact ⟨(a, b), ha.prod_mk hb⟩,
+end
+
+instance [finite ι] [Π i, preorder (π i)] [Π i, topological_space (π i)]
+  [Π i, bounded_ge_nhds_class (π i)] : bounded_ge_nhds_class (Π i, π i) :=
+begin
+  refine ⟨λ x, _⟩,
+  rw nhds_pi,
+  choose f hf using λ i, is_bounded_ge_nhds (x i),
+  exact ⟨f, eventually_pi hf⟩,
+end
+
+end bounded_ge_nhds_class
+
+@[priority 100] -- See note [lower instance priority]
+instance order_top.to_bounded_le_nhds_class [order_top α] : bounded_le_nhds_class α :=
+⟨λ a, is_bounded_le_of_top⟩
+
+@[priority 100] -- See note [lower instance priority]
+instance order_bot.to_bounded_ge_nhds_class [order_bot α] : bounded_ge_nhds_class α :=
+⟨λ a, is_bounded_ge_of_bot⟩
+
+@[priority 100] -- See note [lower instance priority]
+instance order_topology.to_bounded_le_nhds_class [is_directed α (≤)] [order_topology α] :
+  bounded_le_nhds_class α :=
+⟨λ a, (is_top_or_exists_gt a).elim (λ h, ⟨a, eventually_of_forall h⟩) $ Exists.imp $ λ b,
+  ge_mem_nhds⟩
+
+@[priority 100] -- See note [lower instance priority]
+instance order_topology.to_bounded_ge_nhds_class [is_directed α (≥)] [order_topology α] :
+  bounded_ge_nhds_class α :=
+⟨λ a, (is_bot_or_exists_lt a).elim (λ h, ⟨a, eventually_of_forall h⟩) $ Exists.imp $ λ b,
+  le_mem_nhds⟩
+
+end preorder
+
+section liminf_limsup
 
 section conditionally_complete_linear_order
 variables [conditionally_complete_linear_order α]
@@ -224,7 +308,7 @@ end liminf_limsup
 
 section monotone
 
-variables {ι R S : Type*} {F : filter ι} [ne_bot F]
+variables {F : filter ι} [ne_bot F]
   [complete_linear_order R] [topological_space R] [order_topology R]
   [complete_linear_order S] [topological_space S] [order_topology S]
 
@@ -334,7 +418,7 @@ open_locale topology
 
 open filter set
 
-variables {ι : Type*} {R : Type*} [complete_linear_order R] [topological_space R] [order_topology R]
+variables [complete_linear_order R] [topological_space R] [order_topology R]
 
 lemma infi_eq_of_forall_le_of_tendsto {x : R} {as : ι → R}
   (x_le : ∀ i, x ≤ as i) {F : filter ι} [filter.ne_bot F] (as_lim : filter.tendsto as F (𝓝 x)) :
@@ -349,7 +433,7 @@ lemma supr_eq_of_forall_le_of_tendsto {x : R} {as : ι → R}
   (⨆ i, as i) = x :=
 @infi_eq_of_forall_le_of_tendsto ι (order_dual R) _ _ _ x as le_x F _ as_lim
 
-lemma Union_Ici_eq_Ioi_of_lt_of_tendsto {ι : Type*} (x : R) {as : ι → R} (x_lt : ∀ i, x < as i)
+lemma Union_Ici_eq_Ioi_of_lt_of_tendsto (x : R) {as : ι → R} (x_lt : ∀ i, x < as i)
   {F : filter ι} [filter.ne_bot F] (as_lim : filter.tendsto as F (𝓝 x)) :
   (⋃ (i : ι), Ici (as i)) = Ioi x :=
 begin
@@ -361,10 +445,10 @@ begin
   exact Union_Ici_eq_Ioi_infi obs,
 end
 
-lemma Union_Iic_eq_Iio_of_lt_of_tendsto {ι : Type*} (x : R) {as : ι → R} (lt_x : ∀ i, as i < x)
+lemma Union_Iic_eq_Iio_of_lt_of_tendsto (x : R) {as : ι → R} (lt_x : ∀ i, as i < x)
   {F : filter ι} [filter.ne_bot F] (as_lim : filter.tendsto as F (𝓝 x)) :
   (⋃ (i : ι), Iic (as i)) = Iio x :=
-@Union_Ici_eq_Ioi_of_lt_of_tendsto (order_dual R) _ _ _ ι x as lt_x F _ as_lim
+@Union_Ici_eq_Ioi_of_lt_of_tendsto ι Rᵒᵈ _ _ _ _ _ lt_x F _ as_lim
 
 end infi_and_supr
 
diff --git a/src/topology/algebra/order/upper_lower.lean b/src/topology/algebra/order/upper_lower.lean
index 792ad0b431a15..c1286acac2cdc 100644
--- a/src/topology/algebra/order/upper_lower.lean
+++ b/src/topology/algebra/order/upper_lower.lean
@@ -5,6 +5,7 @@ Authors: Yaël Dillies
 -/
 import algebra.order.upper_lower
 import topology.algebra.group.basic
+import topology.order.basic
 
 /-!
 # Topological facts about upper/lower/order-connected sets
@@ -46,7 +47,33 @@ instance ordered_comm_group.to_has_upper_lower_closure [ordered_comm_group α]
   is_open_upper_closure := λ s hs, by { rw [←mul_one s, ←mul_upper_closure], exact hs.mul_right },
   is_open_lower_closure := λ s hs, by { rw [←mul_one s, ←mul_lower_closure], exact hs.mul_right } }
 
-variables [preorder α] [has_upper_lower_closure α] {s : set α}
+variables [preorder α]
+
+section order_closed_topology
+variables [order_closed_topology α] {s : set α}
+
+@[simp] lemma upper_bounds_closure (s : set α) :
+  upper_bounds (closure s : set α) = upper_bounds s :=
+ext $ λ a, by simp_rw [mem_upper_bounds_iff_subset_Iic, is_closed_Iic.closure_subset_iff]
+
+@[simp] lemma lower_bounds_closure (s : set α) :
+  lower_bounds (closure s : set α) = lower_bounds s :=
+ext $ λ a, by simp_rw [mem_lower_bounds_iff_subset_Ici, is_closed_Ici.closure_subset_iff]
+
+@[simp] lemma bdd_above_closure : bdd_above (closure s) ↔ bdd_above s :=
+by simp_rw [bdd_above, upper_bounds_closure]
+
+@[simp] lemma bdd_below_closure : bdd_below (closure s) ↔ bdd_below s :=
+by simp_rw [bdd_below, lower_bounds_closure]
+
+alias bdd_above_closure ↔ bdd_above.of_closure bdd_above.closure
+alias bdd_below_closure ↔ bdd_below.of_closure bdd_below.closure
+
+attribute [protected] bdd_above.closure bdd_below.closure
+
+end order_closed_topology
+
+variables [has_upper_lower_closure α] {s : set α}
 
 protected lemma is_upper_set.closure : is_upper_set s → is_upper_set (closure s) :=
 has_upper_lower_closure.is_upper_set_closure _
diff --git a/src/topology/metric_space/antilipschitz.lean b/src/topology/metric_space/antilipschitz.lean
index c08fbf9d2ef79..7974ab7cbf9d0 100644
--- a/src/topology/metric_space/antilipschitz.lean
+++ b/src/topology/metric_space/antilipschitz.lean
@@ -192,7 +192,8 @@ namespace antilipschitz_with
 
 open metric
 
-variables [pseudo_metric_space α] [pseudo_metric_space β] {K : ℝ≥0} {f : α → β}
+variables [pseudo_metric_space α] [pseudo_metric_space β] [pseudo_metric_space γ]
+variables {K : ℝ≥0} {f : α → β}
 
 lemma bounded_preimage (hf : antilipschitz_with K f)
   {s : set β} (hs : bounded s) :
@@ -219,6 +220,28 @@ begin
   exact (hf.image_preimage _).symm
 end
 
+lemma bounded_of_image2_left (f : α → β → γ) {K₁ : ℝ≥0}
+  (hf : ∀ b, antilipschitz_with K₁ (λ a, f a b))
+  {s : set α} {t : set β} (hst : bounded (set.image2 f s t)) :
+  bounded s ∨ bounded t :=
+begin
+  contrapose! hst,
+  obtain ⟨b, hb⟩ : t.nonempty := nonempty_of_unbounded hst.2,
+  have : ¬bounded (set.image2 f s {b}),
+  { intro h,
+    apply hst.1,
+    rw set.image2_singleton_right at h,
+    replace h := (hf b).bounded_preimage h,
+    refine h.mono (subset_preimage_image _ _) },
+  exact mt (bounded.mono (image2_subset subset.rfl (singleton_subset_iff.mpr hb))) this,
+end
+
+lemma bounded_of_image2_right {f : α → β → γ} {K₂ : ℝ≥0}
+  (hf : ∀ a, antilipschitz_with K₂ (f a))
+  {s : set α} {t : set β} (hst : bounded (set.image2 f s t)) :
+  bounded s ∨ bounded t :=
+or.symm $ bounded_of_image2_left (flip f) hf $ image2_swap f s t ▸ hst
+
 end antilipschitz_with
 
 lemma lipschitz_with.to_right_inverse [pseudo_emetric_space α] [pseudo_emetric_space β] {K : ℝ≥0}
diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean
index de0baf9a61b0a..76e23c4a7f391 100644
--- a/src/topology/metric_space/basic.lean
+++ b/src/topology/metric_space/basic.lean
@@ -52,7 +52,7 @@ metric, pseudo_metric, dist
 
 open set filter topological_space bornology
 
-open_locale uniformity topology big_operators filter nnreal ennreal
+open_locale uniformity topology big_operators filter nnreal ennreal pointwise
 
 universes u v w
 variables {α : Type u} {β : Type v} {X ι : Type*}
@@ -2171,6 +2171,13 @@ end
 @[simp] lemma bounded_empty : bounded (∅ : set α) :=
 ⟨0, by simp⟩
 
+lemma nonempty_of_unbounded (h : ¬ bounded s) : s.nonempty :=
+begin
+  rw nonempty_iff_ne_empty,
+  rintro rfl,
+  exact h bounded_empty
+end
+
 lemma bounded_iff_mem_bounded : bounded s ↔ ∀ x ∈ s, bounded s :=
 ⟨λ h _ _, h, λ H,
   s.eq_empty_or_nonempty.elim
@@ -2453,6 +2460,8 @@ diam_subsingleton subsingleton_empty
 @[simp] lemma diam_singleton : diam ({x} : set α) = 0 :=
 diam_subsingleton subsingleton_singleton
 
+@[simp, to_additive] lemma diam_one [has_one α] : diam (1 : set α) = 0 := diam_singleton
+
 -- Does not work as a simp-lemma, since {x, y} reduces to (insert y {x})
 lemma diam_pair : diam ({x, y} : set α) = dist x y :=
 by simp only [diam, emetric.diam_pair, dist_edist]
diff --git a/src/topology/metric_space/emetric_space.lean b/src/topology/metric_space/emetric_space.lean
index 983cb4e4990ce..c30cfc396c9a9 100644
--- a/src/topology/metric_space/emetric_space.lean
+++ b/src/topology/metric_space/emetric_space.lean
@@ -32,7 +32,7 @@ to `emetric_space` at the end.
 
 open set filter classical
 
-open_locale uniformity topology big_operators filter nnreal ennreal
+open_locale uniformity topology big_operators filter nnreal ennreal pointwise
 
 universes u v w
 variables {α : Type u} {β : Type v} {X : Type*}
@@ -793,6 +793,8 @@ diam_subsingleton subsingleton_empty
 @[simp] lemma diam_singleton : diam ({x} : set α) = 0 :=
 diam_subsingleton subsingleton_singleton
 
+@[simp, to_additive] lemma diam_one [has_one α] : diam (1 : set α) = 0 := diam_singleton
+
 lemma diam_Union_mem_option {ι : Type*} (o : option ι) (s : ι → set α) :
   diam (⋃ i ∈ o, s i) = ⨆ i ∈ o, diam (s i) :=
 by cases o; simp
diff --git a/src/topology/metric_space/lipschitz.lean b/src/topology/metric_space/lipschitz.lean
index 08d7ec3473268..235c668ff913e 100644
--- a/src/topology/metric_space/lipschitz.lean
+++ b/src/topology/metric_space/lipschitz.lean
@@ -465,6 +465,20 @@ protected lemma comp {g : β → γ} {t : set β} {Kg : ℝ≥0} (hg : lipschitz
   lipschitz_on_with (Kg * K) (g ∘ f) s :=
 lipschitz_on_with_iff_restrict.mpr $ hg.to_restrict.comp (hf.to_restrict_maps_to hmaps)
 
+lemma ediam_image2_le (f : α → β → γ) {K₁ K₂ : ℝ≥0}
+  (s : set α) (t : set β)
+  (hf₁ : ∀ b ∈ t, lipschitz_on_with K₁ (λ a, f a b) s)
+  (hf₂ : ∀ a ∈ s, lipschitz_on_with K₂ (f a) t) :
+  emetric.diam (set.image2 f s t) ≤ ↑K₁ * emetric.diam s + ↑K₂ * emetric.diam t :=
+begin
+  apply emetric.diam_le,
+  rintros _ ⟨a₁, b₁, ha₁, hb₁, rfl⟩ _  ⟨a₂, b₂, ha₂, hb₂, rfl⟩,
+  refine (edist_triangle _ (f a₂ b₁) _).trans _,
+  exact add_le_add
+    ((hf₁ b₁ hb₁ ha₁ ha₂).trans $ ennreal.mul_left_mono $ emetric.edist_le_diam_of_mem ha₁ ha₂)
+    ((hf₂ a₂ ha₂ hb₁ hb₂).trans $ ennreal.mul_left_mono $ emetric.edist_le_diam_of_mem hb₁ hb₂),
+end
+
 end emetric
 
 section metric
@@ -512,6 +526,17 @@ protected lemma iff_le_add_mul {f : α → ℝ} {K : ℝ≥0} :
   lipschitz_on_with K f s ↔ ∀ (x ∈ s) (y ∈ s), f x ≤ f y + K * dist x y :=
 ⟨lipschitz_on_with.le_add_mul, lipschitz_on_with.of_le_add_mul K⟩
 
+lemma bounded_image2 (f : α → β → γ) {K₁ K₂ : ℝ≥0}
+  {s : set α} {t : set β} (hs : metric.bounded s) (ht : metric.bounded t)
+  (hf₁ : ∀ b ∈ t, lipschitz_on_with K₁ (λ a, f a b) s)
+  (hf₂ : ∀ a ∈ s, lipschitz_on_with K₂ (f a) t) :
+  metric.bounded (set.image2 f s t) :=
+metric.bounded_iff_ediam_ne_top.2 $ ne_top_of_le_ne_top
+  (ennreal.add_ne_top.mpr ⟨
+    ennreal.mul_ne_top ennreal.coe_ne_top hs.ediam_ne_top,
+    ennreal.mul_ne_top ennreal.coe_ne_top ht.ediam_ne_top⟩)
+  (ediam_image2_le _ _ _ hf₁ hf₂)
+
 end metric
 
 end lipschitz_on_with