[codex] Add finset supremum and infimum convergence lemmas

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

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⟩

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

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
 

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

Mathlib/Algebra/Order/Module/PositiveLinearMap.lean

@@ -38,24 +38,23 @@ 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₂]
   [Module R E₁] [Module R E₂] [FunLike F E₁ E₂] [LinearMapClass F R E₁ E₂]
   [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'

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]
 

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

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
 

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))

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)

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
 

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

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

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