From 68d8c1cf52670f0c10938f4b3fc1143e0da01394 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Thu, 3 Aug 2023 14:13:27 +0000
Subject: [PATCH 01/15] feat: Extending convex functions Match
 https://github.com/leanprover-community/mathlib/pull/18797

---
 Mathlib/Algebra/Order/Module.lean             | 15 ++-
 Mathlib/Algebra/Order/Monoid/Lemmas.lean      | 23 ++++-
 Mathlib/Algebra/Order/SMul.lean               | 20 +++-
 Mathlib/Analysis/Convex/ProjIcc.lean          | 99 +++++++++++++++++++
 Mathlib/Data/Set/Intervals/Basic.lean         | 29 +++++-
 .../Data/Set/Intervals/UnorderedInterval.lean | 30 +++++-
 Mathlib/Order/Lattice.lean                    | 55 ++++++++++-
 7 files changed, 262 insertions(+), 9 deletions(-)
 create mode 100644 Mathlib/Analysis/Convex/ProjIcc.lean

diff --git a/Mathlib/Algebra/Order/Module.lean b/Mathlib/Algebra/Order/Module.lean
index c62f18aedb850..7fdd4fb34f4a5 100644
--- a/Mathlib/Algebra/Order/Module.lean
+++ b/Mathlib/Algebra/Order/Module.lean
@@ -5,7 +5,7 @@ Authors: Frédéric Dupuis, Yaël Dillies
 -/
 import Mathlib.Algebra.Order.SMul
 
-#align_import algebra.order.module from "leanprover-community/mathlib"@"9003f28797c0664a49e4179487267c494477d853"
+#align_import algebra.order.module from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
 
 /-!
 # Ordered module
@@ -217,6 +217,19 @@ theorem BddAbove.smul_of_nonpos (hc : c ≤ 0) (hs : BddAbove s) : BddBelow (c 
 
 end OrderedRing
 
+section LinearOrderedRing
+variable [LinearOrderedRing k] [LinearOrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : k}
+
+theorem smul_max_of_nonpos (ha : a ≤ 0) (b₁ b₂ : M) : a • max b₁ b₂ = min (a • b₁) (a • b₂) :=
+  (antitone_smul_left ha : Antitone (_ : M → M)).map_max
+#align smul_max_of_nonpos smul_max_of_nonpos
+
+theorem smul_min_of_nonpos (ha : a ≤ 0) (b₁ b₂ : M) : a • min b₁ b₂ = max (a • b₁) (a • b₂) :=
+  (antitone_smul_left ha : Antitone (_ : M → M)).map_min
+#align smul_min_of_nonpos smul_min_of_nonpos
+
+end LinearOrderedRing
+
 section LinearOrderedField
 
 variable [LinearOrderedField k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {s : Set M}
diff --git a/Mathlib/Algebra/Order/Monoid/Lemmas.lean b/Mathlib/Algebra/Order/Monoid/Lemmas.lean
index 0441c0ac3f9d8..a2d4abfcb5f02 100644
--- a/Mathlib/Algebra/Order/Monoid/Lemmas.lean
+++ b/Mathlib/Algebra/Order/Monoid/Lemmas.lean
@@ -8,7 +8,7 @@ import Mathlib.Algebra.CovariantAndContravariant
 import Mathlib.Init.Data.Ordering.Basic
 import Mathlib.Order.MinMax
 
-#align_import algebra.order.monoid.lemmas from "leanprover-community/mathlib"@"2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c"
+#align_import algebra.order.monoid.lemmas from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
 
 /-!
 # Ordered monoids
@@ -314,6 +314,27 @@ by simp_rw [min_le_iff, le_max_iff]; contrapose! h; exact mul_lt_mul_of_lt_of_lt
 #align min_le_max_of_add_le_add min_le_max_of_add_le_add
 #align min_le_max_of_mul_le_mul min_le_max_of_mul_le_mul
 
+end LinearOrder
+
+section LinearOrder
+variable [LinearOrder α] [CovariantClass α α (· * ·) (· ≤ ·)]
+  [CovariantClass α α (swap (· * ·)) (· ≤ ·)] {a b c d : α}
+
+@[to_additive max_add_add_le_max_add_max]
+theorem max_mul_mul_le_max_mul_max' : max (a * b) (c * d) ≤ max a c * max b d :=
+  max_le (mul_le_mul' (le_max_left _ _) <| le_max_left _ _) <|
+    mul_le_mul' (le_max_right _ _) <| le_max_right _ _
+#align max_mul_mul_le_max_mul_max' max_mul_mul_le_max_mul_max'
+#align max_add_add_le_max_add_max max_add_add_le_max_add_max
+
+--TODO: Also missing `min_mul_min_le_min_mul_mul`
+@[to_additive min_add_min_le_min_add_add]
+theorem min_mul_min_le_min_mul_mul' : min a c * min b d ≤ min (a * b) (c * d) :=
+  le_min (mul_le_mul' (min_le_left _ _) <| min_le_left _ _) <|
+    mul_le_mul' (min_le_right _ _) <| min_le_right _ _
+#align min_mul_min_le_min_mul_mul' min_mul_min_le_min_mul_mul'
+#align min_add_min_le_min_add_add min_add_min_le_min_add_add
+
 end LinearOrder
 end Mul
 
diff --git a/Mathlib/Algebra/Order/SMul.lean b/Mathlib/Algebra/Order/SMul.lean
index be03aa5077e36..b1836347ab44f 100644
--- a/Mathlib/Algebra/Order/SMul.lean
+++ b/Mathlib/Algebra/Order/SMul.lean
@@ -11,7 +11,7 @@ import Mathlib.Data.Set.Pointwise.SMul
 import Mathlib.Tactic.GCongr.Core
 import Mathlib.Tactic.Positivity
 
-#align_import algebra.order.smul from "leanprover-community/mathlib"@"9003f28797c0664a49e4179487267c494477d853"
+#align_import algebra.order.smul from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
 
 /-!
 # Ordered scalar product
@@ -185,12 +185,26 @@ instance Int.orderedSMul [LinearOrderedAddCommGroup M] : OrderedSMul ℤ M :=
     · cases (Int.negSucc_not_pos _).1 hn
 #align int.ordered_smul Int.orderedSMul
 
+section LinearOrderedSemiring
+variable [LinearOrderedSemiring R] [LinearOrderedAddCommMonoid M] [SMulWithZero R M]
+  [OrderedSMul R M] {a : R}
+
+
 -- TODO: `LinearOrderedField M → OrderedSMul ℚ M`
-instance LinearOrderedSemiring.toOrderedSMul {R : Type _} [LinearOrderedSemiring R] :
-    OrderedSMul R R :=
+instance LinearOrderedSemiring.toOrderedSMul : OrderedSMul R R :=
   OrderedSMul.mk'' fun _ => strictMono_mul_left_of_pos
 #align linear_ordered_semiring.to_ordered_smul LinearOrderedSemiring.toOrderedSMul
 
+theorem smul_max (ha : 0 ≤ a) (b₁ b₂ : M) : a • max b₁ b₂ = max (a • b₁) (a • b₂) :=
+  (monotone_smul_left ha : Monotone (_ : M → M)).map_max
+#align smul_max smul_max
+
+theorem smul_min (ha : 0 ≤ a) (b₁ b₂ : M) : a • min b₁ b₂ = min (a • b₁) (a • b₂) :=
+  (monotone_smul_left ha : Monotone (_ : M → M)).map_min
+#align smul_min smul_min
+
+end LinearOrderedSemiring
+
 section LinearOrderedSemifield
 
 variable [LinearOrderedSemifield 𝕜] [OrderedAddCommMonoid M] [OrderedAddCommMonoid N]
diff --git a/Mathlib/Analysis/Convex/ProjIcc.lean b/Mathlib/Analysis/Convex/ProjIcc.lean
new file mode 100644
index 0000000000000..3214ed3254c2c
--- /dev/null
+++ b/Mathlib/Analysis/Convex/ProjIcc.lean
@@ -0,0 +1,99 @@
+/-
+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.Analysis.Convex.Function
+import Mathlib.Data.Set.Intervals.ProjIcc
+
+#align_import analysis.convex.proj_Icc from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
+
+/-!
+# Convexity of extension from intervals
+
+This file proves that constantly extending monotone/antitone functions preserves their convexity.
+
+## TODO
+
+We could deduplicate the proofs if we had a typeclass stating that `segment 𝕜 x y = [x -[𝕜] y]` as
+`𝕜ᵒᵈ` respects it if `𝕜` does, while `𝕜ᵒᵈ` isn't a `LinearOrderedField` if `𝕜` is.
+-/
+
+open Set
+
+variable {𝕜 β : Type _} [LinearOrderedField 𝕜] [LinearOrderedAddCommMonoid β] [SMul 𝕜 β] {s : Set 𝕜}
+  {f : 𝕜 → β} {z : 𝕜}
+
+/-- A convex set extended towards minus infinity is convex. -/
+protected theorem Convex.IciExtend (hf : Convex 𝕜 s) :
+    Convex 𝕜 {x | IciExtend (restrict (Ici z) (· ∈ s)) x} := by
+  rw [convex_iff_ordConnected] at hf ⊢; exact hf.restrict.Ici_extend
+#align convex.Ici_extend Convex.IciExtend
+
+/-- A convex set extended towards infinity is convex. -/
+protected theorem Convex.IicExtend (hf : Convex 𝕜 s) :
+    Convex 𝕜 {x | IicExtend (restrict (Iic z) (· ∈ s)) x} := by
+  rw [convex_iff_ordConnected] at hf ⊢; exact hf.restrict.Iic_extend
+#align convex.Iic_extend Convex.IicExtend
+
+/-- A convex monotone function extended constantly towards minus infinity is convex. -/
+protected theorem ConvexOn.IciExtend (hf : ConvexOn 𝕜 s f) (hf' : MonotoneOn f s) :
+    ConvexOn 𝕜 {x | IciExtend (restrict (Ici z) (· ∈ s)) x} (IciExtend $ restrict (Ici z) f) := by
+  refine' ⟨hf.1.IciExtend, λ x hx y hy a b ha hb hab ↦ _⟩
+  dsimp [Ici_extend_apply] at hx hy ⊢
+  refine' (hf' (hf.1.OrdConnected.uIcc_subset hx hy $ (Monotone.image_uIcc_subset λ _ _ ↦
+    max_le_max le_rfl) $ mem_image_of_mem _ $ convex_uIcc _ _
+    left_mem_uIcc right_mem_uIcc ha hb hab) (hf.1 hx hy ha hb hab) _).trans (hf.2 hx hy ha hb hab)
+  rw [smul_max ha z, smul_max hb z]
+  refine' le_trans _ max_add_add_le_max_add_max
+  rw [Convex.combo_self hab, smul_eq_mul, smul_eq_mul]
+#align convex_on.Ici_extend ConvexOn.IciExtend
+
+/-- A convex antitone function extended constantly towards infinity is convex. -/
+protected theorem ConvexOn.IicExtend (hf : ConvexOn 𝕜 s f) (hf' : AntitoneOn f s) :
+    ConvexOn 𝕜 {x | IicExtend (restrict (Iic z) (· ∈ s)) x} (IicExtend $ restrict (Iic z) f) := by
+  refine' ⟨hf.1.IicExtend, λ x hx y hy a b ha hb hab ↦ _⟩
+  dsimp [Iic_extend_apply] at hx hy ⊢
+  refine' (hf' (hf.1 hx hy ha hb hab) (hf.1.OrdConnected.uIcc_subset hx hy $
+    (Monotone.image_uIcc_subset λ _ _ ↦ min_le_min le_rfl) $ mem_image_of_mem _ $ convex_uIcc _ _
+    left_mem_uIcc right_mem_uIcc ha hb hab) _).trans (hf.2 hx hy ha hb hab)
+  rw [smul_min ha z, smul_min hb z]
+  refine' min_add_min_le_min_add_add.trans _
+  rw [Convex.combo_self hab, smul_eq_mul, smul_eq_mul]
+#align convex_on.Iic_extend ConvexOn.IicExtend
+
+/-- A concave antitone function extended constantly minus towards infinity is concave. -/
+protected theorem ConcaveOn.IciExtend (hf : ConcaveOn 𝕜 s f) (hf' : AntitoneOn f s) :
+    ConcaveOn 𝕜 {x | IciExtend (restrict (Ici z) (· ∈ s)) x} (IciExtend $ restrict (Ici z) f) :=
+  hf.dual.IciExtend hf'.dual_right
+#align concave_on.Ici_extend ConcaveOn.IciExtend
+
+/-- A concave monotone function extended constantly towards infinity is concave. -/
+protected theorem ConcaveOn.IicExtend (hf : ConcaveOn 𝕜 s f) (hf' : MonotoneOn f s) :
+    ConcaveOn 𝕜 {x | IicExtend (restrict (Iic z) (· ∈ s)) x} (IicExtend $ restrict (Iic z) f) :=
+  hf.dual.IicExtend hf'.dual_right
+#align concave_on.Iic_extend ConcaveOn.IicExtend
+
+/-- A convex monotone function extended constantly towards minus infinity is convex. -/
+protected theorem ConvexOn.IciExtend_of_monotone (hf : ConvexOn 𝕜 univ f) (hf' : Monotone f) :
+    ConvexOn 𝕜 univ (IciExtend $ restrict (Ici z) f) :=
+  hf.IciExtend $ hf'.MonotoneOn _
+#align convex_on.Ici_extend_of_monotone ConvexOn.IciExtend_of_monotone
+
+/-- A convex antitone function extended constantly towards infinity is convex. -/
+protected theorem ConvexOn.IicExtend_of_antitone (hf : ConvexOn 𝕜 univ f) (hf' : Antitone f) :
+    ConvexOn 𝕜 univ (IicExtend $ restrict (Iic z) f) :=
+  hf.IicExtend $ hf'.AntitoneOn _
+#align convex_on.Iic_extend_of_antitone ConvexOn.IicExtend_of_antitone
+
+/-- A concave antitone function extended constantly minus towards infinity is concave. -/
+protected theorem ConcaveOn.IciExtend_of_antitone (hf : ConcaveOn 𝕜 univ f) (hf' : Antitone f) :
+    ConcaveOn 𝕜 univ (IciExtend $ restrict (Ici z) f) :=
+  hf.IciExtend $ hf'.AntitoneOn _
+#align concave_on.Ici_extend_of_antitone ConcaveOn.IciExtend_of_antitone
+
+/-- A concave monotone function extended constantly towards infinity is concave. -/
+protected theorem ConcaveOn.IicExtend_of_monotone (hf : ConcaveOn 𝕜 univ f) (hf' : Monotone f) :
+    ConcaveOn 𝕜 univ (IicExtend $ restrict (Iic z) f) :=
+  hf.IicExtend $ hf'.MonotoneOn _
+#align concave_on.Iic_extend_of_monotone ConcaveOn.IicExtend_of_monotone
diff --git a/Mathlib/Data/Set/Intervals/Basic.lean b/Mathlib/Data/Set/Intervals/Basic.lean
index b1eee30952cad..d4e285800a49e 100644
--- a/Mathlib/Data/Set/Intervals/Basic.lean
+++ b/Mathlib/Data/Set/Intervals/Basic.lean
@@ -6,7 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot, Yury Kudryashov, Rémy
 import Mathlib.Order.MinMax
 import Mathlib.Data.Set.Prod
 
-#align_import data.set.intervals.basic from "leanprover-community/mathlib"@"4367b192b58a665b6f18773f73eb492eb4df7990"
+#align_import data.set.intervals.basic from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
 
 /-!
 # Intervals
@@ -1719,6 +1719,33 @@ theorem Ioo_union_Ioo (h₁ : min a b < max c d) (h₂ : min c d < max a b) :
       le_of_lt h₂, le_of_lt h₁]
 #align set.Ioo_union_Ioo Set.Ioo_union_Ioo
 
+section Lattice
+variable [Lattice β] {f : α → β}
+
+theorem _root_.MonotoneOn.image_Icc_subset (hf : MonotoneOn f (Icc a b)) :
+    f '' Icc a b ⊆ Icc (f a) (f b) :=
+  image_subset_iff.2 fun c hc =>
+    ⟨hf (left_mem_Icc.2 <| hc.1.trans hc.2) hc hc.1,
+      hf hc (right_mem_Icc.2 <| hc.1.trans hc.2) hc.2⟩
+#align monotone_on.image_Icc_subset MonotoneOn.image_Icc_subset
+
+theorem _root_.AntitoneOn.image_Icc_subset (hf : AntitoneOn f (Icc a b)) :
+    f '' Icc a b ⊆ Icc (f b) (f a) :=
+  image_subset_iff.2 fun c hc =>
+    ⟨hf hc (right_mem_Icc.2 <| hc.1.trans hc.2) hc.2,
+      hf (left_mem_Icc.2 <| hc.1.trans hc.2) hc hc.1⟩
+#align antitone_on.image_Icc_subset AntitoneOn.image_Icc_subset
+
+theorem _root_.Monotone.image_Icc_subset (hf : Monotone f) : f '' Icc a b ⊆ Icc (f a) (f b) :=
+  (hf.monotoneOn _).image_Icc_subset
+#align monotone.image_Icc_subset Monotone.image_Icc_subset
+
+theorem _root_.Antitone.image_Icc_subset (hf : Antitone f) : f '' Icc a b ⊆ Icc (f b) (f a) :=
+  (hf.antitoneOn _).image_Icc_subset
+#align antitone.image_Icc_subset Antitone.image_Icc_subset
+
+end Lattice
+
 end LinearOrder
 
 section Lattice
diff --git a/Mathlib/Data/Set/Intervals/UnorderedInterval.lean b/Mathlib/Data/Set/Intervals/UnorderedInterval.lean
index f8d5d15ae21b1..aa1e5735a3443 100644
--- a/Mathlib/Data/Set/Intervals/UnorderedInterval.lean
+++ b/Mathlib/Data/Set/Intervals/UnorderedInterval.lean
@@ -6,7 +6,7 @@ Authors: Zhouhang Zhou
 import Mathlib.Order.Bounds.Basic
 import Mathlib.Data.Set.Intervals.Basic
 
-#align_import data.set.intervals.unordered_interval from "leanprover-community/mathlib"@"4020ddee5b4580a409bfda7d2f42726ce86ae674"
+#align_import data.set.intervals.unordered_interval from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
 
 /-!
 # Intervals without endpoints ordering
@@ -179,8 +179,34 @@ lemma uIcc_injective_left (a : α) : Injective (uIcc a) := by
 end DistribLattice
 
 section LinearOrder
+variable [LinearOrder α]
 
-variable [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} {a a₁ a₂ b b₁ b₂ c x : α}
+section Lattice
+variable [Lattice β] {f : α → β} {s : Set α} {a b : α}
+
+theorem _root_.MonotoneOn.image_uIcc_subset (hf : MonotoneOn f (uIcc a b)) :
+    f '' uIcc a b ⊆ uIcc (f a) (f b) :=
+  hf.image_Icc_subset.trans <| by
+    rw [hf.map_sup left_mem_uIcc right_mem_uIcc, hf.map_inf left_mem_uIcc right_mem_uIcc, uIcc]
+#align monotone_on.image_uIcc_subset MonotoneOn.image_uIcc_subset
+
+theorem _root_.AntitoneOn.image_uIcc_subset (hf : AntitoneOn f (uIcc a b)) :
+    f '' uIcc a b ⊆ uIcc (f a) (f b) :=
+  hf.image_Icc_subset.trans <| by
+    rw [hf.map_sup left_mem_uIcc right_mem_uIcc, hf.map_inf left_mem_uIcc right_mem_uIcc, uIcc]
+#align antitone_on.image_uIcc_subset AntitoneOn.image_uIcc_subset
+
+theorem _root_.Monotone.image_uIcc_subset (hf : Monotone f) : f '' uIcc a b ⊆ uIcc (f a) (f b) :=
+  (hf.monotoneOn _).image_uIcc_subset
+#align monotone.image_uIcc_subset Monotone.image_uIcc_subset
+
+theorem _root_.Antitone.image_uIcc_subset (hf : Antitone f) : f '' uIcc a b ⊆ uIcc (f a) (f b) :=
+  (hf.antitoneOn _).image_uIcc_subset
+#align antitone.image_uIcc_subset Antitone.image_uIcc_subset
+
+end Lattice
+
+variable [LinearOrder β] {f : α → β} {s : Set α} {a a₁ a₂ b b₁ b₂ c d x : α}
 
 theorem Icc_min_max : Icc (min a b) (max a b) = [[a, b]] :=
   rfl
diff --git a/Mathlib/Order/Lattice.lean b/Mathlib/Order/Lattice.lean
index b219932616314..7655f079b0149 100644
--- a/Mathlib/Order/Lattice.lean
+++ b/Mathlib/Order/Lattice.lean
@@ -9,7 +9,7 @@ import Mathlib.Order.Monotone.Basic
 import Mathlib.Order.ULift
 import Mathlib.Tactic.GCongr.Core
 
-#align_import order.lattice from "leanprover-community/mathlib"@"e4bc74cbaf429d706cb9140902f7ca6c431e75a4"
+#align_import order.lattice from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
 
 /-!
 # (Semi-)lattices
@@ -1135,6 +1135,7 @@ theorem map_inf [SemilatticeInf β] {f : α → β} (hf : Monotone f) (x y : α)
 end Monotone
 
 namespace MonotoneOn
+variable {f : α → β} {s : Set α} {x y : α}
 
 /-- Pointwise supremum of two monotone functions is a monotone function. -/
 protected theorem sup [Preorder α] [SemilatticeSup β] {f g : α → β} {s : Set α}
@@ -1160,6 +1161,32 @@ protected theorem min [Preorder α] [LinearOrder β] {f g : α → β} {s : Set
   hf.inf hg
 #align monotone_on.min MonotoneOn.min
 
+theorem of_map_inf [SemilatticeInf α] [SemilatticeInf β]
+    (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊓ y) = f x ⊓ f y) : MonotoneOn f s := fun x hx y hy hxy =>
+  inf_eq_left.1 <| by rw [← h _ hx _ hy, inf_eq_left.2 hxy]
+#align monotone_on.of_map_inf MonotoneOn.of_map_inf
+
+theorem of_map_sup [SemilatticeSup α] [SemilatticeSup β]
+    (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊔ y) = f x ⊔ f y) : MonotoneOn f s :=
+  (@of_map_inf αᵒᵈ βᵒᵈ _ _ _ _ h).dual
+#align monotone_on.of_map_sup MonotoneOn.of_map_sup
+
+variable [LinearOrder α]
+
+theorem map_sup [SemilatticeSup β] (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y ∈ s) :
+    f (x ⊔ y) = f x ⊔ f y := by
+  cases le_total x y <;> have := hf ?_ ?_ ‹_› <;>
+    first
+    | assumption
+    | simp only [*, sup_of_le_left, sup_of_le_right]
+
+#align monotone_on.map_sup MonotoneOn.map_sup
+
+theorem map_inf [SemilatticeInf β] (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y ∈ s) :
+    f (x ⊓ y) = f x ⊓ f y :=
+  hf.dual.map_sup hx hy
+#align monotone_on.map_inf MonotoneOn.map_inf
+
 end MonotoneOn
 
 namespace Antitone
@@ -1215,6 +1242,7 @@ theorem map_inf [SemilatticeSup β] {f : α → β} (hf : Antitone f) (x y : α)
 end Antitone
 
 namespace AntitoneOn
+variable {f : α → β} {s : Set α} {x y : α}
 
 /-- Pointwise supremum of two antitone functions is an antitone function. -/
 protected theorem sup [Preorder α] [SemilatticeSup β] {f g : α → β} {s : Set α}
@@ -1240,6 +1268,31 @@ protected theorem min [Preorder α] [LinearOrder β] {f g : α → β} {s : Set
   hf.inf hg
 #align antitone_on.min AntitoneOn.min
 
+theorem of_map_inf [SemilatticeInf α] [SemilatticeSup β]
+    (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊓ y) = f x ⊔ f y) : AntitoneOn f s := fun x hx y hy hxy =>
+  sup_eq_left.1 <| by rw [← h _ hx _ hy, inf_eq_left.2 hxy]
+#align antitone_on.of_map_inf AntitoneOn.of_map_inf
+
+theorem of_map_sup [SemilatticeSup α] [SemilatticeInf β]
+    (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊔ y) = f x ⊓ f y) : AntitoneOn f s :=
+  (@of_map_inf αᵒᵈ βᵒᵈ _ _ _ _ h).dual
+#align antitone_on.of_map_sup AntitoneOn.of_map_sup
+
+variable [LinearOrder α]
+
+theorem map_sup [SemilatticeInf β] (hf : AntitoneOn f s) (hx : x ∈ s) (hy : y ∈ s) :
+    f (x ⊔ y) = f x ⊓ f y := by
+  cases le_total x y <;> have := hf ?_ ?_ ‹_› <;>
+    first
+    | assumption
+    | simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]
+#align antitone_on.map_sup AntitoneOn.map_sup
+
+theorem map_inf [SemilatticeSup β] (hf : AntitoneOn f s) (hx : x ∈ s) (hy : y ∈ s) :
+    f (x ⊓ y) = f x ⊔ f y :=
+  hf.dual.map_sup hx hy
+#align antitone_on.map_inf AntitoneOn.map_inf
+
 end AntitoneOn
 
 /-!

From 89c37669f39c68b4893b66d0d63617c7863048d7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Tue, 29 Aug 2023 09:58:14 +0000
Subject: [PATCH 02/15] fix

---
 Mathlib.lean                          | 1 +
 Mathlib/Data/Set/Intervals/Basic.lean | 4 ++--
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 3a882982519f9..37356e575ea42 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -641,6 +641,7 @@ import Mathlib.Analysis.Convex.KreinMilman
 import Mathlib.Analysis.Convex.Measure
 import Mathlib.Analysis.Convex.Normed
 import Mathlib.Analysis.Convex.PartitionOfUnity
+import Mathlib.Analysis.Convex.ProjIcc
 import Mathlib.Analysis.Convex.Quasiconvex
 import Mathlib.Analysis.Convex.Segment
 import Mathlib.Analysis.Convex.Side
diff --git a/Mathlib/Data/Set/Intervals/Basic.lean b/Mathlib/Data/Set/Intervals/Basic.lean
index e34eb9fc97f60..115e603ceb01a 100644
--- a/Mathlib/Data/Set/Intervals/Basic.lean
+++ b/Mathlib/Data/Set/Intervals/Basic.lean
@@ -1724,14 +1724,14 @@ variable [Lattice β] {f : α → β}
 
 theorem _root_.MonotoneOn.image_Icc_subset (hf : MonotoneOn f (Icc a b)) :
     f '' Icc a b ⊆ Icc (f a) (f b) :=
-  image_subset_iff.2 fun c hc =>
+  image_subset_iff.2 fun _c hc =>
     ⟨hf (left_mem_Icc.2 <| hc.1.trans hc.2) hc hc.1,
       hf hc (right_mem_Icc.2 <| hc.1.trans hc.2) hc.2⟩
 #align monotone_on.image_Icc_subset MonotoneOn.image_Icc_subset
 
 theorem _root_.AntitoneOn.image_Icc_subset (hf : AntitoneOn f (Icc a b)) :
     f '' Icc a b ⊆ Icc (f b) (f a) :=
-  image_subset_iff.2 fun c hc =>
+  image_subset_iff.2 fun _c hc =>
     ⟨hf hc (right_mem_Icc.2 <| hc.1.trans hc.2) hc.2,
       hf (left_mem_Icc.2 <| hc.1.trans hc.2) hc hc.1⟩
 #align antitone_on.image_Icc_subset AntitoneOn.image_Icc_subset

From d709c9a57d9befd0768c3137d66de90ad92d5219 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Tue, 29 Aug 2023 14:30:44 +0000
Subject: [PATCH 03/15] fix

---
 Mathlib/Data/Set/Intervals/Basic.lean         |  29 +-
 Mathlib/Data/Set/Intervals/Image.lean         | 265 ++++++++++++++----
 .../Data/Set/Intervals/UnorderedInterval.lean |  40 ++-
 3 files changed, 234 insertions(+), 100 deletions(-)

diff --git a/Mathlib/Data/Set/Intervals/Basic.lean b/Mathlib/Data/Set/Intervals/Basic.lean
index 115e603ceb01a..796ab8b68491a 100644
--- a/Mathlib/Data/Set/Intervals/Basic.lean
+++ b/Mathlib/Data/Set/Intervals/Basic.lean
@@ -38,7 +38,7 @@ namespace Set
 
 section Preorder
 
-variable [Preorder α] {a a₁ a₂ b b₁ b₂ c x : α}
+variable [Preorder α] [Preorder β] {f : α → β} {a a₁ a₂ b b₁ b₂ c x : α}
 
 /-- Left-open right-open interval -/
 def Ioo (a b : α) :=
@@ -1719,33 +1719,6 @@ theorem Ioo_union_Ioo (h₁ : min a b < max c d) (h₂ : min c d < max a b) :
       le_of_lt h₂, le_of_lt h₁]
 #align set.Ioo_union_Ioo Set.Ioo_union_Ioo
 
-section Lattice
-variable [Lattice β] {f : α → β}
-
-theorem _root_.MonotoneOn.image_Icc_subset (hf : MonotoneOn f (Icc a b)) :
-    f '' Icc a b ⊆ Icc (f a) (f b) :=
-  image_subset_iff.2 fun _c hc =>
-    ⟨hf (left_mem_Icc.2 <| hc.1.trans hc.2) hc hc.1,
-      hf hc (right_mem_Icc.2 <| hc.1.trans hc.2) hc.2⟩
-#align monotone_on.image_Icc_subset MonotoneOn.image_Icc_subset
-
-theorem _root_.AntitoneOn.image_Icc_subset (hf : AntitoneOn f (Icc a b)) :
-    f '' Icc a b ⊆ Icc (f b) (f a) :=
-  image_subset_iff.2 fun _c hc =>
-    ⟨hf hc (right_mem_Icc.2 <| hc.1.trans hc.2) hc.2,
-      hf (left_mem_Icc.2 <| hc.1.trans hc.2) hc hc.1⟩
-#align antitone_on.image_Icc_subset AntitoneOn.image_Icc_subset
-
-theorem _root_.Monotone.image_Icc_subset (hf : Monotone f) : f '' Icc a b ⊆ Icc (f a) (f b) :=
-  (hf.monotoneOn _).image_Icc_subset
-#align monotone.image_Icc_subset Monotone.image_Icc_subset
-
-theorem _root_.Antitone.image_Icc_subset (hf : Antitone f) : f '' Icc a b ⊆ Icc (f b) (f a) :=
-  (hf.antitoneOn _).image_Icc_subset
-#align antitone.image_Icc_subset Antitone.image_Icc_subset
-
-end Lattice
-
 end LinearOrder
 
 section Lattice
diff --git a/Mathlib/Data/Set/Intervals/Image.lean b/Mathlib/Data/Set/Intervals/Image.lean
index f41830e5648ee..523806cdbac13 100644
--- a/Mathlib/Data/Set/Intervals/Image.lean
+++ b/Mathlib/Data/Set/Intervals/Image.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Kim Liesinger. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Liesinger
+Authors: Kim Liesinger, Yaël Dillies
 -/
 import Mathlib.Data.Set.Intervals.Basic
 import Mathlib.Data.Set.Function
@@ -15,90 +15,233 @@ variable {f : α → β}
 
 open Set
 
-section
-variable [Preorder α] [Preorder β]
+section Preorder
+variable [Preorder α] [Preorder β] {a b : α}
 
-theorem Monotone.mapsTo_Icc (h : Monotone f) :
-    MapsTo f (Icc a b) (Icc (f a) (f b)) :=
-  fun _ _ => by aesop
+lemma MonotoneOn.mapsTo_Ici (h : MonotoneOn f (Ici a)) : MapsTo f (Ici a) (Ici (f a)) :=
+λ _c hc ↦ by aesop
 
-theorem StrictMono.mapsTo_Ioo (h : StrictMono f) :
-    MapsTo f (Ioo a b) (Ioo (f a) (f b)) :=
-  fun _ _ => by aesop
+lemma MonotoneOn.mapsTo_Iic (h : MonotoneOn f (Iic b)) : MapsTo f (Iic b) (Iic (f b)) :=
+λ _c hc ↦ by aesop
 
-theorem Monotone.mapsTo_Ici  (h : Monotone f) :
-    MapsTo f (Ici a) (Ici (f a)) :=
-  fun _ _ => by aesop
+lemma MonotoneOn.mapsTo_Icc (h : MonotoneOn f (Icc a b)) : MapsTo f (Icc a b) (Icc (f a) (f b)) :=
+λ _c hc ↦
+  ⟨h (left_mem_Icc.2 $ hc.1.trans hc.2) hc hc.1, h hc (right_mem_Icc.2 $ hc.1.trans hc.2) hc.2⟩
 
-theorem Monotone.mapsTo_Iic (h : Monotone f) :
-    MapsTo f (Iic a) (Iic (f a)) :=
-  fun _ _ => by aesop
+lemma AntitoneOn.mapsTo_Ici (h : AntitoneOn f (Ici a)) : MapsTo f (Ici a) (Iic (f a)) :=
+λ _c hc ↦ by aesop
 
-theorem StrictMono.mapsTo_Ioi (h : StrictMono f) :
-    MapsTo f (Ioi a) (Ioi (f a)) :=
-  fun _ _ => by aesop
+lemma AntitoneOn.mapsTo_Iic (h : AntitoneOn f (Iic b)) : MapsTo f (Iic b) (Ici (f b)) :=
+λ _c hc ↦ by aesop
 
-theorem StrictMono.mapsTo_Iio (h : StrictMono f) :
-    MapsTo f (Iio a) (Iio (f a)) :=
-  fun _ _ => by aesop
+lemma AntitoneOn.mapsTo_Icc (h : AntitoneOn f (Icc a b)) : MapsTo f (Icc a b) (Icc (f b) (f a)) :=
+λ _c hc ↦
+  ⟨h hc (right_mem_Icc.2 $ hc.1.trans hc.2) hc.2, h (left_mem_Icc.2 $ hc.1.trans hc.2) hc hc.1⟩
 
-end
+lemma StrictMonoOn.mapsTo_Ioi (h : StrictMonoOn f (Ici a)) : MapsTo f (Ioi a) (Ioi (f a)) :=
+λ _c hc ↦ h le_rfl hc.le hc
 
-section
-variable [PartialOrder α] [Preorder β]
+lemma StrictMonoOn.mapsTo_Iio (h : StrictMonoOn f (Iic b)) : MapsTo f (Iio b) (Iio (f b)) :=
+λ _c hc ↦ h hc.le le_rfl hc
+
+lemma StrictMonoOn.mapsTo_Ioo (h : StrictMonoOn f (Icc a b)) :
+  MapsTo f (Ioo a b) (Ioo (f a) (f b)) :=
+λ _c hc ↦
+  ⟨h (left_mem_Icc.2 (hc.1.trans hc.2).le) (Ioo_subset_Icc_self hc) hc.1,
+   h (Ioo_subset_Icc_self hc) (right_mem_Icc.2 (hc.1.trans hc.2).le) hc.2⟩
+
+lemma StrictAntiOn.mapsTo_Ioi (h : StrictAntiOn f (Ici a)) : MapsTo f (Ioi a) (Iio (f a)) :=
+λ _c hc ↦ h le_rfl hc.le hc
+
+lemma StrictAntiOn.mapsTo_Iio (h : StrictAntiOn f (Iic b)) : MapsTo f (Iio b) (Ioi (f b)) :=
+λ _c hc ↦ h hc.le le_rfl hc
+
+lemma StrictAntiOn.mapsTo_Ioo (h : StrictAntiOn f (Icc a b)) :
+  MapsTo f (Ioo a b) (Ioo (f b) (f a)) :=
+λ _c hc ↦
+  ⟨h (Ioo_subset_Icc_self hc) (right_mem_Icc.2 (hc.1.trans hc.2).le) hc.2,
+   h (left_mem_Icc.2 (hc.1.trans hc.2).le) (Ioo_subset_Icc_self hc) hc.1⟩
+
+lemma Monotone.mapsTo_Ici (h : Monotone f) : MapsTo f (Ici a) (Ici (f a)) :=
+(h.monotoneOn _).mapsTo_Ici
+
+lemma Monotone.mapsTo_Iic (h : Monotone f) : MapsTo f (Iic b) (Iic (f b)) :=
+(h.monotoneOn _).mapsTo_Iic
+
+lemma Monotone.mapsTo_Icc (h : Monotone f) : MapsTo f (Icc a b) (Icc (f a) (f b)) :=
+(h.monotoneOn _).mapsTo_Icc
+
+lemma Antitone.mapsTo_Ici (h : Antitone f) : MapsTo f (Ici a) (Iic (f a)) :=
+(h.antitoneOn _).mapsTo_Ici
+
+lemma Antitone.mapsTo_Iic (h : Antitone f) : MapsTo f (Iic b) (Ici (f b)) :=
+(h.antitoneOn _).mapsTo_Iic
+
+lemma Antitone.mapsTo_Icc (h : Antitone f) : MapsTo f (Icc a b) (Icc (f b) (f a)) :=
+(h.antitoneOn _).mapsTo_Icc
+
+lemma StrictMono.mapsTo_Ioi (h : StrictMono f) : MapsTo f (Ioi a) (Ioi (f a)) :=
+(h.strictMonoOn _).mapsTo_Ioi
+
+lemma StrictMono.mapsTo_Iio (h : StrictMono f) : MapsTo f (Iio b) (Iio (f b)) :=
+(h.strictMonoOn _).mapsTo_Iio
+
+lemma StrictMono.mapsTo_Ioo (h : StrictMono f) : MapsTo f (Ioo a b) (Ioo (f a) (f b)) :=
+(h.strictMonoOn _).mapsTo_Ioo
+
+lemma StrictAnti.mapsTo_Ioi (h : StrictAnti f) : MapsTo f (Ioi a) (Iio (f a)) :=
+(h.strictAntiOn _).mapsTo_Ioi
+
+lemma StrictAnti.mapsTo_Iio (h : StrictAnti f) : MapsTo f (Iio b) (Ioi (f b)) :=
+(h.strictAntiOn _).mapsTo_Iio
+
+lemma StrictAnti.mapsTo_Ioo (h : StrictAnti f) : MapsTo f (Ioo a b) (Ioo (f b) (f a)) :=
+(h.strictAntiOn _).mapsTo_Ioo
+
+lemma MonotoneOn.image_Ici_subset (h : MonotoneOn f (Ici a)) : f '' Ici a ⊆ Ici (f a) :=
+h.mapsTo_Ici.image_subset
+
+lemma MonotoneOn.image_Iic_subset (h : MonotoneOn f (Iic b)) : f '' Iic b ⊆ Iic (f b) :=
+h.mapsTo_Iic.image_subset
+
+lemma MonotoneOn.image_Icc_subset (h : MonotoneOn f (Icc a b)) : f '' Icc a b ⊆ Icc (f a) (f b) :=
+h.mapsTo_Icc.image_subset
+
+lemma AntitoneOn.image_Ici_subset (h : AntitoneOn f (Ici a)) : f '' Ici a ⊆ Iic (f a) :=
+h.mapsTo_Ici.image_subset
+
+lemma AntitoneOn.image_Iic_subset (h : AntitoneOn f (Iic b)) : f '' Iic b ⊆ Ici (f b) :=
+h.mapsTo_Iic.image_subset
+
+lemma AntitoneOn.image_Icc_subset (h : AntitoneOn f (Icc a b)) : f '' Icc a b ⊆ Icc (f b) (f a) :=
+h.mapsTo_Icc.image_subset
 
-theorem StrictMono.mapsTo_Ico (h : StrictMono f) :
-    MapsTo f (Ico a b) (Ico (f a) (f b)) :=
-  -- It makes me sad that `aesop` doesn't do this. There are clearly missing lemmas.
-  fun _ m => ⟨h.monotone m.1, h m.2⟩
+lemma StrictMonoOn.image_Ioi_subset (h : StrictMonoOn f (Ici a)) : f '' Ioi a ⊆ Ioi (f a) :=
+h.mapsTo_Ioi.image_subset
 
-theorem StrictMono.mapsTo_Ioc (h : StrictMono f) :
-    MapsTo f (Ioc a b) (Ioc (f a) (f b)) :=
-  fun _ m => ⟨h m.1, h.monotone m.2⟩
+lemma StrictMonoOn.image_Iio_subset (h : StrictMonoOn f (Iic b)) : f '' Iio b ⊆ Iio (f b) :=
+h.mapsTo_Iio.image_subset
 
-end
+lemma StrictMonoOn.image_Ioo_subset (h : StrictMonoOn f (Icc a b)) :
+  f '' Ioo a b ⊆ Ioo (f a) (f b) :=
+h.mapsTo_Ioo.image_subset
 
-section
-variable [Preorder α] [Preorder β]
+lemma StrictAntiOn.image_Ioi_subset (h : StrictAntiOn f (Ici a)) : f '' Ioi a ⊆ Iio (f a) :=
+h.mapsTo_Ioi.image_subset
 
-theorem Monotone.image_Icc_subset (h : Monotone f) :
-    f '' Icc a b ⊆ Icc (f a) (f b) :=
-  h.mapsTo_Icc.image_subset
+lemma StrictAntiOn.image_Iio_subset (h : StrictAntiOn f (Iic b)) : f '' Iio b ⊆ Ioi (f b) :=
+h.mapsTo_Iio.image_subset
 
-theorem StrictMono.image_Ioo_subset (h : StrictMono f) :
-    f '' Ioo a b ⊆ Ioo (f a) (f b) :=
-  h.mapsTo_Ioo.image_subset
+lemma StrictAntiOn.image_Ioo_subset (h : StrictAntiOn f (Icc a b)) :
+  f '' Ioo a b ⊆ Ioo (f b) (f a) :=
+h.mapsTo_Ioo.image_subset
 
-theorem Monotone.image_Ici_subset (h : Monotone f) :
-    f '' Ici a ⊆ Ici (f a) :=
-  h.mapsTo_Ici.image_subset
+lemma Monotone.image_Ici_subset (h : Monotone f) : f '' Ici a ⊆ Ici (f a) :=
+(h.monotoneOn _).image_Ici_subset
 
-theorem Monotone.image_Iic_subset (h : Monotone f) :
-    f '' Iic a ⊆ Iic (f a) :=
-  h.mapsTo_Iic.image_subset
+lemma Monotone.image_Iic_subset (h : Monotone f) : f '' Iic b ⊆ Iic (f b) :=
+(h.monotoneOn _).image_Iic_subset
 
-theorem StrictMono.image_Ioi_subset (h : StrictMono f) :
-    f '' Ioi a ⊆ Ioi (f a) :=
-  h.mapsTo_Ioi.image_subset
+lemma Monotone.image_Icc_subset (h : Monotone f) : f '' Icc a b ⊆ Icc (f a) (f b) :=
+(h.monotoneOn _).image_Icc_subset
 
-theorem StrictMono.image_Iio_subset (h : StrictMono f) :
-    f '' Iio a ⊆ Iio (f a) :=
-  h.mapsTo_Iio.image_subset
+lemma Antitone.image_Ici_subset (h : Antitone f) : f '' Ici a ⊆ Iic (f a) :=
+(h.antitoneOn _).image_Ici_subset
 
-end
+lemma Antitone.image_Iic_subset (h : Antitone f) : f '' Iic b ⊆ Ici (f b) :=
+(h.antitoneOn _).image_Iic_subset
 
-section
+lemma Antitone.image_Icc_subset (h : Antitone f) : f '' Icc a b ⊆ Icc (f b) (f a) :=
+(h.antitoneOn _).image_Icc_subset
+
+lemma StrictMono.image_Ioi_subset (h : StrictMono f) : f '' Ioi a ⊆ Ioi (f a) :=
+(h.strictMonoOn _).image_Ioi_subset
+
+lemma StrictMono.image_Iio_subset (h : StrictMono f) : f '' Iio b ⊆ Iio (f b) :=
+(h.strictMonoOn _).image_Iio_subset
+
+lemma StrictMono.image_Ioo_subset (h : StrictMono f) : f '' Ioo a b ⊆ Ioo (f a) (f b) :=
+(h.strictMonoOn _).image_Ioo_subset
+
+lemma StrictAnti.image_Ioi_subset (h : StrictAnti f) : f '' Ioi a ⊆ Iio (f a) :=
+(h.strictAntiOn _).image_Ioi_subset
+
+lemma StrictAnti.image_Iio_subset (h : StrictAnti f) : f '' Iio b ⊆ Ioi (f b) :=
+(h.strictAntiOn _).image_Iio_subset
+
+lemma StrictAnti.image_Ioo_subset (h : StrictAnti f) : f '' Ioo a b ⊆ Ioo (f b) (f a) :=
+(h.strictAntiOn _).image_Ioo_subset
+
+end Preorder
+
+section PartialOrder
 variable [PartialOrder α] [Preorder β]
 
-theorem StrictMono.imageIco_subset (h : StrictMono f) :
-    f '' Ico a b ⊆ Ico (f a) (f b) :=
-  h.mapsTo_Ico.image_subset
+lemma StrictMonoOn.mapsTo_Ico (h : StrictMonoOn f (Icc a b)) :
+  MapsTo f (Ico a b) (Ico (f a) (f b)) :=
+λ _c hc ↦
+  ⟨h.monotoneOn (left_mem_Icc.2 $ hc.1.trans hc.2.le) (Ico_subset_Icc_self hc) hc.1,
+   h (Ico_subset_Icc_self hc) (right_mem_Icc.2 $ hc.1.trans hc.2.le) hc.2⟩
+
+lemma StrictMonoOn.mapsTo_Ioc (h : StrictMonoOn f (Icc a b)) :
+  MapsTo f (Ioc a b) (Ioc (f a) (f b)) :=
+λ _c hc ↦
+  ⟨h (left_mem_Icc.2 $ hc.1.le.trans hc.2) (Ioc_subset_Icc_self hc) hc.1,
+   h.monotoneOn (Ioc_subset_Icc_self hc) (right_mem_Icc.2 $ hc.1.le.trans hc.2) hc.2⟩
+
+lemma StrictAntiOn.mapsTo_Ico (h : StrictAntiOn f (Icc a b)) :
+  MapsTo f (Ico a b) (Ioc (f b) (f a)) :=
+λ _c hc ↦
+  ⟨h (Ico_subset_Icc_self hc) (right_mem_Icc.2 $ hc.1.trans hc.2.le) hc.2,
+   h.antitoneOn (left_mem_Icc.2 $ hc.1.trans hc.2.le) (Ico_subset_Icc_self hc) hc.1⟩
+
+lemma StrictAntiOn.mapsTo_Ioc (h : StrictAntiOn f (Icc a b)) :
+  MapsTo f (Ioc a b) (Ico (f b) (f a)) :=
+λ _c hc ↦
+  ⟨h.antitoneOn (Ioc_subset_Icc_self hc) (right_mem_Icc.2 $ hc.1.le.trans hc.2) hc.2,
+   h (left_mem_Icc.2 $ hc.1.le.trans hc.2) (Ioc_subset_Icc_self hc) hc.1⟩
+
+lemma StrictMono.mapsTo_Ico (h : StrictMono f) : MapsTo f (Ico a b) (Ico (f a) (f b)) :=
+(h.strictMonoOn _).mapsTo_Ico
+
+lemma StrictMono.mapsTo_Ioc (h : StrictMono f) : MapsTo f (Ioc a b) (Ioc (f a) (f b)) :=
+(h.strictMonoOn _).mapsTo_Ioc
+
+lemma StrictAnti.mapsTo_Ico (h : StrictAnti f) : MapsTo f (Ico a b) (Ioc (f b) (f a)) :=
+(h.strictAntiOn _).mapsTo_Ico
+
+lemma StrictAnti.mapsTo_Ioc (h : StrictAnti f) : MapsTo f (Ioc a b) (Ico (f b) (f a)) :=
+(h.strictAntiOn _).mapsTo_Ioc
+
+lemma StrictMonoOn.image_Ico_subset (h : StrictMonoOn f (Icc a b)) :
+  f '' Ico a b ⊆ Ico (f a) (f b) :=
+h.mapsTo_Ico.image_subset
+
+lemma StrictMonoOn.image_Ioc_subset (h : StrictMonoOn f (Icc a b)) :
+  f '' Ioc a b ⊆ Ioc (f a) (f b) :=
+h.mapsTo_Ioc.image_subset
+
+lemma StrictAntiOn.image_Ico_subset (h : StrictAntiOn f (Icc a b)) :
+  f '' Ico a b ⊆ Ioc (f b) (f a) :=
+h.mapsTo_Ico.image_subset
+
+lemma StrictAntiOn.image_Ioc_subset (h : StrictAntiOn f (Icc a b)) :
+  f '' Ioc a b ⊆ Ico (f b) (f a) :=
+h.mapsTo_Ioc.image_subset
+
+lemma StrictMono.image_Ico_subset (h : StrictMono f) : f '' Ico a b ⊆ Ico (f a) (f b) :=
+(h.strictMonoOn _).image_Ico_subset
+
+lemma StrictMono.image_Ioc_subset (h : StrictMono f) : f '' Ioc a b ⊆ Ioc (f a) (f b) :=
+(h.strictMonoOn _).image_Ioc_subset
+
+lemma StrictAnti.image_Ico_subset (h : StrictAnti f) : f '' Ico a b ⊆ Ioc (f b) (f a) :=
+(h.strictAntiOn _).image_Ico_subset
 
-theorem StrictMono.imageIoc_subset (h : StrictMono f) :
-    f '' Ioc a b ⊆ Ioc (f a) (f b) :=
-  h.mapsTo_Ioc.image_subset
+lemma StrictAnti.image_Ioc_subset (h : StrictAnti f) : f '' Ioc a b ⊆ Ico (f b) (f a) :=
+(h.strictAntiOn _).image_Ioc_subset
 
-end
+end PartialOrder
 
 namespace Set
 
diff --git a/Mathlib/Data/Set/Intervals/UnorderedInterval.lean b/Mathlib/Data/Set/Intervals/UnorderedInterval.lean
index 84b45452a86f4..6492e9d777b66 100644
--- a/Mathlib/Data/Set/Intervals/UnorderedInterval.lean
+++ b/Mathlib/Data/Set/Intervals/UnorderedInterval.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhouhang Zhou
 -/
 import Mathlib.Order.Bounds.Basic
-import Mathlib.Data.Set.Intervals.Basic
+import Mathlib.Data.Set.Intervals.Image
 
 #align_import data.set.intervals.unordered_interval from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
 
@@ -184,23 +184,41 @@ variable [LinearOrder α]
 section Lattice
 variable [Lattice β] {f : α → β} {s : Set α} {a b : α}
 
-theorem _root_.MonotoneOn.image_uIcc_subset (hf : MonotoneOn f (uIcc a b)) :
-    f '' uIcc a b ⊆ uIcc (f a) (f b) :=
-  hf.image_Icc_subset.trans <| by
-    rw [hf.map_sup left_mem_uIcc right_mem_uIcc, hf.map_inf left_mem_uIcc right_mem_uIcc, uIcc]
+lemma _root_.MonotoneOn.mapsTo_uIcc (hf : MonotoneOn f (uIcc a b)) :
+  MapsTo f (uIcc a b) (uIcc (f a) (f b)) := by
+  rw [uIcc, uIcc, ←hf.map_sup, ←hf.map_inf] <;>
+    apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]
+#align monotone_on.maps_to_uIcc MonotoneOn.mapsTo_uIcc
+
+lemma _root_.AntitoneOn.mapsTo_uIcc (hf : AntitoneOn f (uIcc a b)) :
+  MapsTo f (uIcc a b) (uIcc (f a) (f b)) := by
+  rw [uIcc, uIcc, ←hf.map_sup, ←hf.map_inf] <;>
+    apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]
+#align antitone_on.maps_to_uIcc AntitoneOn.mapsTo_uIcc
+
+lemma _root_.Monotone.mapsTo_uIcc (hf : Monotone f) : MapsTo f (uIcc a b) (uIcc (f a) (f b)) :=
+  (hf.monotoneOn _).mapsTo_uIcc
+#align monotone.maps_to_uIcc Monotone.mapsTo_uIcc
+
+lemma _root_.Antitone.mapsTo_uIcc (hf : Antitone f) : MapsTo f (uIcc a b) (uIcc (f a) (f b)) :=
+  (hf.antitoneOn _).mapsTo_uIcc
+#align antitone.maps_to_uIcc Antitone.mapsTo_uIcc
+
+lemma _root_.MonotoneOn.image_uIcc_subset (hf : MonotoneOn f (uIcc a b)) :
+  f '' uIcc a b ⊆ uIcc (f a) (f b) :=
+hf.mapsTo_uIcc.image_subset
 #align monotone_on.image_uIcc_subset MonotoneOn.image_uIcc_subset
 
-theorem _root_.AntitoneOn.image_uIcc_subset (hf : AntitoneOn f (uIcc a b)) :
-    f '' uIcc a b ⊆ uIcc (f a) (f b) :=
-  hf.image_Icc_subset.trans <| by
-    rw [hf.map_sup left_mem_uIcc right_mem_uIcc, hf.map_inf left_mem_uIcc right_mem_uIcc, uIcc]
+lemma _root_.AntitoneOn.image_uIcc_subset (hf : AntitoneOn f (uIcc a b)) :
+  f '' uIcc a b ⊆ uIcc (f a) (f b) :=
+hf.mapsTo_uIcc.image_subset
 #align antitone_on.image_uIcc_subset AntitoneOn.image_uIcc_subset
 
-theorem _root_.Monotone.image_uIcc_subset (hf : Monotone f) : f '' uIcc a b ⊆ uIcc (f a) (f b) :=
+lemma _root_.Monotone.image_uIcc_subset (hf : Monotone f) : f '' uIcc a b ⊆ uIcc (f a) (f b) :=
   (hf.monotoneOn _).image_uIcc_subset
 #align monotone.image_uIcc_subset Monotone.image_uIcc_subset
 
-theorem _root_.Antitone.image_uIcc_subset (hf : Antitone f) : f '' uIcc a b ⊆ uIcc (f a) (f b) :=
+lemma _root_.Antitone.image_uIcc_subset (hf : Antitone f) : f '' uIcc a b ⊆ uIcc (f a) (f b) :=
   (hf.antitoneOn _).image_uIcc_subset
 #align antitone.image_uIcc_subset Antitone.image_uIcc_subset
 

From 3d82c870c7d060b1360572317e6d9d94152873d4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Tue, 29 Aug 2023 15:31:44 +0000
Subject: [PATCH 04/15] fix analysis.convex.projicc

---
 Mathlib/Analysis/Convex/ProjIcc.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Analysis/Convex/ProjIcc.lean b/Mathlib/Analysis/Convex/ProjIcc.lean
index 3214ed3254c2c..fbca1b06fc137 100644
--- a/Mathlib/Analysis/Convex/ProjIcc.lean
+++ b/Mathlib/Analysis/Convex/ProjIcc.lean
@@ -27,20 +27,20 @@ variable {𝕜 β : Type _} [LinearOrderedField 𝕜] [LinearOrderedAddCommMonoi
 /-- A convex set extended towards minus infinity is convex. -/
 protected theorem Convex.IciExtend (hf : Convex 𝕜 s) :
     Convex 𝕜 {x | IciExtend (restrict (Ici z) (· ∈ s)) x} := by
-  rw [convex_iff_ordConnected] at hf ⊢; exact hf.restrict.Ici_extend
+  rw [convex_iff_ordConnected] at hf ⊢; exact hf.restrict.IciExtend
 #align convex.Ici_extend Convex.IciExtend
 
 /-- A convex set extended towards infinity is convex. -/
 protected theorem Convex.IicExtend (hf : Convex 𝕜 s) :
     Convex 𝕜 {x | IicExtend (restrict (Iic z) (· ∈ s)) x} := by
-  rw [convex_iff_ordConnected] at hf ⊢; exact hf.restrict.Iic_extend
+  rw [convex_iff_ordConnected] at hf ⊢; exact hf.restrict.IicExtend
 #align convex.Iic_extend Convex.IicExtend
 
 /-- A convex monotone function extended constantly towards minus infinity is convex. -/
 protected theorem ConvexOn.IciExtend (hf : ConvexOn 𝕜 s f) (hf' : MonotoneOn f s) :
     ConvexOn 𝕜 {x | IciExtend (restrict (Ici z) (· ∈ s)) x} (IciExtend $ restrict (Ici z) f) := by
   refine' ⟨hf.1.IciExtend, λ x hx y hy a b ha hb hab ↦ _⟩
-  dsimp [Ici_extend_apply] at hx hy ⊢
+  dsimp [IciExtend_apply] at hx hy ⊢
   refine' (hf' (hf.1.OrdConnected.uIcc_subset hx hy $ (Monotone.image_uIcc_subset λ _ _ ↦
     max_le_max le_rfl) $ mem_image_of_mem _ $ convex_uIcc _ _
     left_mem_uIcc right_mem_uIcc ha hb hab) (hf.1 hx hy ha hb hab) _).trans (hf.2 hx hy ha hb hab)
@@ -53,7 +53,7 @@ protected theorem ConvexOn.IciExtend (hf : ConvexOn 𝕜 s f) (hf' : MonotoneOn
 protected theorem ConvexOn.IicExtend (hf : ConvexOn 𝕜 s f) (hf' : AntitoneOn f s) :
     ConvexOn 𝕜 {x | IicExtend (restrict (Iic z) (· ∈ s)) x} (IicExtend $ restrict (Iic z) f) := by
   refine' ⟨hf.1.IicExtend, λ x hx y hy a b ha hb hab ↦ _⟩
-  dsimp [Iic_extend_apply] at hx hy ⊢
+  dsimp [IicExtend_apply] at hx hy ⊢
   refine' (hf' (hf.1 hx hy ha hb hab) (hf.1.OrdConnected.uIcc_subset hx hy $
     (Monotone.image_uIcc_subset λ _ _ ↦ min_le_min le_rfl) $ mem_image_of_mem _ $ convex_uIcc _ _
     left_mem_uIcc right_mem_uIcc ha hb hab) _).trans (hf.2 hx hy ha hb hab)

From cef319110621955436587e60c9c64dc0431c2689 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Tue, 29 Aug 2023 15:32:57 +0000
Subject: [PATCH 05/15] fix a bit more

---
 Mathlib/Analysis/Convex/ProjIcc.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Analysis/Convex/ProjIcc.lean b/Mathlib/Analysis/Convex/ProjIcc.lean
index fbca1b06fc137..4a08f0683fec6 100644
--- a/Mathlib/Analysis/Convex/ProjIcc.lean
+++ b/Mathlib/Analysis/Convex/ProjIcc.lean
@@ -77,23 +77,23 @@ protected theorem ConcaveOn.IicExtend (hf : ConcaveOn 𝕜 s f) (hf' : MonotoneO
 /-- A convex monotone function extended constantly towards minus infinity is convex. -/
 protected theorem ConvexOn.IciExtend_of_monotone (hf : ConvexOn 𝕜 univ f) (hf' : Monotone f) :
     ConvexOn 𝕜 univ (IciExtend $ restrict (Ici z) f) :=
-  hf.IciExtend $ hf'.MonotoneOn _
+  hf.IciExtend $ hf'.monotoneOn _
 #align convex_on.Ici_extend_of_monotone ConvexOn.IciExtend_of_monotone
 
 /-- A convex antitone function extended constantly towards infinity is convex. -/
 protected theorem ConvexOn.IicExtend_of_antitone (hf : ConvexOn 𝕜 univ f) (hf' : Antitone f) :
     ConvexOn 𝕜 univ (IicExtend $ restrict (Iic z) f) :=
-  hf.IicExtend $ hf'.AntitoneOn _
+  hf.IicExtend $ hf'.antitoneOn _
 #align convex_on.Iic_extend_of_antitone ConvexOn.IicExtend_of_antitone
 
 /-- A concave antitone function extended constantly minus towards infinity is concave. -/
 protected theorem ConcaveOn.IciExtend_of_antitone (hf : ConcaveOn 𝕜 univ f) (hf' : Antitone f) :
     ConcaveOn 𝕜 univ (IciExtend $ restrict (Ici z) f) :=
-  hf.IciExtend $ hf'.AntitoneOn _
+  hf.IciExtend $ hf'.antitoneOn _
 #align concave_on.Ici_extend_of_antitone ConcaveOn.IciExtend_of_antitone
 
 /-- A concave monotone function extended constantly towards infinity is concave. -/
 protected theorem ConcaveOn.IicExtend_of_monotone (hf : ConcaveOn 𝕜 univ f) (hf' : Monotone f) :
     ConcaveOn 𝕜 univ (IicExtend $ restrict (Iic z) f) :=
-  hf.IicExtend $ hf'.MonotoneOn _
+  hf.IicExtend $ hf'.monotoneOn _
 #align concave_on.Iic_extend_of_monotone ConcaveOn.IicExtend_of_monotone

From 26118c20ffae612cec656649929ef925eae44bfc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Tue, 29 Aug 2023 18:20:13 +0000
Subject: [PATCH 06/15] fix a bit more

---
 Mathlib/Analysis/Convex/ProjIcc.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Analysis/Convex/ProjIcc.lean b/Mathlib/Analysis/Convex/ProjIcc.lean
index 4a08f0683fec6..f49f9c9ccff1b 100644
--- a/Mathlib/Analysis/Convex/ProjIcc.lean
+++ b/Mathlib/Analysis/Convex/ProjIcc.lean
@@ -41,7 +41,7 @@ protected theorem ConvexOn.IciExtend (hf : ConvexOn 𝕜 s f) (hf' : MonotoneOn
     ConvexOn 𝕜 {x | IciExtend (restrict (Ici z) (· ∈ s)) x} (IciExtend $ restrict (Ici z) f) := by
   refine' ⟨hf.1.IciExtend, λ x hx y hy a b ha hb hab ↦ _⟩
   dsimp [IciExtend_apply] at hx hy ⊢
-  refine' (hf' (hf.1.OrdConnected.uIcc_subset hx hy $ (Monotone.image_uIcc_subset λ _ _ ↦
+  refine' (hf' (hf.1.ordConnected.uIcc_subset hx hy $ (Monotone.image_uIcc_subset λ _ _ ↦
     max_le_max le_rfl) $ mem_image_of_mem _ $ convex_uIcc _ _
     left_mem_uIcc right_mem_uIcc ha hb hab) (hf.1 hx hy ha hb hab) _).trans (hf.2 hx hy ha hb hab)
   rw [smul_max ha z, smul_max hb z]
@@ -54,7 +54,7 @@ protected theorem ConvexOn.IicExtend (hf : ConvexOn 𝕜 s f) (hf' : AntitoneOn
     ConvexOn 𝕜 {x | IicExtend (restrict (Iic z) (· ∈ s)) x} (IicExtend $ restrict (Iic z) f) := by
   refine' ⟨hf.1.IicExtend, λ x hx y hy a b ha hb hab ↦ _⟩
   dsimp [IicExtend_apply] at hx hy ⊢
-  refine' (hf' (hf.1 hx hy ha hb hab) (hf.1.OrdConnected.uIcc_subset hx hy $
+  refine' (hf' (hf.1 hx hy ha hb hab) (hf.1.ordConnected.uIcc_subset hx hy $
     (Monotone.image_uIcc_subset λ _ _ ↦ min_le_min le_rfl) $ mem_image_of_mem _ $ convex_uIcc _ _
     left_mem_uIcc right_mem_uIcc ha hb hab) _).trans (hf.2 hx hy ha hb hab)
   rw [smul_min ha z, smul_min hb z]

From 698e75b520dd247e1da5a24d6cb4b4896617ee84 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Sat, 9 Sep 2023 21:51:39 +0000
Subject: [PATCH 07/15] Eric's comments

---
 Mathlib/Algebra/Order/Monoid/Lemmas.lean          | 4 ++--
 Mathlib/Algebra/Order/SMul.lean                   | 1 -
 Mathlib/Analysis/Convex/ProjIcc.lean              | 2 +-
 Mathlib/Data/Set/Intervals/Basic.lean             | 2 +-
 Mathlib/Data/Set/Intervals/Image.lean             | 4 ++++
 Mathlib/Data/Set/Intervals/UnorderedInterval.lean | 4 ----
 6 files changed, 8 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Algebra/Order/Monoid/Lemmas.lean b/Mathlib/Algebra/Order/Monoid/Lemmas.lean
index 84af89be5ce14..03fa8b96f0254 100644
--- a/Mathlib/Algebra/Order/Monoid/Lemmas.lean
+++ b/Mathlib/Algebra/Order/Monoid/Lemmas.lean
@@ -317,8 +317,8 @@ by simp_rw [min_le_iff, le_max_iff]; contrapose! h; exact mul_lt_mul_of_lt_of_lt
 end LinearOrder
 
 section LinearOrder
-variable [LinearOrder α] [CovariantClass α α (· * ·) (· ≤ ·)]
-  [CovariantClass α α (swap (· * ·)) (· ≤ ·)] {a b c d : α}
+variable [LinearOrder α] [CovariantClass α α HMUL.hMul LE.le]
+  [CovariantClass α α (swap HMUL.hMul) LE.le] {a b c d : α}
 
 @[to_additive max_add_add_le_max_add_max]
 theorem max_mul_mul_le_max_mul_max' : max (a * b) (c * d) ≤ max a c * max b d :=
diff --git a/Mathlib/Algebra/Order/SMul.lean b/Mathlib/Algebra/Order/SMul.lean
index 2de39a52ce853..f56a2e78823ca 100644
--- a/Mathlib/Algebra/Order/SMul.lean
+++ b/Mathlib/Algebra/Order/SMul.lean
@@ -190,7 +190,6 @@ section LinearOrderedSemiring
 variable [LinearOrderedSemiring R] [LinearOrderedAddCommMonoid M] [SMulWithZero R M]
   [OrderedSMul R M] {a : R}
 
-
 -- TODO: `LinearOrderedField M → OrderedSMul ℚ M`
 instance LinearOrderedSemiring.toOrderedSMul : OrderedSMul R R :=
   OrderedSMul.mk'' fun _ => strictMono_mul_left_of_pos
diff --git a/Mathlib/Analysis/Convex/ProjIcc.lean b/Mathlib/Analysis/Convex/ProjIcc.lean
index f49f9c9ccff1b..e704829159cb0 100644
--- a/Mathlib/Analysis/Convex/ProjIcc.lean
+++ b/Mathlib/Analysis/Convex/ProjIcc.lean
@@ -21,7 +21,7 @@ We could deduplicate the proofs if we had a typeclass stating that `segment 𝕜
 
 open Set
 
-variable {𝕜 β : Type _} [LinearOrderedField 𝕜] [LinearOrderedAddCommMonoid β] [SMul 𝕜 β] {s : Set 𝕜}
+variable {𝕜 β : Type*} [LinearOrderedField 𝕜] [LinearOrderedAddCommMonoid β] [SMul 𝕜 β] {s : Set 𝕜}
   {f : 𝕜 → β} {z : 𝕜}
 
 /-- A convex set extended towards minus infinity is convex. -/
diff --git a/Mathlib/Data/Set/Intervals/Basic.lean b/Mathlib/Data/Set/Intervals/Basic.lean
index 796ab8b68491a..3bd31ab138d51 100644
--- a/Mathlib/Data/Set/Intervals/Basic.lean
+++ b/Mathlib/Data/Set/Intervals/Basic.lean
@@ -38,7 +38,7 @@ namespace Set
 
 section Preorder
 
-variable [Preorder α] [Preorder β] {f : α → β} {a a₁ a₂ b b₁ b₂ c x : α}
+variable [Preorder α] {a a₁ a₂ b b₁ b₂ c x : α}
 
 /-- Left-open right-open interval -/
 def Ioo (a b : α) :=
diff --git a/Mathlib/Data/Set/Intervals/Image.lean b/Mathlib/Data/Set/Intervals/Image.lean
index 523806cdbac13..5931b463d409a 100644
--- a/Mathlib/Data/Set/Intervals/Image.lean
+++ b/Mathlib/Data/Set/Intervals/Image.lean
@@ -100,6 +100,7 @@ lemma StrictAnti.mapsTo_Ioo (h : StrictAnti f) : MapsTo f (Ioo a b) (Ioo (f b) (
 
 lemma MonotoneOn.image_Ici_subset (h : MonotoneOn f (Ici a)) : f '' Ici a ⊆ Ici (f a) :=
 h.mapsTo_Ici.image_subset
+#align monotone_on.image_Icc_subset MonotoneOn.image_Icc_subset
 
 lemma MonotoneOn.image_Iic_subset (h : MonotoneOn f (Iic b)) : f '' Iic b ⊆ Iic (f b) :=
 h.mapsTo_Iic.image_subset
@@ -115,6 +116,7 @@ h.mapsTo_Iic.image_subset
 
 lemma AntitoneOn.image_Icc_subset (h : AntitoneOn f (Icc a b)) : f '' Icc a b ⊆ Icc (f b) (f a) :=
 h.mapsTo_Icc.image_subset
+#align antitone_on.image_Icc_subset AntitoneOn.image_Icc_subset
 
 lemma StrictMonoOn.image_Ioi_subset (h : StrictMonoOn f (Ici a)) : f '' Ioi a ⊆ Ioi (f a) :=
 h.mapsTo_Ioi.image_subset
@@ -144,6 +146,7 @@ lemma Monotone.image_Iic_subset (h : Monotone f) : f '' Iic b ⊆ Iic (f b) :=
 
 lemma Monotone.image_Icc_subset (h : Monotone f) : f '' Icc a b ⊆ Icc (f a) (f b) :=
 (h.monotoneOn _).image_Icc_subset
+#align monotone.image_Icc_subset Monotone.image_Icc_subset
 
 lemma Antitone.image_Ici_subset (h : Antitone f) : f '' Ici a ⊆ Iic (f a) :=
 (h.antitoneOn _).image_Ici_subset
@@ -153,6 +156,7 @@ lemma Antitone.image_Iic_subset (h : Antitone f) : f '' Iic b ⊆ Ici (f b) :=
 
 lemma Antitone.image_Icc_subset (h : Antitone f) : f '' Icc a b ⊆ Icc (f b) (f a) :=
 (h.antitoneOn _).image_Icc_subset
+#align antitone.image_Icc_subset Antitone.image_Icc_subset
 
 lemma StrictMono.image_Ioi_subset (h : StrictMono f) : f '' Ioi a ⊆ Ioi (f a) :=
 (h.strictMonoOn _).image_Ioi_subset
diff --git a/Mathlib/Data/Set/Intervals/UnorderedInterval.lean b/Mathlib/Data/Set/Intervals/UnorderedInterval.lean
index 6492e9d777b66..809e148ea300e 100644
--- a/Mathlib/Data/Set/Intervals/UnorderedInterval.lean
+++ b/Mathlib/Data/Set/Intervals/UnorderedInterval.lean
@@ -188,21 +188,17 @@ lemma _root_.MonotoneOn.mapsTo_uIcc (hf : MonotoneOn f (uIcc a b)) :
   MapsTo f (uIcc a b) (uIcc (f a) (f b)) := by
   rw [uIcc, uIcc, ←hf.map_sup, ←hf.map_inf] <;>
     apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]
-#align monotone_on.maps_to_uIcc MonotoneOn.mapsTo_uIcc
 
 lemma _root_.AntitoneOn.mapsTo_uIcc (hf : AntitoneOn f (uIcc a b)) :
   MapsTo f (uIcc a b) (uIcc (f a) (f b)) := by
   rw [uIcc, uIcc, ←hf.map_sup, ←hf.map_inf] <;>
     apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]
-#align antitone_on.maps_to_uIcc AntitoneOn.mapsTo_uIcc
 
 lemma _root_.Monotone.mapsTo_uIcc (hf : Monotone f) : MapsTo f (uIcc a b) (uIcc (f a) (f b)) :=
   (hf.monotoneOn _).mapsTo_uIcc
-#align monotone.maps_to_uIcc Monotone.mapsTo_uIcc
 
 lemma _root_.Antitone.mapsTo_uIcc (hf : Antitone f) : MapsTo f (uIcc a b) (uIcc (f a) (f b)) :=
   (hf.antitoneOn _).mapsTo_uIcc
-#align antitone.maps_to_uIcc Antitone.mapsTo_uIcc
 
 lemma _root_.MonotoneOn.image_uIcc_subset (hf : MonotoneOn f (uIcc a b)) :
   f '' uIcc a b ⊆ uIcc (f a) (f b) :=

From f5332a0c1f0db4d45698bcf803a861f72c252b68 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Tue, 12 Sep 2023 09:28:37 +0000
Subject: [PATCH 08/15] undo ProjIcc

---
 Mathlib/Algebra/Order/Monoid/Lemmas.lean |  4 +-
 Mathlib/Analysis/Convex/ProjIcc.lean     | 99 ------------------------
 2 files changed, 2 insertions(+), 101 deletions(-)
 delete mode 100644 Mathlib/Analysis/Convex/ProjIcc.lean

diff --git a/Mathlib/Algebra/Order/Monoid/Lemmas.lean b/Mathlib/Algebra/Order/Monoid/Lemmas.lean
index f5cc3ec3540bd..fd38945089995 100644
--- a/Mathlib/Algebra/Order/Monoid/Lemmas.lean
+++ b/Mathlib/Algebra/Order/Monoid/Lemmas.lean
@@ -318,8 +318,8 @@ by simp_rw [min_le_iff, le_max_iff]; contrapose! h; exact mul_lt_mul_of_lt_of_lt
 end LinearOrder
 
 section LinearOrder
-variable [LinearOrder α] [CovariantClass α α HMUL.hMul LE.le]
-  [CovariantClass α α (swap HMUL.hMul) LE.le] {a b c d : α}
+variable [LinearOrder α] [CovariantClass α α HMul.hMul LE.le]
+  [CovariantClass α α (swap HMul.hMul) LE.le] {a b c d : α}
 
 @[to_additive max_add_add_le_max_add_max]
 theorem max_mul_mul_le_max_mul_max' : max (a * b) (c * d) ≤ max a c * max b d :=
diff --git a/Mathlib/Analysis/Convex/ProjIcc.lean b/Mathlib/Analysis/Convex/ProjIcc.lean
deleted file mode 100644
index e704829159cb0..0000000000000
--- a/Mathlib/Analysis/Convex/ProjIcc.lean
+++ /dev/null
@@ -1,99 +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.Analysis.Convex.Function
-import Mathlib.Data.Set.Intervals.ProjIcc
-
-#align_import analysis.convex.proj_Icc from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
-
-/-!
-# Convexity of extension from intervals
-
-This file proves that constantly extending monotone/antitone functions preserves their convexity.
-
-## TODO
-
-We could deduplicate the proofs if we had a typeclass stating that `segment 𝕜 x y = [x -[𝕜] y]` as
-`𝕜ᵒᵈ` respects it if `𝕜` does, while `𝕜ᵒᵈ` isn't a `LinearOrderedField` if `𝕜` is.
--/
-
-open Set
-
-variable {𝕜 β : Type*} [LinearOrderedField 𝕜] [LinearOrderedAddCommMonoid β] [SMul 𝕜 β] {s : Set 𝕜}
-  {f : 𝕜 → β} {z : 𝕜}
-
-/-- A convex set extended towards minus infinity is convex. -/
-protected theorem Convex.IciExtend (hf : Convex 𝕜 s) :
-    Convex 𝕜 {x | IciExtend (restrict (Ici z) (· ∈ s)) x} := by
-  rw [convex_iff_ordConnected] at hf ⊢; exact hf.restrict.IciExtend
-#align convex.Ici_extend Convex.IciExtend
-
-/-- A convex set extended towards infinity is convex. -/
-protected theorem Convex.IicExtend (hf : Convex 𝕜 s) :
-    Convex 𝕜 {x | IicExtend (restrict (Iic z) (· ∈ s)) x} := by
-  rw [convex_iff_ordConnected] at hf ⊢; exact hf.restrict.IicExtend
-#align convex.Iic_extend Convex.IicExtend
-
-/-- A convex monotone function extended constantly towards minus infinity is convex. -/
-protected theorem ConvexOn.IciExtend (hf : ConvexOn 𝕜 s f) (hf' : MonotoneOn f s) :
-    ConvexOn 𝕜 {x | IciExtend (restrict (Ici z) (· ∈ s)) x} (IciExtend $ restrict (Ici z) f) := by
-  refine' ⟨hf.1.IciExtend, λ x hx y hy a b ha hb hab ↦ _⟩
-  dsimp [IciExtend_apply] at hx hy ⊢
-  refine' (hf' (hf.1.ordConnected.uIcc_subset hx hy $ (Monotone.image_uIcc_subset λ _ _ ↦
-    max_le_max le_rfl) $ mem_image_of_mem _ $ convex_uIcc _ _
-    left_mem_uIcc right_mem_uIcc ha hb hab) (hf.1 hx hy ha hb hab) _).trans (hf.2 hx hy ha hb hab)
-  rw [smul_max ha z, smul_max hb z]
-  refine' le_trans _ max_add_add_le_max_add_max
-  rw [Convex.combo_self hab, smul_eq_mul, smul_eq_mul]
-#align convex_on.Ici_extend ConvexOn.IciExtend
-
-/-- A convex antitone function extended constantly towards infinity is convex. -/
-protected theorem ConvexOn.IicExtend (hf : ConvexOn 𝕜 s f) (hf' : AntitoneOn f s) :
-    ConvexOn 𝕜 {x | IicExtend (restrict (Iic z) (· ∈ s)) x} (IicExtend $ restrict (Iic z) f) := by
-  refine' ⟨hf.1.IicExtend, λ x hx y hy a b ha hb hab ↦ _⟩
-  dsimp [IicExtend_apply] at hx hy ⊢
-  refine' (hf' (hf.1 hx hy ha hb hab) (hf.1.ordConnected.uIcc_subset hx hy $
-    (Monotone.image_uIcc_subset λ _ _ ↦ min_le_min le_rfl) $ mem_image_of_mem _ $ convex_uIcc _ _
-    left_mem_uIcc right_mem_uIcc ha hb hab) _).trans (hf.2 hx hy ha hb hab)
-  rw [smul_min ha z, smul_min hb z]
-  refine' min_add_min_le_min_add_add.trans _
-  rw [Convex.combo_self hab, smul_eq_mul, smul_eq_mul]
-#align convex_on.Iic_extend ConvexOn.IicExtend
-
-/-- A concave antitone function extended constantly minus towards infinity is concave. -/
-protected theorem ConcaveOn.IciExtend (hf : ConcaveOn 𝕜 s f) (hf' : AntitoneOn f s) :
-    ConcaveOn 𝕜 {x | IciExtend (restrict (Ici z) (· ∈ s)) x} (IciExtend $ restrict (Ici z) f) :=
-  hf.dual.IciExtend hf'.dual_right
-#align concave_on.Ici_extend ConcaveOn.IciExtend
-
-/-- A concave monotone function extended constantly towards infinity is concave. -/
-protected theorem ConcaveOn.IicExtend (hf : ConcaveOn 𝕜 s f) (hf' : MonotoneOn f s) :
-    ConcaveOn 𝕜 {x | IicExtend (restrict (Iic z) (· ∈ s)) x} (IicExtend $ restrict (Iic z) f) :=
-  hf.dual.IicExtend hf'.dual_right
-#align concave_on.Iic_extend ConcaveOn.IicExtend
-
-/-- A convex monotone function extended constantly towards minus infinity is convex. -/
-protected theorem ConvexOn.IciExtend_of_monotone (hf : ConvexOn 𝕜 univ f) (hf' : Monotone f) :
-    ConvexOn 𝕜 univ (IciExtend $ restrict (Ici z) f) :=
-  hf.IciExtend $ hf'.monotoneOn _
-#align convex_on.Ici_extend_of_monotone ConvexOn.IciExtend_of_monotone
-
-/-- A convex antitone function extended constantly towards infinity is convex. -/
-protected theorem ConvexOn.IicExtend_of_antitone (hf : ConvexOn 𝕜 univ f) (hf' : Antitone f) :
-    ConvexOn 𝕜 univ (IicExtend $ restrict (Iic z) f) :=
-  hf.IicExtend $ hf'.antitoneOn _
-#align convex_on.Iic_extend_of_antitone ConvexOn.IicExtend_of_antitone
-
-/-- A concave antitone function extended constantly minus towards infinity is concave. -/
-protected theorem ConcaveOn.IciExtend_of_antitone (hf : ConcaveOn 𝕜 univ f) (hf' : Antitone f) :
-    ConcaveOn 𝕜 univ (IciExtend $ restrict (Ici z) f) :=
-  hf.IciExtend $ hf'.antitoneOn _
-#align concave_on.Ici_extend_of_antitone ConcaveOn.IciExtend_of_antitone
-
-/-- A concave monotone function extended constantly towards infinity is concave. -/
-protected theorem ConcaveOn.IicExtend_of_monotone (hf : ConcaveOn 𝕜 univ f) (hf' : Monotone f) :
-    ConcaveOn 𝕜 univ (IicExtend $ restrict (Iic z) f) :=
-  hf.IicExtend $ hf'.monotoneOn _
-#align concave_on.Iic_extend_of_monotone ConcaveOn.IicExtend_of_monotone

From e4d1aa76ba2b7c2f28eaa5b286dd37d9c0168d46 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Tue, 12 Sep 2023 09:31:07 +0000
Subject: [PATCH 09/15] fix align

---
 Mathlib/Data/Set/Intervals/Image.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Set/Intervals/Image.lean b/Mathlib/Data/Set/Intervals/Image.lean
index 5931b463d409a..861e432ab1c79 100644
--- a/Mathlib/Data/Set/Intervals/Image.lean
+++ b/Mathlib/Data/Set/Intervals/Image.lean
@@ -100,13 +100,13 @@ lemma StrictAnti.mapsTo_Ioo (h : StrictAnti f) : MapsTo f (Ioo a b) (Ioo (f b) (
 
 lemma MonotoneOn.image_Ici_subset (h : MonotoneOn f (Ici a)) : f '' Ici a ⊆ Ici (f a) :=
 h.mapsTo_Ici.image_subset
-#align monotone_on.image_Icc_subset MonotoneOn.image_Icc_subset
 
 lemma MonotoneOn.image_Iic_subset (h : MonotoneOn f (Iic b)) : f '' Iic b ⊆ Iic (f b) :=
 h.mapsTo_Iic.image_subset
 
 lemma MonotoneOn.image_Icc_subset (h : MonotoneOn f (Icc a b)) : f '' Icc a b ⊆ Icc (f a) (f b) :=
 h.mapsTo_Icc.image_subset
+#align monotone_on.image_Icc_subset MonotoneOn.image_Icc_subset
 
 lemma AntitoneOn.image_Ici_subset (h : AntitoneOn f (Ici a)) : f '' Ici a ⊆ Iic (f a) :=
 h.mapsTo_Ici.image_subset

From ede0969bede8804b9f679253d7abe29270ab0bb5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Tue, 12 Sep 2023 09:31:37 +0000
Subject: [PATCH 10/15] revert Data.Set.Intervals.Image

---
 Mathlib/Data/Set/Intervals/Image.lean | 269 ++++++--------------------
 1 file changed, 61 insertions(+), 208 deletions(-)

diff --git a/Mathlib/Data/Set/Intervals/Image.lean b/Mathlib/Data/Set/Intervals/Image.lean
index 861e432ab1c79..f41830e5648ee 100644
--- a/Mathlib/Data/Set/Intervals/Image.lean
+++ b/Mathlib/Data/Set/Intervals/Image.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Kim Liesinger. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Liesinger, Yaël Dillies
+Authors: Kim Liesinger
 -/
 import Mathlib.Data.Set.Intervals.Basic
 import Mathlib.Data.Set.Function
@@ -15,237 +15,90 @@ variable {f : α → β}
 
 open Set
 
-section Preorder
-variable [Preorder α] [Preorder β] {a b : α}
+section
+variable [Preorder α] [Preorder β]
 
-lemma MonotoneOn.mapsTo_Ici (h : MonotoneOn f (Ici a)) : MapsTo f (Ici a) (Ici (f a)) :=
-λ _c hc ↦ by aesop
+theorem Monotone.mapsTo_Icc (h : Monotone f) :
+    MapsTo f (Icc a b) (Icc (f a) (f b)) :=
+  fun _ _ => by aesop
 
-lemma MonotoneOn.mapsTo_Iic (h : MonotoneOn f (Iic b)) : MapsTo f (Iic b) (Iic (f b)) :=
-λ _c hc ↦ by aesop
+theorem StrictMono.mapsTo_Ioo (h : StrictMono f) :
+    MapsTo f (Ioo a b) (Ioo (f a) (f b)) :=
+  fun _ _ => by aesop
 
-lemma MonotoneOn.mapsTo_Icc (h : MonotoneOn f (Icc a b)) : MapsTo f (Icc a b) (Icc (f a) (f b)) :=
-λ _c hc ↦
-  ⟨h (left_mem_Icc.2 $ hc.1.trans hc.2) hc hc.1, h hc (right_mem_Icc.2 $ hc.1.trans hc.2) hc.2⟩
+theorem Monotone.mapsTo_Ici  (h : Monotone f) :
+    MapsTo f (Ici a) (Ici (f a)) :=
+  fun _ _ => by aesop
 
-lemma AntitoneOn.mapsTo_Ici (h : AntitoneOn f (Ici a)) : MapsTo f (Ici a) (Iic (f a)) :=
-λ _c hc ↦ by aesop
+theorem Monotone.mapsTo_Iic (h : Monotone f) :
+    MapsTo f (Iic a) (Iic (f a)) :=
+  fun _ _ => by aesop
 
-lemma AntitoneOn.mapsTo_Iic (h : AntitoneOn f (Iic b)) : MapsTo f (Iic b) (Ici (f b)) :=
-λ _c hc ↦ by aesop
+theorem StrictMono.mapsTo_Ioi (h : StrictMono f) :
+    MapsTo f (Ioi a) (Ioi (f a)) :=
+  fun _ _ => by aesop
 
-lemma AntitoneOn.mapsTo_Icc (h : AntitoneOn f (Icc a b)) : MapsTo f (Icc a b) (Icc (f b) (f a)) :=
-λ _c hc ↦
-  ⟨h hc (right_mem_Icc.2 $ hc.1.trans hc.2) hc.2, h (left_mem_Icc.2 $ hc.1.trans hc.2) hc hc.1⟩
+theorem StrictMono.mapsTo_Iio (h : StrictMono f) :
+    MapsTo f (Iio a) (Iio (f a)) :=
+  fun _ _ => by aesop
 
-lemma StrictMonoOn.mapsTo_Ioi (h : StrictMonoOn f (Ici a)) : MapsTo f (Ioi a) (Ioi (f a)) :=
-λ _c hc ↦ h le_rfl hc.le hc
+end
 
-lemma StrictMonoOn.mapsTo_Iio (h : StrictMonoOn f (Iic b)) : MapsTo f (Iio b) (Iio (f b)) :=
-λ _c hc ↦ h hc.le le_rfl hc
-
-lemma StrictMonoOn.mapsTo_Ioo (h : StrictMonoOn f (Icc a b)) :
-  MapsTo f (Ioo a b) (Ioo (f a) (f b)) :=
-λ _c hc ↦
-  ⟨h (left_mem_Icc.2 (hc.1.trans hc.2).le) (Ioo_subset_Icc_self hc) hc.1,
-   h (Ioo_subset_Icc_self hc) (right_mem_Icc.2 (hc.1.trans hc.2).le) hc.2⟩
-
-lemma StrictAntiOn.mapsTo_Ioi (h : StrictAntiOn f (Ici a)) : MapsTo f (Ioi a) (Iio (f a)) :=
-λ _c hc ↦ h le_rfl hc.le hc
-
-lemma StrictAntiOn.mapsTo_Iio (h : StrictAntiOn f (Iic b)) : MapsTo f (Iio b) (Ioi (f b)) :=
-λ _c hc ↦ h hc.le le_rfl hc
-
-lemma StrictAntiOn.mapsTo_Ioo (h : StrictAntiOn f (Icc a b)) :
-  MapsTo f (Ioo a b) (Ioo (f b) (f a)) :=
-λ _c hc ↦
-  ⟨h (Ioo_subset_Icc_self hc) (right_mem_Icc.2 (hc.1.trans hc.2).le) hc.2,
-   h (left_mem_Icc.2 (hc.1.trans hc.2).le) (Ioo_subset_Icc_self hc) hc.1⟩
-
-lemma Monotone.mapsTo_Ici (h : Monotone f) : MapsTo f (Ici a) (Ici (f a)) :=
-(h.monotoneOn _).mapsTo_Ici
-
-lemma Monotone.mapsTo_Iic (h : Monotone f) : MapsTo f (Iic b) (Iic (f b)) :=
-(h.monotoneOn _).mapsTo_Iic
-
-lemma Monotone.mapsTo_Icc (h : Monotone f) : MapsTo f (Icc a b) (Icc (f a) (f b)) :=
-(h.monotoneOn _).mapsTo_Icc
-
-lemma Antitone.mapsTo_Ici (h : Antitone f) : MapsTo f (Ici a) (Iic (f a)) :=
-(h.antitoneOn _).mapsTo_Ici
-
-lemma Antitone.mapsTo_Iic (h : Antitone f) : MapsTo f (Iic b) (Ici (f b)) :=
-(h.antitoneOn _).mapsTo_Iic
-
-lemma Antitone.mapsTo_Icc (h : Antitone f) : MapsTo f (Icc a b) (Icc (f b) (f a)) :=
-(h.antitoneOn _).mapsTo_Icc
-
-lemma StrictMono.mapsTo_Ioi (h : StrictMono f) : MapsTo f (Ioi a) (Ioi (f a)) :=
-(h.strictMonoOn _).mapsTo_Ioi
-
-lemma StrictMono.mapsTo_Iio (h : StrictMono f) : MapsTo f (Iio b) (Iio (f b)) :=
-(h.strictMonoOn _).mapsTo_Iio
-
-lemma StrictMono.mapsTo_Ioo (h : StrictMono f) : MapsTo f (Ioo a b) (Ioo (f a) (f b)) :=
-(h.strictMonoOn _).mapsTo_Ioo
-
-lemma StrictAnti.mapsTo_Ioi (h : StrictAnti f) : MapsTo f (Ioi a) (Iio (f a)) :=
-(h.strictAntiOn _).mapsTo_Ioi
-
-lemma StrictAnti.mapsTo_Iio (h : StrictAnti f) : MapsTo f (Iio b) (Ioi (f b)) :=
-(h.strictAntiOn _).mapsTo_Iio
-
-lemma StrictAnti.mapsTo_Ioo (h : StrictAnti f) : MapsTo f (Ioo a b) (Ioo (f b) (f a)) :=
-(h.strictAntiOn _).mapsTo_Ioo
-
-lemma MonotoneOn.image_Ici_subset (h : MonotoneOn f (Ici a)) : f '' Ici a ⊆ Ici (f a) :=
-h.mapsTo_Ici.image_subset
-
-lemma MonotoneOn.image_Iic_subset (h : MonotoneOn f (Iic b)) : f '' Iic b ⊆ Iic (f b) :=
-h.mapsTo_Iic.image_subset
-
-lemma MonotoneOn.image_Icc_subset (h : MonotoneOn f (Icc a b)) : f '' Icc a b ⊆ Icc (f a) (f b) :=
-h.mapsTo_Icc.image_subset
-#align monotone_on.image_Icc_subset MonotoneOn.image_Icc_subset
-
-lemma AntitoneOn.image_Ici_subset (h : AntitoneOn f (Ici a)) : f '' Ici a ⊆ Iic (f a) :=
-h.mapsTo_Ici.image_subset
-
-lemma AntitoneOn.image_Iic_subset (h : AntitoneOn f (Iic b)) : f '' Iic b ⊆ Ici (f b) :=
-h.mapsTo_Iic.image_subset
-
-lemma AntitoneOn.image_Icc_subset (h : AntitoneOn f (Icc a b)) : f '' Icc a b ⊆ Icc (f b) (f a) :=
-h.mapsTo_Icc.image_subset
-#align antitone_on.image_Icc_subset AntitoneOn.image_Icc_subset
-
-lemma StrictMonoOn.image_Ioi_subset (h : StrictMonoOn f (Ici a)) : f '' Ioi a ⊆ Ioi (f a) :=
-h.mapsTo_Ioi.image_subset
-
-lemma StrictMonoOn.image_Iio_subset (h : StrictMonoOn f (Iic b)) : f '' Iio b ⊆ Iio (f b) :=
-h.mapsTo_Iio.image_subset
-
-lemma StrictMonoOn.image_Ioo_subset (h : StrictMonoOn f (Icc a b)) :
-  f '' Ioo a b ⊆ Ioo (f a) (f b) :=
-h.mapsTo_Ioo.image_subset
-
-lemma StrictAntiOn.image_Ioi_subset (h : StrictAntiOn f (Ici a)) : f '' Ioi a ⊆ Iio (f a) :=
-h.mapsTo_Ioi.image_subset
-
-lemma StrictAntiOn.image_Iio_subset (h : StrictAntiOn f (Iic b)) : f '' Iio b ⊆ Ioi (f b) :=
-h.mapsTo_Iio.image_subset
-
-lemma StrictAntiOn.image_Ioo_subset (h : StrictAntiOn f (Icc a b)) :
-  f '' Ioo a b ⊆ Ioo (f b) (f a) :=
-h.mapsTo_Ioo.image_subset
-
-lemma Monotone.image_Ici_subset (h : Monotone f) : f '' Ici a ⊆ Ici (f a) :=
-(h.monotoneOn _).image_Ici_subset
-
-lemma Monotone.image_Iic_subset (h : Monotone f) : f '' Iic b ⊆ Iic (f b) :=
-(h.monotoneOn _).image_Iic_subset
-
-lemma Monotone.image_Icc_subset (h : Monotone f) : f '' Icc a b ⊆ Icc (f a) (f b) :=
-(h.monotoneOn _).image_Icc_subset
-#align monotone.image_Icc_subset Monotone.image_Icc_subset
-
-lemma Antitone.image_Ici_subset (h : Antitone f) : f '' Ici a ⊆ Iic (f a) :=
-(h.antitoneOn _).image_Ici_subset
-
-lemma Antitone.image_Iic_subset (h : Antitone f) : f '' Iic b ⊆ Ici (f b) :=
-(h.antitoneOn _).image_Iic_subset
-
-lemma Antitone.image_Icc_subset (h : Antitone f) : f '' Icc a b ⊆ Icc (f b) (f a) :=
-(h.antitoneOn _).image_Icc_subset
-#align antitone.image_Icc_subset Antitone.image_Icc_subset
-
-lemma StrictMono.image_Ioi_subset (h : StrictMono f) : f '' Ioi a ⊆ Ioi (f a) :=
-(h.strictMonoOn _).image_Ioi_subset
-
-lemma StrictMono.image_Iio_subset (h : StrictMono f) : f '' Iio b ⊆ Iio (f b) :=
-(h.strictMonoOn _).image_Iio_subset
-
-lemma StrictMono.image_Ioo_subset (h : StrictMono f) : f '' Ioo a b ⊆ Ioo (f a) (f b) :=
-(h.strictMonoOn _).image_Ioo_subset
-
-lemma StrictAnti.image_Ioi_subset (h : StrictAnti f) : f '' Ioi a ⊆ Iio (f a) :=
-(h.strictAntiOn _).image_Ioi_subset
-
-lemma StrictAnti.image_Iio_subset (h : StrictAnti f) : f '' Iio b ⊆ Ioi (f b) :=
-(h.strictAntiOn _).image_Iio_subset
-
-lemma StrictAnti.image_Ioo_subset (h : StrictAnti f) : f '' Ioo a b ⊆ Ioo (f b) (f a) :=
-(h.strictAntiOn _).image_Ioo_subset
-
-end Preorder
-
-section PartialOrder
+section
 variable [PartialOrder α] [Preorder β]
 
-lemma StrictMonoOn.mapsTo_Ico (h : StrictMonoOn f (Icc a b)) :
-  MapsTo f (Ico a b) (Ico (f a) (f b)) :=
-λ _c hc ↦
-  ⟨h.monotoneOn (left_mem_Icc.2 $ hc.1.trans hc.2.le) (Ico_subset_Icc_self hc) hc.1,
-   h (Ico_subset_Icc_self hc) (right_mem_Icc.2 $ hc.1.trans hc.2.le) hc.2⟩
-
-lemma StrictMonoOn.mapsTo_Ioc (h : StrictMonoOn f (Icc a b)) :
-  MapsTo f (Ioc a b) (Ioc (f a) (f b)) :=
-λ _c hc ↦
-  ⟨h (left_mem_Icc.2 $ hc.1.le.trans hc.2) (Ioc_subset_Icc_self hc) hc.1,
-   h.monotoneOn (Ioc_subset_Icc_self hc) (right_mem_Icc.2 $ hc.1.le.trans hc.2) hc.2⟩
+theorem StrictMono.mapsTo_Ico (h : StrictMono f) :
+    MapsTo f (Ico a b) (Ico (f a) (f b)) :=
+  -- It makes me sad that `aesop` doesn't do this. There are clearly missing lemmas.
+  fun _ m => ⟨h.monotone m.1, h m.2⟩
 
-lemma StrictAntiOn.mapsTo_Ico (h : StrictAntiOn f (Icc a b)) :
-  MapsTo f (Ico a b) (Ioc (f b) (f a)) :=
-λ _c hc ↦
-  ⟨h (Ico_subset_Icc_self hc) (right_mem_Icc.2 $ hc.1.trans hc.2.le) hc.2,
-   h.antitoneOn (left_mem_Icc.2 $ hc.1.trans hc.2.le) (Ico_subset_Icc_self hc) hc.1⟩
+theorem StrictMono.mapsTo_Ioc (h : StrictMono f) :
+    MapsTo f (Ioc a b) (Ioc (f a) (f b)) :=
+  fun _ m => ⟨h m.1, h.monotone m.2⟩
 
-lemma StrictAntiOn.mapsTo_Ioc (h : StrictAntiOn f (Icc a b)) :
-  MapsTo f (Ioc a b) (Ico (f b) (f a)) :=
-λ _c hc ↦
-  ⟨h.antitoneOn (Ioc_subset_Icc_self hc) (right_mem_Icc.2 $ hc.1.le.trans hc.2) hc.2,
-   h (left_mem_Icc.2 $ hc.1.le.trans hc.2) (Ioc_subset_Icc_self hc) hc.1⟩
+end
 
-lemma StrictMono.mapsTo_Ico (h : StrictMono f) : MapsTo f (Ico a b) (Ico (f a) (f b)) :=
-(h.strictMonoOn _).mapsTo_Ico
+section
+variable [Preorder α] [Preorder β]
 
-lemma StrictMono.mapsTo_Ioc (h : StrictMono f) : MapsTo f (Ioc a b) (Ioc (f a) (f b)) :=
-(h.strictMonoOn _).mapsTo_Ioc
+theorem Monotone.image_Icc_subset (h : Monotone f) :
+    f '' Icc a b ⊆ Icc (f a) (f b) :=
+  h.mapsTo_Icc.image_subset
 
-lemma StrictAnti.mapsTo_Ico (h : StrictAnti f) : MapsTo f (Ico a b) (Ioc (f b) (f a)) :=
-(h.strictAntiOn _).mapsTo_Ico
+theorem StrictMono.image_Ioo_subset (h : StrictMono f) :
+    f '' Ioo a b ⊆ Ioo (f a) (f b) :=
+  h.mapsTo_Ioo.image_subset
 
-lemma StrictAnti.mapsTo_Ioc (h : StrictAnti f) : MapsTo f (Ioc a b) (Ico (f b) (f a)) :=
-(h.strictAntiOn _).mapsTo_Ioc
+theorem Monotone.image_Ici_subset (h : Monotone f) :
+    f '' Ici a ⊆ Ici (f a) :=
+  h.mapsTo_Ici.image_subset
 
-lemma StrictMonoOn.image_Ico_subset (h : StrictMonoOn f (Icc a b)) :
-  f '' Ico a b ⊆ Ico (f a) (f b) :=
-h.mapsTo_Ico.image_subset
+theorem Monotone.image_Iic_subset (h : Monotone f) :
+    f '' Iic a ⊆ Iic (f a) :=
+  h.mapsTo_Iic.image_subset
 
-lemma StrictMonoOn.image_Ioc_subset (h : StrictMonoOn f (Icc a b)) :
-  f '' Ioc a b ⊆ Ioc (f a) (f b) :=
-h.mapsTo_Ioc.image_subset
+theorem StrictMono.image_Ioi_subset (h : StrictMono f) :
+    f '' Ioi a ⊆ Ioi (f a) :=
+  h.mapsTo_Ioi.image_subset
 
-lemma StrictAntiOn.image_Ico_subset (h : StrictAntiOn f (Icc a b)) :
-  f '' Ico a b ⊆ Ioc (f b) (f a) :=
-h.mapsTo_Ico.image_subset
+theorem StrictMono.image_Iio_subset (h : StrictMono f) :
+    f '' Iio a ⊆ Iio (f a) :=
+  h.mapsTo_Iio.image_subset
 
-lemma StrictAntiOn.image_Ioc_subset (h : StrictAntiOn f (Icc a b)) :
-  f '' Ioc a b ⊆ Ico (f b) (f a) :=
-h.mapsTo_Ioc.image_subset
+end
 
-lemma StrictMono.image_Ico_subset (h : StrictMono f) : f '' Ico a b ⊆ Ico (f a) (f b) :=
-(h.strictMonoOn _).image_Ico_subset
-
-lemma StrictMono.image_Ioc_subset (h : StrictMono f) : f '' Ioc a b ⊆ Ioc (f a) (f b) :=
-(h.strictMonoOn _).image_Ioc_subset
+section
+variable [PartialOrder α] [Preorder β]
 
-lemma StrictAnti.image_Ico_subset (h : StrictAnti f) : f '' Ico a b ⊆ Ioc (f b) (f a) :=
-(h.strictAntiOn _).image_Ico_subset
+theorem StrictMono.imageIco_subset (h : StrictMono f) :
+    f '' Ico a b ⊆ Ico (f a) (f b) :=
+  h.mapsTo_Ico.image_subset
 
-lemma StrictAnti.image_Ioc_subset (h : StrictAnti f) : f '' Ioc a b ⊆ Ico (f b) (f a) :=
-(h.strictAntiOn _).image_Ioc_subset
+theorem StrictMono.imageIoc_subset (h : StrictMono f) :
+    f '' Ioc a b ⊆ Ioc (f a) (f b) :=
+  h.mapsTo_Ioc.image_subset
 
-end PartialOrder
+end
 
 namespace Set
 

From fc49843c6450561995f73c84e33edf4a17d82c98 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Tue, 12 Sep 2023 09:44:19 +0000
Subject: [PATCH 11/15] fix all

---
 Mathlib.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 65b6162bb14a4..38d34591b6689 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -649,7 +649,6 @@ import Mathlib.Analysis.Convex.KreinMilman
 import Mathlib.Analysis.Convex.Measure
 import Mathlib.Analysis.Convex.Normed
 import Mathlib.Analysis.Convex.PartitionOfUnity
-import Mathlib.Analysis.Convex.ProjIcc
 import Mathlib.Analysis.Convex.Quasiconvex
 import Mathlib.Analysis.Convex.Segment
 import Mathlib.Analysis.Convex.Side

From 82f4495a2ac19208373a64e6638e545235f3053f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Tue, 12 Sep 2023 09:59:12 +0000
Subject: [PATCH 12/15] revert Data.Set.Intervals.UnorderedInterval

---
 .../Data/Set/Intervals/UnorderedInterval.lean | 46 ++-----------------
 1 file changed, 3 insertions(+), 43 deletions(-)

diff --git a/Mathlib/Data/Set/Intervals/UnorderedInterval.lean b/Mathlib/Data/Set/Intervals/UnorderedInterval.lean
index 722f4369675c6..9db65a92d4dba 100644
--- a/Mathlib/Data/Set/Intervals/UnorderedInterval.lean
+++ b/Mathlib/Data/Set/Intervals/UnorderedInterval.lean
@@ -3,11 +3,11 @@ Copyright (c) 2020 Zhouhang Zhou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhouhang Zhou
 -/
-import Mathlib.Data.Set.Intervals.Image
 import Mathlib.Order.Bounds.Basic
+import Mathlib.Data.Set.Intervals.Basic
 import Mathlib.Tactic.Common
 
-#align_import data.set.intervals.unordered_interval from "leanprover-community/mathlib"@"3ba15165bd6927679be7c22d6091a87337e3cd0c"
+#align_import data.set.intervals.unordered_interval from "leanprover-community/mathlib"@"4020ddee5b4580a409bfda7d2f42726ce86ae674"
 
 /-!
 # Intervals without endpoints ordering
@@ -180,48 +180,8 @@ lemma uIcc_injective_left (a : α) : Injective (uIcc a) := by
 end DistribLattice
 
 section LinearOrder
-variable [LinearOrder α]
 
-section Lattice
-variable [Lattice β] {f : α → β} {s : Set α} {a b : α}
-
-lemma _root_.MonotoneOn.mapsTo_uIcc (hf : MonotoneOn f (uIcc a b)) :
-  MapsTo f (uIcc a b) (uIcc (f a) (f b)) := by
-  rw [uIcc, uIcc, ←hf.map_sup, ←hf.map_inf] <;>
-    apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]
-
-lemma _root_.AntitoneOn.mapsTo_uIcc (hf : AntitoneOn f (uIcc a b)) :
-  MapsTo f (uIcc a b) (uIcc (f a) (f b)) := by
-  rw [uIcc, uIcc, ←hf.map_sup, ←hf.map_inf] <;>
-    apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]
-
-lemma _root_.Monotone.mapsTo_uIcc (hf : Monotone f) : MapsTo f (uIcc a b) (uIcc (f a) (f b)) :=
-  (hf.monotoneOn _).mapsTo_uIcc
-
-lemma _root_.Antitone.mapsTo_uIcc (hf : Antitone f) : MapsTo f (uIcc a b) (uIcc (f a) (f b)) :=
-  (hf.antitoneOn _).mapsTo_uIcc
-
-lemma _root_.MonotoneOn.image_uIcc_subset (hf : MonotoneOn f (uIcc a b)) :
-  f '' uIcc a b ⊆ uIcc (f a) (f b) :=
-hf.mapsTo_uIcc.image_subset
-#align monotone_on.image_uIcc_subset MonotoneOn.image_uIcc_subset
-
-lemma _root_.AntitoneOn.image_uIcc_subset (hf : AntitoneOn f (uIcc a b)) :
-  f '' uIcc a b ⊆ uIcc (f a) (f b) :=
-hf.mapsTo_uIcc.image_subset
-#align antitone_on.image_uIcc_subset AntitoneOn.image_uIcc_subset
-
-lemma _root_.Monotone.image_uIcc_subset (hf : Monotone f) : f '' uIcc a b ⊆ uIcc (f a) (f b) :=
-  (hf.monotoneOn _).image_uIcc_subset
-#align monotone.image_uIcc_subset Monotone.image_uIcc_subset
-
-lemma _root_.Antitone.image_uIcc_subset (hf : Antitone f) : f '' uIcc a b ⊆ uIcc (f a) (f b) :=
-  (hf.antitoneOn _).image_uIcc_subset
-#align antitone.image_uIcc_subset Antitone.image_uIcc_subset
-
-end Lattice
-
-variable [LinearOrder β] {f : α → β} {s : Set α} {a a₁ a₂ b b₁ b₂ c d x : α}
+variable [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} {a a₁ a₂ b b₁ b₂ c x : α}
 
 theorem Icc_min_max : Icc (min a b) (max a b) = [[a, b]] :=
   rfl

From b476ebb8fdd70425dd015bfa0ce8a64e3b17cbce Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 13 Sep 2023 09:24:15 +0100
Subject: [PATCH 13/15] Add missing align

---
 Mathlib/Data/Set/Intervals/Image.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Data/Set/Intervals/Image.lean b/Mathlib/Data/Set/Intervals/Image.lean
index f41830e5648ee..ffb3d9a296ed2 100644
--- a/Mathlib/Data/Set/Intervals/Image.lean
+++ b/Mathlib/Data/Set/Intervals/Image.lean
@@ -64,6 +64,7 @@ variable [Preorder α] [Preorder β]
 theorem Monotone.image_Icc_subset (h : Monotone f) :
     f '' Icc a b ⊆ Icc (f a) (f b) :=
   h.mapsTo_Icc.image_subset
+#align monotone.image_Icc_subset Monotone.image_Icc_subset
 
 theorem StrictMono.image_Ioo_subset (h : StrictMono f) :
     f '' Ioo a b ⊆ Ioo (f a) (f b) :=

From 14a7c4c32e27ef5f1c2bd68c4564f1e88dc7e69b Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 5 Oct 2023 22:57:42 +0100
Subject: [PATCH 14/15] Add aligns

---
 Mathlib/Data/Set/Intervals/Image.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Mathlib/Data/Set/Intervals/Image.lean b/Mathlib/Data/Set/Intervals/Image.lean
index 54820fd0fb753..1e1ca90b1cb4c 100644
--- a/Mathlib/Data/Set/Intervals/Image.lean
+++ b/Mathlib/Data/Set/Intervals/Image.lean
@@ -110,6 +110,7 @@ lemma MonotoneOn.image_Iic_subset (h : MonotoneOn f (Iic b)) : f '' Iic b ⊆ Ii
 
 lemma MonotoneOn.image_Icc_subset (h : MonotoneOn f (Icc a b)) : f '' Icc a b ⊆ Icc (f a) (f b) :=
   h.mapsTo_Icc.image_subset
+#align monotone_on.image_Icc_subset MonotoneOn.image_Icc_subset
 
 lemma AntitoneOn.image_Ici_subset (h : AntitoneOn f (Ici a)) : f '' Ici a ⊆ Iic (f a) :=
   h.mapsTo_Ici.image_subset
@@ -119,6 +120,7 @@ lemma AntitoneOn.image_Iic_subset (h : AntitoneOn f (Iic b)) : f '' Iic b ⊆ Ic
 
 lemma AntitoneOn.image_Icc_subset (h : AntitoneOn f (Icc a b)) : f '' Icc a b ⊆ Icc (f b) (f a) :=
   h.mapsTo_Icc.image_subset
+#align antitone_on.image_Icc_subset AntitoneOn.image_Icc_subset
 
 lemma StrictMonoOn.image_Ioi_subset (h : StrictMonoOn f (Ici a)) : f '' Ioi a ⊆ Ioi (f a) :=
   h.mapsTo_Ioi.image_subset
@@ -146,6 +148,7 @@ lemma Monotone.image_Iic_subset (h : Monotone f) : f '' Iic b ⊆ Iic (f b) :=
 
 lemma Monotone.image_Icc_subset (h : Monotone f) : f '' Icc a b ⊆ Icc (f a) (f b) :=
   (h.monotoneOn _).image_Icc_subset
+#align monotone.image_Icc_subset Monotone.image_Icc_subset
 
 lemma Antitone.image_Ici_subset (h : Antitone f) : f '' Ici a ⊆ Iic (f a) :=
   (h.antitoneOn _).image_Ici_subset
@@ -155,6 +158,7 @@ lemma Antitone.image_Iic_subset (h : Antitone f) : f '' Iic b ⊆ Ici (f b) :=
 
 lemma Antitone.image_Icc_subset (h : Antitone f) : f '' Icc a b ⊆ Icc (f b) (f a) :=
   (h.antitoneOn _).image_Icc_subset
+#align antitone.image_Icc_subset Antitone.image_Icc_subset
 
 lemma StrictMono.image_Ioi_subset (h : StrictMono f) : f '' Ioi a ⊆ Ioi (f a) :=
   (h.strictMonoOn _).image_Ioi_subset

From db766ae704021c23bb74e262c494c9a023f7010e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Fri, 6 Oct 2023 08:03:22 +0000
Subject: [PATCH 15/15] revert uglification

---
 Mathlib/Algebra/Order/Monoid/Lemmas.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/Order/Monoid/Lemmas.lean b/Mathlib/Algebra/Order/Monoid/Lemmas.lean
index 118d5a04900ef..7b1fa597fdda3 100644
--- a/Mathlib/Algebra/Order/Monoid/Lemmas.lean
+++ b/Mathlib/Algebra/Order/Monoid/Lemmas.lean
@@ -358,8 +358,8 @@ variable [LinearOrder α] {a b c d : α}
 end LinearOrder
 
 section LinearOrder
-variable [LinearOrder α] [CovariantClass α α HMul.hMul LE.le]
-  [CovariantClass α α (swap HMul.hMul) LE.le] {a b c d : α}
+variable [LinearOrder α] [CovariantClass α α (· * ·) (· ≤ ·)]
+  [CovariantClass α α (swap (· * ·)) (· ≤ ·)] {a b c d : α}
 
 @[to_additive max_add_add_le_max_add_max]
 theorem max_mul_mul_le_max_mul_max' : max (a * b) (c * d) ≤ max a c * max b d :=