Merge remote-tracking branch 'origin/master' into jyxu/FiniteLength

.github/build.in.yml

@@ -133,8 +133,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get Mathlib.Init
-          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          lake exe cache get #Mathlib.Init
+          #lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all

.github/workflows/bors.yml

@@ -143,8 +143,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get Mathlib.Init
-          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          lake exe cache get #Mathlib.Init
+          #lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all

.github/workflows/build.yml

@@ -150,8 +150,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get Mathlib.Init
-          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          lake exe cache get #Mathlib.Init
+          #lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all

.github/workflows/build_fork.yml

@@ -147,8 +147,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get Mathlib.Init
-          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          lake exe cache get #Mathlib.Init
+          #lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all

Archive/Imo/Imo1962Q1.lean

@@ -107,7 +107,7 @@ lemma case_more_digits {c n : ℕ} (hc : (digits 10 c).length ≥ 6) (hpp : Prob
   calc
     n ≥ 10 * c := le.intro hpp.left.symm
     _ ≥ 10 ^ (digits 10 c).length := base_pow_length_digits_le 10 c (by decide) hnz
-    _ ≥ 10 ^ 6 := pow_le_pow_right (by decide) hc
+    _ ≥ 10 ^ 6 := pow_right_mono₀ (by decide) hc
     _ ≥ 153846 := by norm_num
 
 /-!

Archive/Wiedijk100Theorems/AbelRuffini.lean

@@ -115,7 +115,7 @@ theorem real_roots_Phi_ge_aux (hab : b < a) :
   · have hf1 : f 1 < 0 := by simp [hf, hb]
     have hfa : 0 ≤ f a := by
       simp_rw [hf, ← sq]
-      refine add_nonneg (sub_nonneg.mpr (pow_le_pow_right ha ?_)) ?_ <;> norm_num
+      refine add_nonneg (sub_nonneg.mpr (pow_right_mono₀ ha ?_)) ?_ <;> norm_num
     obtain ⟨x, ⟨-, hx1⟩, hx2⟩ := intermediate_value_Ico' hle (hc _) (Set.mem_Ioc.mpr ⟨hf1, hf0⟩)
     obtain ⟨y, ⟨hy1, -⟩, hy2⟩ := intermediate_value_Ioc ha (hc _) (Set.mem_Ioc.mpr ⟨hf1, hfa⟩)
     exact ⟨x, y, (hx1.trans hy1).ne, hx2, hy2⟩
@@ -126,7 +126,7 @@ theorem real_roots_Phi_ge_aux (hab : b < a) :
         f (-a) = (a : ℝ) ^ 2 - (a : ℝ) ^ 5 + b := by
           norm_num [hf, ← sq, sub_eq_add_neg, add_comm, Odd.neg_pow (by decide : Odd 5)]
         _ ≤ (a : ℝ) ^ 2 - (a : ℝ) ^ 3 + (a - 1) := by
-          refine add_le_add (sub_le_sub_left (pow_le_pow_right ha ?_) _) ?_ <;> linarith
+          refine add_le_add (sub_le_sub_left (pow_right_mono₀ ha ?_) _) ?_ <;> linarith
         _ = -((a : ℝ) - 1) ^ 2 * (a + 1) := by ring
         _ ≤ 0 := by nlinarith
     have ha' := neg_nonpos.mpr (hle.trans ha)

Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean

@@ -154,7 +154,7 @@ theorem card_le_two_pow {x k : ℕ} :
     card M₁ ≤ card (image f K) := card_le_card h
     _ ≤ card K := card_image_le
     _ ≤ 2 ^ card (image Nat.succ (range k)) := by simp only [K, card_powerset]; rfl
-    _ ≤ 2 ^ card (range k) := pow_le_pow_right one_le_two card_image_le
+    _ ≤ 2 ^ card (range k) := pow_right_mono₀ one_le_two card_image_le
     _ = 2 ^ k := by rw [card_range k]
 
 /--

Counterexamples/SorgenfreyLine.lean

@@ -141,7 +141,7 @@ theorem continuous_toReal : Continuous toReal :=
     exact inf_le_left
 
 instance : OrderClosedTopology ℝₗ :=
-  ⟨isClosed_le_prod.preimage (continuous_toReal.prod_map continuous_toReal)⟩
+  ⟨isClosed_le_prod.preimage (continuous_toReal.prodMap continuous_toReal)⟩
 
 instance : ContinuousAdd ℝₗ := by
   refine ⟨continuous_iff_continuousAt.2 ?_⟩

Mathlib/Algebra/Algebra/Basic.lean

@@ -23,12 +23,12 @@ universe u v w u₁ v₁
 
 namespace Algebra
 
-variable {R : Type u} {S : Type v} {A : Type w} {B : Type*}
+variable {R : Type u} {A : Type w}
 
 section Semiring
 
-variable [CommSemiring R] [CommSemiring S]
-variable [Semiring A] [Algebra R A] [Semiring B] [Algebra R B]
+variable [CommSemiring R]
+variable [Semiring A] [Algebra R A]
 
 section PUnit
 
@@ -319,7 +319,6 @@ section IsScalarTower
 variable {R : Type*} [CommSemiring R]
 variable (A : Type*) [Semiring A] [Algebra R A]
 variable {M : Type*} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M]
-variable {N : Type*} [AddCommMonoid N] [Module A N] [Module R N] [IsScalarTower R A N]
 
 theorem algebra_compatible_smul (r : R) (m : M) : r • m = (algebraMap R A) r • m := by
   rw [← one_smul A m, ← smul_assoc, Algebra.smul_def, mul_one, one_smul]

Mathlib/Algebra/DirectSum/LinearMap.lean

@@ -100,27 +100,27 @@ lemma trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero
     [IsDomain R] [IsPrincipalIdealRing R] [Module.Free R M] [Module.Finite R M]
     {f g : Module.End R M}
     (h_comm : Commute f g)
-    (hf : ⨆ μ, ⨆ k, f.genEigenspace μ k = ⊤)
-    (hg : ∀ μ, trace R _ (g.restrict (f.mapsTo_iSup_genEigenspace_of_comm h_comm μ)) = 0) :
+    (hf : ⨆ μ, f.maxGenEigenspace μ = ⊤)
+    (hg : ∀ μ, trace R _ (g.restrict (f.mapsTo_maxGenEigenspace_of_comm h_comm μ)) = 0) :
     trace R _ (g ∘ₗ f) = 0 := by
   have hfg : ∀ μ,
-      MapsTo (g ∘ₗ f) ↑(⨆ k, f.genEigenspace μ k) ↑(⨆ k, f.genEigenspace μ k) :=
-    fun μ ↦ (f.mapsTo_iSup_genEigenspace_of_comm h_comm μ).comp
-      (f.mapsTo_iSup_genEigenspace_of_comm rfl μ)
+      MapsTo (g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ) :=
+    fun μ ↦ (f.mapsTo_maxGenEigenspace_of_comm h_comm μ).comp
+      (f.mapsTo_maxGenEigenspace_of_comm rfl μ)
   suffices ∀ μ, trace R _ ((g ∘ₗ f).restrict (hfg μ)) = 0 by
     classical
     have hds := DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top
-      f.independent_genEigenspace hf
-    have h_fin : {μ | ⨆ k, f.genEigenspace μ k ≠ ⊥}.Finite :=
+      f.independent_maxGenEigenspace hf
+    have h_fin : {μ | f.maxGenEigenspace μ ≠ ⊥}.Finite :=
       CompleteLattice.WellFounded.finite_ne_bot_of_independent IsWellFounded.wf
-        f.independent_genEigenspace
+        f.independent_maxGenEigenspace
     simp [trace_eq_sum_trace_restrict' hds h_fin hfg, this]
   intro μ
-  replace h_comm : Commute (g.restrict (f.mapsTo_iSup_genEigenspace_of_comm h_comm μ))
-      (f.restrict (f.mapsTo_iSup_genEigenspace_of_comm rfl μ)) :=
+  replace h_comm : Commute (g.restrict (f.mapsTo_maxGenEigenspace_of_comm h_comm μ))
+      (f.restrict (f.mapsTo_maxGenEigenspace_of_comm rfl μ)) :=
     restrict_commute h_comm.symm _ _
   rw [restrict_comp, trace_comp_eq_mul_of_commute_of_isNilpotent μ h_comm
-    (f.isNilpotent_restrict_iSup_sub_algebraMap μ), hg, mul_zero]
+    (f.isNilpotent_restrict_maxGenEigenspace_sub_algebraMap μ), hg, mul_zero]
 
 lemma mapsTo_biSup_of_mapsTo {ι : Type*} {N : ι → Submodule R M}
     (s : Set ι) {f : Module.End R M} (hf : ∀ i, MapsTo f (N i) (N i)) :

Mathlib/Algebra/Group/Action/Opposite.lean

@@ -27,7 +27,7 @@ With `open scoped RightActions`, this provides:
 
 assert_not_exists MonoidWithZero
 
-variable {R M N α : Type*}
+variable {M N α : Type*}
 
 /-!
 ### Actions _on_ the opposite type

Mathlib/Algebra/Group/Hom/CompTypeclasses.lean

@@ -48,7 +48,6 @@ attribute [simp] CompTriple.comp_eq
 
 namespace CompTriple
 
-variable {M' : Type*} [Monoid M']
 variable {M N P : Type*} [Monoid M] [Monoid N] [Monoid P]
 
 /-- Class of Id maps -/

Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

@@ -420,7 +420,7 @@ theorem union_mul_inter_subset_union : (s₁ ∪ s₂) * (t₁ ∩ t₂) ⊆ s
       `s'`, `t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' + t'`."]
 theorem subset_mul {s t : Set α} :
     ↑u ⊆ s * t → ∃ s' t' : Finset α, ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' * t' :=
-  subset_image₂
+  subset_set_image₂
 
 @[to_additive]
 theorem image_mul [DecidableEq β] : (s * t).image (f : α → β) = s.image f * t.image f :=
@@ -606,7 +606,7 @@ theorem union_div_inter_subset_union : (s₁ ∪ s₂) / (t₁ ∩ t₂) ⊆ s
       `s'`, `t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' - t'`."]
 theorem subset_div {s t : Set α} :
     ↑u ⊆ s / t → ∃ s' t' : Finset α, ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' / t' :=
-  subset_image₂
+  subset_set_image₂
 
 @[to_additive (attr := simp (default + 1))]
 lemma sup_div_le [SemilatticeSup β] [OrderBot β] {s t : Finset α} {f : α → β} {a : β} :
@@ -1200,7 +1200,7 @@ theorem union_smul_inter_subset_union [DecidableEq α] : (s₁ ∪ s₂) • (t
       finsets `s'`, `t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' +ᵥ t'`."]
 theorem subset_smul {s : Set α} {t : Set β} :
     ↑u ⊆ s • t → ∃ (s' : Finset α) (t' : Finset β), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' • t' :=
-  subset_image₂
+  subset_set_image₂
 
 end SMul
 
@@ -1310,7 +1310,7 @@ end
 finsets `s'`, `t'` such that `s' ⊆ s`, `t' ⊆ t` and `u ⊆ s' -ᵥ t'`. -/
 theorem subset_vsub {s t : Set β} :
     ↑u ⊆ s -ᵥ t → ∃ s' t' : Finset β, ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' -ᵥ t' :=
-  subset_image₂
+  subset_set_image₂
 
 end VSub
 

Mathlib/Algebra/GroupWithZero/Indicator.lean

@@ -40,6 +40,12 @@ lemma indicator_mul_right (s : Set ι) (f g : ι → M₀) :
   · rfl
   · rw [mul_zero]
 
+lemma indicator_mul_const (s : Set ι) (f : ι → M₀) (a : M₀) (i : ι) :
+    s.indicator (f · * a) i = s.indicator f i * a := by rw [indicator_mul_left]
+
+lemma indicator_const_mul (s : Set ι) (f : ι → M₀) (a : M₀) (i : ι) :
+    s.indicator (a * f ·) i = a * s.indicator f i := by rw [indicator_mul_right]
+
 lemma inter_indicator_mul (f g : ι → M₀) (i : ι) :
     (s ∩ t).indicator (fun j ↦ f j * g j) i = s.indicator f i * t.indicator g i := by
   rw [← Set.indicator_indicator]

Mathlib/Algebra/Lie/TraceForm.lean

@@ -226,9 +226,9 @@ lemma traceForm_eq_sum_genWeightSpaceOf
     convert finite_genWeightSpaceOf_ne_bot R L M z
     exact LieSubmodule.coeSubmodule_eq_bot_iff (genWeightSpaceOf M _ _)
   classical
-  have hds := DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top
-    (LieSubmodule.independent_iff_coe_toSubmodule.mp <| independent_genWeightSpaceOf R L M z)
-    (IsTriangularizable.iSup_eq_top z)
+  have h := LieSubmodule.independent_iff_coe_toSubmodule.mp <| independent_genWeightSpaceOf R L M z
+  have hds := DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top h <| by
+    simp [← LieSubmodule.iSup_coe_toSubmodule]
   simp only [LinearMap.coeFn_sum, Finset.sum_apply, traceForm_apply_apply,
     LinearMap.trace_eq_sum_trace_restrict' hds hfin hxy]
   exact Finset.sum_congr (by simp) (fun χ _ ↦ rfl)
@@ -276,9 +276,9 @@ lemma lowerCentralSeries_one_inf_center_le_ker_traceForm [Module.Free R M] [Modu
     intro y
     exact y.induction_on rfl (fun a u ↦ by simp [hzc u]) (fun u v hu hv ↦ by simp [hu, hv])
   apply LinearMap.trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero
-  · exact IsTriangularizable.iSup_eq_top (1 ⊗ₜ[R] x)
+  · simpa only [Module.End.maxGenEigenspace_def] using IsTriangularizable.iSup_eq_top (1 ⊗ₜ[R] x)
   · exact fun μ ↦ trace_toEnd_eq_zero_of_mem_lcs A (A ⊗[R] L)
-      (genWeightSpaceOf (A ⊗[R] M) μ (1 ⊗ₜ x)) (le_refl 1) hz
+      (genWeightSpaceOf (A ⊗[R] M) μ ((1:A) ⊗ₜ[R] x)) (le_refl 1) hz
   · exact commute_toEnd_of_mem_center_right (A ⊗[R] M) hzc (1 ⊗ₜ x)
 
 /-- A nilpotent Lie algebra with a representation whose trace form is non-singular is Abelian. -/

Mathlib/Algebra/Lie/Weights/Basic.lean

@@ -782,8 +782,10 @@ lemma iSup_genWeightSpace_eq_top [IsTriangularizable K L M] :
     ⨆ χ : L → K, genWeightSpace M χ = ⊤ := by
   simp only [← LieSubmodule.coe_toSubmodule_eq_iff, LieSubmodule.iSup_coe_toSubmodule,
     LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.top_coeSubmodule, genWeightSpace]
-  exact Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo (toEnd K L M)
-    (fun x y φ z ↦ (genWeightSpaceOf M φ y).lie_mem) (IsTriangularizable.iSup_eq_top)
+  refine Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo (toEnd K L M)
+    (fun x y φ z ↦ (genWeightSpaceOf M φ y).lie_mem) ?_
+  simp_rw [Module.End.maxGenEigenspace_def]
+  apply IsTriangularizable.iSup_eq_top
 
 lemma iSup_genWeightSpace_eq_top' [IsTriangularizable K L M] :
     ⨆ χ : Weight K L M, genWeightSpace M χ = ⊤ := by

Mathlib/Algebra/MvPolynomial/PDeriv.lean

@@ -65,12 +65,12 @@ theorem pderiv_def [DecidableEq σ] (i : σ) : pderiv i = mkDerivation R (Pi.sin
 theorem pderiv_monomial {i : σ} :
     pderiv i (monomial s a) = monomial (s - single i 1) (a * s i) := by
   classical
-    simp only [pderiv_def, mkDerivation_monomial, Finsupp.smul_sum, smul_eq_mul, ← smul_mul_assoc,
-      ← (monomial _).map_smul]
-    refine (Finset.sum_eq_single i (fun j _ hne => ?_) fun hi => ?_).trans ?_
-    · simp [Pi.single_eq_of_ne hne]
-    · rw [Finsupp.not_mem_support_iff] at hi; simp [hi]
-    · simp
+  simp only [pderiv_def, mkDerivation_monomial, Finsupp.smul_sum, smul_eq_mul, ← smul_mul_assoc,
+    ← (monomial _).map_smul]
+  refine (Finset.sum_eq_single i (fun j _ hne => ?_) fun hi => ?_).trans ?_
+  · simp [Pi.single_eq_of_ne hne]
+  · rw [Finsupp.not_mem_support_iff] at hi; simp [hi]
+  · simp
 
 theorem pderiv_C {i : σ} : pderiv i (C a) = 0 :=
   derivation_C _ _
@@ -115,9 +115,10 @@ theorem pderiv_map {S} [CommSemiring S] {φ : R →+* S} {f : MvPolynomial σ R}
   · simp [eq]
   · simp [eq, h]
 
-lemma pderiv_rename {τ : Type*} [DecidableEq τ] [DecidableEq σ] {f : σ → τ}
-    (hf : Function.Injective f) (x : σ) (p : MvPolynomial σ R) :
+lemma pderiv_rename {τ : Type*} {f : σ → τ} (hf : Function.Injective f)
+    (x : σ) (p : MvPolynomial σ R) :
     pderiv (f x) (rename f p) = rename f (pderiv x p) := by
+  classical
   induction' p using MvPolynomial.induction_on with a p q hp hq p a h
   · simp
   · simp [hp, hq]

Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

@@ -210,6 +210,16 @@ theorem prod_le_prod_fiberwise_of_prod_fiber_le_one' {t : Finset ι'} {g : ι 
 
 end OrderedCommMonoid
 
+@[to_additive]
+lemma max_prod_le [LinearOrderedCommMonoid M] {f g : ι → M} {s : Finset ι} :
+    max (s.prod f) (s.prod g) ≤ s.prod (fun i ↦ max (f i) (g i)) :=
+  Multiset.max_prod_le
+
+@[to_additive]
+lemma prod_min_le [LinearOrderedCommMonoid M] {f g : ι → M} {s : Finset ι} :
+    s.prod (fun i ↦ min (f i) (g i)) ≤ min (s.prod f) (s.prod g) :=
+  Multiset.prod_min_le
+
 theorem abs_sum_le_sum_abs {G : Type*} [LinearOrderedAddCommGroup G] (f : ι → G) (s : Finset ι) :
     |∑ i ∈ s, f i| ≤ ∑ i ∈ s, |f i| := le_sum_of_subadditive _ abs_zero abs_add s f
 

Mathlib/Algebra/Order/BigOperators/Group/List.lean

@@ -119,6 +119,24 @@ lemma one_le_prod_of_one_le [Preorder M] [CovariantClass M M (· * ·) (· ≤ 
   rw [prod_cons]
   exact one_le_mul (hl₁ hd (mem_cons_self hd tl)) (ih fun x h => hl₁ x (mem_cons_of_mem hd h))
 
+@[to_additive]
+lemma max_prod_le (l : List α) (f g : α → M) [LinearOrder M]
+    [CovariantClass M M (· * ·) (· ≤ ·)] [CovariantClass M M (Function.swap (· * ·)) (· ≤ ·)] :
+    max (l.map f).prod (l.map g).prod ≤ (l.map fun i ↦ max (f i) (g i)).prod := by
+  rw [max_le_iff]
+  constructor <;> apply List.prod_le_prod' <;> intros
+  · apply le_max_left
+  · apply le_max_right
+
+@[to_additive]
+lemma prod_min_le [LinearOrder M] [CovariantClass M M (· * ·) (· ≤ ·)]
+    [CovariantClass M M (Function.swap (· * ·)) (· ≤ ·)] (l : List α) (f g : α → M) :
+    (l.map fun i ↦ min (f i) (g i)).prod ≤ min (l.map f).prod (l.map g).prod := by
+  rw [le_min_iff]
+  constructor <;> apply List.prod_le_prod' <;> intros
+  · apply min_le_left
+  · apply min_le_right
+
 end Monoid
 
 -- TODO: develop theory of tropical rings

Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean

@@ -156,6 +156,20 @@ lemma max_le_of_forall_le {α : Type*} [LinearOrder α] [OrderBot α] (l : Multi
   induction l using Quotient.inductionOn
   simpa using List.max_le_of_forall_le _ _ h
 
+@[to_additive]
+lemma max_prod_le [LinearOrderedCommMonoid α] {s : Multiset ι} {f g : ι → α} :
+    max (s.map f).prod (s.map g).prod ≤ (s.map fun i ↦ max (f i) (g i)).prod := by
+  obtain ⟨l⟩ := s
+  simp_rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
+  apply List.max_prod_le
+
+@[to_additive]
+lemma prod_min_le [LinearOrderedCommMonoid α] {s : Multiset ι} {f g : ι → α} :
+    (s.map fun i ↦ min (f i) (g i)).prod ≤ min (s.map f).prod (s.map g).prod := by
+  obtain ⟨l⟩ := s
+  simp_rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
+  apply List.prod_min_le
+
 lemma abs_sum_le_sum_abs [LinearOrderedAddCommGroup α] {s : Multiset α} :
     |s.sum| ≤ (s.map abs).sum :=
   le_sum_of_subadditive _ abs_zero abs_add s

Mathlib/Algebra/Order/Field/Basic.lean

@@ -415,7 +415,7 @@ theorem one_div_strictAntiOn : StrictAntiOn (fun x : α => 1 / x) (Set.Ioi 0) :=
 
 theorem one_div_pow_le_one_div_pow_of_le (a1 : 1 ≤ a) {m n : ℕ} (mn : m ≤ n) :
     1 / a ^ n ≤ 1 / a ^ m := by
-  refine (one_div_le_one_div ?_ ?_).mpr (pow_le_pow_right a1 mn) <;>
+  refine (one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ a1 mn) <;>
     exact pow_pos (zero_lt_one.trans_le a1) _
 
 theorem one_div_pow_lt_one_div_pow_of_lt (a1 : 1 < a) {m n : ℕ} (mn : m < n) :

Mathlib/Algebra/Order/Floor.lean

@@ -222,21 +222,13 @@ theorem floor_eq_zero : ⌊a⌋₊ = 0 ↔ a < 1 := by
   rw [← lt_one_iff, ← @cast_one α]
   exact floor_lt' Nat.one_ne_zero
 
-#adaptation_note
-/--
-After nightly-2024-09-06 we can remove the `_root_` prefix below.
--/
 theorem floor_eq_iff (ha : 0 ≤ a) : ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1 := by
   rw [← le_floor_iff ha, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt ha, Nat.lt_add_one_iff,
-    le_antisymm_iff, _root_.and_comm]
+    le_antisymm_iff, and_comm]
 
-#adaptation_note
-/--
-After nightly-2024-09-06 we can remove the `_root_` prefix below.
--/
 theorem floor_eq_iff' (hn : n ≠ 0) : ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1 := by
   rw [← le_floor_iff' hn, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt' (Nat.add_one_ne_zero n),
-    Nat.lt_add_one_iff, le_antisymm_iff, _root_.and_comm]
+    Nat.lt_add_one_iff, le_antisymm_iff, and_comm]
 
 theorem floor_eq_on_Ico (n : ℕ) : ∀ a ∈ (Set.Ico n (n + 1) : Set α), ⌊a⌋₊ = n := fun _ ⟨h₀, h₁⟩ =>
   (floor_eq_iff <| n.cast_nonneg.trans h₀).mpr ⟨h₀, h₁⟩
@@ -328,14 +320,10 @@ theorem floor_lt_ceil_of_lt_of_pos {a b : α} (h : a < b) (h' : 0 < b) : ⌊a⌋
     exact h.trans_le (le_ceil _)
   · rwa [floor_of_nonpos ha.le, lt_ceil, Nat.cast_zero]
 
-#adaptation_note
-/--
-After nightly-2024-09-06 we can remove the `_root_` prefix below.
--/
 theorem ceil_eq_iff (hn : n ≠ 0) : ⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ a ≤ n := by
   rw [← ceil_le, ← not_le, ← ceil_le, not_le,
     tsub_lt_iff_right (Nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)), Nat.lt_add_one_iff,
-    le_antisymm_iff, _root_.and_comm]
+    le_antisymm_iff, and_comm]
 
 @[simp]
 theorem preimage_ceil_zero : (Nat.ceil : α → ℕ) ⁻¹' {0} = Iic 0 :=