diff --git a/Archive/Imo/Imo1982Q1.lean b/Archive/Imo/Imo1982Q1.lean
index ef97cd79289882..544af84ecc0474 100644
--- a/Archive/Imo/Imo1982Q1.lean
+++ b/Archive/Imo/Imo1982Q1.lean
@@ -93,7 +93,7 @@ lemma part_1 : 660 ≤ f (1980) := by
 lemma part_2 : f 1980 ≤ 660 := by
   have h : 5 * f 1980 + 33 * f 3 ≤ 5 * 660 + 33 := by
     calc (5 : ℕ+) * f 1980 + (33 : ℕ+) * f 3 ≤ f (5 * 1980 + 33 * 3) := by apply hf.superlinear
-    _ = f 9999 := by rfl
+    _ = f 9999 := rfl
     _ = 5 * 660 + 33 := by rw [hf.f_9999]
   rw [hf.f₃, mul_one] at h
   -- from 5 * f 1980 + 33 ≤ 5 * 660 + 33 we show f 1980 ≤ 660
diff --git a/Counterexamples/CharPZeroNeCharZero.lean b/Counterexamples/CharPZeroNeCharZero.lean
index 39e01fe8e56397..fcb0eb5e258ee4 100644
--- a/Counterexamples/CharPZeroNeCharZero.lean
+++ b/Counterexamples/CharPZeroNeCharZero.lean
@@ -24,7 +24,7 @@ namespace Counterexample
 
 @[simp]
 theorem add_one_eq_one (x : WithZero Unit) : x + 1 = 1 :=
-  WithZero.cases_on x (by rfl) fun h => by rfl
+  WithZero.cases_on x rfl fun h => by rfl
 
 theorem withZero_unit_charP_zero : CharP (WithZero Unit) 0 :=
   ⟨fun x => by cases x <;> simp⟩
diff --git a/Mathlib.lean b/Mathlib.lean
index 2ac87fdbac13e4..2ba33f02117f1e 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6202,6 +6202,7 @@ public import Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
 public import Mathlib.Probability.CondVar
 public import Mathlib.Probability.ConditionalExpectation
 public import Mathlib.Probability.ConditionalProbability
+public import Mathlib.Probability.Decision.BayesEstimator
 public import Mathlib.Probability.Decision.Risk.Basic
 public import Mathlib.Probability.Decision.Risk.Countable
 public import Mathlib.Probability.Decision.Risk.Defs
@@ -6491,6 +6492,7 @@ public import Mathlib.RingTheory.Extension.Cotangent.Basic
 public import Mathlib.RingTheory.Extension.Cotangent.Basis
 public import Mathlib.RingTheory.Extension.Cotangent.Free
 public import Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
+public import Mathlib.RingTheory.Extension.ExtendScalars
 public import Mathlib.RingTheory.Extension.Generators
 public import Mathlib.RingTheory.Extension.Presentation.Basic
 public import Mathlib.RingTheory.Extension.Presentation.Core
diff --git a/Mathlib/Algebra/DirectSum/Internal.lean b/Mathlib/Algebra/DirectSum/Internal.lean
index 4aeb4fab711013..b0f553a0a9d362 100644
--- a/Mathlib/Algebra/DirectSum/Internal.lean
+++ b/Mathlib/Algebra/DirectSum/Internal.lean
@@ -320,7 +320,7 @@ theorem Submodule.iSup_eq_toSubmodule_range [AddMonoid ι] [CommSemiring S] [Sem
 theorem DirectSum.coeAlgHom_of [AddMonoid ι] [CommSemiring S] [Semiring R] [Algebra S R]
     (A : ι → Submodule S R) [SetLike.GradedMonoid A] (i : ι) (x : A i) :
     DirectSum.coeAlgHom A (DirectSum.of (fun i => A i) i x) = x :=
-  DirectSum.toSemiring_of _ (by rfl) (fun _ _ => (by rfl)) _ _
+  DirectSum.toSemiring_of _ rfl (fun _ _ => rfl) _ _
 
 end DirectSum
 
diff --git a/Mathlib/Algebra/Order/CauSeq/Completion.lean b/Mathlib/Algebra/Order/CauSeq/Completion.lean
index b48635495389f0..9d8794438abc3f 100644
--- a/Mathlib/Algebra/Order/CauSeq/Completion.lean
+++ b/Mathlib/Algebra/Order/CauSeq/Completion.lean
@@ -142,7 +142,7 @@ theorem ofRat_injective : Function.Injective (ofRat : β → Cauchy abv) := fun
   simpa [ofRat, mk_eq, ← const_sub, const_limZero, sub_eq_zero] using h
 
 instance Cauchy.ring : Ring (Cauchy abv) := fast_instance%
-  Function.Surjective.ring mk Quotient.mk'_surjective (by rfl) (by rfl)
+  Function.Surjective.ring mk Quotient.mk'_surjective rfl rfl
     (fun _ _ => (mk_add _ _).symm) (fun _ _ => (mk_mul _ _).symm) (fun _ => (mk_neg _).symm)
     (fun _ _ => (mk_sub _ _).symm) (fun _ _ => (mk_smul _ _).symm) (fun _ _ => (mk_smul _ _).symm)
     (fun _ _ => (mk_pow _ _).symm) (fun _ => rfl) fun _ => rfl
@@ -170,7 +170,7 @@ variable {α : Type*} [Field α] [LinearOrder α] [IsStrictOrderedRing α]
 variable {β : Type*} [CommRing β] {abv : β → α} [IsAbsoluteValue abv]
 
 instance Cauchy.commRing : CommRing (Cauchy abv) := fast_instance%
-  Function.Surjective.commRing mk Quotient.mk'_surjective (by rfl) (by rfl)
+  Function.Surjective.commRing mk Quotient.mk'_surjective rfl rfl
     (fun _ _ => (mk_add _ _).symm) (fun _ _ => (mk_mul _ _).symm) (fun _ => (mk_neg _).symm)
     (fun _ _ => (mk_sub _ _).symm) (fun _ _ => (mk_smul _ _).symm) (fun _ _ => (mk_smul _ _).symm)
     (fun _ _ => (mk_pow _ _).symm) (fun _ => rfl) fun _ => rfl
diff --git a/Mathlib/Algebra/Order/Module/PositiveLinearMap.lean b/Mathlib/Algebra/Order/Module/PositiveLinearMap.lean
index b5141ae70a6e97..e32de62a976895 100644
--- a/Mathlib/Algebra/Order/Module/PositiveLinearMap.lean
+++ b/Mathlib/Algebra/Order/Module/PositiveLinearMap.lean
@@ -38,7 +38,7 @@ add_decl_doc PositiveLinearMap.toOrderHom
 /-- Notation for a `PositiveLinearMap`. -/
 notation:25 E " →ₚ[" R:25 "] " F:0 => PositiveLinearMap R E F
 
-namespace PositiveLinearMapClass
+section PositiveLinearMapClass
 
 variable {F R E₁ E₂ : Type*} [Semiring R]
   [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂]
@@ -46,16 +46,15 @@ variable {F R E₁ E₂ : Type*} [Semiring R]
   [OrderHomClass F E₁ E₂]
 
 /-- Reinterpret an element of a type of positive linear maps as a positive linear map. -/
-def toPositiveLinearMap (f : F) : E₁ →ₚ[R] E₂ :=
+def PositiveLinearMap.ofClass (f : F) : E₁ →ₚ[R] E₂ :=
   { (f : E₁ →ₗ[R] E₂), (f : E₁ →o E₂) with }
 
-/-- Reinterpret an element of a type of positive linear maps as a positive linear map. -/
-instance instCoeToLinearMap : CoeHead F (E₁ →ₚ[R] E₂) where
-  coe f := toPositiveLinearMap f
+@[deprecated (since := "2026-06-10")]
+alias PositiveLinearMapClass.toPositiveLinearMap := PositiveLinearMap.ofClass
 
-/-- An additive group homomorphism that maps nonnegative elements to nonnegative elements
-is an order homomorphism. -/
-lemma _root_.OrderHomClass.of_addMonoidHom {F' E₁' E₂' : Type*} [FunLike F' E₁' E₂'] [AddGroup E₁']
+/-- A type of additive group homomorphisms that map nonnegative elements to nonnegative elements
+is also a type of order homomorphisms. -/
+lemma OrderHomClass.of_addMonoidHom {F' E₁' E₂' : Type*} [FunLike F' E₁' E₂'] [AddGroup E₁']
     [LE E₁'] [AddRightMono E₁'] [AddGroup E₂'] [LE E₂'] [AddRightMono E₂']
     [AddMonoidHomClass F' E₁' E₂']
     (h : ∀ f : F', ∀ x, 0 ≤ x → 0 ≤ f x) : OrderHomClass F' E₁' E₂' where
@@ -67,9 +66,11 @@ namespace PositiveLinearMap
 
 section general
 
-variable {R E₁ E₂ : Type*} [Semiring R]
-  [AddCommMonoid E₁] [PartialOrder E₁] [AddCommMonoid E₂] [PartialOrder E₂]
-  [Module R E₁] [Module R E₂]
+variable {R E₁ E₂ E₃ : Type*} [Semiring R]
+    [AddCommMonoid E₁] [PartialOrder E₁]
+    [AddCommMonoid E₂] [PartialOrder E₂]
+    [AddCommMonoid E₃] [PartialOrder E₃]
+    [Module R E₁] [Module R E₂] [Module R E₃]
 
 instance : FunLike (E₁ →ₚ[R] E₂) E₁ E₂ where
   coe f := f.toFun
@@ -80,10 +81,33 @@ instance : FunLike (E₁ →ₚ[R] E₂) E₁ E₂ where
     apply DFunLike.coe_injective
     exact h
 
+initialize_simps_projections PositiveLinearMap (toFun → apply, as_prefix toLinearMap)
+
 @[ext]
 lemma ext {f g : E₁ →ₚ[R] E₂} (h : ∀ x, f x = g x) : f = g :=
   DFunLike.ext f g h
 
+variable (R E₁) in
+/-- The identity as a positive linear map. -/
+@[simps! apply toLinearMap] protected def id : E₁ →ₚ[R] E₁ where
+  __ := LinearMap.id
+  __ := OrderHom.id
+
+@[simp] lemma toOrderHom_id : (PositiveLinearMap.id R E₁).toOrderHom = .id := rfl
+
+/-- The composition of positive linear maps is again a positive linear map. -/
+@[simps! apply toLinearMap]
+def comp (g : E₂ →ₚ[R] E₃) (f : E₁ →ₚ[R] E₂) : E₁ →ₚ[R] E₃ where
+  toLinearMap := g.toLinearMap.comp f.toLinearMap
+  monotone' := g.monotone'.comp f.monotone'
+
+@[simp] lemma toOrderHom_comp (g : E₂ →ₚ[R] E₃) (f : E₁ →ₚ[R] E₂) :
+    (g.comp f).toOrderHom = g.toOrderHom.comp f.toOrderHom :=
+  rfl
+
+@[simp] lemma comp_id (f : E₁ →ₚ[R] E₂) : f.comp (.id R E₁) = f := rfl
+@[simp] lemma id_comp (f : E₁ →ₚ[R] E₂) : (PositiveLinearMap.id R E₂).comp f = f := rfl
+
 instance : LinearMapClass (E₁ →ₚ[R] E₂) R E₁ E₂ where
   map_add f := map_add f.toLinearMap
   map_smulₛₗ f := f.toLinearMap.map_smul'
diff --git a/Mathlib/Algebra/Order/Star/Basic.lean b/Mathlib/Algebra/Order/Star/Basic.lean
index 5e2ab31abba409..99fa9e39b070f5 100644
--- a/Mathlib/Algebra/Order/Star/Basic.lean
+++ b/Mathlib/Algebra/Order/Star/Basic.lean
@@ -171,7 +171,7 @@ section NonUnitalSemiring
 
 variable [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R]
 
-lemma IsSelfAdjoint.mono {x y : R} (h : x ≤ y) (hx : IsSelfAdjoint x) : IsSelfAdjoint y := by
+lemma IsSelfAdjoint.of_ge {x y : R} (h : x ≤ y) (hx : IsSelfAdjoint x) : IsSelfAdjoint y := by
   rw [StarOrderedRing.le_iff] at h
   obtain ⟨d, hd, rfl⟩ := h
   rw [IsSelfAdjoint, star_add, hx.star_eq]
@@ -180,9 +180,11 @@ lemma IsSelfAdjoint.mono {x y : R} (h : x ≤ y) (hx : IsSelfAdjoint x) : IsSelf
   rintro - ⟨s, rfl⟩
   simp
 
+@[deprecated (since := "2026-06-12")] alias IsSelfAdjoint.mono := IsSelfAdjoint.of_ge
+
 @[aesop 10% apply, grind ←]
 lemma IsSelfAdjoint.of_nonneg {x : R} (hx : 0 ≤ x) : IsSelfAdjoint x :=
-  .mono hx <| .zero R
+  .of_ge hx <| .zero R
 
 /-- An alias of `IsSelfAdjoint.of_nonneg` for use with dot notation. -/
 alias LE.le.isSelfAdjoint := IsSelfAdjoint.of_nonneg
@@ -204,6 +206,7 @@ protected theorem IsSelfAdjoint.mul_self_nonneg {a : R} (ha : IsSelfAdjoint a) :
   simpa [ha.star_eq] using star_mul_self_nonneg a
 
 /-- A star projection is non-negative in a star-ordered ring. -/
+@[grind →, aesop safe forward (rule_sets := [CStarAlgebra])]
 theorem IsStarProjection.nonneg {p : R} (hp : IsStarProjection p) : 0 ≤ p :=
   hp.isIdempotentElem ▸ hp.isSelfAdjoint.mul_self_nonneg
 
@@ -316,6 +319,19 @@ theorem mul_star_self_pos [Nontrivial R] {x : R} (hx : IsRegular x) : 0 < x * st
 
 end NonUnitalSemiring
 
+section NonUnitalRing
+
+variable [NonUnitalRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R]
+
+lemma IsSelfAdjoint.iff_of_le {a b : R} (hab : a ≤ b) :
+    IsSelfAdjoint a ↔ IsSelfAdjoint b := by
+  replace hab := (sub_nonneg.mpr hab).isSelfAdjoint
+  aesop (add simp IsSelfAdjoint)
+
+alias ⟨_, IsSelfAdjoint.of_le⟩ := IsSelfAdjoint.iff_of_le
+
+end NonUnitalRing
+
 section Semiring
 variable [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R]
 
diff --git a/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean b/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
index ab32228a31290d..0e759020348256 100644
--- a/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
+++ b/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
@@ -158,6 +158,11 @@ lemma eventually_star_eq {l : Filter A} (hl : l.IsIncreasingApproximateUnit) :
     ∀ᶠ x in l, star x = x :=
   hl.eventually_isSelfAdjoint.mp <| .of_forall fun _ ↦ IsSelfAdjoint.star_eq
 
+omit [StarOrderedRing A] in
+lemma closedBall_mem {l : Filter A} (hl : l.IsIncreasingApproximateUnit) :
+    Metric.closedBall 0 1 ∈ l := by
+  simpa [Metric.closedBall] using! hl.eventually_norm
+
 lemma pure_one (A : Type*) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] :
     (pure 1 : Filter A).IsIncreasingApproximateUnit where
   toIsApproximateUnit := .pure_one A
@@ -326,6 +331,8 @@ lemma increasingApproximateUnit :
   neBot := hasBasis_approximateUnit A |>.neBot_iff.mpr
     fun hx ↦ ⟨_, ⟨le_rfl, by simpa using hx.2.le⟩⟩
 
+instance : (approximateUnit A).NeBot := (increasingApproximateUnit A).neBot
+
 end CStarAlgebra
 
 end ApproximateUnit
diff --git a/Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean b/Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean
index dc4dabe59f7fbd..a5d0adb3aab838 100644
--- a/Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean
+++ b/Mathlib/Analysis/CStarAlgebra/PositiveLinearMap.lean
@@ -130,7 +130,7 @@ instance {F : Type*} [FunLike F A₁ A₂] [LinearMapClass F ℂ A₁ A₂] [Ord
     ContinuousLinearMapClass F ℂ A₁ A₂ where
   map_continuous f := by
     have hbound : ∃ C : ℝ, ∀ a, ‖f a‖ ≤ C * ‖a‖ := by
-      obtain ⟨C, h⟩ := exists_norm_apply_le (f : A₁ →ₚ[ℂ] A₂)
+      obtain ⟨C, h⟩ := exists_norm_apply_le (.ofClass f)
       exact ⟨C, h⟩
     exact (LinearMap.mkContinuousOfExistsBound (f : A₁ →ₗ[ℂ] A₂) hbound).continuous
 
diff --git a/Mathlib/Analysis/Complex/Exponential.lean b/Mathlib/Analysis/Complex/Exponential.lean
index d2ba768f73a164..4fbc28c76c4d3e 100644
--- a/Mathlib/Analysis/Complex/Exponential.lean
+++ b/Mathlib/Analysis/Complex/Exponential.lean
@@ -11,6 +11,8 @@ public import Mathlib.Algebra.Order.CauSeq.BigOperators
 public import Mathlib.Algebra.Order.Star.Basic
 public import Mathlib.Data.Complex.BigOperators
 public import Mathlib.Data.Nat.Choose.Sum
+public import Mathlib.Tactic.NormNum.BigOperators
+public import Mathlib.Tactic.NormNum.NatFactorial
 
 /-!
 # Exponential Function
@@ -648,12 +650,35 @@ theorem one_sub_div_pow_le_exp_neg {n : ℕ} {t : ℝ} (ht' : t ≤ n) : (1 - t
       · exact one_sub_le_exp_neg _
     _ = rexp (-t) := by rw [← Real.exp_nat_mul, mul_neg, mul_comm, div_mul_cancel₀]; positivity
 
+lemma one_add_inv_pow_le_exp {n : ℕ} : (1 + (n : ℝ)⁻¹) ^ n ≤ exp 1 := by
+  convert one_sub_div_pow_le_exp_neg (n := n) (t := -1) (by grind) using 1
+  · field
+  · simp
+
 lemma le_inv_mul_exp (x : ℝ) {c : ℝ} (hc : 0 < c) : x ≤ c⁻¹ * exp (c * x) := by
   rw [le_inv_mul_iff₀ hc]
   calc c * x
   _ ≤ c * x + 1 := le_add_of_nonneg_right zero_le_one
   _ ≤ _ := Real.add_one_le_exp (c * x)
 
+lemma exp_lt_two_add_div_two_sub {x : ℝ} (hx : 0 < x) (hx' : x < 2) :
+    exp x < (2 + x) / (2 - x) := by calc
+  _ = exp (x / 2) ^ 2 := by grind [Real.exp_nat_mul (x / 2) 2]
+  _ ≤ _ := by
+    grw [Real.exp_bound' (x := x / 2) (by grind) (by grind) (n := 3) (by simp)]
+    apply Real.exp_nonneg
+  _ < (2 + x) / (2 - x) := by
+    rw [lt_div_iff₀ (by linarith), ← sub_pos]
+    simp only [Finset.sum_range_succ]
+    ring_nf
+    positivity
+
+lemma exp_le_two_add_div_two_sub {x : ℝ} (hx : 0 ≤ x) (hx' : x < 2) :
+    exp x ≤ (2 + x) / (2 - x) := by
+  obtain rfl | hx₀ := hx.eq_or_lt
+  · simp
+  · exact (exp_lt_two_add_div_two_sub hx₀ hx').le
+
 theorem prod_one_add_le_exp_sum {ι : Type*} (s : Finset ι) {f : ι → ℝ}
     (hf : ∀ i, 0 ≤ f i) : ∏ i ∈ s, (1 + f i) ≤ exp (∑ i ∈ s, f i) :=
   (Finset.prod_le_prod (fun i _ ↦ add_nonneg zero_le_one (hf i))
diff --git a/Mathlib/Analysis/Complex/ExponentialBounds.lean b/Mathlib/Analysis/Complex/ExponentialBounds.lean
index 56d1b556a6c820..190f489b95125a 100644
--- a/Mathlib/Analysis/Complex/ExponentialBounds.lean
+++ b/Mathlib/Analysis/Complex/ExponentialBounds.lean
@@ -77,7 +77,7 @@ theorem log_two_near_10 : |log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10 := by
   norm_num1 at z
   rw [one_div (2 : ℝ), log_inv, ← sub_eq_add_neg, _root_.abs_sub_comm] at z
   apply le_trans (_root_.abs_sub_le _ _ _) (add_le_add z _)
-  norm_num [sum_range_succ]
+  norm_num
 
 theorem log_two_gt_d9 : 0.6931471803 < log 2 :=
   lt_of_lt_of_le (by norm_num1) (sub_le_comm.1 (abs_sub_le_iff.1 log_two_near_10).2)
diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
index 9fe6d6e66a330f..40edeb5bc6a42d 100644
--- a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
@@ -242,7 +242,7 @@ theorem GammaSeq_add_one_left (s : ℂ) {n : ℕ} (hn : n ≠ 0) :
       ← mul_assoc, mul_comm _ (Finset.prod _ _)]
   congr 3
   · rw [cpow_add _ _ (Nat.cast_ne_zero.mpr hn), cpow_one, mul_comm]
-  · refine Finset.prod_congr (by rfl) fun x _ => ?_
+  · refine Finset.prod_congr rfl fun x _ => ?_
     push_cast; ring
   · abel
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
index 04ddb94fdc1d91..ab6a43aa827bb2 100644
--- a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
@@ -336,6 +336,16 @@ theorem abs_log_mul_self_lt (x : ℝ) (h1 : 0 < x) (h2 : x ≤ 1) : |log x * x|
   rw [← abs_of_nonneg aux, neg_mul, abs_neg] at this
   exact this
 
+lemma le_log_one_add_of_nonneg {x : ℝ} (hx : 0 ≤ x) : 2 * x / (x + 2) ≤ log (1 + x) := by
+  rw [le_log_iff_exp_le (by grind)]
+  convert exp_le_two_add_div_two_sub (x := 2 * x / (x + 2)) (by positivity) _ using 1
+  all_goals field_simp; grind
+
+lemma lt_log_one_add_of_pos {x : ℝ} (hx : 0 < x) : 2 * x / (x + 2) < log (1 + x) := by
+  rw [lt_log_iff_exp_lt (by grind)]
+  convert exp_lt_two_add_div_two_sub (x := 2 * x / (x + 2)) (by positivity) _ using 1
+  all_goals field_simp; grind
+
 /-- The real logarithm function tends to `+∞` at `+∞`. -/
 theorem tendsto_log_atTop : Tendsto log atTop atTop :=
   tendsto_comp_exp_atTop.1 <| by simpa only [log_exp] using! tendsto_id
diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean b/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
index a8ca2fea64a7fa..99ebf667e962ce 100644
--- a/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
@@ -423,14 +423,4 @@ theorem hasSum_log_one_add {a : ℝ} (h : 0 ≤ a) :
   · convert! hasSum_log_one_add_inv (inv_pos.mpr (lt_of_le_of_ne h ha0.symm)) using 4
     all_goals simp [field, add_comm]
 
-lemma le_log_one_add_of_nonneg {x : ℝ} (hx : 0 ≤ x) : 2 * x / (x + 2) ≤ log (1 + x) := by
-  convert! le_hasSum (hasSum_log_one_add hx) 0 (by intros; positivity) using 1
-  simp [field]
-
-lemma lt_log_one_add_of_pos {x : ℝ} (hx : 0 < x) : 2 * x / (x + 2) < log (1 + x) := by
-  convert!
-    lt_hasSum (hasSum_log_one_add hx.le) 0 (by intros; positivity) 1 (by positivity)
-      (by positivity) using 1
-  simp [field]
-
 end Real
diff --git a/Mathlib/CategoryTheory/Category/PartialFun.lean b/Mathlib/CategoryTheory/Category/PartialFun.lean
index b6a34630701d81..d544ff514b4e8e 100644
--- a/Mathlib/CategoryTheory/Category/PartialFun.lean
+++ b/Mathlib/CategoryTheory/Category/PartialFun.lean
@@ -146,7 +146,7 @@ noncomputable def partialFunEquivPointed : PartialFun.{u} ≌ Pointed where
             exact hw.symm
   counitIso :=
     NatIso.ofComponents
-      (fun X ↦ Pointed.Iso.mk (by classical exact Equiv.optionSubtypeNe X.point) (by rfl))
+      (fun X ↦ Pointed.Iso.mk (by classical exact Equiv.optionSubtypeNe X.point) rfl)
       fun {X Y} f ↦ Pointed.Hom.ext <| funext fun a ↦ by
         obtain _ | ⟨a, ha⟩ := a
         · exact f.map_point.symm
diff --git a/Mathlib/CategoryTheory/Filtered/Final.lean b/Mathlib/CategoryTheory/Filtered/Final.lean
index bebaba5487036e..edd610db14229d 100644
--- a/Mathlib/CategoryTheory/Filtered/Final.lean
+++ b/Mathlib/CategoryTheory/Filtered/Final.lean
@@ -60,12 +60,12 @@ theorem Functor.initial_of_isCofiltered_costructuredArrow
     [∀ d, IsCofiltered (CostructuredArrow F d)] : Initial F where
   out _ := IsCofiltered.isConnected _
 
-theorem isFiltered_structuredArrow_of_isFiltered_of_exists [IsFilteredOrEmpty C]
-    (h₁ : ∀ d, ∃ c, Nonempty (d ⟶ F.obj c)) (h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c),
-      ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t) (d : D) :
+theorem isFiltered_structuredArrow_of_isFiltered_of_exists [IsFilteredOrEmpty C] (d : D)
+    (h₁ : ∃ c, Nonempty (d ⟶ F.obj c)) (h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c),
+      ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t) :
     IsFiltered (StructuredArrow d F) := by
   have : Nonempty (StructuredArrow d F) := by
-    obtain ⟨c, ⟨f⟩⟩ := h₁ d
+    obtain ⟨c, ⟨f⟩⟩ := h₁
     exact ⟨.mk f⟩
   suffices IsFilteredOrEmpty (StructuredArrow d F) from IsFiltered.mk
   refine ⟨fun f g => ?_, fun f g η μ => ?_⟩
@@ -78,18 +78,17 @@ theorem isFiltered_structuredArrow_of_isFiltered_of_exists [IsFilteredOrEmpty C]
       StructuredArrow.homMk (IsFiltered.coeqHom η.right μ.right) (by simp), ?_⟩
     simpa using IsFiltered.coeq_condition _ _
 
-theorem isCofiltered_costructuredArrow_of_isCofiltered_of_exists [IsCofilteredOrEmpty C]
-    (h₁ : ∀ d, ∃ c, Nonempty (F.obj c ⟶ d)) (h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d),
-      ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s') (d : D) :
+theorem isCofiltered_costructuredArrow_of_isCofiltered_of_exists [IsCofilteredOrEmpty C] (d : D)
+    (h₁ : ∃ c, Nonempty (F.obj c ⟶ d)) (h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d),
+      ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s') :
     IsCofiltered (CostructuredArrow F d) := by
   suffices IsFiltered (CostructuredArrow F d)ᵒᵖ from isCofiltered_of_isFiltered_op _
   suffices IsFiltered (StructuredArrow (op d) F.op) from
     IsFiltered.of_equivalence (costructuredArrowOpEquivalence _ _).symm
   apply isFiltered_structuredArrow_of_isFiltered_of_exists
-  · intro d
-    obtain ⟨c, ⟨t⟩⟩ := h₁ d.unop
+  · obtain ⟨c, ⟨t⟩⟩ := h₁
     exact ⟨op c, ⟨Quiver.Hom.op t⟩⟩
-  · intro d c s s'
+  · intro c s s'
     obtain ⟨c', t, ht⟩ := h₂ s.unop s'.unop
     exact ⟨op c', Quiver.Hom.op t, Quiver.Hom.unop_inj ht⟩
 
@@ -99,7 +98,7 @@ theorem Functor.final_of_exists_of_isFiltered [IsFilteredOrEmpty C]
     (h₁ : ∀ d, ∃ c, Nonempty (d ⟶ F.obj c)) (h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c),
       ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t) : Functor.Final F := by
   suffices ∀ d, IsFiltered (StructuredArrow d F) from final_of_isFiltered_structuredArrow F
-  exact isFiltered_structuredArrow_of_isFiltered_of_exists F h₁ h₂
+  exact fun d => isFiltered_structuredArrow_of_isFiltered_of_exists F d (h₁ d) h₂
 
 /-- The inclusion of a terminal object is final. -/
 theorem Functor.final_const_of_isTerminal [IsFiltered C] {X : D} (hX : IsTerminal X) :
@@ -119,7 +118,7 @@ theorem Functor.initial_of_exists_of_isCofiltered [IsCofilteredOrEmpty C]
       ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s') : Functor.Initial F := by
   suffices ∀ d, IsCofiltered (CostructuredArrow F d) from
     initial_of_isCofiltered_costructuredArrow F
-  exact isCofiltered_costructuredArrow_of_isCofiltered_of_exists F h₁ h₂
+  exact fun d => isCofiltered_costructuredArrow_of_isCofiltered_of_exists F d (h₁ d) h₂
 
 /-- The inclusion of an initial object is initial. -/
 theorem Functor.initial_const_of_isInitial [IsCofiltered C] {X : D} (hX : IsInitial X) :
@@ -196,16 +195,14 @@ theorem Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful [IsCofiltered
 /-- Any under category on a filtered or empty category is filtered.
 (Note that under categories are always cofiltered since they have an initial object.) -/
 instance IsFiltered.under [IsFilteredOrEmpty C] (c : C) : IsFiltered (Under c) :=
-  isFiltered_structuredArrow_of_isFiltered_of_exists _
-    (fun c' => ⟨c', ⟨𝟙 _⟩⟩)
-    (fun s s' => IsFilteredOrEmpty.cocone_maps s s') c
+  isFiltered_structuredArrow_of_isFiltered_of_exists _ c ⟨c, ⟨𝟙 _⟩⟩
+    (fun s s' => IsFilteredOrEmpty.cocone_maps s s')
 
 /-- Any over category on a cofiltered or empty category is cofiltered.
 (Note that over categories are always filtered since they have a terminal object.) -/
 instance IsCofiltered.over [IsCofilteredOrEmpty C] (c : C) : IsCofiltered (Over c) :=
-  isCofiltered_costructuredArrow_of_isCofiltered_of_exists _
-    (fun c' => ⟨c', ⟨𝟙 _⟩⟩)
-    (fun s s' => IsCofilteredOrEmpty.cone_maps s s') c
+  isCofiltered_costructuredArrow_of_isCofiltered_of_exists _ c ⟨c, ⟨𝟙 _⟩⟩
+    (fun s s' => IsCofilteredOrEmpty.cone_maps s s')
 
 set_option backward.defeqAttrib.useBackward true in
 /-- The forgetful functor of the under category on any filtered or empty category is final. -/
@@ -296,7 +293,7 @@ theorem Functor.final_iff_isFiltered_structuredArrow [IsFilteredOrEmpty C] :
     Final F ↔ ∀ d, IsFiltered (StructuredArrow d F) := by
   refine ⟨?_, fun h => final_of_isFiltered_structuredArrow F⟩
   rw [final_iff_of_isFiltered]
-  exact fun h => isFiltered_structuredArrow_of_isFiltered_of_exists F h.1 h.2
+  exact fun h d => isFiltered_structuredArrow_of_isFiltered_of_exists F d (h.1 d) h.2
 
 /-- If `C` is cofiltered, then `F : C ⥤ D` is initial if and only if `CostructuredArrow F d` is
 cofiltered for all `d : D`. -/
@@ -304,7 +301,7 @@ theorem Functor.initial_iff_isCofiltered_costructuredArrow [IsCofilteredOrEmpty
     Initial F ↔ ∀ d, IsCofiltered (CostructuredArrow F d) := by
   refine ⟨?_, fun h => initial_of_isCofiltered_costructuredArrow F⟩
   rw [initial_iff_of_isCofiltered]
-  exact fun h => isCofiltered_costructuredArrow_of_isCofiltered_of_exists F h.1 h.2
+  exact fun h d => isCofiltered_costructuredArrow_of_isCofiltered_of_exists F d (h.1 d) h.2
 
 /-- If `C` is filtered, then the structured arrow category on the diagonal functor `C ⥤ C × C`
 is filtered as well. -/
diff --git a/Mathlib/CategoryTheory/Sites/Sheaf.lean b/Mathlib/CategoryTheory/Sites/Sheaf.lean
index 0483c6977df99f..1ee14826e07ea4 100644
--- a/Mathlib/CategoryTheory/Sites/Sheaf.lean
+++ b/Mathlib/CategoryTheory/Sites/Sheaf.lean
@@ -103,7 +103,7 @@ def conesEquivSieveCompatibleFamily :
   toFun π :=
     ⟨fun _ f h => π.app (op ⟨Over.mk f, h⟩), fun X Y f g hf => by
       let φ : S.arrows.categoryMk (g ≫ f) (S.downward_closed hf g) ⟶
-        S.arrows.categoryMk f hf := ObjectProperty.homMk (Over.homMk _ (by rfl))
+        S.arrows.categoryMk f hf := ObjectProperty.homMk (Over.homMk _ rfl)
       simpa using! π.naturality φ.op⟩
   invFun x :=
     { app := fun f => x.1 f.unop.1.hom f.unop.2
diff --git a/Mathlib/Combinatorics/SimpleGraph/Maps.lean b/Mathlib/Combinatorics/SimpleGraph/Maps.lean
index a4d9325a549275..3fbde0b4f959eb 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Maps.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Maps.lean
@@ -45,7 +45,7 @@ open Function
 
 namespace SimpleGraph
 
-variable {V W X : Type*} (G : SimpleGraph V) (G' : SimpleGraph W) {u v : V}
+variable {V W X Y : Type*} (G : SimpleGraph V) (G' : SimpleGraph W) {u v : V}
 
 /-! ## Map and comap -/
 
@@ -420,7 +420,7 @@ theorem le_comap (f : H →g G) : H ≤ G.comap f :=
 theorem nonempty_hom_iff_exists_le_comap : Nonempty (H →g G) ↔ ∃ f, H ≤ G.comap f :=
   ⟨fun ⟨f⟩ ↦ ⟨f, f.le_comap⟩, fun ⟨f, h⟩ ↦ ⟨f, (h ·)⟩⟩
 
-variable {G'' : SimpleGraph X}
+variable {G'' : SimpleGraph X} {G''' : SimpleGraph Y}
 
 /-- Composition of graph homomorphisms. -/
 abbrev comp (f' : G' →g G'') (f : G →g G') : G →g G'' :=
@@ -430,6 +430,15 @@ abbrev comp (f' : G' →g G'') (f : G →g G') : G →g G'' :=
 theorem coe_comp (f' : G' →g G'') (f : G →g G') : ⇑(f'.comp f) = f' ∘ f :=
   rfl
 
+theorem comp_assoc (f : G'' →g G''') (g : G' →g G'') (h : G →g G') :
+    f.comp (g.comp h) = (f.comp g).comp h := rfl
+
+@[simp]
+theorem comp_id (f : G →g G') : f.comp .id = f := rfl
+
+@[simp]
+theorem id_comp (f : G →g G') : .comp .id f = f := rfl
+
 @[simp]
 theorem comp_comap_ofLE (f : H →g G) : .comp (.comap f G) (.ofLE f.le_comap) = f :=
   rfl
@@ -533,7 +542,7 @@ protected def completeGraph {α β : Type*} (f : α ↪ β) : completeGraph α 
 
 @[simp] lemma coe_completeGraph {α β : Type*} (f : α ↪ β) : ⇑(Embedding.completeGraph f) = f := rfl
 
-variable {G'' : SimpleGraph X}
+variable {G'' : SimpleGraph X} {G''' : SimpleGraph Y}
 
 /-- Composition of graph embeddings. -/
 abbrev comp (f' : G' ↪g G'') (f : G ↪g G') : G ↪g G'' :=
@@ -543,6 +552,15 @@ abbrev comp (f' : G' ↪g G'') (f : G ↪g G') : G ↪g G'' :=
 theorem coe_comp (f' : G' ↪g G'') (f : G ↪g G') : ⇑(f'.comp f) = f' ∘ f :=
   rfl
 
+theorem comp_assoc (f : G'' ↪g G''') (g : G' ↪g G'') (h : G ↪g G') :
+    f.comp (g.comp h) = (f.comp g).comp h := rfl
+
+@[simp]
+theorem comp_refl (f : G ↪g G') : f.comp .refl = f := rfl
+
+@[simp]
+theorem refl_comp (f : G ↪g G') : .comp .refl f = f := rfl
+
 /-- Graph embeddings from `G` to `H` are the same thing as graph embeddings from `Gᶜ` to `Hᶜ`. -/
 def complEquiv : G ↪g H ≃ Gᶜ ↪g Hᶜ where
   toFun f := ⟨f.toEmbedding, by simp⟩
@@ -713,7 +731,7 @@ theorem toEmbedding_completeGraph {α β : Type*} (f : α ≃ β) :
     (Iso.completeGraph f).toEmbedding = Embedding.completeGraph f.toEmbedding :=
   rfl
 
-variable {G'' : SimpleGraph X}
+variable {G'' : SimpleGraph X} {G''' : SimpleGraph Y}
 
 /-- Composition of graph isomorphisms. -/
 abbrev comp (f' : G' ≃g G'') (f : G ≃g G') : G ≃g G'' :=
@@ -723,6 +741,15 @@ abbrev comp (f' : G' ≃g G'') (f : G ≃g G') : G ≃g G'' :=
 theorem coe_comp (f' : G' ≃g G'') (f : G ≃g G') : ⇑(f'.comp f) = f' ∘ f :=
   rfl
 
+theorem comp_assoc (f : G'' ≃g G''') (g : G' ≃g G'') (h : G ≃g G') :
+    f.comp (g.comp h) = (f.comp g).comp h := rfl
+
+@[simp]
+theorem comp_refl (f : G ≃g G') : f.comp .refl = f := rfl
+
+@[simp]
+theorem refl_comp (f : G ≃g G') : .comp .refl f = f := rfl
+
 section induce
 
 variable {s : Set V} {t : Set W} {r : Set X}
diff --git a/Mathlib/Data/Vector/Basic.lean b/Mathlib/Data/Vector/Basic.lean
index 7ceba21415a26f..a056a01b21f9fc 100644
--- a/Mathlib/Data/Vector/Basic.lean
+++ b/Mathlib/Data/Vector/Basic.lean
@@ -522,7 +522,7 @@ def casesOn₃ {motive : ∀ {n}, Vector α n → Vector β n → Vector γ n 
 
 /-- Cast a vector to an array. -/
 def toArray : Vector α n → Array α
-  | ⟨xs, _⟩ => cast (by rfl) xs.toArray
+  | ⟨xs, _⟩ => xs.toArray
 
 section InsertIdx
 
diff --git a/Mathlib/Dynamics/Flow.lean b/Mathlib/Dynamics/Flow.lean
index 6c6fe71cb8f661..bad8543dece3ee 100644
--- a/Mathlib/Dynamics/Flow.lean
+++ b/Mathlib/Dynamics/Flow.lean
@@ -247,7 +247,7 @@ theorem IsFactorOf.trans (h₁ : IsFactorOf ϕ ψ) (h₂ : IsFactorOf ψ χ) : I
   h₁.elim fun π hπ => h₂.elim fun ρ hρ => ⟨π ∘ ρ, hρ.comp χ ψ ϕ hπ⟩
 
 /-- Every flow is a factor of itself. -/
-theorem IsFactorOf.self : IsFactorOf ϕ ϕ := ⟨id, (isSemiconjugacy_id_iff_eq ϕ ϕ).mpr (by rfl)⟩
+theorem IsFactorOf.self : IsFactorOf ϕ ϕ := ⟨id, (isSemiconjugacy_id_iff_eq ϕ ϕ).mpr rfl⟩
 
 end Flow
 
diff --git a/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean b/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
index 12e8258353a615..3f596fe43485df 100644
--- a/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
+++ b/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
@@ -601,7 +601,7 @@ instance : Algebra A⟮b⟯ A⟮(algebraMap B C) b⟯ :=
   RingHom.toAlgebra (RingHom.adjoinAlgebraMap _)
 
 instance : IsScalarTower A⟮b⟯ A⟮(algebraMap B C) b⟯ C :=
-  IsScalarTower.of_algebraMap_eq' (by rfl)
+  IsScalarTower.of_algebraMap_eq' rfl
 
 end AdjoinSimple
 
diff --git a/Mathlib/GroupTheory/FreeGroup/Basic.lean b/Mathlib/GroupTheory/FreeGroup/Basic.lean
index 8a1e4753bdb254..3a4a00e0b12b57 100644
--- a/Mathlib/GroupTheory/FreeGroup/Basic.lean
+++ b/Mathlib/GroupTheory/FreeGroup/Basic.lean
@@ -931,7 +931,7 @@ def freeGroupUnitEquivInt : FreeGroup Unit ≃ ℤ where
     rintro ⟨L⟩
     simp only [quot_mk_eq_mk, map.mk, sum_mk, List.map_map]
     exact List.recOn L
-     (by rfl)
+     rfl
      (fun ⟨⟨⟩, b⟩ tl ih => by
         cases b <;> simp [zpow_add, ih] <;> rfl)
   right_inv x :=
diff --git a/Mathlib/GroupTheory/MonoidLocalization/Basic.lean b/Mathlib/GroupTheory/MonoidLocalization/Basic.lean
index b8440d8c517a69..6b2cb8e36d0c07 100644
--- a/Mathlib/GroupTheory/MonoidLocalization/Basic.lean
+++ b/Mathlib/GroupTheory/MonoidLocalization/Basic.lean
@@ -235,7 +235,7 @@ then `f` is defined on the whole `AddLocalization S`. -/]
 def rec {p : Localization S → Sort u} (f : ∀ (a : M) (b : S), p (mk a b))
     (H : ∀ {a c : M} {b d : S} (h : r S (a, b) (c, d)),
       (Eq.ndrec (f a b) (mk_eq_mk_iff.mpr h) : p (mk c d)) = f c d) (x) : p x :=
-  Quot.rec (fun y ↦ Eq.ndrec (f y.1 y.2) (by rfl))
+  Quot.rec (fun y ↦ f y.1 y.2)
     (fun y z h ↦ by cases y; cases z; exact H (r_iff_oreEqv_r.mpr h)) x
 
 /-- Copy of `Quotient.recOnSubsingleton₂` for `Localization` -/
diff --git a/Mathlib/LinearAlgebra/Complex/Module.lean b/Mathlib/LinearAlgebra/Complex/Module.lean
index 30edae0cc3b9f8..7db6282b5b709a 100644
--- a/Mathlib/LinearAlgebra/Complex/Module.lean
+++ b/Mathlib/LinearAlgebra/Complex/Module.lean
@@ -7,11 +7,13 @@ module
 
 public import Mathlib.Algebra.Algebra.RestrictScalars
 public import Mathlib.Algebra.CharP.Invertible
+public import Mathlib.Algebra.Order.Star.Basic
 public import Mathlib.Algebra.Star.Unitary
 public import Mathlib.Data.Complex.Basic
 public import Mathlib.Data.Real.Star
 public import Mathlib.LinearAlgebra.Matrix.ToLin
 import Mathlib.Algebra.Module.Torsion.Field
+import Mathlib.Algebra.Order.Monoid.Submonoid
 
 /-!
 # Complex number as a vector space over `ℝ`
@@ -595,6 +597,42 @@ lemma star_mul_self_eq_realPart_sq_add_imaginaryPart_sq (x : A) [hx : IsStarNorm
 
 end NonUnitalNonAssocRing
 
+section StarOrderedRing
+
+variable [NonUnitalRing A] [StarRing A] [PartialOrder A]
+    [StarOrderedRing A] [Module ℂ A] [StarModule ℂ A]
+
+lemma nonneg_iff_realPart_imaginaryPart {a : A} :
+    0 ≤ a ↔ 0 ≤ ℜ a ∧ ℑ a = 0 := by
+  refine ⟨fun h ↦ ⟨?_, h.isSelfAdjoint.imaginaryPart⟩, fun h ↦ ?_⟩
+  · simpa +singlePass [← h.isSelfAdjoint.coe_realPart] using! h
+  · rw [← realPart_add_I_smul_imaginaryPart a, h.2]
+    simpa using! h.1
+
+lemma nonpos_iff_realPart_imaginaryPart {a : A} :
+    a ≤ 0 ↔ ℜ a ≤ 0 ∧ ℑ a = 0 := by
+  simpa using nonneg_iff_realPart_imaginaryPart (a := -a)
+
+lemma realPart_nonneg_of_nonneg {a : A} (ha : 0 ≤ a) : 0 ≤ ℜ a :=
+  nonneg_iff_realPart_imaginaryPart.mp ha |>.1
+
+lemma realPart_nonpos_of_nonpos {a : A} (ha : a ≤ 0) : ℜ a ≤ 0 :=
+  nonpos_iff_realPart_imaginaryPart.mp ha |>.1
+
+lemma le_iff_realPart_imaginaryPart {a b : A} :
+    a ≤ b ↔ ℜ a ≤ ℜ b ∧ ℑ a = ℑ b := by
+  simpa [sub_eq_zero, eq_comm (a := ℑ a)] using nonneg_iff_realPart_imaginaryPart (a := b - a)
+
+lemma imaginaryPart_eq_of_le {a b : A} (hab : a ≤ b) :
+    ℑ a = ℑ b :=
+  le_iff_realPart_imaginaryPart.mp hab |>.2
+
+lemma realPart_mono {a b : A} (hab : a ≤ b) :
+    ℜ a ≤ ℜ b :=
+  le_iff_realPart_imaginaryPart.mp hab |>.1
+
+end StarOrderedRing
+
 @[simp]
 lemma realPart_one [Ring A] [StarRing A] [Module ℂ A] [StarModule ℂ A] :
     ℜ (1 : A) = 1 := by
diff --git a/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean b/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean
index 2fe493d15670d3..7d25c166b20b66 100644
--- a/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean
+++ b/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean
@@ -181,6 +181,15 @@ theorem ConvexOn.map_condExp_le (hm : m ≤ mα) [SigmaFinite (μ.trim hm)]
   filter_upwards [h1, h2, h3] with a ha hb hc
   simpa [← ha, ← hb]
 
+theorem ConvexOn.map_condExp_le_trim {mE : MeasurableSpace E} [BorelSpace E]
+    (hm : m ≤ mα) [SigmaFinite (μ.trim hm)]
+    (hφ_cvx : ConvexOn ℝ s φ) (hφ_cont : LowerSemicontinuousOn φ s)
+    (hφ_meas : StronglyMeasurable φ) (hf : ∀ᵐ a ∂μ, f a ∈ s)
+    (hs : IsClosed s) (hf_int : Integrable f μ) (hφ_int : Integrable (φ ∘ f) μ) :
+    φ ∘ μ[f | m] ≤ᵐ[μ.trim hm] μ[φ ∘ f | m] := by
+  rw [StronglyMeasurable.ae_le_trim_iff hm (by fun_prop) (by fun_prop)]
+  exact hφ_cvx.map_condExp_le hm hφ_cont hf hs hf_int hφ_int
+
 theorem ConcaveOn.condExp_map_le (hm : m ≤ mα) [SigmaFinite (μ.trim hm)]
     (hφ_cvx : ConcaveOn ℝ s φ) (hφ_cont : UpperSemicontinuousOn φ s) (hf : ∀ᵐ a ∂μ, f a ∈ s)
     (hs : IsClosed s) (hf_int : Integrable f μ) (hφ_int : Integrable (φ ∘ f) μ) :
@@ -189,6 +198,15 @@ theorem ConcaveOn.condExp_map_le (hm : m ≤ mα) [SigmaFinite (μ.trim hm)]
     condExp_neg (φ ∘ f) m] with a h ha
   simp_all [Pi.neg_comp]
 
+theorem ConcaveOn.condExp_map_le_trim {mE : MeasurableSpace E} [BorelSpace E]
+    (hm : m ≤ mα) [SigmaFinite (μ.trim hm)]
+    (hφ_cvx : ConcaveOn ℝ s φ) (hφ_cont : UpperSemicontinuousOn φ s)
+    (hφ_meas : StronglyMeasurable φ) (hf : ∀ᵐ a ∂μ, f a ∈ s)
+    (hs : IsClosed s) (hf_int : Integrable f μ) (hφ_int : Integrable (φ ∘ f) μ) :
+    μ[φ ∘ f | m] ≤ᵐ[μ.trim hm] φ ∘ μ[f | m] := by
+  rw [StronglyMeasurable.ae_le_trim_iff hm (by fun_prop) (by fun_prop)]
+  exact hφ_cvx.condExp_map_le hm hφ_cont hf hs hf_int hφ_int
+
 /-- **Conditional Jensen's inequality**: in a Banach space `E` with a measure `μ` that is σ-finite
 on a sub-σ-algebra `m`, if `φ : E → ℝ` is convex and lower-semicontinuous, then for any `f : α → E`
 such that `f` and `φ ∘ f` are integrable, we have `φ (𝔼[f | m]) ≤ᵐ[μ] 𝔼[φ ∘ f | m]`. -/
@@ -199,6 +217,14 @@ theorem ConvexOn.map_condExp_le_univ (hm : m ≤ mα) [SigmaFinite (μ.trim hm)]
   ConvexOn.map_condExp_le hm hφ_cvx (lowerSemicontinuousOn_univ_iff.2 hφ_cont) (by simp)
     isClosed_univ hf_int hφ_int
 
+theorem ConvexOn.map_condExp_le_trim_univ {mE : MeasurableSpace E} [BorelSpace E]
+    (hm : m ≤ mα) [SigmaFinite (μ.trim hm)]
+    (hφ_cvx : ConvexOn ℝ univ φ) (hφ_cont : LowerSemicontinuous φ)
+    (hφ_meas : StronglyMeasurable φ) (hf_int : Integrable f μ) (hφ_int : Integrable (φ ∘ f) μ) :
+    φ ∘ μ[f | m] ≤ᵐ[μ.trim hm] μ[φ ∘ f | m] := by
+  rw [StronglyMeasurable.ae_le_trim_iff hm (by fun_prop) (by fun_prop)]
+  exact hφ_cvx.map_condExp_le_univ hm hφ_cont hf_int hφ_int
+
 theorem ConcaveOn.condExp_map_le_univ (hm : m ≤ mα) [SigmaFinite (μ.trim hm)]
     (hφ_cvx : ConcaveOn ℝ univ φ) (hφ_cont : UpperSemicontinuous φ)
     (hf_int : Integrable f μ) (hφ_int : Integrable (φ ∘ f) μ) :
@@ -207,6 +233,14 @@ theorem ConcaveOn.condExp_map_le_univ (hm : m ≤ mα) [SigmaFinite (μ.trim hm)
     condExp_neg (φ ∘ f) m] with a h ha
   simp_all [Pi.neg_comp]
 
+theorem ConcaveOn.condExp_map_le_trim_univ {mE : MeasurableSpace E} [BorelSpace E]
+    (hm : m ≤ mα) [SigmaFinite (μ.trim hm)]
+    (hφ_cvx : ConcaveOn ℝ univ φ) (hφ_cont : UpperSemicontinuous φ)
+    (hφ_meas : StronglyMeasurable φ) (hf_int : Integrable f μ) (hφ_int : Integrable (φ ∘ f) μ) :
+    μ[φ ∘ f | m] ≤ᵐ[μ.trim hm] φ ∘ μ[f | m] := by
+  rw [StronglyMeasurable.ae_le_trim_iff hm (by fun_prop) (by fun_prop)]
+  exact hφ_cvx.condExp_map_le_univ hm hφ_cont hf_int hφ_int
+
 /-- In a Banach space `E` with a measure `μ`, then for any `f : α → E`, we have
 `‖𝔼[f | m]‖ ≤ᵐ[μ] 𝔼[‖f‖ | m]`. -/
 theorem norm_condExp_le : (‖μ[f | m] ·‖) ≤ᵐ[μ] μ[(‖f ·‖) | m] := by
diff --git a/Mathlib/NumberTheory/BernoulliPolynomials.lean b/Mathlib/NumberTheory/BernoulliPolynomials.lean
index 6adffaddb78dfa..51e293fd0ad465 100644
--- a/Mathlib/NumberTheory/BernoulliPolynomials.lean
+++ b/Mathlib/NumberTheory/BernoulliPolynomials.lean
@@ -111,7 +111,7 @@ theorem derivative_bernoulli_add_one (k : ℕ) :
   rw [range_add_one, sum_insert notMem_range_self, tsub_self, cast_zero, mul_zero,
     map_zero, zero_add, mul_sum]
   -- the rest of the sum is termwise equal:
-  refine sum_congr (by rfl) fun m _ => ?_
+  refine sum_congr rfl fun m _ => ?_
   conv_rhs => rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_natCast, C_mul_monomial, mul_comm]
   rw [mul_assoc, mul_assoc, ← Nat.cast_mul, ← Nat.cast_mul]
   congr 3
diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean b/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
index 31ad01f242423e..9237a25656763b 100644
--- a/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
+++ b/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
@@ -68,7 +68,7 @@ theorem WithTop.sInf_eq [InfSet α] {s : Set (WithTop α)} (hs : ¬s ⊆ {⊤})
     sInf s = ↑(sInf ((↑) ⁻¹' s) : α) :=
   if_neg <| by simp [hs, h's]
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem WithTop.sInf_empty [InfSet α] : sInf (∅ : Set (WithTop α)) = ⊤ :=
   if_pos <| by simp
 
@@ -105,10 +105,6 @@ theorem WithTop.coe_sSup' [SupSet α] {s : Set α} (hs : BddAbove s) :
   · exact Option.some_injective _
   · rintro ⟨x, _, ⟨⟩⟩
 
-@[simp]
-theorem WithBot.sSup_empty [SupSet α] : sSup (∅ : Set (WithBot α)) = ⊥ :=
-  WithTop.sInf_empty (α := αᵒᵈ)
-
 @[to_dual]
 theorem WithTop.sSup_empty (α : Type*) [CompleteLattice α] : (sSup ∅ : WithTop α) = ⊥ := by
   rw [sSup_eq (by simp) (OrderTop.bddAbove _), Set.preimage_empty, _root_.sSup_empty, coe_bot]
@@ -264,19 +260,16 @@ theorem notMem_of_csSup_lt {x : α} {s : Set α} (h : sSup s < x) (hs : BddAbove
 /-- Introduction rule to prove that `b` is the supremum of `s`: it suffices to check that `b`
 is larger than all elements of `s`, and that this is not the case of any `w<b`.
 See `sSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in complete lattices. -/
+@[to_dual csInf_eq_of_forall_ge_of_forall_gt_exists_lt
+/-- Introduction rule to prove that `b` is the infimum of `s`: it suffices to check that `b`
+is smaller than all elements of `s`, and that this is not the case of any `w>b`.
+See `sInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices. -/]
 theorem csSup_eq_of_forall_le_of_forall_lt_exists_gt (hs : s.Nonempty) (H : ∀ a ∈ s, a ≤ b)
     (H' : ∀ w, w < b → ∃ a ∈ s, w < a) : sSup s = b :=
   (eq_of_le_of_not_lt (csSup_le hs H)) fun hb =>
     let ⟨_, ha, ha'⟩ := H' _ hb
     lt_irrefl _ <| ha'.trans_le <| le_csSup ⟨b, H⟩ ha
 
-/-- Introduction rule to prove that `b` is the infimum of `s`: it suffices to check that `b`
-is smaller than all elements of `s`, and that this is not the case of any `w>b`.
-See `sInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices. -/
-theorem csInf_eq_of_forall_ge_of_forall_gt_exists_lt :
-    s.Nonempty → (∀ a ∈ s, b ≤ a) → (∀ w, b < w → ∃ a ∈ s, a < w) → sInf s = b :=
-  csSup_eq_of_forall_le_of_forall_lt_exists_gt (α := αᵒᵈ)
-
 /-- `b < sSup s` when there is an element `a` in `s` with `b < a`, when `s` is bounded above.
 This is essentially an iff, except that the assumptions for the two implications are
 slightly different (one needs boundedness above for one direction, nonemptiness and linear
diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean b/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
index c6f70a19799255..7d6f6da9bbd401 100644
--- a/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
+++ b/Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
@@ -21,6 +21,26 @@ open Set
 
 variable {ι α β γ : Type*}
 
+section ConditionallyCompleteLattice
+
+variable [ConditionallyCompleteLattice α]
+
+/-- Supremum of `a i`, `i : ι`, is equal to the supremum over finite suprema of `a`. -/
+@[to_dual
+/-- Infimum of `a i`, `i : ι`, is equal to the infimum over finite infima of `a`. -/]
+theorem ciSup_eq_ciSup_finset [OrderBot α] [Nonempty ι] {a : ι → α}
+    (ha : BddAbove (range a)) :
+    ⨆ i, a i = ⨆ F : Finset ι, F.sup a := by
+  have hbdd : BddAbove (Set.range fun F : Finset ι => F.sup a) := by
+    refine ⟨⨆ i, a i, ?_⟩
+    rintro _ ⟨F, rfl⟩
+    exact Finset.sup_le fun i _ => le_ciSup ha i
+  refine le_antisymm ?_ ?_
+  · exact ciSup_le fun i => (Finset.le_sup (by simp)).trans (le_ciSup hbdd {i})
+  · exact ciSup_le fun F => Finset.sup_le fun i _ => le_ciSup ha i
+
+end ConditionallyCompleteLattice
+
 section ConditionallyCompleteLinearOrder
 
 variable [ConditionallyCompleteLinearOrder α] {s t : Set α} {a b : α}
@@ -179,6 +199,42 @@ end ListMultiset
 
 end ConditionallyCompleteLinearOrder
 
+section CompleteLinearOrder
+
+variable {α : Type*} [CompleteLinearOrder α] {ι : Sort*}
+
+theorem sSup_ne_of_notMem {s : Set α} (hfin : s.Finite) {a : α} (hne : a ≠ ⊥) (hmem : a ∉ s) :
+    sSup s ≠ a := by
+  rcases s.eq_empty_or_nonempty with rfl | hnonempty
+  · simp [eq_comm, hne]
+  exact (hmem <| · ▸ hnonempty.csSup_mem hfin)
+
+theorem sInf_ne_of_notMem {s : Set α} (hfin : s.Finite) {a : α} (hne : a ≠ ⊤) (hmem : a ∉ s) :
+    sInf s ≠ a :=
+  sSup_ne_of_notMem (α := αᵒᵈ) hfin hne hmem
+
+theorem sSup_ne_top [Nontrivial α] {s : Set α} (hfin : s.Finite) (htop : ⊤ ∉ s) : sSup s ≠ ⊤ :=
+  sSup_ne_of_notMem hfin top_ne_bot htop
+
+theorem sInf_ne_bot [Nontrivial α] {s : Set α} (hfin : s.Finite) (hbot : ⊥ ∉ s) : sInf s ≠ ⊥ :=
+  sSup_ne_top (α := αᵒᵈ) hfin hbot
+
+theorem iSup_ne_of_notMem [Finite ι] {f : ι → α} {a : α} (hne : a ≠ ⊥) (h : ∀ x, f x ≠ a) :
+    iSup f ≠ a :=
+  sSup_ne_of_notMem (Set.finite_range f) hne <| by grind
+
+theorem iInf_ne_of_notMem [Finite ι] {f : ι → α} {a : α} (hne : a ≠ ⊤) (h : ∀ x, f x ≠ a) :
+    iInf f ≠ a :=
+  iSup_ne_of_notMem (α := αᵒᵈ) hne h
+
+theorem iSup_ne_top [Finite ι] [Nontrivial α] {f : ι → α} (h : ∀ x, f x ≠ ⊤) : iSup f ≠ ⊤ :=
+  iSup_ne_of_notMem top_ne_bot h
+
+theorem iInf_ne_bot [Finite ι] [Nontrivial α] {f : ι → α} (h : ∀ x, f x ≠ ⊥) : iInf f ≠ ⊥ :=
+  iSup_ne_top (α := αᵒᵈ) h
+
+end CompleteLinearOrder
+
 /-!
 ### Relation between `sSup` / `sInf` and `Finset.sup'` / `Finset.inf'`
 
diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean b/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
index 65502dab75bcbf..217a256864676b 100644
--- a/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
+++ b/Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
@@ -33,30 +33,21 @@ Extension of `iSup` and `iInf` from a preorder `α` to `WithTop α` and `WithBot
 
 variable [Preorder α]
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem WithTop.iInf_empty [IsEmpty ι] [InfSet α] (f : ι → WithTop α) :
-    ⨅ i, f i = ⊤ := by rw [iInf, range_eq_empty, WithTop.sInf_empty]
+    ⨅ i, f i = ⊤ := by
+  rw [iInf_of_isEmpty, WithTop.sInf_empty]
 
-@[norm_cast]
+@[to_dual (attr := norm_cast)]
 theorem WithTop.coe_iInf [Nonempty ι] [InfSet α] {f : ι → α} (hf : BddBelow (range f)) :
     ↑(⨅ i, f i) = (⨅ i, f i : WithTop α) := by
   rw [iInf, iInf, WithTop.coe_sInf' (range_nonempty f) hf, ← range_comp, Function.comp_def]
 
-@[norm_cast]
+@[to_dual (attr := norm_cast)]
 theorem WithTop.coe_iSup [SupSet α] (f : ι → α) (h : BddAbove (Set.range f)) :
     ↑(⨆ i, f i) = (⨆ i, f i : WithTop α) := by
   rw [iSup, iSup, WithTop.coe_sSup' h, ← range_comp, Function.comp_def]
 
-@[simp]
-theorem WithBot.ciSup_empty [IsEmpty ι] [SupSet α] (f : ι → WithBot α) :
-    ⨆ i, f i = ⊥ :=
-  WithTop.iInf_empty (α := αᵒᵈ) _
-
-@[norm_cast]
-theorem WithBot.coe_iSup [Nonempty ι] [SupSet α] {f : ι → α} (hf : BddAbove (range f)) :
-    ↑(⨆ i, f i) = (⨆ i, f i : WithBot α) :=
-  WithTop.coe_iInf (α := αᵒᵈ) hf
-
 theorem WithBot.coe_biSup {ι : Type*} {s : Set ι} (hs : s.Nonempty)
     {α : Type*} [CompleteLattice α] (f : ι → α) :
     ⨆ i ∈ s, f i = ⨆ i ∈ s, (f i : WithBot α) := by
@@ -69,11 +60,6 @@ theorem WithBot.coe_biSup {ι : Type*} {s : Set ι} (hs : s.Nonempty)
   · simpa only [iSup_pos h] using by apply le_biSup _ h
   · simpa only [iSup_neg h] using le_trans (by simp) (le_biSup _ hj)
 
-@[norm_cast]
-theorem WithBot.coe_iInf [InfSet α] (f : ι → α) (h : BddBelow (Set.range f)) :
-    ↑(⨅ i, f i) = (⨅ i, f i : WithBot α) :=
-  WithTop.coe_iSup (α := αᵒᵈ) _ h
-
 theorem WithBot.coe_biInf {ι : Type*} {s : Set ι} {α : Type*} [CompleteLattice α] (f : ι → α) :
     ⨅ i ∈ s, f i = ⨅ i ∈ s, (f i : WithBot α) := by
   refine le_antisymm (by simpa using fun _ ↦ biInf_le _) <|
@@ -88,65 +74,56 @@ section ConditionallyCompleteLattice
 
 variable [ConditionallyCompleteLattice α] {a b : α}
 
+@[to_dual]
 theorem isLUB_ciSup [Nonempty ι] {f : ι → α} (H : BddAbove (range f)) :
     IsLUB (range f) (⨆ i, f i) :=
   isLUB_csSup (range_nonempty f) H
 
+@[to_dual]
 theorem isLUB_ciSup_set {f : β → α} {s : Set β} (H : BddAbove (f '' s)) (Hne : s.Nonempty) :
     IsLUB (f '' s) (⨆ i : s, f i) := by
   rw [← sSup_image']
   exact isLUB_csSup (Hne.image _) H
 
-theorem isGLB_ciInf [Nonempty ι] {f : ι → α} (H : BddBelow (range f)) :
-    IsGLB (range f) (⨅ i, f i) :=
-  isGLB_csInf (range_nonempty f) H
-
-theorem isGLB_ciInf_set {f : β → α} {s : Set β} (H : BddBelow (f '' s)) (Hne : s.Nonempty) :
-    IsGLB (f '' s) (⨅ i : s, f i) :=
-  isLUB_ciSup_set (α := αᵒᵈ) H Hne
-
+@[to_dual le_ciInf_iff]
 theorem ciSup_le_iff [Nonempty ι] {f : ι → α} {a : α} (hf : BddAbove (range f)) :
     iSup f ≤ a ↔ ∀ i, f i ≤ a :=
   (isLUB_le_iff <| isLUB_ciSup hf).trans forall_mem_range
 
-theorem le_ciInf_iff [Nonempty ι] {f : ι → α} {a : α} (hf : BddBelow (range f)) :
-    a ≤ iInf f ↔ ∀ i, a ≤ f i :=
-  (le_isGLB_iff <| isGLB_ciInf hf).trans forall_mem_range
-
+@[to_dual le_ciInf_set_iff]
 theorem ciSup_set_le_iff {ι : Type*} {s : Set ι} {f : ι → α} {a : α} (hs : s.Nonempty)
     (hf : BddAbove (f '' s)) : ⨆ i : s, f i ≤ a ↔ ∀ i ∈ s, f i ≤ a :=
   (isLUB_le_iff <| isLUB_ciSup_set hf hs).trans forall_mem_image
 
-theorem le_ciInf_set_iff {ι : Type*} {s : Set ι} {f : ι → α} {a : α} (hs : s.Nonempty)
-    (hf : BddBelow (f '' s)) : (a ≤ ⨅ i : s, f i) ↔ ∀ i ∈ s, a ≤ f i :=
-  (le_isGLB_iff <| isGLB_ciInf_set hf hs).trans forall_mem_image
-
+@[to_dual]
 theorem IsLUB.ciSup_eq [Nonempty ι] {f : ι → α} (H : IsLUB (range f) a) : ⨆ i, f i = a :=
   H.csSup_eq (range_nonempty f)
 
+@[to_dual]
 theorem IsLUB.ciSup_set_eq {s : Set β} {f : β → α} (H : IsLUB (f '' s) a) (Hne : s.Nonempty) :
     ⨆ i : s, f i = a :=
   IsLUB.csSup_eq (image_eq_range f s ▸ H) (image_eq_range f s ▸ Hne.image f)
 
-theorem IsGLB.ciInf_eq [Nonempty ι] {f : ι → α} (H : IsGLB (range f) a) : ⨅ i, f i = a :=
-  H.csInf_eq (range_nonempty f)
-
-theorem IsGLB.ciInf_set_eq {s : Set β} {f : β → α} (H : IsGLB (f '' s) a) (Hne : s.Nonempty) :
-    ⨅ i : s, f i = a :=
-  IsGLB.csInf_eq (image_eq_range f s ▸ H) (image_eq_range f s ▸ Hne.image f)
-
-/-- The indexed supremum of a function is bounded above by a uniform bound -/
+/-- The indexed supremum of a function is bounded above by a uniform bound. -/
+@[to_dual le_ciInf /-- The indexed minimum of a function is bounded below by a uniform lower
+bound. -/]
 theorem ciSup_le [Nonempty ι] {f : ι → α} {c : α} (H : ∀ x, f x ≤ c) : iSup f ≤ c :=
   csSup_le (range_nonempty f) (by rwa [forall_mem_range])
 
 /-- The indexed supremum of a function is bounded below by the value taken at one point -/
+@[to_dual ciInf_le /-- The indexed infimum of a function is bounded above by the value taken
+at one point. -/]
 theorem le_ciSup {f : ι → α} (H : BddAbove (range f)) (c : ι) : f c ≤ iSup f :=
   le_csSup H (mem_range_self _)
 
+@[to_dual ciInf_le_of_le]
 theorem le_ciSup_of_le {f : ι → α} (H : BddAbove (range f)) (c : ι) (h : a ≤ f c) : a ≤ iSup f :=
   le_trans h (le_ciSup H c)
 
 /-- If the set of all `f i j` is bounded above, then so is the set of the supremums of every row -/
+@[to_dual
+  /-- If the set of all `f i j` is bounded below, then so is the set of the infimums
+  of every row -/]
 theorem BddAbove.range_iSup_of_iUnion_range {κ : ι → Sort*} {f : ∀ i, κ i → α}
     (H : BddAbove <| ⋃ i, range (f i)) : BddAbove <| range fun i ↦ ⨆ j, f i j := by
   have ⟨a, h⟩ := H
@@ -155,19 +132,23 @@ theorem BddAbove.range_iSup_of_iUnion_range {κ : ι → Sort*} {f : ∀ i, κ i
   · exact iSup_of_empty' (f i) ▸ le_sup_right
   exact ciSup_le fun j ↦ le_sup_of_le_left <| h ⟨_, ⟨i, rfl⟩, ⟨j, rfl⟩⟩
 
+@[to_dual ciInf₂_le]
 theorem le_ciSup₂ {κ : ι → Sort*} {f : ∀ i, κ i → α} (H : BddAbove <| ⋃ i, range (f i)) (i : ι)
     (j : κ i) : f i j ≤ ⨆ (i) (j), f i j :=
   le_ciSup_of_le H.range_iSup_of_iUnion_range i <|
     le_ciSup (H.mono <| subset_iUnion (range <| f ·) i) j
 
 /-- The indexed suprema of two functions are comparable if the functions are pointwise comparable -/
-@[gcongr low]
+@[to_dual (attr := gcongr low)
+/-- The indexed infimum of two functions are comparable if the functions are pointwise
+comparable -/]
 theorem ciSup_mono {f g : ι → α} (B : BddAbove (range g)) (H : ∀ x, f x ≤ g x) :
     iSup f ≤ iSup g := by
   cases isEmpty_or_nonempty ι
   · rw [iSup_of_empty', iSup_of_empty']
   · exact ciSup_le fun x => le_ciSup_of_le B x (H x)
 
+@[to_dual]
 theorem ciSup_sup_eq {f g : ι → α} (Hf : BddAbove <| range f) (Hg : BddAbove <| range g) :
     ⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ (⨆ x, g x) := by
   cases isEmpty_or_nonempty ι
@@ -176,60 +157,21 @@ theorem ciSup_sup_eq {f g : ι → α} (Hf : BddAbove <| range f) (Hg : BddAbove
   have := bbdAbove_range_sup Hf Hg
   exact sup_le (ciSup_mono this fun _ ↦ le_sup_left) (ciSup_mono this fun _ ↦ le_sup_right)
 
+@[to_dual ciInf_set_le]
 theorem le_ciSup_set {f : β → α} {s : Set β} (H : BddAbove (f '' s)) {c : β} (hc : c ∈ s) :
     f c ≤ ⨆ i : s, f i :=
   (le_csSup H <| mem_image_of_mem f hc).trans_eq sSup_image'
 
-/-- The indexed infimum of two functions are comparable if the functions are pointwise comparable -/
-@[gcongr low]
-theorem ciInf_mono {f g : ι → α} (B : BddBelow (range f)) (H : ∀ x, f x ≤ g x) : iInf f ≤ iInf g :=
-  ciSup_mono (α := αᵒᵈ) B H
-
-theorem ciInf_inf_eq {f g : ι → α} (Hf : BddBelow <| range f) (Hg : BddBelow <| range g) :
-    ⨅ x, f x ⊓ g x = (⨅ x, f x) ⊓ (⨅ x, g x) :=
-  ciSup_sup_eq (α := αᵒᵈ) Hf Hg
-
-/-- The indexed minimum of a function is bounded below by a uniform lower bound -/
-theorem le_ciInf [Nonempty ι] {f : ι → α} {c : α} (H : ∀ x, c ≤ f x) : c ≤ iInf f :=
-  ciSup_le (α := αᵒᵈ) H
-
-/-- The indexed infimum of a function is bounded above by the value taken at one point -/
-theorem ciInf_le {f : ι → α} (H : BddBelow (range f)) (c : ι) : iInf f ≤ f c :=
-  le_ciSup (α := αᵒᵈ) H c
-
-theorem ciInf_le_of_le {f : ι → α} (H : BddBelow (range f)) (c : ι) (h : f c ≤ a) : iInf f ≤ a :=
-  le_ciSup_of_le (α := αᵒᵈ) H c h
-
+@[to_dual]
 theorem ciSup_mono_of_forall_exists {ι'} [Nonempty ι] {f : ι → α} {g : ι' → α}
     (hg : BddAbove <| range g) (h : ∀ i, ∃ i', f i ≤ g i') : ⨆ i, f i ≤ ⨆ i', g i' :=
   ciSup_le fun i ↦ h i |>.elim <| le_ciSup_of_le hg
 
-theorem ciInf_mono_of_forall_exists {ι'} [Nonempty ι'] {f : ι → α} {g : ι' → α}
-    (hf : BddBelow <| range f) (h : ∀ i', ∃ i, f i ≤ g i') : ⨅ i, f i ≤ ⨅ i', g i' :=
-  ciSup_mono_of_forall_exists (α := αᵒᵈ) hf h
-
-/-- If the set of all `f i j` is bounded below, then so is the set of the infimums of every row -/
-theorem BddBelow.range_iInf_of_iUnion_range {κ : ι → Sort*} {f : ∀ i, κ i → α}
-    (H : BddBelow <| ⋃ i, range (f i)) : BddBelow <| range fun i ↦ ⨅ j, f i j := by
-  have ⟨a, h⟩ := H
-  refine ⟨a ⊓ (sInf ∅), fun x ⟨i, hx⟩ ↦ hx ▸ ?_⟩
-  cases isEmpty_or_nonempty <| κ i
-  · exact iInf_of_isEmpty (f i) ▸ inf_le_right
-  exact le_ciInf fun j ↦ inf_le_of_left_le <| h ⟨_, ⟨i, rfl⟩, ⟨j, rfl⟩⟩
-
-theorem ciInf₂_le {κ : ι → Sort*} {f : ∀ i, κ i → α} (H : BddBelow <| ⋃ i, range (f i)) (i : ι)
-    (j : κ i) : ⨅ (i) (j), f i j ≤ f i j :=
-  ciInf_le_of_le H.range_iInf_of_iUnion_range i <|
-    ciInf_le (H.mono <| subset_iUnion (range <| f ·) i) j
-
-theorem ciInf_set_le {f : β → α} {s : Set β} (H : BddBelow (f '' s)) {c : β} (hc : c ∈ s) :
-    ⨅ i : s, f i ≤ f c :=
-  le_ciSup_set (α := αᵒᵈ) H hc
-
 lemma ciInf_le_ciSup [Nonempty ι] {f : ι → α} (hf : BddBelow (range f)) (hf' : BddAbove (range f)) :
     ⨅ i, f i ≤ ⨆ i, f i :=
   (ciInf_le hf (Classical.arbitrary _)).trans <| le_ciSup hf' (Classical.arbitrary _)
 
+@[to_dual]
 lemma ciSup_prod {f : β × γ → α} (hf : BddAbove (Set.range f)) :
     ⨆ p, f p = ⨆ b, ⨆ c, f (b, c) := by
   rcases isEmpty_or_nonempty β
@@ -251,34 +193,25 @@ lemma ciSup_prod {f : β × γ → α} (hf : BddAbove (Set.range f)) :
   conv_rhs => enter [b]; rw [ciSup_le_iff (h₂ b)]
   simp [Prod.forall]
 
-lemma ciInf_prod {f : β × γ → α} (hf : BddBelow (Set.range f)) :
-    ⨅ p, f p = ⨅ b, ⨅ c, f (b, c) :=
-  ciSup_prod (α := αᵒᵈ) hf
-
 /-- Introduction rule to prove that `b` is the supremum of `f`: it suffices to check that `b`
 is larger than `f i` for all `i`, and that this is not the case of any `w<b`.
 See `iSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in complete lattices. -/
+@[to_dual ciInf_eq_of_forall_ge_of_forall_gt_exists_lt
+/-- Introduction rule to prove that `b` is the infimum of `f`: it suffices to check that `b`
+is smaller than `f i` for all `i`, and that this is not the case of any `w>b`.
+See `iInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices. -/]
 theorem ciSup_eq_of_forall_le_of_forall_lt_exists_gt [Nonempty ι] {f : ι → α} (h₁ : ∀ i, f i ≤ b)
     (h₂ : ∀ w, w < b → ∃ i, w < f i) : ⨆ i : ι, f i = b :=
   csSup_eq_of_forall_le_of_forall_lt_exists_gt (range_nonempty f) (forall_mem_range.mpr h₁)
     fun w hw => exists_range_iff.mpr <| h₂ w hw
 
-/-- Introduction rule to prove that `b` is the infimum of `f`: it suffices to check that `b`
-is smaller than `f i` for all `i`, and that this is not the case of any `w>b`.
-See `iInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices. -/
-theorem ciInf_eq_of_forall_ge_of_forall_gt_exists_lt [Nonempty ι] {f : ι → α} (h₁ : ∀ i, b ≤ f i)
-    (h₂ : ∀ w, b < w → ∃ i, f i < w) : ⨅ i : ι, f i = b :=
-  ciSup_eq_of_forall_le_of_forall_lt_exists_gt (α := αᵒᵈ) h₁ h₂
-
+@[to_dual]
 lemma Set.Iic_ciInf [Nonempty ι] {f : ι → α} (hf : BddBelow (range f)) :
     Iic (⨅ i, f i) = ⋂ i, Iic (f i) := by
   ext
   simpa using le_ciInf_iff hf
 
-lemma Set.Ici_ciSup [Nonempty ι] {f : ι → α} (hf : BddAbove (range f)) :
-    Ici (⨆ i, f i) = ⋂ i, Ici (f i) :=
-  Iic_ciInf (α := αᵒᵈ) hf
-
+@[to_dual]
 theorem ciSup_subtype {p : ι → Prop} {f : Subtype p → α}
     (hf : BddAbove (Set.range f)) (hf' : sSup ∅ ≤ iSup f) :
     iSup f = ⨆ (i) (h : p i), f ⟨i, h⟩ := by
@@ -300,11 +233,7 @@ theorem ciSup_subtype {p : ι → Prop} {f : Subtype p → α}
     · exact le_ciSup hf ?_
     · exact hf'
 
-theorem ciInf_subtype {p : ι → Prop} {f : Subtype p → α}
-    (hf : BddBelow (Set.range f)) (hf' : iInf f ≤ sInf ∅) :
-    iInf f = ⨅ (i) (h : p i), f ⟨i, h⟩ :=
-  ciSup_subtype (α := αᵒᵈ) hf hf'
-
+@[to_dual]
 theorem cbiSup_eq_ciSup_subtype {p : ι → Prop} {f : ∀ i, p i → α}
     (hf : BddAbove (Set.range (fun i : Subtype p ↦ f i i.prop)))
     (hf' : sSup ∅ ≤ ⨆ (i : Subtype p), f i i.prop) :
@@ -313,14 +242,9 @@ theorem cbiSup_eq_ciSup_subtype {p : ι → Prop} {f : ∀ i, p i → α}
 
 @[deprecated (since := "2026-04-04")] alias ciSup_subtype' := cbiSup_eq_ciSup_subtype
 
-theorem cbiInf_eq_ciInf_subtype {p : ι → Prop} {f : ∀ i, p i → α}
-    (hf : BddBelow (Set.range (fun i : Subtype p ↦ f i i.prop)))
-    (hf' : ⨅ (i : Subtype p), f i i.prop ≤ sInf ∅) :
-    ⨅ (i) (h), f i h = ⨅ x : Subtype p, f x x.property :=
-  (ciInf_subtype (f := fun x => f x.val x.property) hf hf').symm
-
 @[deprecated (since := "2026-04-04")] alias ciInf_subtype' := cbiInf_eq_ciInf_subtype
 
+@[to_dual]
 theorem ciSup_subtype_fun {ι} {s : Set ι} {f : ι → α}
     (hf : BddAbove (Set.range fun i : s ↦ f i)) (hf' : sSup ∅ ≤ ⨆ i : s, f i) :
     ⨆ i : s, f i = ⨆ (t : ι) (_ : t ∈ s), f t :=
@@ -328,33 +252,21 @@ theorem ciSup_subtype_fun {ι} {s : Set ι} {f : ι → α}
 
 @[deprecated (since := "2026-04-04")] alias ciSup_subtype'' := ciSup_subtype_fun
 
-theorem ciInf_subtype_fun {ι} {s : Set ι} {f : ι → α}
-    (hf : BddBelow (Set.range fun i : s ↦ f i)) (hf' : ⨅ i : s, f i ≤ sInf ∅) :
-    ⨅ i : s, f i = ⨅ (t : ι) (_ : t ∈ s), f t :=
-  ciInf_subtype hf hf'
-
 @[deprecated (since := "2026-04-04")] alias ciInf_subtype'' := ciInf_subtype_fun
 
+@[to_dual]
 theorem csSup_image {s : Set β} {f : β → α}
     (hf : BddAbove (Set.range fun i : s ↦ f i)) (hf' : sSup ∅ ≤ ⨆ i : s, f i) :
     sSup (f '' s) = ⨆ a ∈ s, f a := by
   rw [← ciSup_subtype_fun hf hf', iSup, Set.image_eq_range]
 
-theorem csInf_image {s : Set β} {f : β → α}
-    (hf : BddBelow (Set.range fun i : s ↦ f i)) (hf' : ⨅ i : s, f i ≤ sInf ∅) :
-    sInf (f '' s) = ⨅ a ∈ s, f a :=
-  csSup_image (α := αᵒᵈ) hf hf'
-
+@[to_dual]
 theorem cbiSup_id {s : Set α} (hs : BddAbove s) (h : sSup ∅ ≤ sSup s) : ⨆ i ∈ s, i = sSup s := by
   rw [← csSup_image (Subtype.range_coe ▸ hs), Set.image_id']
   · convert! h
     rw [← sSup_range, Subtype.range_coe]
 
-theorem cbiInf_id {s : Set α} (hs : BddBelow s) (h : sInf s ≤ sInf ∅) : ⨅ i ∈ s, i = sInf s := by
-  rw [← csInf_image (Subtype.range_coe ▸ hs), Set.image_id']
-  · convert! h
-    rw [← sInf_range, Subtype.range_coe]
-
+@[to_dual]
 lemma ciSup_image {ι ι' : Type*} {s : Set ι} {f : ι → ι'} {g : ι' → α}
     (hf : BddAbove (Set.range fun i : s ↦ g (f i))) (hg' : sSup ∅ ≤ ⨆ i : s, g (f i)) :
     ⨆ i ∈ (f '' s), g i = ⨆ x ∈ s, g (f x) := by
@@ -375,13 +287,9 @@ lemma ciSup_image {ι ι' : Type*} {s : Set ι} {f : ι → ι'} {g : ι' → α
     simpa [bddAbove_def] using hf
   rw [← csSup_image hg hf', ← csSup_image hf hg', ← Set.image_comp, comp_def]
 
-lemma ciInf_image {ι ι' : Type*} {s : Set ι} {f : ι → ι'} {g : ι' → α}
-    (hf : BddBelow (Set.range fun i : s ↦ g (f i))) (hg' : ⨅ i : s, g (f i) ≤ sInf ∅) :
-    ⨅ i ∈ (f '' s), g i = ⨅ x ∈ s, g (f x) :=
-  ciSup_image (α := αᵒᵈ) hf hg'
-
 /-- Note that equality need not hold: consider `ι := Bool, p := (·), α := ℤ, f := fun _ ↦ -1`,
 then the LHS is `-1` but the RHS is `-1 ⊔ sSup ∅ = -1 ⊔ 0 = 0`. -/
+@[to_dual]
 theorem ciSup_exists_le {p : ι → Prop} {f : Exists p → α} : ⨆ ih, f ih ≤ ⨆ (i) (h), f ⟨i, h⟩ := by
   by_cases! h : Exists p
   · have : Nonempty <| Exists p := ⟨h⟩
@@ -391,15 +299,10 @@ theorem ciSup_exists_le {p : ι → Prop} {f : Exists p → α} : ⨆ ih, f ih 
   · cases isEmpty_or_nonempty ι <;>
       simp [h, iSup_of_empty', ciSup_const]
 
-theorem le_ciInf_exists {p : ι → Prop} {f : Exists p → α} : ⨅ (i) (h), f ⟨i, h⟩ ≤ ⨅ ih, f ih :=
-  ciSup_exists_le (α := αᵒᵈ)
-
+@[to_dual]
 theorem ciSup_and {p q : Prop} {f : p ∧ q → α} : ⨆ ih, f ih = ⨆ (h₁) (h₂), f ⟨h₁, h₂⟩ := by
   by_cases hp : p <;> by_cases hq : q <;> simp [hp, hq, iSup_of_empty']
 
-theorem ciInf_and {p q : Prop} {f : p ∧ q → α} : ⨅ ih, f ih = ⨅ (h₁) (h₂), f ⟨h₁, h₂⟩ :=
-  ciSup_and (α := αᵒᵈ)
-
 end ConditionallyCompleteLattice
 
 section ConditionallyCompleteLinearOrder
@@ -421,16 +324,14 @@ theorem ciInf_inf_le {f g : ι → α} : (⨅ x, f x) ⊓ (⨅ x, g x) ≤ ⨅ x
 /-- Indexed version of `exists_lt_of_lt_csSup`.
 When `b < iSup f`, there is an element `i` such that `b < f i`.
 -/
+@[to_dual exists_lt_of_ciInf_lt
+/-- Indexed version of `exists_lt_of_csInf_lt`.
+When `iInf f < a`, there is an element `i` such that `f i < a`.
+-/]
 theorem exists_lt_of_lt_ciSup [Nonempty ι] {f : ι → α} (h : b < iSup f) : ∃ i, b < f i :=
   let ⟨_, ⟨i, rfl⟩, h⟩ := exists_lt_of_lt_csSup (range_nonempty f) h
   ⟨i, h⟩
 
-/-- Indexed version of `exists_lt_of_csInf_lt`.
-When `iInf f < a`, there is an element `i` such that `f i < a`.
--/
-theorem exists_lt_of_ciInf_lt [Nonempty ι] {f : ι → α} (h : iInf f < a) : ∃ i, f i < a :=
-  exists_lt_of_lt_ciSup (α := αᵒᵈ) h
-
 theorem lt_ciSup_iff [Nonempty ι] {f : ι → α} (hb : BddAbove (range f)) :
     a < iSup f ↔ ∃ i, a < f i := by
   simpa only [mem_range, exists_exists_eq_and] using! lt_csSup_iff hb (range_nonempty _)
@@ -566,38 +467,26 @@ namespace GaloisConnection
 variable [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [Nonempty ι] {l : α → β}
   {u : β → α}
 
+@[to_dual u_csInf]
 theorem l_csSup (gc : GaloisConnection l u) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) :
     l (sSup s) = ⨆ x : s, l x :=
   Eq.symm <| IsLUB.ciSup_set_eq (gc.isLUB_l_image <| isLUB_csSup hne hbdd) hne
 
+@[to_dual u_csInf']
 theorem l_csSup' (gc : GaloisConnection l u) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) :
     l (sSup s) = sSup (l '' s) := by rw [gc.l_csSup hne hbdd, sSup_image']
 
+@[to_dual u_ciInf]
 theorem l_ciSup (gc : GaloisConnection l u) {f : ι → α} (hf : BddAbove (range f)) :
     l (⨆ i, f i) = ⨆ i, l (f i) := by rw [iSup, gc.l_csSup (range_nonempty _) hf, iSup_range']
 
+@[to_dual u_ciInf_set]
 theorem l_ciSup_set (gc : GaloisConnection l u) {s : Set γ} {f : γ → α} (hf : BddAbove (f '' s))
     (hne : s.Nonempty) : l (⨆ i : s, f i) = ⨆ i : s, l (f i) := by
   haveI := hne.to_subtype
   rw [image_eq_range] at hf
   exact gc.l_ciSup hf
 
-theorem u_csInf (gc : GaloisConnection l u) {s : Set β} (hne : s.Nonempty) (hbdd : BddBelow s) :
-    u (sInf s) = ⨅ x : s, u x :=
-  gc.dual.l_csSup hne hbdd
-
-theorem u_csInf' (gc : GaloisConnection l u) {s : Set β} (hne : s.Nonempty) (hbdd : BddBelow s) :
-    u (sInf s) = sInf (u '' s) :=
-  gc.dual.l_csSup' hne hbdd
-
-theorem u_ciInf (gc : GaloisConnection l u) {f : ι → β} (hf : BddBelow (range f)) :
-    u (⨅ i, f i) = ⨅ i, u (f i) :=
-  gc.dual.l_ciSup hf
-
-theorem u_ciInf_set (gc : GaloisConnection l u) {s : Set γ} {f : γ → β} (hf : BddBelow (f '' s))
-    (hne : s.Nonempty) : u (⨅ i : s, f i) = ⨅ i : s, u (f i) :=
-  gc.dual.l_ciSup_set hf hne
-
 end GaloisConnection
 
 namespace OrderIso
@@ -605,38 +494,26 @@ namespace OrderIso
 section ConditionallyCompleteLattice
 variable [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [Nonempty ι]
 
+@[to_dual]
 theorem map_csSup (e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) :
     e (sSup s) = ⨆ x : s, e x :=
   e.to_galoisConnection.l_csSup hne hbdd
 
+@[to_dual]
 theorem map_csSup' (e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) :
     e (sSup s) = sSup (e '' s) :=
   e.to_galoisConnection.l_csSup' hne hbdd
 
+@[to_dual]
 theorem map_ciSup (e : α ≃o β) {f : ι → α} (hf : BddAbove (range f)) :
     e (⨆ i, f i) = ⨆ i, e (f i) :=
   e.to_galoisConnection.l_ciSup hf
 
+@[to_dual]
 theorem map_ciSup_set (e : α ≃o β) {s : Set γ} {f : γ → α} (hf : BddAbove (f '' s))
     (hne : s.Nonempty) : e (⨆ i : s, f i) = ⨆ i : s, e (f i) :=
   e.to_galoisConnection.l_ciSup_set hf hne
 
-theorem map_csInf (e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddBelow s) :
-    e (sInf s) = ⨅ x : s, e x :=
-  e.dual.map_csSup hne hbdd
-
-theorem map_csInf' (e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddBelow s) :
-    e (sInf s) = sInf (e '' s) :=
-  e.dual.map_csSup' hne hbdd
-
-theorem map_ciInf (e : α ≃o β) {f : ι → α} (hf : BddBelow (range f)) :
-    e (⨅ i, f i) = ⨅ i, e (f i) :=
-  e.dual.map_ciSup hf
-
-theorem map_ciInf_set (e : α ≃o β) {s : Set γ} {f : γ → α} (hf : BddBelow (f '' s))
-    (hne : s.Nonempty) : e (⨅ i : s, f i) = ⨅ i : s, e (f i) :=
-  e.dual.map_ciSup_set hf hne
-
 end ConditionallyCompleteLattice
 
 section ConditionallyCompleteLinearOrderBot
diff --git a/Mathlib/Order/Filter/Germ/Basic.lean b/Mathlib/Order/Filter/Germ/Basic.lean
index 7390a26c100c7e..dd0aa8723d3e62 100644
--- a/Mathlib/Order/Filter/Germ/Basic.lean
+++ b/Mathlib/Order/Filter/Germ/Basic.lean
@@ -406,7 +406,7 @@ theorem const_pow [Pow G M] (a : G) (n : M) : (↑(a ^ n) : Germ l G) = (↑a :
 -- TODO: https://github.com/leanprover-community/mathlib4/pull/7432
 @[to_additive]
 instance instMonoid [Monoid M] : Monoid (Germ l M) :=
-  { Function.Surjective.monoid ofFun Quot.mk_surjective (by rfl)
+  { Function.Surjective.monoid ofFun Quot.mk_surjective rfl
       (fun _ _ => by rfl) fun _ _ => by rfl with
     toSemigroup := instSemigroup
     toOne := instOne
diff --git a/Mathlib/Probability/Decision/BayesEstimator.lean b/Mathlib/Probability/Decision/BayesEstimator.lean
new file mode 100644
index 00000000000000..7f3991f3a74edc
--- /dev/null
+++ b/Mathlib/Probability/Decision/BayesEstimator.lean
@@ -0,0 +1,168 @@
+/-
+Copyright (c) 2025 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne, Lorenzo Luccioli
+-/
+module
+
+public import Mathlib.Probability.Decision.Risk.Defs
+public import Mathlib.Probability.Kernel.Posterior
+
+import Mathlib.Probability.Decision.Risk.Basic
+
+/-!
+# Bayes estimator
+
+Let `Θ` be a parameter space, `𝓧` a data space, `𝓨` a prediction space, `P : Kernel Θ 𝓧` a
+data generating kernel, `π` a prior on the parameter space, and `ℓ : Θ → 𝓨 → ℝ≥0∞` a loss function.
+
+An estimator (a `Kernel 𝓧 𝓨`) is said to be a Bayes estimator if it attains the Bayes risk for
+the estimation problem.
+It can be written as a measurable function `x ↦ argmin_y P†π(x)[θ ↦ ℓ θ y]`
+for `(P ∘ₘ π)`-almost every `x`, where `P†π` is the posterior kernel, whenever we can select
+the argmin in a measurable way.
+
+## Main definitions
+
+* `IsBayesEstimator`: an estimator is a Bayes estimator if it attains the Bayes risk for the prior.
+* `IsArgminEstimator`: a measurable function `f : 𝓧 → 𝓨` is an argmin estimator
+  if for `(P ∘ₘ π)`-almost every `x` the value `f x` belongs to `argmin_y P†π(x)[θ ↦ ℓ θ y]`.
+* `HasArgminEstimator`: the estimation problem admits an argmin estimator.
+  That is, we can choose the argmin of the posterior expected loss in a measurable way.
+
+## Main statements
+
+* `lintegral_iInf_posterior_le_bayesRisk`: the Bayes risk with respect to a prior is bounded
+  from below by the integral over the data (with distribution `P ∘ₘ π`) of the infimum over the
+  possible predictions `y` of the posterior loss `∫⁻ θ, ℓ θ y ∂((P†π) x)`:
+  `∫⁻ x, ⨅ y : 𝓨, ∫⁻ θ, ℓ θ y ∂((P†π) x) ∂(P ∘ₘ π) ≤ bayesRisk ℓ P π`
+* `IsArgminEstimator.isBayesEstimator`: an argmin Bayes estimator is a Bayes estimator.
+  That is, it minimizes the Bayesian risk.
+* `bayesRisk_eq_of_hasArgminEstimator`: if the estimation problem admits an argmin estimator,
+  then the Bayesian risk attains the risk lower bound `∫⁻ x, ⨅ y, ∫⁻ θ, ℓ θ y ∂(P†π) x ∂(P ∘ₘ π)`.
+
+## TODO
+
+Once Mathlib has measurable selection theorems, we will be able to prove `HasArgminEstimator` under
+general conditions on the measurable spaces `𝓧` and/or `𝓨`.
+
+-/
+
+@[expose] public section
+
+open MeasureTheory
+open scoped ENNReal NNReal
+
+namespace ProbabilityTheory
+
+variable {Θ 𝓧 𝓨 : Type*} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨}
+  {ℓ : Θ → 𝓨 → ℝ≥0∞} {P : Kernel Θ 𝓧} {κ : Kernel 𝓧 𝓨} {π : Measure Θ}
+
+section Posterior
+
+variable [StandardBorelSpace Θ] [Nonempty Θ]
+
+/-- The average risk of an estimator `κ` with respect to a prior `π` can be expressed as
+an integral in the following way: `R_π(κ) = ((P†π × κ) ∘ P ∘ π)[(θ, y) ↦ ℓ θ y]`. -/
+lemma avgRisk_eq_lintegral_posterior_prod
+    (hl : Measurable (Function.uncurry ℓ)) (P : Kernel Θ 𝓧) [IsFiniteKernel P]
+    (κ : Kernel 𝓧 𝓨) [IsSFiniteKernel κ] (π : Measure Θ) [IsFiniteMeasure π] :
+    avgRisk ℓ P κ π = ∫⁻ θy, ℓ θy.1 θy.2 ∂(((P†π) ×ₖ κ) ∘ₘ (P ∘ₘ π)) := by
+  rw [avgRisk, ← Measure.lintegral_compProd (f := fun θy ↦ ℓ θy.1 θy.2) (by fun_prop)]
+  congr
+  calc π ⊗ₘ (κ ∘ₖ P) = (Kernel.id ∥ₖ κ) ∘ₘ (π ⊗ₘ P) := Measure.parallelComp_comp_compProd.symm
+  _ = (Kernel.id ∥ₖ κ) ∘ₘ ((P†π) ×ₖ Kernel.id) ∘ₘ P ∘ₘ π := by rw [posterior_prod_id_comp]
+  _ = ((P†π) ×ₖ κ) ∘ₘ P ∘ₘ π := by
+      rw [Measure.comp_assoc, Kernel.parallelComp_comp_prod, Kernel.id_comp, Kernel.comp_id]
+
+lemma avgRisk_eq_lintegral_lintegral_lintegral
+    (hl : Measurable (Function.uncurry ℓ)) (P : Kernel Θ 𝓧) [IsFiniteKernel P]
+    (κ : Kernel 𝓧 𝓨) [IsSFiniteKernel κ] (π : Measure Θ) [IsFiniteMeasure π] :
+    avgRisk ℓ P κ π = ∫⁻ x, ∫⁻ y, ∫⁻ θ, ℓ θ y ∂(P†π) x ∂κ x ∂(P ∘ₘ π) := by
+  rw [avgRisk_eq_lintegral_posterior_prod hl, Measure.lintegral_bind (by fun_prop) (by fun_prop)]
+  congr with x
+  rw [Kernel.prod_apply, lintegral_prod_symm' _ (by fun_prop)]
+
+lemma lintegral_iInf_posterior_le_avgRisk
+    (hl : Measurable (Function.uncurry ℓ)) (P : Kernel Θ 𝓧) [IsFiniteKernel P]
+    (κ : Kernel 𝓧 𝓨) [IsMarkovKernel κ] (π : Measure Θ) [IsFiniteMeasure π] :
+    ∫⁻ x, ⨅ y : 𝓨, ∫⁻ θ, ℓ θ y ∂((P†π) x) ∂(P ∘ₘ π) ≤ avgRisk ℓ P κ π := by
+  rw [avgRisk_eq_lintegral_lintegral_lintegral hl]
+  gcongr with x
+  exact iInf_le_lintegral _
+
+lemma lintegral_iInf_posterior_le_bayesRisk
+    (hl : Measurable (Function.uncurry ℓ)) (P : Kernel Θ 𝓧) [IsFiniteKernel P]
+    (π : Measure Θ) [IsFiniteMeasure π] :
+    ∫⁻ x, ⨅ y : 𝓨, ∫⁻ θ, ℓ θ y ∂((P†π) x) ∂(P ∘ₘ π) ≤ bayesRisk ℓ P π :=
+  le_iInf₂ fun κ _ ↦ lintegral_iInf_posterior_le_avgRisk hl P κ π
+
+end Posterior
+
+/-- An estimator is a Bayes estimator for a prior `π` if it attains the Bayes risk for `π`. -/
+def IsBayesEstimator (ℓ : Θ → 𝓨 → ℝ≥0∞) (P : Kernel Θ 𝓧) (κ : Kernel 𝓧 𝓨) (π : Measure Θ) : Prop :=
+  avgRisk ℓ P κ π = bayesRisk ℓ P π
+
+variable [StandardBorelSpace Θ] [Nonempty Θ] {f : 𝓧 → 𝓨} [IsFiniteKernel P] [IsFiniteMeasure π]
+
+/-- We say that a measurable function `f : 𝓧 → 𝓨` is an argmin estimator
+with respect to the prior `π` if for `(P ∘ₘ π)`-almost every `x` it is of
+the form `x ↦ argmin_y P†π(x)[θ ↦ ℓ θ y]`. -/
+structure IsArgminEstimator {𝓨 : Type*} [MeasurableSpace 𝓨]
+    (ℓ : Θ → 𝓨 → ℝ≥0∞) (P : Kernel Θ 𝓧) [IsFiniteKernel P]
+    (π : Measure Θ) [IsFiniteMeasure π] (f : 𝓧 → 𝓨) : Prop where
+  measurable : Measurable f
+  property : ∀ᵐ x ∂(P ∘ₘ π), ∫⁻ θ, ℓ θ (f x) ∂(P†π) x = ⨅ y, ∫⁻ θ, ℓ θ y ∂(P†π) x
+
+/-- Given an argmin estimator `f`, we can define a deterministic kernel. -/
+protected noncomputable
+abbrev IsArgminEstimator.kernel (h : IsArgminEstimator ℓ P π f) : Kernel 𝓧 𝓨 :=
+  Kernel.deterministic f h.measurable
+
+/-- The risk of an argmin estimator is the risk lower bound
+`∫⁻ x, ⨅ z, ∫⁻ θ, ℓ θ z ∂(P†π) x ∂(P ∘ₘ π)`. -/
+lemma IsArgminEstimator.avgRisk_eq_lintegral_iInf (hf : IsArgminEstimator ℓ P π f)
+    (hl : Measurable (Function.uncurry ℓ)) :
+    avgRisk ℓ P hf.kernel π = ∫⁻ x, ⨅ y, ∫⁻ θ, ℓ θ y ∂(P†π) x ∂(P ∘ₘ π) := by
+  rw [avgRisk_eq_lintegral_lintegral_lintegral hl]
+  refine lintegral_congr_ae ?_
+  filter_upwards [hf.property] with x hx
+  rwa [Kernel.lintegral_deterministic' _ (by fun_prop)]
+
+/-- An argmin estimator is a Bayes estimator: that is, it minimizes the Bayesian risk. -/
+lemma IsArgminEstimator.isBayesEstimator (hf : IsArgminEstimator ℓ P π f)
+    (hl : Measurable (Function.uncurry ℓ)) :
+    IsBayesEstimator ℓ P hf.kernel π := by
+  refine le_antisymm ?_ (bayesRisk_le_avgRisk _ _ _ _)
+  rw [hf.avgRisk_eq_lintegral_iInf hl]
+  exact lintegral_iInf_posterior_le_bayesRisk hl _ _
+
+/-- The estimation problem admits an argmin estimator with respect to the prior `π`.
+That is, we can choose the argmin of the posterior expected loss in a measurable way. -/
+structure HasArgminEstimator {𝓨 : Type*} [MeasurableSpace 𝓨]
+    (ℓ : Θ → 𝓨 → ℝ≥0∞) (P : Kernel Θ 𝓧) [IsFiniteKernel P] (π : Measure Θ) [IsFiniteMeasure π] :
+    Prop where
+  exists_isArgminEstimator : ∃ f : 𝓧 → 𝓨, IsArgminEstimator ℓ P π f
+
+namespace HasArgminEstimator
+
+/-- An estimator for an estimation problem that for `(P ∘ₘ π)`-almost every `x` is of
+the form `x ↦ argmin_y P†π(x)[θ ↦ ℓ θ y]`. -/
+noncomputable
+def argminEstimator (h : HasArgminEstimator ℓ P π) : 𝓧 → 𝓨 :=
+  h.exists_isArgminEstimator.choose
+
+lemma isArgminEstimator_argminEstimator (h : HasArgminEstimator ℓ P π) :
+    IsArgminEstimator ℓ P π h.argminEstimator :=
+  h.exists_isArgminEstimator.choose_spec
+
+/-- If the estimation problem admits an argmin estimator, then the Bayesian risk
+attains the risk lower bound `∫⁻ x, ⨅ y, ∫⁻ θ, ℓ θ y ∂((P†π) x) ∂(P ∘ₘ π)`. -/
+lemma bayesRisk_eq (hl : Measurable (Function.uncurry ℓ)) (h : HasArgminEstimator ℓ P π) :
+    bayesRisk ℓ P π = ∫⁻ x, ⨅ y, ∫⁻ θ, ℓ θ y ∂((P†π) x) ∂(P ∘ₘ π) := by
+  rw [← h.isArgminEstimator_argminEstimator.isBayesEstimator hl,
+    h.isArgminEstimator_argminEstimator.avgRisk_eq_lintegral_iInf hl]
+
+end HasArgminEstimator
+
+end ProbabilityTheory
diff --git a/Mathlib/RepresentationTheory/Intertwining.lean b/Mathlib/RepresentationTheory/Intertwining.lean
index a4931239af1b82..ebcc0244e85ec0 100644
--- a/Mathlib/RepresentationTheory/Intertwining.lean
+++ b/Mathlib/RepresentationTheory/Intertwining.lean
@@ -498,7 +498,7 @@ noncomputable def equivAlgEnd :
     IntertwiningMap ρ ρ ≃ₐ[A] Module.End A[G] ρ.asModule :=
   AlgEquiv.ofLinearEquiv
     (equivLinearMapAsModule ρ ρ)
-    (by rfl)
+    rfl
     (by intro f g; rfl)
 
 theorem isIntertwiningMap_of_mem_center (g : G) (hg : g ∈ Submonoid.center G) :
diff --git a/Mathlib/RingTheory/AdicCompletion/Completeness.lean b/Mathlib/RingTheory/AdicCompletion/Completeness.lean
index ef7db25d3cb756..5f8b5b456c3b61 100644
--- a/Mathlib/RingTheory/AdicCompletion/Completeness.lean
+++ b/Mathlib/RingTheory/AdicCompletion/Completeness.lean
@@ -102,8 +102,8 @@ def ofValEqZero {n : ℕ} {x : AdicCompletion I M} (hxn : x.val n = 0) :
   val i := ofValEqZeroAux I (Eq.refl (i + n)) hxn
   property {i j} h := by
     obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
-    rw [← (powSMulQuotInclusion_injective I (by rfl) ⊤).eq_iff, ofValEqZeroAux_prop,
-      ← LinearMap.comp_apply, ← factorPow_comp_powSMulQuotInclusion I (by rfl)
+    rw [← (powSMulQuotInclusion_injective I rfl ⊤).eq_iff, ofValEqZeroAux_prop,
+      ← LinearMap.comp_apply, ← factorPow_comp_powSMulQuotInclusion I rfl
       (show i + k + n = k + (i + n) by ring), LinearMap.comp_apply, ofValEqZeroAux_prop]
     exact x.prop (by lia)
 
@@ -112,7 +112,7 @@ theorem ofPowSMul_ofValEqZero {n : ℕ} {x : AdicCompletion I M} (hxn : x.val n
     ofPowSMul I M n (ofValEqZero I hxn) = x := by
   ext i; by_cases! h : n ≤ i
   · obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le' h
-    rw [ofPowSMul_val_apply _ (by rfl), ofValEqZero, ofValEqZeroAux_prop]
+    rw [ofPowSMul_val_apply _ rfl, ofValEqZero, ofValEqZeroAux_prop]
   rw [ofPowSMul_val_apply_eq_zero _ h.le, ← x.prop h.le, hxn, _root_.map_zero]
 
 theorem restrictScalars_range_ofPowSMul_eq_ker_eval {n : ℕ} :
diff --git a/Mathlib/RingTheory/Adjoin/Singleton.lean b/Mathlib/RingTheory/Adjoin/Singleton.lean
index 1bde86bb66cd0c..2b26c1ddf9c972 100644
--- a/Mathlib/RingTheory/Adjoin/Singleton.lean
+++ b/Mathlib/RingTheory/Adjoin/Singleton.lean
@@ -55,7 +55,7 @@ instance : Algebra A[b] A[(algebraMap B C) b] :=
   RingHom.toAlgebra (RingHom.adjoinAlgebraMap b)
 
 instance : IsScalarTower A[b] A[(algebraMap B C) b] C :=
-  IsScalarTower.of_algebraMap_eq' (by rfl)
+  IsScalarTower.of_algebraMap_eq' rfl
 
 /-- If the `algebraMap` injective then we have a Ring isomorphism between A[b] and A[↑b]. -/
 noncomputable def RingHom.adjoinAlgebraMapEquiv [FaithfulSMul B C] :
diff --git a/Mathlib/RingTheory/Algebraic/Basic.lean b/Mathlib/RingTheory/Algebraic/Basic.lean
index d1fefdb9b42f5a..e4771691dbe162 100644
--- a/Mathlib/RingTheory/Algebraic/Basic.lean
+++ b/Mathlib/RingTheory/Algebraic/Basic.lean
@@ -343,7 +343,7 @@ theorem isAlgebraic_of_isAlgebraic_bot {x : S} (halg : IsAlgebraic (⊥ : Subalg
 theorem isAlgebraic_bot_iff (h : Function.Injective (algebraMap R S)) {x : S} :
     IsAlgebraic (⊥ : Subalgebra R S) x ↔ IsAlgebraic R x :=
   isAlgebraic_ringHom_iff_of_comp_eq (Algebra.botEquivOfInjective h).symm (RingHom.id S)
-    Function.injective_id (by rfl)
+    Function.injective_id rfl
 
 variable (R S) in
 theorem algebra_isAlgebraic_of_algebra_isAlgebraic_bot_left
diff --git a/Mathlib/RingTheory/Extension/Cotangent/Basic.lean b/Mathlib/RingTheory/Extension/Cotangent/Basic.lean
index e389a24689ec0e..0f6e4172bbc0d5 100644
--- a/Mathlib/RingTheory/Extension/Cotangent/Basic.lean
+++ b/Mathlib/RingTheory/Extension/Cotangent/Basic.lean
@@ -68,6 +68,12 @@ def cotangentComplex : P.Cotangent →ₗ[S] P.CotangentSpace :=
 lemma cotangentComplex_mk (x) : P.cotangentComplex (.mk x) = 1 ⊗ₜ .D _ _ x :=
   rfl
 
+lemma Cotangent.mk_C_mem_ker_cotangentComplex {σ : Type*} (G : Generators R S σ)
+    {r : R} (hr : C r ∈ G.ker) :
+    Extension.Cotangent.mk ⟨C r, hr⟩ ∈ G.toExtension.cotangentComplex.ker := by
+  have : D R G.toExtension.Ring (C r) = 0 := Derivation.map_algebraMap ..
+  simp [this]
+
 section baseChange
 
 variable {A : Type*} [CommRing A] [Algebra S A] [Algebra P.Ring A] [IsScalarTower P.Ring S A]
@@ -435,6 +441,11 @@ def H1Cotangent.equiv {P₁ P₂ : Extension R S} (f₁ : P₁.Hom P₂) (f₂ :
     rw [← Extension.H1Cotangent.map_id, eq_comm, map_eq _ (f₁.comp f₂),
       Extension.H1Cotangent.map_comp]; rfl
 
+omit [IsScalarTower R S S'] in
+lemma Cotangent.map_comp_h1Cotangentι (f : P.Hom P') :
+    Cotangent.map f ∘ₗ P.h1Cotangentι =
+      P'.h1Cotangentι.restrictScalars S ∘ₗ H1Cotangent.map f := rfl
+
 end Extension
 
 namespace Generators
diff --git a/Mathlib/RingTheory/Extension/ExtendScalars.lean b/Mathlib/RingTheory/Extension/ExtendScalars.lean
new file mode 100644
index 00000000000000..0037ec8ed4ea75
--- /dev/null
+++ b/Mathlib/RingTheory/Extension/ExtendScalars.lean
@@ -0,0 +1,167 @@
+/-
+Copyright (c) 2024 Bingyu Xia. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bingyu Xia
+-/
+module
+
+public import Mathlib.RingTheory.Kaehler.JacobiZariski
+
+/-!
+# Extension of Scalars for Algebra Extensions
+
+This file provides APIs for extending the base ring of an algebra extension `P : Extension R S`
+to its own extension ring `P.Ring`. We introduce canonical maps and isomorphisms between
+the cotangent spaces and the first homology of naive cotangent complex associated with
+`P.extendScalars` and `P`. We provide commutativity results of these maps and ismorphisms
+(See https://github.com/leanprover-community/mathlib4/pull/39520 for an image of the full diagram).
+In particular, we show the boundary map of the Jacobi-Zariski sequence of `R → P.Ring → S`
+coincides with `P.cotangentComplex` via a canonical isomorphism `P.h1CotangentEquivCotangent`.
+
+## Main definitions and results
+
+- `extendScalars`: Views `P : Extension R S` as `Extension P.Ring S`.
+- `toExtendScalars`: The canonical homomorphism from `P` to `P.extendScalars` induced by
+  the identity map on the underlying extension rings.
+- `cotangentExtendScalarsEquiv` : The linear equivalence between the cotangent spaces of
+  `P.extensScalars` and `P` induced by the identity map.
+- `h1CotangentExtendScalarsEquiv`: `P.extensScalars` can be used to compute the first homology of
+  the naive cotangent complex of `S` over `P.Ring`.
+- `h1CotangentEquivOfSurjective`: If `R → P.Ring` is surjective, this is the linear isomorphism
+  induced by `P.h1Cotangentι`.
+- `h1CotangentEquivCotangent`: This is the linear equivalence between `H1Cotangent P.Ring S` and
+  `P.Cotangent` defined by the composition of `h1CotangentExtendScalarsEquiv.symm`,
+  `h1CotangentEquivOfSurjective` and `cotangentExtendScalarsEquiv`.
+- `cotangentComplex_comp_h1CotangentEquivCotangent`,
+  `h1CotangentEquivCotangent_comp_map`: commutativity results.
+
+-/
+
+@[expose] public section
+
+open KaehlerDifferential
+
+namespace Algebra.Extension
+
+universe w v u
+
+variable {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
+
+/-- Given an extension `P` of `S` over `R`, `P.extendScalars` is the same extension
+but viewed as an extension of `S` over `P.Ring`. -/
+@[simps]
+def extendScalars {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
+    (P : Extension.{w} R S) : Extension P.Ring S where
+  Ring := P.Ring
+  σ := P.σ
+  algebraMap_σ := P.algebraMap_σ
+
+set_option backward.isDefEq.respectTransparency false in
+set_option backward.defeqAttrib.useBackward true in
+/-- The canonical homomorphism from `P` to `P.extendScalars` induced by the identity map
+on the underlying extension rings. -/
+@[simps!]
+noncomputable
+def toExtendScalars {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
+    (P : Extension.{w} R S) : P.Hom P.extendScalars :=
+  .ofAlgHom (IsScalarTower.toAlgHom R P.Ring P.extendScalars.Ring)
+    (by dsimp; ext; simp)
+
+/-- `Extension.extendScalars` does not change the cotangent space of an extension. -/
+noncomputable
+def cotangentExtendScalarsEquiv {R : Type u} {S : Type v} [CommRing R] [CommRing S]
+    [Algebra R S] (P : Extension.{w} R S) :
+    P.extendScalars.Cotangent ≃ₗ[S] P.Cotangent :=
+  LinearEquiv.refl _ _
+
+@[simp]
+lemma cotangentExtendScalarsEquiv_symm_toLinearMap (P : Extension.{w} R S) :
+    P.cotangentExtendScalarsEquiv.symm.toLinearMap = Cotangent.map P.toExtendScalars := by
+  ext x
+  obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
+  rfl
+
+set_option backward.isDefEq.respectTransparency false in
+theorem H1Cotangent.map_toExtendScalars_injective (P : Extension.{w} R S) :
+    Function.Injective (H1Cotangent.map P.toExtendScalars) := by
+  rw [← LinearMap.ker_eq_bot, H1Cotangent.map, LinearMap.ker_restrict,
+    ← cotangentExtendScalarsEquiv_symm_toLinearMap, LinearEquiv.ker,
+    Submodule.comap_bot, Submodule.ker_subtype]
+
+/-- The first homology of the naive cotangent complex of `P.extendScalars` is
+linearly equivalent to that of `S` over `P.Ring`. -/
+@[simps! toLinearMap]
+noncomputable
+def h1CotangentExtendScalarsEquiv {R : Type u} {S : Type v} [CommRing R] [CommRing S]
+    [Algebra R S] (P : Extension.{w} R S) :
+    P.extendScalars.H1Cotangent ≃ₗ[S] H1Cotangent P.Ring S :=
+  Extension.H1Cotangent.equiv
+    (.ofAlgHom (Algebra.ofId _ _) (by ext)) P.extendScalars.defaultHom
+
+@[simp]
+lemma h1CotangentExtendScalarsEquiv_symm_toLinearMap (P : Extension.{w} R S) :
+  P.h1CotangentExtendScalarsEquiv.symm = H1Cotangent.map P.extendScalars.defaultHom := rfl
+
+/-- Given an extension `P` of `S` over `R` such that `algebraMap R P.Ring` is surjective,
+this is the equivalence induced by `P.h1Cotangentι`. -/
+@[simps! toLinearMap]
+noncomputable
+def h1CotangentEquivOfSurjective {R : Type u} {S : Type v} [CommRing R] [CommRing S]
+    [Algebra R S] (P : Extension.{w} R S) (h : Function.Surjective (algebraMap R P.Ring)) :
+    P.H1Cotangent ≃ₗ[S] P.Cotangent where
+  __ := P.h1Cotangentι
+  invFun x := ⟨x, by
+    have : Subsingleton Ω[P.Ring⁄R] := subsingleton_of_surjective R P.Ring h
+    exact Subsingleton.elim _ _⟩
+
+/-- Given an extension `P : Extension R S`, this is the linear equivalence between
+the first homology of the naive cotangent complex of `S` over `P.Ring` and
+the cotangent space of `P`. -/
+noncomputable
+def h1CotangentEquivCotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S]
+    [Algebra R S] (P : Extension.{w} R S) :
+    H1Cotangent P.Ring S ≃ₗ[S] P.Cotangent :=
+  P.h1CotangentExtendScalarsEquiv.symm ≪≫ₗ
+    P.extendScalars.h1CotangentEquivOfSurjective Function.surjective_id ≪≫ₗ
+    P.cotangentExtendScalarsEquiv
+
+theorem cotangentComplex_comp_h1CotangentEquivCotangent (P : Extension.{w} R S) :
+    P.cotangentComplex.comp P.h1CotangentEquivCotangent.toLinearMap =
+      H1Cotangent.δ R P.Ring S := by
+  rw [h1CotangentEquivCotangent, LinearEquiv.coe_trans, LinearEquiv.coe_trans,
+    h1CotangentEquivOfSurjective_toLinearMap, ← LinearMap.comp_assoc, ← LinearMap.comp_assoc,
+    LinearEquiv.comp_toLinearMap_symm_eq, LinearMap.comp_assoc,
+    h1CotangentExtendScalarsEquiv_toLinearMap]
+  ext ⟨x, _⟩
+  obtain ⟨⟨x : P.Ring, x_in : x ∈ P.ker⟩, rfl⟩ := Cotangent.mk_surjective x
+  trans 1 ⊗ₜ[P.Ring] D R P.Ring x; · exact cotangentComplex_mk P ⟨x, x_in⟩
+  let u : (Generators.self P.Ring S).toExtension.ker :=
+    ⟨algebraMap P.Ring (Generators.self P.Ring S).toExtension.Ring x, by
+      rwa [← Ideal.mem_comap, RingHom.comap_ker, ← IsScalarTower.algebraMap_eq]⟩
+  rw [← Generators.H1Cotangent.δ_C _ _ u.prop]
+  congr
+
+theorem h1CotangentEquivCotangent_comp_map (P : Extension.{w} R S) :
+    P.h1CotangentEquivCotangent.toLinearMap.comp (Algebra.H1Cotangent.map R P.Ring S S) =
+      h1Cotangentι.comp (H1Cotangent.map P.defaultHom) := by
+  rw [h1CotangentEquivCotangent, LinearEquiv.coe_trans, LinearEquiv.coe_trans,
+    h1CotangentExtendScalarsEquiv_symm_toLinearMap, h1CotangentEquivOfSurjective_toLinearMap,
+    LinearMap.comp_assoc, LinearMap.comp_assoc, Algebra.H1Cotangent.map,
+    ← (H1Cotangent.map P.extendScalars.defaultHom).restrictScalars_self, ← H1Cotangent.map_comp,
+    eq_comm, ← LinearEquiv.toLinearMap_symm_comp_eq, cotangentExtendScalarsEquiv_symm_toLinearMap,
+    ← LinearMap.comp_assoc, Cotangent.map_comp_h1Cotangentι, LinearMap.restrictScalars_self,
+    LinearMap.comp_assoc, ← (H1Cotangent.map P.toExtendScalars).restrictScalars_self,
+    ← H1Cotangent.map_comp, H1Cotangent.map_eq]
+
+theorem H1Cotangent.map_defaultHom_surjective (P : Extension.{w} R S) :
+    Function.Surjective (H1Cotangent.map P.defaultHom) := by
+  rw [← LinearMap.range_eq_top,
+    ← (Submodule.map_injective_of_injective h1Cotangentι_injective).eq_iff,
+    ← LinearMap.range_comp, ← P.h1CotangentEquivCotangent_comp_map, LinearMap.range_comp,
+    ← (Algebra.H1Cotangent.exact_map_δ R P.Ring S).linearMap_ker_eq, Submodule.map_top,
+    ← exact_hCotangentι_cotangentComplex.linearMap_ker_eq, Submodule.map_equiv_eq_comap_symm,
+    LinearMap.ker, LinearMap.ker, ← Submodule.comap_comp]
+  congr
+  rw [LinearEquiv.comp_toLinearMap_symm_eq, P.cotangentComplex_comp_h1CotangentEquivCotangent]
+
+end Algebra.Extension
diff --git a/Mathlib/RingTheory/Extension/Generators.lean b/Mathlib/RingTheory/Extension/Generators.lean
index a165eabc2a2ff7..1e3ede9f668cb7 100644
--- a/Mathlib/RingTheory/Extension/Generators.lean
+++ b/Mathlib/RingTheory/Extension/Generators.lean
@@ -798,3 +798,16 @@ lemma toAlgHom_ofComp_localizationAway (g : S) [IsLocalization.Away g T] :
 end Hom
 
 end Algebra.Generators
+
+namespace Algebra.Extension
+
+set_option backward.isDefEq.respectTransparency false in
+set_option backward.defeqAttrib.useBackward true in
+/-- The canonical homomorphism of extensions from the universal extension `R[S] → S`
+(given by `Generators.self R S`) to any extension `P` defined via the designated section `P.σ`. -/
+@[simps!]
+noncomputable
+def defaultHom (P : Extension.{w} R S) : (Generators.self R S).toExtension.Hom P :=
+  .ofAlgHom (MvPolynomial.aeval P.σ) (by dsimp; ext; simp)
+
+end Algebra.Extension
diff --git a/Mathlib/RingTheory/Kaehler/JacobiZariski.lean b/Mathlib/RingTheory/Kaehler/JacobiZariski.lean
index 0175dfdec63ab4..1220b5ccd0bf32 100644
--- a/Mathlib/RingTheory/Kaehler/JacobiZariski.lean
+++ b/Mathlib/RingTheory/Kaehler/JacobiZariski.lean
@@ -400,6 +400,11 @@ lemma δ_eq_δAux (x : Q.ker) (hx) :
       ((Q.comp P).toExtension.cotangentComplex y)
     rw [CotangentSpace.fst_compEquiv, Extension.CotangentSpace.map_cotangentComplex, hy, hx]
 
+lemma δ_C {r : S} (hr : C r ∈ Q.ker) :
+    δ Q P ⟨Extension.Cotangent.mk ⟨C r, hr⟩, Extension.Cotangent.mk_C_mem_ker_cotangentComplex ..⟩
+      = 1 ⊗ₜ[S] D R S r := by
+  rw [δ_eq_δAux, δAux_C]
+
 lemma δ_eq_δ : δ Q P = δ Q P' := by
   ext ⟨x, hx⟩
   obtain ⟨x, rfl⟩ := Extension.Cotangent.mk_surjective x
diff --git a/Mathlib/Topology/CWComplex/Classical/Basic.lean b/Mathlib/Topology/CWComplex/Classical/Basic.lean
index 9ddc89d00f237c..97b4720eaba62a 100644
--- a/Mathlib/Topology/CWComplex/Classical/Basic.lean
+++ b/Mathlib/Topology/CWComplex/Classical/Basic.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Analysis.Normed.Module.RCLike.Real
 public import Mathlib.Data.ENat.Basic
 public import Mathlib.Logic.Equiv.PartialEquiv
+public import Mathlib.Util.AliasIn
 
 /-!
 # CW complexes
@@ -62,6 +63,19 @@ together.
   cells `cell C` of an absolute CW complex `C`, this actually refers to `RelCWComplex.cell C`
   through this instance. Again, we want typeclass inference to first consider absolute CW
   structures.
+* The namespaces `CWComplex` and `RelCWComplex` generally should not be opened at the same time
+  as they contain many declarations with identical names. Still, we want working with absolute
+  CW complexes to be  as convenient as possible. Thus every declaration about relative CW complexes
+  that doesn't have a modified version for absolute CW complexes should receive an alias in the
+  `CWComplex` namespace. It is recommended to use the `alias_in` attribute for this here. See
+  below for a restriction on when we want to create aliases.
+* For types and definitions relevant to CW complexes like `cell`, `openCell`, `closedCell`,
+  `cellFrontier`, `skeletonLT` and similar, we want there to exist only one actually used version,
+  namely the version in the `RelCWComplex` namespace (and thus no seperate definition in the
+  `CWComplex` namespace.) This is to avoid unnecessary duplication of lemmas. To achieve this,
+  definitions from the `RelCWComplex` namespace should be added to the `CWComplex` namespace with
+  `export` intead of `alias_in`/`alias`. These will then apply to the absolute CW complex through
+  the instance `CWComplex.instRelCWComplex`.
 * For statements, the auxiliary construction `skeletonLT` is preferred over `skeleton` as it makes
   the base case of inductions easier. The statement about `skeleton` should then be derived from the
   one about `skeletonLT`.
@@ -199,7 +213,7 @@ def RelCWComplex.cellFrontier [RelCWComplex C D] (n : ℕ) (i : cell C n) : Set
 
 namespace CWComplex
 
-export RelCWComplex (cell map source_eq continuousOn continuousOn_symm mapsTo isClosedBase openCell
+export RelCWComplex (cell map source_eq continuousOn continuousOn_symm isClosedBase openCell
   closedCell cellFrontier)
 
 end CWComplex
@@ -210,14 +224,17 @@ lemma CWComplex.mapsTo [CWComplex C] (n : ℕ) (i : cell C n) : ∃ I : Π m, Fi
   simp_rw [empty_union] at this
   exact this
 
+@[alias_in CWComplex]
 lemma RelCWComplex.pairwiseDisjoint [RelCWComplex C D] :
     (univ : Set (Σ n, cell C n)).PairwiseDisjoint (fun ni ↦ openCell ni.1 ni.2) :=
   RelCWComplex.pairwiseDisjoint'
 
+@[alias_in CWComplex]
 lemma RelCWComplex.disjointBase [RelCWComplex C D] (n : ℕ) (i : cell C n) :
     Disjoint (openCell n i) D :=
   RelCWComplex.disjointBase' n i
 
+@[alias_in CWComplex]
 lemma RelCWComplex.disjoint_openCell_of_ne [RelCWComplex C D] {n m : ℕ} {i : cell C n}
     {j : cell C m} (ne : (⟨n, i⟩ : Σ n, cell C n) ≠ ⟨m, j⟩) :
     Disjoint (openCell n i) (openCell m j) :=
@@ -246,23 +263,28 @@ lemma CWComplex.union [CWComplex C] : ⋃ (n : ℕ) (j : cell C n), closedCell n
   rw [empty_union] at this
   exact this
 
+@[alias_in CWComplex]
 lemma RelCWComplex.openCell_subset_closedCell [RelCWComplex C D] (n : ℕ) (i : cell C n) :
     openCell n i ⊆ closedCell n i := image_mono Metric.ball_subset_closedBall
 
+@[alias_in CWComplex]
 lemma RelCWComplex.cellFrontier_subset_closedCell [RelCWComplex C D] (n : ℕ) (i : cell C n) :
     cellFrontier n i ⊆ closedCell n i := image_mono Metric.sphere_subset_closedBall
 
+@[alias_in CWComplex]
 lemma RelCWComplex.cellFrontier_union_openCell_eq_closedCell [RelCWComplex C D] (n : ℕ)
     (i : cell C n) : cellFrontier n i ∪ openCell n i = closedCell n i := by
   rw [cellFrontier, openCell, closedCell, ← image_union]
   congrm map n i '' ?_
   exact sphere_union_ball
 
+@[alias_in CWComplex]
 lemma RelCWComplex.map_zero_mem_openCell [RelCWComplex C D] (n : ℕ) (i : cell C n) :
     map n i 0 ∈ openCell n i := by
   apply mem_image_of_mem
   simp only [mem_ball, dist_self, zero_lt_one]
 
+@[alias_in CWComplex]
 lemma RelCWComplex.map_zero_mem_closedCell [RelCWComplex C D] (n : ℕ) (i : cell C n) :
     map n i 0 ∈ closedCell n i :=
   openCell_subset_closedCell _ _ (map_zero_mem_openCell _ _)
@@ -298,21 +320,26 @@ lemma CWComplex.eq_of_eq_union_iUnion [CWComplex C] (I J : Π n, Set (cell C n))
   apply RelCWComplex.eq_of_eq_union_iUnion
   simp_rw [empty_union, hIJ]
 
+@[alias_in CWComplex]
 lemma RelCWComplex.isCompact_closedCell [RelCWComplex C D] {n : ℕ} {i : cell C n} :
     IsCompact (closedCell n i) :=
   (isCompact_closedBall _ _).image_of_continuousOn (continuousOn n i)
 
+@[alias_in CWComplex]
 lemma RelCWComplex.isClosed_closedCell [RelCWComplex C D] [T2Space X] {n : ℕ} {i : cell C n} :
     IsClosed (closedCell n i) := isCompact_closedCell.isClosed
 
+@[alias_in CWComplex]
 lemma RelCWComplex.isCompact_cellFrontier [RelCWComplex C D] {n : ℕ} {i : cell C n} :
     IsCompact (cellFrontier n i) :=
   (isCompact_sphere _ _).image_of_continuousOn ((continuousOn n i).mono sphere_subset_closedBall)
 
+@[alias_in CWComplex]
 lemma RelCWComplex.isClosed_cellFrontier [RelCWComplex C D] [T2Space X] {n : ℕ} {i : cell C n} :
     IsClosed (cellFrontier n i) :=
   isCompact_cellFrontier.isClosed
 
+@[alias_in CWComplex]
 lemma RelCWComplex.closure_openCell_eq_closedCell [RelCWComplex C D] [T2Space X] {n : ℕ}
     {j : cell C n} : closure (openCell n j) = closedCell n j := by
   apply subset_antisymm (isClosed_closedCell.closure_subset_iff.2 (openCell_subset_closedCell n j))
@@ -332,31 +359,38 @@ lemma CWComplex.closed (C : Set X) [CWComplex C] [T2Space X] (A : Set X) (asubc
   have := RelCWComplex.closed C A asubc
   simp_all
 
+@[alias_in CWComplex]
 lemma RelCWComplex.closedCell_subset_complex [RelCWComplex C D] (n : ℕ) (j : cell C n) :
     closedCell n j ⊆ C := by
   simp_rw [← union]
   exact subset_union_of_subset_right (subset_iUnion₂ _ _) _
 
+@[alias_in CWComplex]
 lemma RelCWComplex.openCell_subset_complex [RelCWComplex C D] (n : ℕ) (j : cell C n) :
     openCell n j ⊆ C :=
   (openCell_subset_closedCell _ _).trans (closedCell_subset_complex _ _)
 
+@[alias_in CWComplex]
 lemma RelCWComplex.cellFrontier_subset_complex [RelCWComplex C D] (n : ℕ) (j : cell C n) :
     cellFrontier n j ⊆ C :=
   (cellFrontier_subset_closedCell n j).trans (closedCell_subset_complex n j)
 
+@[alias_in CWComplex]
 lemma RelCWComplex.closedCell_zero_eq_singleton [RelCWComplex C D] {j : cell C 0} :
     closedCell 0 j = {map 0 j ![]} := by
   simp [closedCell, Matrix.empty_eq]
 
+@[alias_in CWComplex]
 lemma RelCWComplex.openCell_zero_eq_singleton [RelCWComplex C D] {j : cell C 0} :
     openCell 0 j = {map 0 j ![]} := by
   simp [openCell, Matrix.empty_eq]
 
+@[alias_in CWComplex]
 lemma RelCWComplex.cellFrontier_zero_eq_empty [RelCWComplex C D] {j : cell C 0} :
     cellFrontier 0 j = ∅ := by
   simp [cellFrontier, sphere_eq_empty_of_subsingleton]
 
+@[alias_in CWComplex]
 lemma RelCWComplex.nonempty_cellFrontier [CWComplex C] {n : ℕ} (hn : n ≠ 0) (j : cell C n) :
     (cellFrontier n j).Nonempty := by
   letI : NeZero n := ⟨hn⟩
@@ -365,6 +399,7 @@ lemma RelCWComplex.nonempty_cellFrontier [CWComplex C] {n : ℕ} (hn : n ≠ 0)
   use Pi.single 0 1, by simp [Pi.norm_single]
 
 /-- If two 0-cells have the same characteristic image point, they are equal. -/
+@[alias_in CWComplex]
 lemma RelCWComplex.injective_map_zero (C : Set X) [RelCWComplex C D] :
     Injective ((map 0 · ![]) : cell C 0 → X) := by
   rintro x z h
@@ -372,23 +407,26 @@ lemma RelCWComplex.injective_map_zero (C : Set X) [RelCWComplex C D] :
   exact not_disjoint_iff.mpr ⟨map 0 x ![], by simp [openCell_zero_eq_singleton, h]⟩
     <| disjoint_openCell_of_ne (by grind : (⟨0, x⟩ : Σ n, cell C n) ≠ ⟨0, z⟩)
 
-@[simp]
+@[simp, alias_in CWComplex]
 lemma RelCWComplex.map_zero_eq_self_iff (C : Set X) [RelCWComplex C D] {x z : cell C 0} :
     map 0 x ![] = map 0 z ![] ↔ x = z :=
   ⟨fun h ↦ injective_map_zero C h, fun h ↦ h ▸ rfl⟩
 
+@[alias_in CWComplex]
 lemma RelCWComplex.closedCell_zero_injective (C : Set X) [RelCWComplex C D] :
     Injective (closedCell 0 : cell C 0 → _) := by
   intro x y h
   rw [closedCell_zero_eq_singleton, closedCell_zero_eq_singleton, singleton_eq_singleton_iff] at h
   exact injective_map_zero C h
 
+@[alias_in CWComplex]
 lemma RelCWComplex.openCell_zero_injective (C : Set X) [RelCWComplex C D] :
     Injective (openCell 0 : cell C 0 → _) := by
   intro x y h
   rw [openCell_zero_eq_singleton, openCell_zero_eq_singleton, singleton_eq_singleton_iff] at h
   exact injective_map_zero C h
 
+@[alias_in CWComplex]
 lemma RelCWComplex.cellFrontier_one_eq [RelCWComplex C D] (e : cell C 1) :
     cellFrontier 1 e = map 1 e '' {-1, 1} := by
   rw [cellFrontier]
@@ -411,10 +449,12 @@ lemma CWComplex.exists_cellFrontier_one_eq [CWComplex C] (e : cell C 1) :
   simp [RelCWComplex.cellFrontier_one_eq, image_pair, RelCWComplex.closedCell_zero_eq_singleton,
     hun1, hv1, pair_comm]
 
+@[alias_in CWComplex]
 lemma RelCWComplex.base_subset_complex [RelCWComplex C D] : D ⊆ C := by
   simp_rw [← union]
   exact subset_union_left
 
+@[alias_in CWComplex]
 lemma RelCWComplex.isClosed [T2Space X] [RelCWComplex C D] : IsClosed C := by
   rw [closed C C (by rfl)]
   constructor
@@ -467,6 +507,7 @@ lemma CWComplex.iUnion_openCell_eq_complex [CWComplex C] :
   simpa using RelCWComplex.union_iUnion_openCell_eq_complex (C := C)
 
 /-- The contrapositive of `disjoint_openCell_of_ne`. -/
+@[alias_in CWComplex]
 lemma RelCWComplex.eq_of_not_disjoint_openCell [RelCWComplex C D] {n : ℕ} {j : cell C n} {m : ℕ}
     {i : cell C m} (h : ¬ Disjoint (openCell n j) (openCell m i)) :
     (⟨n, j⟩ : (Σ n, cell C n)) = ⟨m, i⟩ := by
@@ -629,13 +670,17 @@ instance : PartialOrder (Subcomplex C) := .ofSetLike (Subcomplex C) X
 
 initialize_simps_projections Subcomplex (carrier → coe, as_prefix coe)
 
+@[alias_in CWComplex.Subcomplex]
 lemma mem_carrier {E : Subcomplex C} {x : X} : x ∈ E.carrier ↔ x ∈ (E : Set X) := Iff.rfl
 
+@[alias_in CWComplex.Subcomplex]
 lemma coe_eq_carrier {E : Subcomplex C} : (E : Set X) = E.carrier := rfl
 
-@[ext] lemma ext {E F : Subcomplex C} (h : ∀ x, x ∈ E ↔ x ∈ F) : E = F :=
+@[ext, alias_in CWComplex.Subcomplex]
+lemma ext {E F : Subcomplex C} (h : ∀ x, x ∈ E ↔ x ∈ F) : E = F :=
   SetLike.ext h
 
+@[alias_in CWComplex.Subcomplex]
 lemma eq_iff (E F : Subcomplex C) : E = F ↔ (E : Set X) = F :=
   SetLike.coe_injective.eq_iff.symm
 
@@ -648,10 +693,12 @@ protected def copy (E : Subcomplex C) (F : Set X) (hF : F = E) (J : (n : ℕ) 
     closed' := hF.symm ▸ E.closed'
     union' := hF.symm ▸ hJ ▸ E.union' }
 
-@[simp] lemma coe_copy (E : Subcomplex C) (F : Set X) (hF : F = E) (J : (n : ℕ) → Set (cell C n))
+@[simp, alias_in CWComplex.Subcomplex]
+lemma coe_copy (E : Subcomplex C) (F : Set X) (hF : F = E) (J : (n : ℕ) → Set (cell C n))
     (hJ : J = E.I) : (E.copy F hF J hJ : Set X) = F :=
   rfl
 
+@[alias_in CWComplex.Subcomplex]
 lemma copy_eq (E : Subcomplex C) (F : Set X) (hF : F = E) (J : (n : ℕ) → Set (cell C n))
     (hJ : J = E.I) : E.copy F hF J hJ = E :=
   SetLike.coe_injective hF
@@ -661,6 +708,7 @@ lemma union (E : Subcomplex C) :
   rw [E.union']
   rfl
 
+@[alias_in CWComplex.Subcomplex]
 lemma closed (E : Subcomplex C) : IsClosed (E : Set X) := E.closed'
 
 end Subcomplex
@@ -669,13 +717,9 @@ end RelCWComplex
 
 namespace CWComplex
 
-export RelCWComplex (Subcomplex)
+export RelCWComplex (Subcomplex Subcomplex.I Subcomplex.copy)
 
-namespace Subcomplex
-
-export RelCWComplex.Subcomplex (I closed union mem_carrier coe_eq_carrier ext copy coe_copy copy_eq)
-
-end CWComplex.Subcomplex
+end CWComplex
 
 lemma CWComplex.Subcomplex.union {C : Set X} [CWComplex C] {E : Subcomplex C} :
     ⋃ (n : ℕ) (j : E.I n), openCell (C := C) n j = E := by
@@ -749,22 +793,18 @@ def CWComplex.Subcomplex.mk'' [T2Space X] (C : Set X) [h : CWComplex C] (E : Set
     rw [empty_union]
     exact union
 
+@[alias_in CWComplex.Subcomplex]
 lemma RelCWComplex.Subcomplex.subset_complex {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) :
     ↑E ⊆ C := by
   simp_rw [← union, ← RelCWComplex.union_iUnion_openCell_eq_complex]
   exact union_subset_union_right _ (iUnion_mono fun _ ↦ iUnion_mono' fun j ↦ ⟨j, subset_rfl⟩)
 
+@[alias_in CWComplex.Subcomplex]
 lemma RelCWComplex.Subcomplex.base_subset {C D : Set X} [RelCWComplex C D] (E : Subcomplex C) :
     D ⊆ E := by
   simp_rw [← union]
   exact subset_union_left
 
-namespace CWComplex.Subcomplex
-
-export RelCWComplex.Subcomplex (subset_complex base_subset)
-
-end CWComplex.Subcomplex
-
 end Subcomplex
 
 section skeleton
@@ -778,7 +818,7 @@ This allows the base case of induction to be about the base instead of being abo
 the base and some points.
 The standard `skeleton` is defined in terms of `skeletonLT`. `skeletonLT` is preferred
 in statements. You should then derive the statement about `skeleton`. -/
-@[simps! -isSimp, irreducible]
+@[simps! (attr := alias_in CWComplex) -isSimp, irreducible]
 def skeletonLT (C : Set X) {D : Set X} [RelCWComplex C D] (n : ℕ∞) : Subcomplex C :=
     Subcomplex.mk' _ (D ∪ ⋃ (m : ℕ) (_ : m < n) (j : cell C m), closedCell m j)
     (fun l ↦ {x : cell C l | l < n})
@@ -803,7 +843,7 @@ end RelCWComplex
 
 namespace CWComplex
 
-export RelCWComplex (skeletonLT coe_skeletonLT skeletonLT_I skeleton)
+export RelCWComplex (skeletonLT skeleton)
 
 end CWComplex
 
@@ -813,11 +853,14 @@ lemma RelCWComplex.skeletonLT_zero_eq_base [RelCWComplex C D] : skeletonLT C 0 =
 lemma CWComplex.skeletonLT_zero_eq_empty [CWComplex C] : (skeletonLT C 0 : Set X) = ∅ :=
     RelCWComplex.skeletonLT_zero_eq_base
 
-@[simp] lemma RelCWComplex.skeletonLT_top [RelCWComplex C D] : skeletonLT C ⊤ = C := by
+@[simp, alias_in CWComplex] lemma RelCWComplex.skeletonLT_top [RelCWComplex C D] :
+    skeletonLT C ⊤ = C := by
   simp [coe_skeletonLT, union]
 
-@[simp] lemma RelCWComplex.skeleton_top [RelCWComplex C D] : skeleton C ⊤ = C := skeletonLT_top
+@[simp, alias_in CWComplex] lemma RelCWComplex.skeleton_top [RelCWComplex C D] : skeleton C ⊤ = C :=
+  skeletonLT_top
 
+@[alias_in CWComplex]
 lemma RelCWComplex.skeletonLT_mono [RelCWComplex C D] {n m : ℕ∞} (h : m ≤ n) :
     (skeletonLT C m : Set X) ⊆ skeletonLT C n := by
   simp_rw [coe_skeletonLT]
@@ -827,16 +870,20 @@ lemma RelCWComplex.skeletonLT_mono [RelCWComplex C D] {n m : ℕ∞} (h : m ≤
   obtain ⟨l, lltm, xmeml⟩ := xmem
   exact ⟨l, lt_of_lt_of_le lltm h, xmeml⟩
 
+@[alias_in CWComplex]
 lemma RelCWComplex.skeletonLT_monotone [RelCWComplex C D] : Monotone (skeletonLT C) :=
   fun _ _ h ↦ skeletonLT_mono h
 
+@[alias_in CWComplex]
 lemma RelCWComplex.skeleton_mono [RelCWComplex C D] {n m : ℕ∞} (h : m ≤ n) :
     (skeleton C m : Set X) ⊆ skeleton C n :=
   skeletonLT_mono (by gcongr)
 
+@[alias_in CWComplex]
 lemma RelCWComplex.skeleton_monotone [RelCWComplex C D] : Monotone (skeleton C) :=
   fun _ _ h ↦ skeleton_mono h
 
+@[alias_in CWComplex]
 lemma RelCWComplex.closedCell_subset_skeletonLT [RelCWComplex C D] (n : ℕ) (j : cell C n) :
     closedCell n j ⊆ skeletonLT C (n + 1) := by
   intro x xmem
@@ -845,18 +892,22 @@ lemma RelCWComplex.closedCell_subset_skeletonLT [RelCWComplex C D] (n : ℕ) (j
   simp_rw [mem_iUnion, exists_prop]
   refine ⟨n, (by norm_cast; exact lt_add_one n), ⟨j,xmem⟩⟩
 
+@[alias_in CWComplex]
 lemma RelCWComplex.closedCell_subset_skeleton [RelCWComplex C D] (n : ℕ) (j : cell C n) :
     closedCell n j ⊆ skeleton C n :=
   closedCell_subset_skeletonLT n j
 
+@[alias_in CWComplex]
 lemma RelCWComplex.openCell_subset_skeletonLT [RelCWComplex C D] (n : ℕ) (j : cell C n) :
     openCell n j ⊆ skeletonLT C (n + 1) :=
   (openCell_subset_closedCell _ _).trans (closedCell_subset_skeletonLT _ _)
 
+@[alias_in CWComplex]
 lemma RelCWComplex.openCell_subset_skeleton [RelCWComplex C D] (n : ℕ) (j : cell C n) :
     openCell n j ⊆ skeleton C n :=
   (openCell_subset_closedCell _ _).trans (closedCell_subset_skeleton _ _)
 
+@[alias_in CWComplex]
 lemma RelCWComplex.cellFrontier_subset_skeletonLT [RelCWComplex C D] (n : ℕ) (j : cell C n) :
     cellFrontier n j ⊆ skeletonLT C n := by
   obtain ⟨I, hI⟩ := cellFrontier_subset_base_union_finite_closedCell n j
@@ -868,18 +919,22 @@ lemma RelCWComplex.cellFrontier_subset_skeletonLT [RelCWComplex C D] (n : ℕ) (
   obtain ⟨i, iltn, j, _, xmem⟩ := xmem
   exact ⟨i, by norm_cast, j, xmem⟩
 
+@[alias_in CWComplex]
 lemma RelCWComplex.cellFrontier_subset_skeleton [RelCWComplex C D] (n : ℕ) (j : cell C (n + 1)) :
     cellFrontier (n + 1) j ⊆ skeleton C n :=
   cellFrontier_subset_skeletonLT _ _
 
+@[alias_in CWComplex]
 lemma RelCWComplex.iUnion_cellFrontier_subset_skeletonLT [RelCWComplex C D] (l : ℕ) :
     ⋃ (j : cell C l), cellFrontier l j ⊆ skeletonLT C l :=
   iUnion_subset (fun _ ↦ cellFrontier_subset_skeletonLT _ _)
 
+@[alias_in CWComplex]
 lemma RelCWComplex.iUnion_cellFrontier_subset_skeleton [RelCWComplex C D] (l : ℕ) :
     ⋃ (j : cell C l), cellFrontier l j ⊆ skeleton C l :=
   (iUnion_cellFrontier_subset_skeletonLT l).trans (skeletonLT_mono le_self_add)
 
+@[alias_in CWComplex]
 lemma RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ [RelCWComplex C D]
     (n : ℕ) :
     (skeletonLT C n : Set X) ∪ ⋃ (j : cell C n), closedCell n j = skeletonLT C (n + 1) := by
@@ -888,6 +943,7 @@ lemma RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ [RelCWC
   norm_cast
   exact (biUnion_lt_succ _ _).symm
 
+@[alias_in CWComplex]
 lemma RelCWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ [RelCWComplex C D] (n : ℕ) :
     (skeleton C n : Set X) ∪ ⋃ (j : cell C (n + 1)), closedCell (n + 1) j = skeleton C (n + 1) :=
   skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ _
@@ -909,6 +965,7 @@ lemma CWComplex.iUnion_openCell_eq_skeleton [CWComplex C] (n : ℕ∞) :
     ⋃ (m : ℕ) (_ : m < n + 1) (j : cell C m), openCell m j = skeleton C n :=
   iUnion_openCell_eq_skeletonLT _
 
+@[alias_in CWComplex]
 lemma RelCWComplex.iUnion_skeletonLT_eq_complex [RelCWComplex C D] :
     ⋃ (n : ℕ), skeletonLT C n = C := by
   apply subset_antisymm (iUnion_subset_iff.2 fun _ ↦ (skeletonLT C _).subset_complex)
@@ -916,6 +973,7 @@ lemma RelCWComplex.iUnion_skeletonLT_eq_complex [RelCWComplex C D] :
   exact ⟨subset_iUnion_of_subset 0 (skeletonLT C 0).base_subset,
     fun n i ↦ subset_iUnion_of_subset _ (openCell_subset_skeletonLT n i)⟩
 
+@[alias_in CWComplex]
 lemma RelCWComplex.iUnion_skeleton_eq_complex [RelCWComplex C D] :
     ⋃ (n : ℕ), skeleton C n = C := by
   apply subset_antisymm (iUnion_subset_iff.2 fun _ ↦ (skeleton C _).subset_complex)
@@ -940,11 +998,15 @@ lemma RelCWComplex.mem_skeleton_iff [RelCWComplex C D] {n : ℕ∞} {x : X} :
   · simp
   · rw [← Nat.cast_one, ← Nat.cast_add, Nat.cast_lt, Nat.cast_le, Order.lt_add_one_iff]
 
-lemma CWComplex.exists_mem_openCell_of_mem_skeleton [CWComplex C] {n : ℕ∞} {x : X} :
+lemma CWComplex.mem_skeleton_iff [CWComplex C] {n : ℕ∞} {x : X} :
     x ∈ skeleton C n ↔ ∃ (m : ℕ) (_ : m ≤ n) (j : cell C m), x ∈ openCell m j := by
   rw [RelCWComplex.mem_skeleton_iff, mem_empty_iff_false, false_or]
 
+@[deprecated (since := "2026-04-30")] alias CWComplex.exists_mem_openCell_of_mem_skeleton :=
+  CWComplex.mem_skeleton_iff
+
 /-- A skeleton and an open cell of a higher dimension are disjoint. -/
+@[alias_in CWComplex]
 lemma RelCWComplex.disjoint_skeletonLT_openCell [RelCWComplex C D] {n : ℕ∞} {m : ℕ}
     {j : cell C m} (hnm : n ≤ m) : Disjoint (skeletonLT C n : Set X) (openCell m j) := by
   -- This is a consequence of `iUnion_openCell_eq_skeletonLT` and `disjoint_openCell_of_ne`
@@ -957,12 +1019,14 @@ lemma RelCWComplex.disjoint_skeletonLT_openCell [RelCWComplex C D] {n : ℕ∞}
   exact (lt_self_iff_false m).mp (ENat.coe_lt_coe.1 (hln.trans_le hnm))
 
 /-- A skeleton and an open cell of a higher dimension are disjoint. -/
+@[alias_in CWComplex]
 lemma RelCWComplex.disjoint_skeleton_openCell [RelCWComplex C D] {n : ℕ∞} {m : ℕ}
     {j : cell C m} (nlem : n < m) : Disjoint (skeleton C n : Set X) (openCell m j) :=
   disjoint_skeletonLT_openCell (Order.add_one_le_of_lt nlem)
 
 /-- A skeleton intersected with a closed cell of a higher dimension is the skeleton intersected with
 the boundary of the cell. -/
+@[alias_in CWComplex]
 lemma RelCWComplex.skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier [RelCWComplex C D]
     {n : ℕ∞} {m : ℕ} {j : cell C m} (hnm : n ≤ m) :
     (skeletonLT C n : Set X) ∩ closedCell m j = (skeletonLT C n : Set X) ∩ cellFrontier m j := by
@@ -973,6 +1037,7 @@ lemma RelCWComplex.skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier
   exact empty_subset _
 
 /-- Version of `skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier` using `skeleton`. -/
+@[alias_in CWComplex]
 lemma RelCWComplex.skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier [RelCWComplex C D]
     {n : ℕ∞} {m : ℕ} {j : cell C m} (hnm : n < m) :
     (skeleton C n : Set X) ∩ closedCell m j = (skeleton C n : Set X) ∩ cellFrontier m j :=
@@ -996,24 +1061,4 @@ lemma RelCWComplex.disjoint_interior_base_iUnion_closedCell [T2Space X] [RelCWCo
   simp_rw [disjoint_iff_inter_eq_empty, inter_iUnion, disjoint_interior_base_closedCell.inter_eq,
     iUnion_empty]
 
-namespace CWComplex
-
-export RelCWComplex (pairwiseDisjoint disjoint_openCell_of_ne openCell_subset_closedCell
-  cellFrontier_subset_closedCell cellFrontier_union_openCell_eq_closedCell map_zero_mem_openCell
-  map_zero_mem_closedCell isCompact_closedCell isClosed_closedCell isCompact_cellFrontier
-  isClosed_cellFrontier closure_openCell_eq_closedCell skeletonLT_top skeleton_top skeletonLT_mono
-  skeleton_mono skeletonLT_monotone skeleton_monotone closedCell_subset_skeletonLT
-  closedCell_subset_skeleton closedCell_subset_complex openCell_subset_skeletonLT
-  openCell_subset_skeleton
-  openCell_subset_complex cellFrontier_subset_skeletonLT cellFrontier_subset_skeleton
-  cellFrontier_subset_complex iUnion_cellFrontier_subset_skeletonLT
-  iUnion_cellFrontier_subset_skeleton closedCell_zero_eq_singleton openCell_zero_eq_singleton
-  cellFrontier_zero_eq_empty isClosed skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ
-  skeleton_union_iUnion_closedCell_eq_skeleton_succ iUnion_skeletonLT_eq_complex
-  iUnion_skeleton_eq_complex eq_of_not_disjoint_openCell disjoint_skeletonLT_openCell
-  disjoint_skeleton_openCell skeletonLT_inter_closedCell_eq_skeletonLT_inter_cellFrontier
-  skeleton_inter_closedCell_eq_skeleton_inter_cellFrontier)
-
-end CWComplex
-
 end Topology
diff --git a/Mathlib/Topology/CWComplex/Classical/Finite.lean b/Mathlib/Topology/CWComplex/Classical/Finite.lean
index f28ba68f9b5798..993561d306d25e 100644
--- a/Mathlib/Topology/CWComplex/Classical/Finite.lean
+++ b/Mathlib/Topology/CWComplex/Classical/Finite.lean
@@ -42,18 +42,24 @@ class RelCWComplex.FiniteDimensional.{u} {X : Type u} [TopologicalSpace X] (C :
   /-- For some natural number `n`, the type `cell C m` is empty for all `m ≥ n`. -/
   eventually_isEmpty_cell : ∀ᶠ n in Filter.atTop, IsEmpty (cell C n)
 
+alias CWComplex.FiniteDimensional.eventually_isEmpty_cell :=
+  RelCWComplex.FiniteDimensional.eventually_isEmpty_cell
+
 /-- A CW complex is of finite type if `cell C n` is finite for every `n`. -/
 class RelCWComplex.FiniteType.{u} {X : Type u} [TopologicalSpace X] (C : Set X) {D : Set X}
     [RelCWComplex C D] : Prop where
   /-- `cell C n` is finite for every `n`. -/
   finite_cell (n : ℕ) : Finite (cell C n)
 
+alias CWComplex.FiniteType.finite_cell := RelCWComplex.FiniteType.finite_cell
+
 /-- A CW complex is finite if it is finite dimensional and of finite type. -/
 class RelCWComplex.Finite {X : Type*} [TopologicalSpace X] (C : Set X) {D : Set X}
     [RelCWComplex C D] extends FiniteDimensional C, FiniteType C
 
 variable {X : Type*} [TopologicalSpace X] (C : Set X) {D : Set X} [RelCWComplex C D]
 
+@[alias_in CWComplex]
 lemma RelCWComplex.finite_of_finiteDimensional_finiteType [FiniteDimensional C]
     [FiniteType C] : Finite C where
   eventually_isEmpty_cell := FiniteDimensional.eventually_isEmpty_cell
@@ -61,8 +67,7 @@ lemma RelCWComplex.finite_of_finiteDimensional_finiteType [FiniteDimensional C]
 
 namespace CWComplex
 
-export RelCWComplex (FiniteDimensional FiniteType Finite FiniteDimensional.eventually_isEmpty_cell
-  FiniteType.finite_cell finite_of_finiteDimensional_finiteType)
+export RelCWComplex (FiniteDimensional FiniteType Finite)
 
 end CWComplex
 
@@ -306,6 +311,7 @@ variable {X : Type*} [TopologicalSpace X] {C D : Set X} [RelCWComplex C D]
 
 /-- If the collection of all cells (of any dimension) of a relative CW complex `C` is finite, then
 `C` is finite as a CW complex. -/
+@[alias_in CWComplex]
 lemma RelCWComplex.finite_of_finite_cells (finite : _root_.Finite (Σ n, cell C n)) : Finite C where
   eventually_isEmpty_cell := by
     simp only [Filter.eventually_atTop]
@@ -329,6 +335,7 @@ lemma RelCWComplex.finite_of_finite_cells (finite : _root_.Finite (Σ n, cell C
 
 /-- If `C` is finite as a CW complex then the collection of all cells (of any dimension) is
 finite. -/
+@[alias_in CWComplex]
 lemma RelCWComplex.finite_cells_of_finite [finite : Finite C] : _root_.Finite (Σ n, cell C n) := by
   -- We show that there is a bijection between `Σ n, cell C n` and
   -- `Σ (m : {m : ℕ // m < n}), cell C m`.
@@ -348,13 +355,8 @@ lemma RelCWComplex.finite_cells_of_finite [finite : Finite C] : _root_.Finite (
   exact Finite.instSigma
 
 /-- A CW complex is finite iff the total number of its cells is finite. -/
+@[alias_in CWComplex]
 lemma RelCWComplex.finite_iff_finite_cells : Finite C ↔ _root_.Finite (Σ n, cell C n) :=
   ⟨fun h ↦ finite_cells_of_finite (finite := h), finite_of_finite_cells⟩
 
-namespace CWComplex
-
-export RelCWComplex (finite_of_finite_cells finite_cells_of_finite finite_iff_finite_cells)
-
-end CWComplex
-
 end Topology
diff --git a/Mathlib/Topology/CWComplex/Classical/Subcomplex.lean b/Mathlib/Topology/CWComplex/Classical/Subcomplex.lean
index 438323f8296faf..3c8c3994156c1d 100644
--- a/Mathlib/Topology/CWComplex/Classical/Subcomplex.lean
+++ b/Mathlib/Topology/CWComplex/Classical/Subcomplex.lean
@@ -32,6 +32,7 @@ namespace Topology
 
 variable {X : Type*} [t : TopologicalSpace X] {C D : Set X}
 
+@[alias_in CWComplex.Subcomplex]
 lemma RelCWComplex.Subcomplex.closedCell_subset_of_mem [T2Space X] [RelCWComplex C D]
     (E : Subcomplex C) {n : ℕ} {i : cell C n} (hi : i ∈ E.I n) :
     closedCell n i ⊆ E := by
@@ -40,11 +41,13 @@ lemma RelCWComplex.Subcomplex.closedCell_subset_of_mem [T2Space X] [RelCWComplex
   exact subset_iUnion_of_subset n
     (subset_iUnion (fun (j : ↑(E.I n)) ↦ openCell (C := C) n j) ⟨i, hi⟩)
 
+@[alias_in CWComplex.Subcomplex]
 lemma RelCWComplex.Subcomplex.openCell_subset_of_mem [T2Space X] [RelCWComplex C D]
     (E : Subcomplex C) {n : ℕ} {i : cell C n} (hi : i ∈ E.I n) :
     openCell n i ⊆ E :=
   (openCell_subset_closedCell n i).trans (closedCell_subset_of_mem E hi)
 
+@[alias_in CWComplex.Subcomplex]
 lemma RelCWComplex.Subcomplex.cellFrontier_subset_of_mem [T2Space X] [RelCWComplex C D]
     (E : Subcomplex C) {n : ℕ} {i : cell C n} (hi : i ∈ E.I n) :
     cellFrontier n i ⊆ E :=
@@ -66,6 +69,7 @@ lemma CWComplex.Subcomplex.union_closedCell [T2Space X] [CWComplex C] (E : Subco
     ⋃ (n : ℕ) (j : E.I n), closedCell (C := C) n j = E :=
   (empty_union _).symm.trans (RelCWComplex.Subcomplex.union_closedCell E)
 
+@[alias_in CWComplex.Subcomplex]
 lemma RelCWComplex.Subcomplex.disjoint_openCell_subcomplex_of_not_mem [RelCWComplex C D]
     (E : Subcomplex C) {n : ℕ} {i : cell C n} (h : i ∉ E.I n) : Disjoint (openCell n i) E := by
   simp_rw [← union, disjoint_union_right, disjoint_iUnion_right]
@@ -142,12 +146,14 @@ lemma RelCWComplex.Subcomplex.cellFrontier_eq [T2Space X] [RelCWComplex C D] (E
     (n : ℕ) (i : E.I n) : cellFrontier (C := E) n i = cellFrontier n (i : cell C n) := by
   rfl
 
+@[alias_in CWComplex.Subcomplex]
 instance RelCWComplex.Subcomplex.finiteType_subcomplex_of_finiteType [T2Space X]
     [RelCWComplex C D] [FiniteType C] (E : Subcomplex C) : FiniteType (E : Set X) where
   finite_cell n :=
     let _ := FiniteType.finite_cell (C := C) (D := D) n
     Subtype.finite
 
+@[alias_in CWComplex.Subcomplex]
 instance RelCWComplex.Subcomplex.finiteDimensional_subcomplex_of_finiteDimensional
     [T2Space X] [RelCWComplex C D] [FiniteDimensional C] (E : Subcomplex C) :
     FiniteDimensional (E : Set X) where
@@ -156,17 +162,9 @@ instance RelCWComplex.Subcomplex.finiteDimensional_subcomplex_of_finiteDimension
     simp [isEmpty_subtype]
 
 /-- A subcomplex of a finite CW complex is again finite. -/
+@[alias_in CWComplex.Subcomplex]
 instance RelCWComplex.Subcomplex.finite_subcomplex_of_finite [T2Space X] [RelCWComplex C D]
     [Finite C] (E : Subcomplex C) : Finite (E : Set X) :=
   finite_of_finiteDimensional_finiteType _
 
-namespace CWComplex.Subcomplex
-
-export RelCWComplex.Subcomplex (closedCell_subset_of_mem openCell_subset_of_mem
-  cellFrontier_subset_of_mem disjoint_openCell_subcomplex_of_not_mem subset_complex
-  finiteType_subcomplex_of_finiteType finiteDimensional_subcomplex_of_finiteDimensional
-  finite_subcomplex_of_finite)
-
-end CWComplex.Subcomplex
-
 end Topology
diff --git a/Mathlib/Topology/Order/MonotoneConvergence.lean b/Mathlib/Topology/Order/MonotoneConvergence.lean
index 525b8006cece8f..a2e0766531a8ab 100644
--- a/Mathlib/Topology/Order/MonotoneConvergence.lean
+++ b/Mathlib/Topology/Order/MonotoneConvergence.lean
@@ -111,6 +111,8 @@ end IsGLB
 
 section CiSup
 
+section ConditionallyCompletePartialOrder
+
 variable [ConditionallyCompletePartialOrderSup α] [SupConvergenceClass α] {f : ι → α}
 
 theorem tendsto_atTop_ciSup (h_mono : Monotone f) (hbdd : BddAbove <| range f) :
@@ -124,10 +126,28 @@ theorem tendsto_atTop_ciSup (h_mono : Monotone f) (hbdd : BddAbove <| range f) :
 theorem tendsto_atBot_ciSup (h_anti : Antitone f) (hbdd : BddAbove <| range f) :
     Tendsto f atBot (𝓝 (⨆ i, f i)) := by convert! tendsto_atTop_ciSup h_anti.dual hbdd.dual using 1
 
+end ConditionallyCompletePartialOrder
+
+section ConditionallyCompleteLattice
+
+theorem tendsto_finset_sup_ciSup {ι} [ConditionallyCompleteLattice α] [OrderBot α]
+    [SupConvergenceClass α] [Nonempty ι] {a : ι → α} (ha : BddAbove (range a)) :
+    Tendsto (fun F : Finset ι => F.sup a) atTop (𝓝 (⨆ i, a i)) := by
+  have hmono : Monotone (fun F : Finset ι => F.sup a) := fun F G hFG => Finset.sup_mono hFG
+  have hbdd : BddAbove (Set.range fun F : Finset ι => F.sup a) := by
+    refine ⟨⨆ i, a i, ?_⟩
+    rintro _ ⟨F, rfl⟩
+    exact Finset.sup_le fun i _ => le_ciSup ha i
+  simpa [ciSup_eq_ciSup_finset ha] using tendsto_atTop_ciSup hmono hbdd
+
+end ConditionallyCompleteLattice
+
 end CiSup
 
 section CiInf
 
+section ConditionallyCompletePartialOrder
+
 variable [ConditionallyCompletePartialOrderInf α] [InfConvergenceClass α] {f : ι → α}
 
 theorem tendsto_atBot_ciInf (h_mono : Monotone f) (hbdd : BddBelow <| range f) :
@@ -136,6 +156,17 @@ theorem tendsto_atBot_ciInf (h_mono : Monotone f) (hbdd : BddBelow <| range f) :
 theorem tendsto_atTop_ciInf (h_anti : Antitone f) (hbdd : BddBelow <| range f) :
     Tendsto f atTop (𝓝 (⨅ i, f i)) := by convert! tendsto_atBot_ciSup h_anti.dual hbdd.dual using 1
 
+end ConditionallyCompletePartialOrder
+
+section ConditionallyCompleteLattice
+
+theorem tendsto_finset_inf_ciInf {ι} [ConditionallyCompleteLattice α] [OrderTop α]
+    [InfConvergenceClass α] [Nonempty ι] (a : ι → α) (ha : BddBelow (range a)) :
+    Tendsto (fun F : Finset ι => F.inf a) atTop (𝓝 (⨅ i, a i)) :=
+  tendsto_finset_sup_ciSup (α := αᵒᵈ) ha
+
+end ConditionallyCompleteLattice
+
 end CiInf
 
 section iSup
@@ -145,6 +176,11 @@ variable [CompleteLattice α] [SupConvergenceClass α] {f : ι → α}
 theorem tendsto_atTop_iSup (h_mono : Monotone f) : Tendsto f atTop (𝓝 (⨆ i, f i)) :=
   tendsto_atTop_ciSup h_mono (OrderTop.bddAbove _)
 
+theorem tendsto_finset_sup_iSup {ι} (a : ι → α) :
+    Tendsto (fun F : Finset ι => F.sup a) atTop (𝓝 (⨆ i, a i)) := by
+  have hmono : Monotone (fun F : Finset ι => F.sup a) := fun F G hFG => Finset.sup_mono hFG
+  simpa [Finset.sup_eq_iSup, ← iSup_eq_iSup_finset a] using tendsto_atTop_iSup hmono
+
 theorem tendsto_atBot_iSup (h_anti : Antitone f) : Tendsto f atBot (𝓝 (⨆ i, f i)) :=
   tendsto_atBot_ciSup h_anti (OrderTop.bddAbove _)
 
@@ -157,6 +193,10 @@ variable [CompleteLattice α] [InfConvergenceClass α] {f : ι → α}
 theorem tendsto_atBot_iInf (h_mono : Monotone f) : Tendsto f atBot (𝓝 (⨅ i, f i)) :=
   tendsto_atBot_ciInf h_mono (OrderBot.bddBelow _)
 
+theorem tendsto_finset_inf_iInf {ι} (a : ι → α) :
+    Tendsto (fun F : Finset ι => F.inf a) atTop (𝓝 (⨅ i, a i)) :=
+  tendsto_finset_sup_iSup (α := αᵒᵈ) a
+
 theorem tendsto_atTop_iInf (h_anti : Antitone f) : Tendsto f atTop (𝓝 (⨅ i, f i)) :=
   tendsto_atTop_ciInf h_anti (OrderBot.bddBelow _)