diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean
index 9cfb8c221d..e0d043005d 100644
--- a/LeanCamCombi.lean
+++ b/LeanCamCombi.lean
@@ -6,18 +6,14 @@ import LeanCamCombi.ErdosRenyi.Connectivity
 import LeanCamCombi.ErdosRenyi.GiantComponent
 import LeanCamCombi.ExampleSheets.Graph.ES1
 import LeanCamCombi.ExampleSheets.Graph.ES2
-import LeanCamCombi.FourFunctions
 import LeanCamCombi.KruskalKatona
 import LeanCamCombi.LittlewoodOfford
 import LeanCamCombi.Mathlib.Algebra.Order.Group.Defs
 import LeanCamCombi.Mathlib.Algebra.Order.Monovary
 import LeanCamCombi.Mathlib.Algebra.Order.Ring.Defs
-import LeanCamCombi.Mathlib.Analysis.Convex.Function
 import LeanCamCombi.Mathlib.Analysis.Convex.Mul
-import LeanCamCombi.Mathlib.Analysis.Convex.Strong
 import LeanCamCombi.Mathlib.Combinatorics.Colex
 import LeanCamCombi.Mathlib.Combinatorics.SetFamily.AhlswedeZhang
-import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Shadow
 import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Shatter
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Containment
@@ -26,7 +22,6 @@ import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
 import LeanCamCombi.Mathlib.Data.Finset.Lattice
 import LeanCamCombi.Mathlib.Data.Finset.Pointwise
 import LeanCamCombi.Mathlib.Data.Finset.PosDiffs
-import LeanCamCombi.Mathlib.Data.Finset.Sups
 import LeanCamCombi.Mathlib.Data.Fintype.Basic
 import LeanCamCombi.Mathlib.Data.Nat.Factorization.Basic
 import LeanCamCombi.Mathlib.Data.Nat.Factors
@@ -34,7 +29,6 @@ import LeanCamCombi.Mathlib.Data.Nat.Order.Lemmas
 import LeanCamCombi.Mathlib.Data.Nat.Squarefree
 import LeanCamCombi.Mathlib.Data.Set.Image
 import LeanCamCombi.Mathlib.Data.Set.Prod
-import LeanCamCombi.Mathlib.Data.Sum.Lattice
 import LeanCamCombi.Mathlib.Data.Sym.Sym2
 import LeanCamCombi.Mathlib.GroupTheory.GroupAction.Defs
 import LeanCamCombi.Mathlib.Logic.Basic
@@ -42,15 +36,12 @@ import LeanCamCombi.Mathlib.Logic.Nontrivial.Basic
 import LeanCamCombi.Mathlib.Logic.Relation
 import LeanCamCombi.Mathlib.MeasureTheory.Measure.MeasureSpace
 import LeanCamCombi.Mathlib.NumberTheory.MaricaSchoenheim
-import LeanCamCombi.Mathlib.Order.BooleanAlgebra
 import LeanCamCombi.Mathlib.Order.Category.BoolAlg
 import LeanCamCombi.Mathlib.Order.Disjoint
 import LeanCamCombi.Mathlib.Order.Hom.Lattice
 import LeanCamCombi.Mathlib.Order.Hom.Set
-import LeanCamCombi.Mathlib.Order.RelClasses
 import LeanCamCombi.Mathlib.Order.Sublattice
 import LeanCamCombi.Mathlib.Order.SupClosed
-import LeanCamCombi.Mathlib.Order.Synonym
 import LeanCamCombi.Mathlib.Probability.Independence.Basic
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
 import LeanCamCombi.VanDenBergKesten
diff --git a/LeanCamCombi/FourFunctions.lean b/LeanCamCombi/FourFunctions.lean
deleted file mode 100644
index 460c30c5b8..0000000000
--- a/LeanCamCombi/FourFunctions.lean
+++ /dev/null
@@ -1,356 +0,0 @@
-/-
-Copyright (c) 2023 Yaël Dillies. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yaël Dillies
--/
-import Mathlib.Algebra.BigOperators.Order
-import Mathlib.Algebra.Order.Pi
-import Mathlib.Order.Birkhoff
-import Mathlib.Order.Booleanisation
-import Mathlib.Order.Sublattice
-import Mathlib.Tactic.Ring
-import LeanCamCombi.Mathlib.Data.Finset.Sups
-
-/-!
-# The four functions theorem and corollaries
-
-This file proves the four functions theorem. The statement is that if
-`f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f (a ⊔ b)` for all `a`, `b` in a finite distributive lattice, then
-`(∑ x in s, f₁ x) * (∑ x in t, f₂ x) ≤ (∑ x in s ⊼ t, f₃ x) * (∑ x in s ⊻ t, f₄ x)` where
-`s ⊼ t = {a ⊓ b | a ∈ s, b ∈ t}`, `s ⊻ t = {a ⊔ b | a ∈ s, b ∈ t}`.
-
-The proof uses Birkhoff's representation theorem to restrict to the case where the finite
-distributive lattice is in fact a finite powerset algebra, namely `Finset α` for some finite `α`.
-Then it proves this new statement by induction on the size of `α`.
-
-## Main declarations
-
-The two versions of the four functions theorem are
-* `Finset.four_functions_theorem` for finite powerset algebras.
-* `four_functions_theorem` for any finite distributive lattices.
-
-We deduce a number of corollaries:
-* `Finset.le_card_infs_mul_card_sups`: Daykin inequality. `|s| |t| ≤ |s ⊼ t| |s ⊻ t|`
-* `holley`: Holley inequality.
-* `fkg`: Fortuin-Kastelyn-Ginibre inequality.
-* `Finset.card_le_card_diffs`: Marica-Schönheim inequality. `|s| ≤ |{a \ b | a, b ∈ s}|`
-
-## TODO
-
-Prove that lattices in which `Finset.le_card_infs_mul_card_sups` holds are distributive. See
-Daykin, *A lattice is distributive iff |A| |B| <= |A ∨ B| |A ∧ B|*
-
-Prove the Fishburn-Shepp inequality.
-
-Is `collapse` a construct generally useful for set family inductions? If so, we should move it to an
-earlier file and give it a proper API.
--/
-
-open Finset Fintype
-open scoped BigOperators FinsetFamily
-
-variable {α β : Type*}
-
-section Finset
-variable [DecidableEq α] [LinearOrderedCommSemiring β] [ExistsAddOfLE β] {𝒜 ℬ : Finset (Finset α)}
-  {a : α} {f f₁ f₂ f₃ f₄ g μ : Finset α → β} {s t u : Finset α}
-
-/-- The `n = 1` case of the Ahlswede-Daykin inequality. Note that we can't just expand everything
-out and bound termwise since `c₀ * d₁` appears twice on the RHS of the assumptions while `c₁ * d₀`
-does not appear. -/
-private lemma ineq {a₀ a₁ b₀ b₁ c₀ c₁ d₀ d₁ : β}
-  (ha₀ : 0 ≤ a₀) (ha₁ : 0 ≤ a₁) (hb₀ : 0 ≤ b₀) (hb₁ : 0 ≤ b₁)
-  (hc₀ : 0 ≤ c₀) (hc₁ : 0 ≤ c₁) (hd₀ : 0 ≤ d₀) (hd₁ : 0 ≤ d₁)
-  (h₀₀ : a₀ * b₀ ≤ c₀ * d₀) (h₁₀ : a₁ * b₀ ≤ c₀ * d₁)
-  (h₀₁ : a₀ * b₁ ≤ c₀ * d₁) (h₁₁ : a₁ * b₁ ≤ c₁ * d₁) :
-    (a₀ + a₁) * (b₀ + b₁) ≤ (c₀ + c₁) * (d₀ + d₁) := by
-  calc
-    _ = a₀ * b₀ + (a₀ * b₁ + a₁ * b₀) + a₁ * b₁ := by ring
-    _ ≤ c₀ * d₀ + (c₀ * d₁ + c₁ * d₀) + c₁ * d₁ := add_le_add_three h₀₀ ?_ h₁₁
-    _ = (c₀ + c₁) * (d₀ + d₁) := by ring
-  obtain hcd | hcd := (mul_nonneg hc₀ hd₁).eq_or_gt
-  · rw [hcd] at h₀₁ h₁₀
-    rw [h₀₁.antisymm, h₁₀.antisymm, add_zero] <;> positivity
-  refine' le_of_mul_le_mul_right _ hcd
-  calc (a₀ * b₁ + a₁ * b₀) * (c₀ * d₁)
-      = a₀ * b₁ * (c₀ * d₁) + c₀ * d₁ * (a₁ * b₀) := by ring
-    _ ≤ a₀ * b₁ * (a₁ * b₀) + c₀ * d₁ * (c₀ * d₁) := mul_add_mul_le_mul_add_mul h₀₁ h₁₀
-    _ = a₀ * b₀ * (a₁ * b₁) + c₀ * d₁ * (c₀ * d₁) := by ring
-    _ ≤ c₀ * d₀ * (c₁ * d₁) + c₀ * d₁ * (c₀ * d₁) :=
-        add_le_add_right (mul_le_mul h₀₀ h₁₁ (by positivity) $ by positivity) _
-    _ = (c₀ * d₁ + c₁ * d₀) * (c₀ * d₁) := by ring
-
-private def collapse (𝒜 : Finset (Finset α)) (a : α) (f : Finset α → β) (s : Finset α) : β :=
-  ∑ t in 𝒜.filter λ t ↦ t.erase a = s, f t
-
-private lemma erase_eq_iff (hs : a ∉ s) : t.erase a = s ↔ t = s ∨ t = insert a s := by
-  by_cases ht : a ∈ t <;>
-  · simp [ne_of_mem_of_not_mem', erase_eq_iff_eq_insert, *];
-    aesop
-
-private lemma filter_collapse_eq (ha : a ∉ s) (𝒜 : Finset (Finset α)) :
-    (𝒜.filter λ t ↦ t.erase a = s) =
-      if s ∈ 𝒜 then
-        (if insert a s ∈ 𝒜 then {s, insert a s} else {s})
-      else if
-        insert a s ∈ 𝒜 then {insert a s} else ∅ := by
-  ext t; split_ifs <;> simp [erase_eq_iff ha] <;> aesop
-
-lemma collapse_eq (ha : a ∉ s) (𝒜 : Finset (Finset α)) (f : Finset α → β) :
-    collapse 𝒜 a f s = (if s ∈ 𝒜 then f s else 0) +
-      if insert a s ∈ 𝒜 then f (insert a s) else 0 := by
-  rw [collapse, filter_collapse_eq ha]
-  split_ifs <;> simp [(ne_of_mem_of_not_mem' (mem_insert_self a s) ha).symm, *]
-
-lemma collapse_of_mem (ha : a ∉ s) (ht : t ∈ 𝒜) (hu  : u ∈ 𝒜) (hts : t = s)
-    (hus : u = insert a s) : collapse 𝒜 a f s = f t + f u := by
-  subst hts; subst hus; simp_rw [collapse_eq ha, if_pos ht, if_pos hu]
-
-lemma le_collapse_of_mem (ha : a ∉ s) (hf : 0 ≤ f) (hts : t = s) (ht : t ∈ 𝒜) :
-    f t ≤ collapse 𝒜 a f s := by
-  subst hts
-  rw [collapse_eq ha, if_pos ht]
-  split_ifs
-  · exact le_add_of_nonneg_right $ hf _
-  · rw [add_zero]
-
-lemma le_collapse_of_insert_mem (ha : a ∉ s) (hf : 0 ≤ f) (hts : t = insert a s) (ht : t ∈ 𝒜) :
-    f t ≤ collapse 𝒜 a f s := by
-  rw [collapse_eq ha, ←hts, if_pos ht]
-  split_ifs
-  · exact le_add_of_nonneg_left $ hf _
-  · rw [zero_add]
-
-lemma collapse_nonneg (hf : 0 ≤ f) : 0 ≤ collapse 𝒜 a f := λ _s ↦ sum_nonneg $ λ _t _ ↦ hf _
-
-lemma collapse_modular (hu : a ∉ u) (h₁ : 0 ≤ f₁) (h₂ : 0 ≤ f₂) (h₃ : 0 ≤ f₃) (h₄ : 0 ≤ f₄)
-    (h : ∀ ⦃s⦄, s ⊆ insert a u → ∀ ⦃t⦄, t ⊆ insert a u →  f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t))
-    (𝒜 ℬ : Finset (Finset α)) :
-    ∀ ⦃s⦄, s ⊆ u → ∀ ⦃t⦄, t ⊆ u → collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤
-      collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t) := by
-  rintro s hsu t htu
-  -- Gather a bunch of facts we'll need a lot
-  have := hsu.trans $ subset_insert a _
-  have := htu.trans $ subset_insert a _
-  have := insert_subset_insert a hsu
-  have := insert_subset_insert a htu
-  have has := not_mem_mono hsu hu
-  have hat := not_mem_mono htu hu
-  have : a ∉ s ∩ t := not_mem_mono ((inter_subset_left _ t).trans hsu) hu
-  have := not_mem_union.2 ⟨has, hat⟩
-  rw [collapse_eq has]
-  split_ifs
-  · rw [collapse_eq hat]
-    split_ifs
-    · rw [collapse_of_mem ‹_› (inter_mem_infs ‹_› ‹_›) (inter_mem_infs ‹_› ‹_›) rfl
-        (insert_inter_distrib _ _ _).symm, collapse_of_mem ‹_› (union_mem_sups ‹_› ‹_›)
-        (union_mem_sups ‹_› ‹_›) rfl (insert_union_distrib _ _ _).symm]
-      refine' ineq (h₁ _) (h₁ _) (h₂ _) (h₂ _) (h₃ _) (h₃ _) (h₄ _) (h₄ _) (h ‹_› ‹_›) _ _ _
-      · simpa [*] using h ‹insert a s ⊆ _› ‹t ⊆ _›
-      · simpa [*] using h ‹s ⊆ _› ‹insert a t ⊆ _›
-      · simpa [*] using h ‹insert a s ⊆ _› ‹insert a t ⊆ _›
-    · rw [add_zero, add_mul]
-      refine' (add_le_add (h ‹_› ‹_›) $ h ‹_› ‹_›).trans _
-      rw [collapse_of_mem ‹_› (union_mem_sups ‹_› ‹_›) (union_mem_sups ‹_› ‹_›) rfl
-        (insert_union _ _ _), insert_inter_of_not_mem ‹_›, ←mul_add]
-      exact mul_le_mul_of_nonneg_right (le_collapse_of_mem ‹_› h₃ rfl $ inter_mem_infs ‹_› ‹_›) $
-        add_nonneg (h₄ _) $ h₄ _
-    · rw [zero_add, add_mul]
-      refine' (add_le_add (h ‹_› ‹_›) $ h ‹_› ‹_›).trans _
-      rw [collapse_of_mem ‹_› (inter_mem_infs ‹_› ‹_›) (inter_mem_infs ‹_› ‹_›)
-        (inter_insert_of_not_mem ‹_›) (insert_inter_distrib _ _ _).symm, union_insert,
-        insert_union_distrib, ←add_mul]
-      exact mul_le_mul_of_nonneg_left (le_collapse_of_insert_mem ‹_› h₄
-        (insert_union_distrib _ _ _).symm $ union_mem_sups ‹_› ‹_›) $ add_nonneg (h₃ _) $ h₃ _
-    · rw [add_zero, mul_zero]
-      exact mul_nonneg (collapse_nonneg h₃ _) $ collapse_nonneg h₄ _
-  · rw [add_zero, collapse_eq hat, mul_add]
-    split_ifs
-    · refine' (add_le_add (h ‹_› ‹_›) $ h ‹_› ‹_›).trans _
-      rw [collapse_of_mem ‹_› (union_mem_sups ‹_› ‹_›) (union_mem_sups ‹_› ‹_›) rfl
-        (union_insert _ _ _), inter_insert_of_not_mem ‹_›, ←mul_add]
-      exact mul_le_mul_of_nonneg_right (le_collapse_of_mem ‹_› h₃ rfl $ inter_mem_infs ‹_› ‹_›) $
-        add_nonneg (h₄ _) $ h₄ _
-    · rw [mul_zero, add_zero]
-      exact (h ‹_› ‹_›).trans $ mul_le_mul (le_collapse_of_mem ‹_› h₃ rfl $
-        inter_mem_infs ‹_› ‹_›) (le_collapse_of_mem ‹_› h₄ rfl $ union_mem_sups ‹_› ‹_›)
-        (h₄ _) $ collapse_nonneg h₃ _
-    · rw [mul_zero, zero_add]
-      refine' (h ‹_› ‹_›).trans $ mul_le_mul _ (le_collapse_of_insert_mem ‹_› h₄
-        (union_insert _ _ _) $ union_mem_sups ‹_› ‹_›) (h₄ _) $ collapse_nonneg h₃ _
-      exact le_collapse_of_mem (not_mem_mono (inter_subset_left _ _) ‹_›) h₃
-        (inter_insert_of_not_mem ‹_›) $ inter_mem_infs ‹_› ‹_›
-    · simp_rw [mul_zero, add_zero]
-      exact mul_nonneg (collapse_nonneg h₃ _) $ collapse_nonneg h₄ _
-  · rw [zero_add, collapse_eq hat, mul_add]
-    split_ifs
-    · refine' (add_le_add (h ‹_› ‹_›) $ h ‹_› ‹_›).trans _
-      rw [collapse_of_mem ‹_› (inter_mem_infs ‹_› ‹_›) (inter_mem_infs ‹_› ‹_›)
-        (insert_inter_of_not_mem ‹_›) (insert_inter_distrib _ _ _).symm,
-        insert_inter_of_not_mem ‹_›, ←insert_inter_distrib, insert_union, insert_union_distrib,
-        ←add_mul]
-      exact mul_le_mul_of_nonneg_left (le_collapse_of_insert_mem ‹_› h₄
-        (insert_union_distrib _ _ _).symm $ union_mem_sups ‹_› ‹_›) $ add_nonneg (h₃ _) $ h₃ _
-    · rw [mul_zero, add_zero]
-      refine' (h ‹_› ‹_›).trans $ mul_le_mul (le_collapse_of_mem ‹_› h₃
-        (insert_inter_of_not_mem ‹_›) $ inter_mem_infs ‹_› ‹_›) (le_collapse_of_insert_mem ‹_› h₄
-        (insert_union _ _ _) $ union_mem_sups ‹_› ‹_›) (h₄ _) $ collapse_nonneg h₃ _
-    · rw [mul_zero, zero_add]
-      exact (h ‹_› ‹_›).trans $ mul_le_mul (le_collapse_of_insert_mem ‹_› h₃
-        (insert_inter_distrib _ _ _).symm $ inter_mem_infs ‹_› ‹_›) (le_collapse_of_insert_mem ‹_›
-        h₄ (insert_union_distrib _ _ _).symm $ union_mem_sups ‹_› ‹_›) (h₄ _) $ collapse_nonneg h₃ _
-    · simp_rw [mul_zero, add_zero]
-      exact mul_nonneg (collapse_nonneg h₃ _) $ collapse_nonneg h₄ _
-  · simp_rw [add_zero, zero_mul]
-    exact mul_nonneg (collapse_nonneg h₃ _) $ collapse_nonneg h₄ _
-
-lemma sum_collapse (h𝒜 : 𝒜 ⊆ (insert a u).powerset) (hu : a ∉ u) :
-    ∑ s in u.powerset, collapse 𝒜 a f s = ∑ s in 𝒜, f s := by
-  calc
-    _ = ∑ s in u.powerset ∩ 𝒜, f s + ∑ s in u.powerset.image (insert a) ∩ 𝒜, f s := ?_
-    _ = ∑ s in u.powerset ∩ 𝒜, f s + ∑ s in ((insert a u).powerset \ u.powerset) ∩ 𝒜, f s := ?_
-    _ = ∑ s in 𝒜, f s := ?_
-  · rw [←sum_ite_mem, ←sum_ite_mem, sum_image, ←sum_add_distrib]
-    · exact sum_congr rfl λ s hs ↦ collapse_eq (not_mem_mono (mem_powerset.1 hs) hu) _ _
-    · exact (insert_erase_invOn.2.injOn).mono λ s hs ↦ not_mem_mono (mem_powerset.1 hs) hu
-  · congr with s
-    simp only [mem_image, mem_powerset, mem_sdiff, subset_insert_iff]
-    refine' ⟨_, λ h ↦ ⟨_, h.1, _⟩⟩
-    · rintro ⟨s, hs, rfl⟩
-      exact ⟨subset_insert_iff.1 $ insert_subset_insert _ hs, λ h ↦ hu $ h $ mem_insert_self _ _⟩
-    · rw [insert_erase (erase_ne_self.1 λ hs ↦ ?_)]
-      rw [hs] at h
-      exact h.2 h.1
-  · rw [←sum_union (disjoint_sdiff_self_right.mono inf_le_left inf_le_left), ←inter_distrib_right,
-      union_sdiff_of_subset (powerset_mono.2 $ subset_insert _ _), inter_eq_right.2 h𝒜]
-
-/-- The **Four Functions Theorem** on a powerset algebra. See `four_functions_theorem` for the
-finite distributive lattice generalisation. -/
-protected lemma Finset.four_functions_theorem (u : Finset α)
-    (h₁ : 0 ≤ f₁) (h₂ : 0 ≤ f₂) (h₃ : 0 ≤ f₃) (h₄ : 0 ≤ f₄)
-  (h : ∀ ⦃s⦄, s ⊆ u → ∀ ⦃t⦄, t ⊆ u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t))
-  {𝒜 ℬ : Finset (Finset α)} (h𝒜 : 𝒜 ⊆ u.powerset) (hℬ : ℬ ⊆ u.powerset) :
-    (∑ s in 𝒜, f₁ s) * ∑ s in ℬ, f₂ s ≤ (∑ s in 𝒜 ⊼ ℬ, f₃ s) * ∑ s in 𝒜 ⊻ ℬ, f₄ s := by
-  induction' u using Finset.induction with a u hu ih generalizing f₁ f₂ f₃ f₄ 𝒜 ℬ
-  · simp only [Finset.powerset_empty, Finset.subset_singleton_iff] at h𝒜 hℬ
-    obtain rfl | rfl := h𝒜 <;> obtain rfl | rfl := hℬ <;> simp; exact h subset_rfl subset_rfl
-  specialize ih (collapse_nonneg h₁) (collapse_nonneg h₂) (collapse_nonneg h₃) (collapse_nonneg h₄)
-    (collapse_modular hu h₁ h₂ h₃ h₄ h 𝒜 ℬ) Subset.rfl Subset.rfl
-  have : 𝒜 ⊼ ℬ ⊆ powerset (insert a u) := by simpa using infs_subset h𝒜 hℬ
-  have : 𝒜 ⊻ ℬ ⊆ powerset (insert a u) := by simpa using sups_subset h𝒜 hℬ
-  simpa only [powerset_sups_powerset_self, powerset_infs_powerset_self, sum_collapse, *] using ih
-
-variable (f₁ f₂ f₃ f₄) [Fintype α]
-
-private lemma four_functions_theorem_aux (h₁ : 0 ≤ f₁) (h₂ : 0 ≤ f₂) (h₃ : 0 ≤ f₃) (h₄ : 0 ≤ f₄)
-  (h : ∀ s t, f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)) (𝒜 ℬ : Finset (Finset α)) :
-    (∑ s in 𝒜, f₁ s) * ∑ s in ℬ, f₂ s ≤ (∑ s in 𝒜 ⊼ ℬ, f₃ s) * ∑ s in 𝒜 ⊻ ℬ, f₄ s := by
-    refine' univ.four_functions_theorem h₁ h₂ h₃ h₄ _ _ _ <;> simp [h]
-
-end Finset
-
-section DistribLattice
-variable [DistribLattice α] [DecidableEq α] [LinearOrderedCommSemiring β] [ExistsAddOfLE β]
-  (f f₁ f₂ f₃ f₄ g μ : α → β)
-
-open Function
-
-/-- The **Four Functions Theorem**, aka **Ahlswede-Daykin Inequality**. -/
-lemma four_functions_theorem (h₁ : 0 ≤ f₁) (h₂ : 0 ≤ f₂) (h₃ : 0 ≤ f₃) (h₄ : 0 ≤ f₄)
-    (h : ∀ a b, f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)) (s t : Finset α) :
-    (∑ a in s, f₁ a) * ∑ a in t, f₂ a ≤ (∑ a in s ⊼ t, f₃ a) * ∑ a in s ⊻ t, f₄ a := by
-  classical
-  set L : Sublattice α := ⟨latticeClosure (s ∪ t), isSublattice_latticeClosure.1,
-    isSublattice_latticeClosure.2⟩
-  have : Finite L := (s.finite_toSet.union t.finite_toSet).latticeClosure.to_subtype
-  set s' : Finset L := s.preimage (↑) $ Subtype.coe_injective.injOn _
-  set t' : Finset L := t.preimage (↑) $ Subtype.coe_injective.injOn _
-  have hs' : s'.map ⟨L.subtype, Subtype.coe_injective⟩ = s := by
-    simp [map_eq_image, image_preimage, filter_eq_self]
-    exact λ a ha ↦ subset_latticeClosure $ Set.subset_union_left _ _ ha
-  have ht' : t'.map ⟨L.subtype, Subtype.coe_injective⟩ = t := by
-    simp [map_eq_image, image_preimage, filter_eq_self]
-    exact λ a ha ↦ subset_latticeClosure $ Set.subset_union_right _ _ ha
-  clear_value s' t'
-  obtain ⟨β, _, _, g, hg⟩ := exists_birkhoff_representation L
-  have := four_functions_theorem_aux (extend g (f₁ ∘ (↑)) 0) (extend g (f₂ ∘ (↑)) 0)
-    (extend g (f₃ ∘ (↑)) 0) (extend g (f₄ ∘ (↑)) 0) (extend_nonneg (λ _ ↦ h₁ _) le_rfl)
-    (extend_nonneg (λ _ ↦ h₂ _) le_rfl) (extend_nonneg (λ _ ↦ h₃ _) le_rfl)
-    (extend_nonneg (λ _ ↦ h₄ _) le_rfl) ?_ (s'.map ⟨g, hg⟩) (t'.map ⟨g, hg⟩)
-  simpa only [←hs', ←ht', ←map_sups, ←map_infs, sum_map, Embedding.coeFn_mk, hg.extend_apply]
-    using this
-  rintro s t
-  classical
-  obtain ⟨a, rfl⟩ | hs := em (∃ a, g a = s)
-  · obtain ⟨b, rfl⟩ | ht := em (∃ b, g b = t)
-    · simp_rw [←sup_eq_union, ←inf_eq_inter, ←map_sup, ←map_inf, hg.extend_apply]
-      exact h _ _
-    · simpa [extend_apply' _ _ _ ht] using mul_nonneg
-        (extend_nonneg (λ a : L ↦ h₃ a) le_rfl _) (extend_nonneg (λ a : L ↦ h₄ a) le_rfl _)
-  · simpa [extend_apply' _ _ _ hs] using mul_nonneg
-      (extend_nonneg (λ a : L ↦ h₃ a) le_rfl _) (extend_nonneg (λ a : L ↦ h₄ a) le_rfl _)
-
-/-- An inequality of Daykin. Interestingly, any lattice in which this inequality holds is
-distributive. -/
-lemma Finset.le_card_infs_mul_card_sups (s t : Finset α) :
-    s.card * t.card ≤ (s ⊼ t).card * (s ⊻ t).card := by
-  simpa using four_functions_theorem (1 : α → ℕ) 1 1 1 zero_le_one zero_le_one zero_le_one
-    zero_le_one (λ _ _ ↦ le_rfl) s t
-
-variable [Fintype α]
-
-/-- Special case of the **Four Functions Theorem** when `s = t = univ`. -/
-lemma four_functions_theorem_univ (h₁ : 0 ≤ f₁) (h₂ : 0 ≤ f₂) (h₃ : 0 ≤ f₃) (h₄ : 0 ≤ f₄)
-    (h : ∀ a b, f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)) :
-    (∑ a, f₁ a) * ∑ a, f₂ a ≤ (∑ a, f₃ a) * ∑ a, f₄ a := by
-  simpa using four_functions_theorem f₁ f₂ f₃ f₄ h₁ h₂ h₃ h₄ h univ univ
-
-/-- The **Holley Inequality**. -/
-lemma holley (hμ₀ : 0 ≤ μ) (hf : 0 ≤ f) (hg : 0 ≤ g) (hμ : Monotone μ)
-    (hfg : ∑ a, f a = ∑ a, g a) (h : ∀ a b, f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)) :
-    ∑ a, μ a * f a ≤ ∑ a, μ a * g a := by
-  obtain rfl | hf := hf.eq_or_lt
-  · simp [eq_comm, Fintype.sum_eq_zero_iff_of_nonneg hg] at hfg
-    simp [hfg]
-  obtain rfl | hg := hg.eq_or_lt
-  · simp [Fintype.sum_eq_zero_iff_of_nonneg hf.le] at hfg
-    simp [hfg]
-  have' := four_functions_theorem g (μ * f) f (μ * g) hg.le (mul_nonneg hμ₀ hf.le) hf.le
-    (mul_nonneg hμ₀ hg.le) (λ a b ↦ _) univ univ
-  simpa [hfg, sum_pos hg] using this
-  · simp_rw [Pi.mul_apply, mul_left_comm _ (μ _), mul_comm (g _)]
-    rw [sup_comm, inf_comm]
-    exact mul_le_mul (hμ le_sup_left) (h _ _) (mul_nonneg (hf.le _) $ hg.le _) $ hμ₀ _
-
-/-- The **Fortuin-Kastelyn-Ginibre Inequality**. -/
-lemma fkg (hμ₀ : 0 ≤ μ) (hf₀ : 0 ≤ f) (hg₀ : 0 ≤ g) (hf : Monotone f) (hg : Monotone g)
-    (hμ : ∀ a b, μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)) :
-    (∑ a, μ a * f a) * ∑ a, μ a * g a ≤ (∑ a, μ a) * ∑ a, μ a * (f a * g a) := by
-  refine' four_functions_theorem_univ (μ * f) (μ * g) μ _ (mul_nonneg hμ₀ hf₀) (mul_nonneg hμ₀ hg₀)
-    hμ₀ (mul_nonneg hμ₀ $ mul_nonneg hf₀ hg₀) (λ a b ↦ _)
-  dsimp
-  rw [mul_mul_mul_comm, ←mul_assoc (μ (a ⊓ b))]
-  exact mul_le_mul (hμ _ _) (mul_le_mul (hf le_sup_left) (hg le_sup_right) (hg₀ _) $ hf₀ _)
-    (mul_nonneg (hf₀ _) $ hg₀ _) $ mul_nonneg (hμ₀ _) $ hμ₀ _
-
-end DistribLattice
-
-open Booleanisation
-
-variable [DecidableEq α] [GeneralizedBooleanAlgebra α]
-
-/-- A slight generalisation of the **Marica-Schönheim Inequality**. -/
-lemma Finset.le_card_diffs_mul_card_diffs (s t : Finset α) :
-    s.card * t.card ≤ (s \\ t).card * (t \\ s).card := by
-  have : ∀ s t : Finset α, (s \\ t).map ⟨_, liftLatticeHom_injective⟩ =
-    s.map ⟨_, liftLatticeHom_injective⟩ \\ t.map ⟨_, liftLatticeHom_injective⟩
-  · rintro s t
-    simp_rw [map_eq_image]
-    exact image_image₂_distrib λ a b ↦ rfl
-  simpa [←card_compls (_ ⊻ _), ←map_sup, ←map_inf, ←this] using
-    (s.map ⟨_, liftLatticeHom_injective⟩).le_card_infs_mul_card_sups
-      (t.map ⟨_, liftLatticeHom_injective⟩)ᶜˢ
-
-/-- The **Marica-Schönheim Inequality**. -/
-lemma Finset.card_le_card_diffs (s : Finset α) : s.card ≤ (s \\ s).card :=
-  le_of_pow_le_pow 2 (zero_le _) two_pos $ by simpa [←sq] using s.le_card_diffs_mul_card_diffs s
diff --git a/LeanCamCombi/KruskalKatona.lean b/LeanCamCombi/KruskalKatona.lean
index 88aad439c6..b3d006d063 100644
--- a/LeanCamCombi/KruskalKatona.lean
+++ b/LeanCamCombi/KruskalKatona.lean
@@ -4,14 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Yaël Dillies
 -/
 import Mathlib.Algebra.GeomSum
+import Mathlib.Combinatorics.SetFamily.Compression.UV
 import Mathlib.Combinatorics.SetFamily.Intersecting
+import Mathlib.Combinatorics.SetFamily.Shadow
 import Mathlib.Data.Finset.Fin
 import Mathlib.Data.Finset.Sort
 import Mathlib.Data.Finset.Sups
-import Mathlib.Combinatorics.SetFamily.Compression.UV
 import LeanCamCombi.Mathlib.Combinatorics.Colex
-import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Shadow
-import LeanCamCombi.Mathlib.Order.RelClasses
 
 /-!
 # Kruskal-Katona theorem
diff --git a/LeanCamCombi/Mathlib/Analysis/Convex/Function.lean b/LeanCamCombi/Mathlib/Analysis/Convex/Function.lean
deleted file mode 100644
index 250b71eb3c..0000000000
--- a/LeanCamCombi/Mathlib/Analysis/Convex/Function.lean
+++ /dev/null
@@ -1,35 +0,0 @@
-import Mathlib.Analysis.Convex.Function
-import Mathlib.Order.Filter.Extr
-
-variable {𝕜 E β : Type*}
-
-section LinearOrderedField
-variable [LinearOrderedField 𝕜] [OrderedAddCommMonoid β] [AddCommMonoid E] [SMul 𝕜 E]
-
-section SMul
-variable [SMul 𝕜 β] {s : Set E}
-
-end SMul
-
-section Module
-variable [Module 𝕜 β] [OrderedSMul 𝕜 β] {f : E → β} {s : Set E} {x y : E}
-
-/-- A strictly convex function admits at most one global minimum. -/
-lemma StrictConvexOn.eq_of_isMinOn (hf : StrictConvexOn 𝕜 s f) (hfx : IsMinOn f s x)
-    (hfy : IsMinOn f s y) (hx : x ∈ s) (hy : y ∈ s) : x = y := by
-  by_contra hxy
-  let z := (2 : 𝕜)⁻¹ • x + (2 : 𝕜)⁻¹ • y
-  have hz : z ∈ s := hf.1 hx hy (by norm_num) (by norm_num) $ by norm_num
-  refine lt_irrefl (f z) ?_
-  calc
-    f z < _ := hf.2 hx hy hxy (by norm_num) (by norm_num) $ by norm_num
-    _ ≤ (2 : 𝕜)⁻¹ • f z + (2 : 𝕜)⁻¹ • f z := add_le_add (smul_le_smul_of_nonneg (hfx hz) $ by norm_num) (smul_le_smul_of_nonneg (hfy hz) $ by norm_num)
-    _ = f z := by rw [←_root_.add_smul]; norm_num
-
-/-- A strictly concave function admits at most one global maximum. -/
-lemma StrictConcaveOn.eq_of_isMaxOn (hf : StrictConcaveOn 𝕜 s f) (hfx : IsMaxOn f s x)
-    (hfy : IsMaxOn f s y) (hx : x ∈ s) (hy : y ∈ s) : x = y :=
-  hf.dual.eq_of_isMinOn hfx hfy hx hy
-
-end Module
-end LinearOrderedField
diff --git a/LeanCamCombi/Mathlib/Analysis/Convex/Strong.lean b/LeanCamCombi/Mathlib/Analysis/Convex/Strong.lean
deleted file mode 100644
index 2c6cc1de89..0000000000
--- a/LeanCamCombi/Mathlib/Analysis/Convex/Strong.lean
+++ /dev/null
@@ -1,181 +0,0 @@
-/-
-Copyright (c) 2023 Chenyi Li. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Chenyi Li, Ziyu Wang, Yaël Dillies
--/
-import Mathlib.Analysis.InnerProductSpace.Basic
-import LeanCamCombi.Mathlib.Analysis.Convex.Mul
-
-/-!
-# Uniformly and strongly convex functions
-
-In this file, we define uniformly convex functions and strongly convex functions.
-
-For a real normed space `E`, a uniformly convex function with modulus `φ : ℝ → ℝ` is a function
-`f : E → ℝ` such that `f (t • x + (1 - t) • y) ≤ t • f x + (1 - t) • f y - t * (1 - t) * φ ‖x - y‖`
-for all `t ∈ [0, 1]`.
-
-A `m`-strongly convex function is a uniformly convex function with modulus `fun r ↦ m / 2 * r ^ 2`.
-If `E` is an inner product space, this is equivalent to `x ↦ f x - m / 2 * ‖x‖` being convex.
-
-## TODO
-
-Prove derivative properties of strongly convex functions.
--/
-
-local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y)
-
-open Real
-
-variable {E : Type*} [NormedAddCommGroup E]
-
-section NormedSpace
-variable [NormedSpace ℝ E] {φ ψ : ℝ → ℝ} {s : Set E} {a b m : ℝ} {x y : E} {f g : E → ℝ}
-
-/-- A function `f` from a real normed space is uniformly convex with modulus `φ` if
-`f (t • x + (1 - t) • y) ≤ t • f x + (1 - t) • f y - t * (1 - t) * φ ‖x - y‖` for all `t ∈ [0, 1]`.
-
-`φ` is usually taken to be a monotone function such that `φ r = 0 ↔ r = 0`. -/
-def UniformConvexOn (s : Set E) (φ : ℝ → ℝ) (f : E → ℝ) : Prop :=
-  Convex ℝ s ∧ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 →
-    f (a • x + b • y) ≤ a • f x + b • f y - a * b * φ ‖x - y‖
-
-/-- A function `f` from a real normed space is uniformly concave with modulus `φ` if
-`t • f x + (1 - t) • f y + t * (1 - t) * φ ‖x - y‖ ≤ f (t • x + (1 - t) • y)` for all `t ∈ [0, 1]`.
-
-`φ` is usually taken to be a monotone function such that `φ r = 0 ↔ r = 0`. -/
-def UniformConcaveOn (s : Set E) (φ : ℝ → ℝ) (f : E → ℝ) : Prop :=
-  Convex ℝ s ∧ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 →
-    a • f x + b • f y + a * b * φ ‖x - y‖ ≤ f (a • x + b • y)
-
-@[simp] lemma uniformConvexOn_zero : UniformConvexOn s 0 f ↔ ConvexOn ℝ s f := by
-  simp [UniformConvexOn, ConvexOn]
-
-@[simp] lemma uniformConcaveOn_zero : UniformConcaveOn s 0 f ↔ ConcaveOn ℝ s f := by
-  simp [UniformConcaveOn, ConcaveOn]
-
-protected alias ⟨_, ConvexOn.uniformConvexOn_zero⟩ := uniformConvexOn_zero
-protected alias ⟨_, ConcaveOn.uniformConcaveOn_zero⟩ := uniformConcaveOn_zero
-
-lemma UniformConvexOn.mono (hψφ : ψ ≤ φ) (hf : UniformConvexOn s φ f) : UniformConvexOn s ψ f :=
-  ⟨hf.1, fun x hx y hy a b ha hb hab ↦ (hf.2 hx hy ha hb hab).trans $
-    sub_le_sub_left (mul_le_mul_of_nonneg_left (hψφ _) $ by positivity) _⟩
-
-lemma UniformConcaveOn.mono (hψφ : ψ ≤ φ) (hf : UniformConcaveOn s φ f) : UniformConcaveOn s ψ f :=
-  ⟨hf.1, fun x hx y hy a b ha hb hab ↦ (hf.2 hx hy ha hb hab).trans' $
-    add_le_add_left (mul_le_mul_of_nonneg_left (hψφ _) $ by positivity) _⟩
-
-lemma UniformConvexOn.convexOn (hf : UniformConvexOn s φ f) (hφ : 0 ≤ φ) : ConvexOn ℝ s f := by
-  simpa using hf.mono hφ
-
-lemma UniformConcaveOn.concaveOn (hf : UniformConcaveOn s φ f) (hφ : 0 ≤ φ) : ConcaveOn ℝ s f := by
-  simpa using hf.mono hφ
-
-lemma UniformConvexOn.strictConvexOn (hf : UniformConvexOn s φ f) (hφ : ∀ r, r ≠ 0 → 0 < φ r) :
-    StrictConvexOn ℝ s f := by
-  refine ⟨hf.1, fun x hx y hy hxy a b ha hb hab ↦ (hf.2 hx hy ha.le hb.le hab).trans_lt $
-    sub_lt_self _ ?_⟩
-  rw [←sub_ne_zero, ←norm_pos_iff] at hxy
-  have := hφ _ hxy.ne'
-  positivity
-
-lemma UniformConcaveOn.strictConcaveOn (hf : UniformConcaveOn s φ f) (hφ : ∀ r, r ≠ 0 → 0 < φ r) :
-    StrictConcaveOn ℝ s f := by
-  refine ⟨hf.1, fun x hx y hy hxy a b ha hb hab ↦ (hf.2 hx hy ha.le hb.le hab).trans_lt' $
-    lt_add_of_pos_right _ ?_⟩
-  rw [←sub_ne_zero, ←norm_pos_iff] at hxy
-  have := hφ _ hxy.ne'
-  positivity
-
-lemma UniformConvexOn.add (hf : UniformConvexOn s φ f) (hg : UniformConvexOn s ψ g) :
-    UniformConvexOn s (φ + ψ) (f + g) := by
-  refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ ?_⟩
-  simpa [mul_add, add_add_add_comm, sub_add_sub_comm]
-    using add_le_add (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab)
-
-lemma UniformConcaveOn.add (hf : UniformConcaveOn s φ f) (hg : UniformConcaveOn s ψ g) :
-    UniformConcaveOn s (φ + ψ) (f + g) := by
-  refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ ?_⟩
-  simpa [mul_add, add_add_add_comm] using add_le_add (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab)
-
-lemma UniformConvexOn.neg (hf : UniformConvexOn s φ f) : UniformConcaveOn s φ (-f) := by
-  refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ le_of_neg_le_neg ?_⟩
-  simpa [add_comm, -neg_le_neg_iff, le_sub_iff_add_le'] using hf.2 hx hy ha hb hab
-
-lemma UniformConcaveOn.neg (hf : UniformConcaveOn s φ f) : UniformConvexOn s φ (-f) := by
-  refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ le_of_neg_le_neg ?_⟩
-  simpa [add_comm, -neg_le_neg_iff, ←le_sub_iff_add_le', sub_eq_add_neg, neg_add]
-    using hf.2 hx hy ha hb hab
-
-lemma UniformConvexOn.sub (hf : UniformConvexOn s φ f) (hg : UniformConcaveOn s ψ g) :
-    UniformConvexOn s (φ + ψ) (f - g) := by simpa using hf.add hg.neg
-
-lemma UniformConcaveOn.sub (hf : UniformConcaveOn s φ f) (hg : UniformConvexOn s ψ g) :
-    UniformConcaveOn s (φ + ψ) (f - g) := by simpa using hf.add hg.neg
-
-/-- A function `f` from a real normed space is `m`-strongly convex if
-`f (t • x + (1 - t) • y) ≤ t • f x + (1 - t) • f y - t * (1 - t) * φ ‖x - y‖` for all `t ∈ [0, 1]`.
-
-In an inner product space, this is equivalent to `x ↦ f x - m / 2 * ‖x‖ ^ 2` being convex. -/
-def StrongConvexOn (s : Set E) (m : ℝ) : (E → ℝ) → Prop :=
-  UniformConvexOn s fun r ↦ m / (2 : ℝ) * r ^ 2
-
-/-- A function `f` from a real normed space is `m`-strongly concave if
-`t • f x + (1 - t) • f y + t * (1 - t) * φ ‖x - y‖ ≤ f (t • x + (1 - t) • y)` for all `t ∈ [0, 1]`.
-
-In an inner product space, this is equivalent to `x ↦ f x + m / 2 * ‖x‖ ^ 2` being concave. -/
-def StrongConcaveOn (s : Set E) (m : ℝ) : (E → ℝ) → Prop :=
-  UniformConcaveOn s fun r ↦ m / (2 : ℝ) * r ^ 2
-
-variable {s : Set E} {f : E → ℝ} {m n : ℝ}
-
-nonrec lemma StrongConvexOn.mono (hmn : m ≤ n) (hf : StrongConvexOn s n f) : StrongConvexOn s m f :=
-  hf.mono fun r ↦ mul_le_mul_of_nonneg_right (div_le_div_of_le zero_le_two hmn) $ by positivity
-
-nonrec lemma StrongConcaveOn.mono (hmn : m ≤ n) (hf : StrongConcaveOn s n f) :
-    StrongConcaveOn s m f :=
-  hf.mono fun r ↦ mul_le_mul_of_nonneg_right (div_le_div_of_le zero_le_two hmn) $ by positivity
-
-@[simp] lemma strongConvexOn_zero : StrongConvexOn s 0 f ↔ ConvexOn ℝ s f := by
-  simp [StrongConvexOn, ←Pi.zero_def]
-
-@[simp] lemma strongConcaveOn_zero : StrongConcaveOn s 0 f ↔ ConcaveOn ℝ s f := by
-  simp [StrongConcaveOn, ←Pi.zero_def]
-
-nonrec lemma StrongConvexOn.strictConvexOn (hf : StrongConvexOn s m f) (hm : 0 < m) :
-    StrictConvexOn ℝ s f := hf.strictConvexOn fun r hr ↦ by positivity
-
-nonrec lemma StrongConcaveOn.strictConcaveOn (hf : StrongConcaveOn s m f) (hm : 0 < m) :
-    StrictConcaveOn ℝ s f := hf.strictConcaveOn fun r hr ↦ by positivity
-
-end NormedSpace
-
-section InnerProductSpace
-variable [InnerProductSpace ℝ E] {φ ψ : ℝ → ℝ} {s : Set E} {a b m : ℝ} {x y : E} {f : E → ℝ}
-
-private lemma aux_sub (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
-    a * (f x - m / (2 : ℝ) * ‖x‖ ^ 2) + b * (f y - m / (2 : ℝ) * ‖y‖ ^ 2) +
-      m / (2 : ℝ) * ‖a • x + b • y‖ ^ 2
-      = a * f x + b * f y - m / (2 : ℝ) * a * b * ‖x - y‖ ^ 2 := by
-  rw [norm_add_sq_real, norm_sub_sq_real, norm_smul, norm_smul, real_inner_smul_left,
-    inner_smul_right, norm_of_nonneg ha, norm_of_nonneg hb, mul_pow, mul_pow]
-  obtain rfl := eq_sub_of_add_eq hab
-  ring_nf
-
-private lemma aux_add (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
-    a * (f x + m / (2 : ℝ) * ‖x‖ ^ 2) + b * (f y + m / (2 : ℝ) * ‖y‖ ^ 2) -
-      m / (2 : ℝ) * ‖a • x + b • y‖ ^ 2
-      = a * f x + b * f y + m / (2 : ℝ) * a * b * ‖x - y‖ ^ 2 := by
-  simpa [neg_div] using aux_sub (E := E) (m := -m) ha hb hab
-
-lemma strongConvexOn_iff_convex :
-    StrongConvexOn s m f ↔ ConvexOn ℝ s fun x ↦ f x - m / (2 : ℝ) * ‖x‖ ^ 2 := by
-  refine and_congr_right fun _ ↦ forall₄_congr fun x _ y _ ↦ forall₅_congr fun a b ha hb hab ↦ ?_
-  simp_rw [sub_le_iff_le_add, smul_eq_mul, aux_sub ha hb hab, mul_assoc, mul_left_comm]
-
-lemma strongConcaveOn_iff_convex :
-    StrongConcaveOn s m f ↔ ConcaveOn ℝ s fun x ↦ f x + m / (2 : ℝ) * ‖x‖ ^ 2 := by
-  refine and_congr_right fun _ ↦ forall₄_congr fun x _ y _ ↦ forall₅_congr fun a b ha hb hab ↦ ?_
-  simp_rw [←sub_le_iff_le_add, smul_eq_mul, aux_add ha hb hab, mul_assoc, mul_left_comm]
-
-end InnerProductSpace
diff --git a/LeanCamCombi/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean b/LeanCamCombi/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
index 7b9aa0ea1e..f07f92f765 100644
--- a/LeanCamCombi/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
+++ b/LeanCamCombi/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
@@ -5,10 +5,10 @@ Authors: Yaël Dillies, Vladimir Ivanov
 -/
 import Mathlib.Algebra.BigOperators.Order
 import Mathlib.Algebra.BigOperators.Ring
+import Mathlib.Data.Finset.Sups
 import Mathlib.Order.Hom.Lattice
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.Ring
-import LeanCamCombi.Mathlib.Data.Finset.Sups
 
 /-!
 # The Ahlswede-Zhang identity
diff --git a/LeanCamCombi/Mathlib/Combinatorics/SetFamily/Shadow.lean b/LeanCamCombi/Mathlib/Combinatorics/SetFamily/Shadow.lean
deleted file mode 100644
index d4f07a33da..0000000000
--- a/LeanCamCombi/Mathlib/Combinatorics/SetFamily/Shadow.lean
+++ /dev/null
@@ -1,54 +0,0 @@
-import Mathlib.Combinatorics.SetFamily.Shadow
-
-open Nat
-open scoped FinsetFamily
-
-namespace Finset
-variable {α : Type*} [DecidableEq α] {𝒜 : Finset (Finset α)} {s t : Finset α} {r k : ℕ}
-
-@[simp] lemma shadow_iterate_empty (k : ℕ) : ∂^[k] (∅ : Finset (Finset α)) = ∅ := by
-  induction' k <;> simp [*, shadow_empty]
-
-/-- `t ∈ ∂𝒜` iff `t` is exactly one element less than something from `𝒜` -/
-lemma mem_shadow_iff_exists_sdiff : t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ (s \ t).card = 1 := by
-  simp_rw [mem_shadow_iff_insert_mem, card_eq_one]
-  constructor
-  · rintro ⟨i, hi, ht⟩
-    exact ⟨insert i t, ht, subset_insert _ _, i, insert_sdiff_cancel hi⟩
-  · rintro ⟨s, hs, hts, a, ha⟩
-    refine' ⟨a, (mem_sdiff.1 $ (ext_iff.1 ha _).2 $ mem_singleton_self _).2, _⟩
-    rwa [insert_eq, ←ha, sdiff_union_of_subset hts]
-
-/-- `t ∈ ∂^k 𝒜` iff `t` is exactly `k` elements less than something from `𝒜`. -/
-lemma mem_shadow_iterate_iff_exists_sdiff {𝒜 : Finset (Finset α)} {t : Finset α} (k : ℕ) :
-    t ∈ ∂^[k] 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ (s \ t).card = k := by
-  induction' k with k ih generalizing 𝒜 t
-  · simp only [sdiff_eq_empty_iff_subset, Function.iterate_zero, id.def, card_eq_zero, exists_prop]
-    refine' ⟨fun p ↦ ⟨t, p, Subset.rfl, Subset.rfl⟩, _⟩
-    rintro ⟨s, hs, hst, hts⟩
-    rwa [subset_antisymm hst hts]
-  simp only [exists_prop, Function.comp_apply, Function.iterate_succ, ih,
-    mem_shadow_iff_insert_mem]
-  clear ih
-  constructor
-  · rintro ⟨s, ⟨a, ha, hs⟩, hts, rfl⟩
-    refine' ⟨_, hs, hts.trans $ subset_insert _ _, _⟩
-    rw [insert_sdiff_of_not_mem _ $ not_mem_mono hts ha,
-      card_insert_of_not_mem $ not_mem_mono (sdiff_subset _ _) ha]
-  · rintro ⟨s, hs, hts, hk⟩
-    obtain ⟨a, ha⟩ : (s \ t).Nonempty := by rw [←card_pos, hk]; exact Nat.succ_pos _
-    refine' ⟨erase s a, ⟨a, not_mem_erase _ _, _⟩, subset_erase.2 ⟨hts, (mem_sdiff.1 ha).2⟩, _⟩
-    · rwa [insert_erase (mem_sdiff.1 ha).1]
-    · rw [erase_sdiff_comm, card_erase_of_mem ha, hk, succ_sub_one]
-
-/-- Everything in the `k`-th shadow is `k` smaller than things in the original. -/
-lemma _root_.Set.Sized.shadow_iterate (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
-    (∂^[k] 𝒜 : Set (Finset α)).Sized (r - k) := by
-  simp_rw [Set.Sized, mem_coe, mem_shadow_iterate_iff_exists_sdiff]
-  rintro t ⟨s, hs, hts, rfl⟩
-  rw [card_sdiff hts, ←h𝒜 hs, Nat.sub_sub_self (card_le_of_subset hts)]
-
--- TODO: Fix `_root_` misport
-alias _root_.Set.Sized.shadow := Set.Sized.shadow
-
-end Finset
diff --git a/LeanCamCombi/Mathlib/Data/Finset/Sups.lean b/LeanCamCombi/Mathlib/Data/Finset/Sups.lean
deleted file mode 100644
index f18aab08e4..0000000000
--- a/LeanCamCombi/Mathlib/Data/Finset/Sups.lean
+++ /dev/null
@@ -1,71 +0,0 @@
-import Mathlib.Data.Finset.Slice
-import Mathlib.Data.Finset.Sups
-
-/-!
-# Set family operations
-
-This file defines a few binary operations on `Finset α` for use in set family combinatorics.
-
-## Main declarations
-
-* `Finset.diffs`: Finset of elements of the form `a \ b` where `a ∈ s`, `b ∈ t`.
-* `Finset.compls`: Finset of elements of the form `aᶜ` where `a ∈ s`.
-
-## Notation
-
-We define the following notation in locale `FinsetFamily`:
-* `s \\ t` for `Finset.diffs`
-* `sᶜˢ` for `Finset.compls`
-
-## References
-
-[B. Bollobás, *Combinatorics*][bollobas1986]
--/
-
--- TODO: Is there a better spot for those two instances? Why are they not already inferred from
--- `instDecidablePredMemUpperClosure`, `instDecidablePredMemLowerClosure`?
-namespace Finset
-variable {α : Type*} [Preorder α] [@DecidableRel α (· ≤ ·)] {s : Finset α}
-
-instance decidablePredMemUpperClosure : DecidablePred (· ∈ upperClosure (s : Set α)) :=
-  fun _ ↦ decidableExistsAndFinset
-#align finset.decidable_pred_mem_upper_closure Finset.decidablePredMemUpperClosure
-
-instance decidablePredMemLowerClosure : DecidablePred (· ∈ lowerClosure (s : Set α)) :=
-  fun _ ↦ decidableExistsAndFinset
-#align finset.decidable_pred_mem_lower_closure Finset.decidablePredMemLowerClosure
-
-end Finset
-
-open Fintype Function
-open scoped FinsetFamily
-
-variable {F α β : Type*} [DecidableEq α] [DecidableEq β]
-
-namespace Finset
-section SemilatticeSup
-variable [Fintype α] [SemilatticeSup α] [SemilatticeSup β] [SupHomClass F α β] {s : Finset α}
-
-@[simp] lemma univ_sups_univ : (univ : Finset α) ⊻ univ = univ := top_le_iff.1 subset_sups_self
-
-end SemilatticeSup
-
-section SemilatticeInf
-variable [Fintype α] [SemilatticeInf α] [SemilatticeInf β] [InfHomClass F α β] {s : Finset α}
-
-@[simp] lemma univ_infs_univ : (univ : Finset α) ⊼ univ = univ := top_le_iff.1 subset_infs_self
-
-end SemilatticeInf
-
-variable [DecidableEq α] {𝒜 ℬ : Finset (Finset α)} {s t : Finset α} {a : α}
-
-@[simp] lemma powerset_sups_powerset_self (s : Finset α) :
-    s.powerset ⊻ s.powerset = s.powerset := by simp [←powerset_union]
-
-@[simp] lemma powerset_infs_powerset_self (s : Finset α) :
-    s.powerset ⊼ s.powerset = s.powerset := by simp [←powerset_inter]
-
-lemma union_mem_sups : s ∈ 𝒜 → t ∈ ℬ → s ∪ t ∈ 𝒜 ⊻ ℬ := sup_mem_sups
-lemma inter_mem_infs : s ∈ 𝒜 → t ∈ ℬ → s ∩ t ∈ 𝒜 ⊼ ℬ := inf_mem_infs
-
-end Finset
diff --git a/LeanCamCombi/Mathlib/Data/Sum/Lattice.lean b/LeanCamCombi/Mathlib/Data/Sum/Lattice.lean
deleted file mode 100644
index 7c6ce34236..0000000000
--- a/LeanCamCombi/Mathlib/Data/Sum/Lattice.lean
+++ /dev/null
@@ -1,102 +0,0 @@
-import Mathlib.Data.Sum.Order
-import Mathlib.Order.Hom.Lattice
-import LeanCamCombi.Mathlib.Order.Synonym
-
-open OrderDual
-
-namespace Sum.Lex
-variable {α β : Type*}
-
-section SemilatticeSup
-variable [SemilatticeSup α] [SemilatticeSup β]
-
--- The linter significantly hinders readability here.
-set_option linter.unusedVariables false in
-instance instSemilatticeSup : SemilatticeSup (α ⊕ₗ β) where
-  sup x y := match x, y with
-    | inlₗ a₁, inlₗ a₂ => inl (a₁ ⊔ a₂)
-    | inlₗ a₁, inrₗ b₂ => inr b₂
-    | inrₗ b₁, inlₗ a₂ => inr b₁
-    | inrₗ b₁, inrₗ b₂ => inr (b₁ ⊔ b₂)
-  le_sup_left x y := match x, y with
-    | inlₗ a₁, inlₗ a₂ => inl_le_inl_iff.2 le_sup_left
-    | inlₗ a₁, inrₗ b₂ => inl_le_inr _ _
-    | inrₗ b₁, inlₗ a₂ => le_rfl
-    | inrₗ b₁, inrₗ b₂ => inr_le_inr_iff.2 le_sup_left
-  le_sup_right x y := match x, y with
-    | inlₗ a₁, inlₗ a₂ => inl_le_inl_iff.2 le_sup_right
-    | inlₗ a₁, inrₗ b₂ => le_rfl
-    | inrₗ b₁, inlₗ a₂ => inl_le_inr _ _
-    | inrₗ b₁, inrₗ b₂ => inr_le_inr_iff.2 le_sup_right
-  sup_le x y z hxz hyz := match x, y, z, hxz, hyz with
-    | inlₗ a₁, inlₗ a₂, inlₗ a₃, Lex.inl h₁₃, Lex.inl h₂₃ => inl_le_inl_iff.2 $ sup_le h₁₃ h₂₃
-    | inlₗ a₁, inlₗ a₂, inrₗ b₃, Lex.sep _ _, Lex.sep _ _ => Lex.sep _ _
-    | inlₗ a₁, inrₗ b₂, inrₗ b₃, Lex.sep _ _, Lex.inr h₂₃ => inr_le_inr_iff.2 h₂₃
-    | inrₗ b₁, inlₗ a₂, inrₗ b₃, Lex.inr h₁₃, Lex.sep _ _ => inr_le_inr_iff.2 h₁₃
-    | inrₗ b₁, inrₗ b₂, inrₗ b₃, Lex.inr h₁₃, Lex.inr h₂₃ => inr_le_inr_iff.2 $ sup_le h₁₃ h₂₃
-
-@[simp] lemma inl_sup (a₁ a₂ : α) : (inlₗ (a₁ ⊔ a₂) : α ⊕ β) = inlₗ a₁ ⊔ inlₗ a₂ := rfl
-@[simp] lemma inr_sup (b₁ b₂ : β) : (inrₗ (b₁ ⊔ b₂) : α ⊕ β) = inrₗ b₁ ⊔ inrₗ b₂ := rfl
-
-end SemilatticeSup
-
-section SemilatticeInf
-variable [SemilatticeInf α] [SemilatticeInf β]
-
--- The linter significantly hinders readability here.
-set_option linter.unusedVariables false in
-instance instSemilatticeInf : SemilatticeInf (α ⊕ₗ β) where
-  inf x y := match x, y with
-    | inlₗ a₁, inlₗ a₂ => inl (a₁ ⊓ a₂)
-    | inlₗ a₁, inrₗ b₂ => inl a₁
-    | inrₗ b₁, inlₗ a₂ => inl a₂
-    | inrₗ b₁, inrₗ b₂ => inr (b₁ ⊓ b₂)
-  inf_le_left x y := match x, y with
-    | inlₗ a₁, inlₗ a₂ => inl_le_inl_iff.2 inf_le_left
-    | inlₗ a₁, inrₗ b₂ => le_rfl
-    | inrₗ b₁, inlₗ a₂ => inl_le_inr _ _
-    | inrₗ b₁, inrₗ b₂ => inr_le_inr_iff.2 inf_le_left
-  inf_le_right x y := match x, y with
-    | inlₗ a₁, inlₗ a₂ => inl_le_inl_iff.2 inf_le_right
-    | inlₗ a₁, inrₗ b₂ => inl_le_inr _ _
-    | inrₗ b₁, inlₗ a₂ => le_rfl
-    | inrₗ b₁, inrₗ b₂ => inr_le_inr_iff.2 inf_le_right
-  le_inf x y z hzx hzy := match x, y, z, hzx, hzy with
-    | inlₗ a₁, inlₗ a₂, inlₗ a₃, Lex.inl h₁₃, Lex.inl h₂₃ => inl_le_inl_iff.2 $ le_inf h₁₃ h₂₃
-    | inlₗ a₁, inlₗ a₂, inrₗ b₃, Lex.inl h₁₃, Lex.sep _ _ => inl_le_inl_iff.2 h₁₃
-    | inlₗ a₁, inrₗ b₂, inlₗ a₃, Lex.sep _ _, Lex.inl h₂₃ => inl_le_inl_iff.2 h₂₃
-    | inlₗ a₁, inrₗ b₂, inrₗ b₃, Lex.sep _ _, Lex.sep _ _ => Lex.sep _ _
-    | inrₗ b₁, inrₗ b₂, inrₗ b₃, Lex.inr h₁₃, Lex.inr h₂₃ => inr_le_inr_iff.2 $ le_inf h₁₃ h₂₃
-
-@[simp] lemma inl_inf (a₁ a₂ : α) : (inlₗ (a₁ ⊓ a₂) : α ⊕ β) = inlₗ a₁ ⊓ inlₗ a₂ := rfl
-@[simp] lemma inr_inf (b₁ b₂ : β) : (inrₗ (b₁ ⊓ b₂) : α ⊕ β) = inrₗ b₁ ⊓ inrₗ b₂ := rfl
-
-end SemilatticeInf
-
-section Lattice
-variable [Lattice α] [Lattice β]
-
-instance instLattice : Lattice (α ⊕ₗ β) := { instSemilatticeSup, instSemilatticeInf with }
-
-/-- `Sum.Lex.inlₗ` as a lattice homomorphism. -/
-def inlLatticeHom : LatticeHom α (α ⊕ₗ β) where
-  toFun := inlₗ
-  map_sup' _ _ := rfl
-  map_inf' _ _ := rfl
-
-/-- `Sum.Lex.inrₗ` as a lattice homomorphism. -/
-def inrLatticeHom : LatticeHom β (α ⊕ₗ β) where
-  toFun := inrₗ
-  map_sup' _ _ := rfl
-  map_inf' _ _ := rfl
-
-end Lattice
-
-instance instDistribLattice [DistribLattice α] [DistribLattice β] : DistribLattice (α ⊕ₗ β) where
-  le_sup_inf := by
-    simp only [Lex.forall, Sum.forall, ge_iff_le, inl_le_inl_iff, inr_le_inr_iff, sup_le_iff,
-      le_sup_left, true_and, inl_le_inr, not_inr_le_inl, le_inf_iff, sup_of_le_right, and_self,
-      inf_of_le_left, le_refl, implies_true, and_true, inf_of_le_right, sup_of_le_left, ←inl_sup,
-      ←inr_sup, ←inl_inf, ←inr_inf, sup_inf_left, le_rfl]
-
-end Sum.Lex
diff --git a/LeanCamCombi/Mathlib/NumberTheory/MaricaSchoenheim.lean b/LeanCamCombi/Mathlib/NumberTheory/MaricaSchoenheim.lean
index e2aebf5188..f08b09ead0 100644
--- a/LeanCamCombi/Mathlib/NumberTheory/MaricaSchoenheim.lean
+++ b/LeanCamCombi/Mathlib/NumberTheory/MaricaSchoenheim.lean
@@ -1,5 +1,5 @@
+import Mathlib.Combinatorics.SetFamily.FourFunctions
 import LeanCamCombi.Mathlib.Data.Nat.Squarefree
-import LeanCamCombi.FourFunctions
 
 open Finset
 open scoped BigOperators FinsetFamily
diff --git a/LeanCamCombi/Mathlib/Order/BooleanAlgebra.lean b/LeanCamCombi/Mathlib/Order/BooleanAlgebra.lean
deleted file mode 100644
index 6341ba95c6..0000000000
--- a/LeanCamCombi/Mathlib/Order/BooleanAlgebra.lean
+++ /dev/null
@@ -1,10 +0,0 @@
-import Mathlib.Order.BooleanAlgebra
-
-namespace Prod
-variable {α β : Type*} [GeneralizedBooleanAlgebra α] [GeneralizedBooleanAlgebra β]
-
-instance instGeneralizedBooleanAlgebra : GeneralizedBooleanAlgebra (α × β) where
-  sup_inf_sdiff _ _ := ext (sup_inf_sdiff _ _) (sup_inf_sdiff _ _)
-  inf_inf_sdiff _ _ := ext (inf_inf_sdiff _ _) (inf_inf_sdiff _ _)
-
-end Prod
diff --git a/LeanCamCombi/Mathlib/Order/RelClasses.lean b/LeanCamCombi/Mathlib/Order/RelClasses.lean
deleted file mode 100644
index dd3f9995a0..0000000000
--- a/LeanCamCombi/Mathlib/Order/RelClasses.lean
+++ /dev/null
@@ -1,6 +0,0 @@
-import Mathlib.Order.RelClasses
-
-variable {α : Type*} [Preorder α]
-
-lemma wellFounded_lt [WellFoundedLT α] : @WellFounded α (· < ·) := IsWellFounded.wf
-lemma wellFounded_gt [WellFoundedGT α] : @WellFounded α (· > ·) := IsWellFounded.wf
diff --git a/LeanCamCombi/Mathlib/Order/Synonym.lean b/LeanCamCombi/Mathlib/Order/Synonym.lean
deleted file mode 100644
index 8c518900bf..0000000000
--- a/LeanCamCombi/Mathlib/Order/Synonym.lean
+++ /dev/null
@@ -1,9 +0,0 @@
-import Mathlib.Order.Synonym
-
-namespace Lex
-variable {α : Type*}
-
-@[simp] lemma «forall» {p : Lex α → Prop} : (∀ a, p a) ↔ ∀ a, p (toLex a) := Iff.rfl
-@[simp] lemma «exists» {p : Lex α → Prop} : (∃ a, p a) ↔ ∃ a, p (toLex a) := Iff.rfl
-
-end Lex
diff --git a/lake-manifest.json b/lake-manifest.json
index 6669e34051..8999ff07f8 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "41442e1fb9b35c5ded0e2e43b51ac14f576801ae",
+    "rev": "874ff0574c19582d3d275d1c803846549cd53dce",
     "opts": {},
     "name": "mathlib",
     "inputRev?": null,
@@ -20,7 +20,7 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "a71c160b1934814837d37f377efaf2964e55c433",
+    "rev": "9bfbd2a12ee9cf2e159a8a6b4d1ef6c149728f66",
     "opts": {},
     "name": "std",
     "inputRev?": "main",
@@ -28,26 +28,18 @@
   {"git":
    {"url": "https://github.com/leanprover-community/quote4",
     "subDir?": null,
-    "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
+    "rev": "396201245bf244f9d78e9007a02dd1c388193d27",
     "opts": {},
     "name": "Qq",
     "inputRev?": "master",
     "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/aesop",
-    "subDir?": null,
-    "rev": "ed733adcb79e54e157fafb805ce3518d4411ab70",
-    "opts": {},
-    "name": "aesop",
-    "inputRev?": "master",
-    "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover/lean4-cli",
     "subDir?": null,
-    "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
+    "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
     "opts": {},
     "name": "Cli",
-    "inputRev?": "nightly",
+    "inputRev?": "main",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover-community/ProofWidgets4",
@@ -57,6 +49,14 @@
     "name": "proofwidgets",
     "inputRev?": "v0.0.21",
     "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/aesop",
+    "subDir?": null,
+    "rev": "cb87803274405db79ec578fc07c4730c093efb90",
+    "opts": {},
+    "name": "aesop",
+    "inputRev?": "master",
+    "inherited": true}},
   {"git":
    {"url": "https://github.com/xubaiw/CMark.lean",
     "subDir?": null,