bump to nightly-2023-12-28-06

mathlib commit leanprover-community/mathlib@65a1391

Archive/Imo/Imo2006Q5.lean

@@ -154,7 +154,7 @@ theorem imo2006_q5' {P : Polynomial ℤ} (hP : 1 < P.natDegree) :
   by_cases H : (P.comp P - X).roots.toFinset ⊆ (P - X).roots.toFinset
   ·
     exact
-      (Finset.card_le_of_subset H).trans
+      (Finset.card_le_card H).trans
         ((Multiset.toFinset_card_le _).trans ((card_roots' _).trans_eq hPX))
   -- Otherwise, take a, b with P(a) = b, P(b) = a, a ≠ b.
   · rcases Finset.not_subset.1 H with ⟨a, ha, hab⟩
@@ -184,7 +184,7 @@ theorem imo2006_q5' {P : Polynomial ℤ} (hP : 1 < P.natDegree) :
     suffices H' : (P.comp P - X).roots.toFinset ⊆ (P + X - a - b).roots.toFinset
     ·
       exact
-        (Finset.card_le_of_subset H').trans
+        (Finset.card_le_card H').trans
           ((Multiset.toFinset_card_le _).trans <| (card_roots' _).trans_eq hPab)
     · -- Let t be a root of P(P(t)) - t, define u = P(t).
       intro t ht
@@ -212,7 +212,7 @@ open imo2006_q5
 theorem imo2006_q5 {P : Polynomial ℤ} (hP : 1 < P.natDegree) {k : ℕ} (hk : 0 < k) :
     ((P.comp^[k]) X - X).roots.toFinset.card ≤ P.natDegree :=
   by
-  apply (Finset.card_le_of_subset fun t ht => _).trans (imo2006_q5' hP)
+  apply (Finset.card_le_card fun t ht => _).trans (imo2006_q5' hP)
   have hP' : P.comp P - X ≠ 0 := by simpa using polynomial.iterate_comp_sub_X_ne hP zero_lt_two
   replace ht := is_root_of_mem_roots (Multiset.mem_toFinset.1 ht)
   simp only [sub_eq_zero, is_root.def, eval_sub, iterate_comp_eval, eval_X] at ht 

Archive/Imo/Imo2021Q1.lean

@@ -74,7 +74,7 @@ theorem radical_inequality {n : ℕ} (h : 107 ≤ n) : sqrt (4 + 2 * n) ≤ 2 *
   have h1n : 0 ≤ 1 + (n : ℝ) := by norm_cast; exact Nat.zero_le _
   rw [sqrt_le_iff]
   constructor
-  · simp only [sub_nonneg, zero_le_mul_left, zero_lt_two, le_sqrt zero_lt_three.le h1n]
+  · simp only [sub_nonneg, mul_nonneg_iff_of_pos_left, zero_lt_two, le_sqrt zero_lt_three.le h1n]
     norm_cast; linarith only [h]
   ring
   rw [pow_two, ← sqrt_mul h1n, sqrt_mul_self h1n]

Archive/Sensitivity.lean

@@ -487,7 +487,7 @@ theorem huang_degree_theorem (H : Set (Q (m + 1))) (hH : Card H ≥ 2 ^ m + 1) :
       by
       refine' (mul_le_mul_right H_q_pos).2 _
       norm_cast
-      apply Finset.card_le_of_subset
+      apply Finset.card_le_card
       rw [Set.toFinset_inter]
       convert Finset.inter_subset_inter_right coeffs_support
 #align sensitivity.huang_degree_theorem Sensitivity.huang_degree_theorem

Mathbin/Algebra/BigOperators/Basic.lean

@@ -174,14 +174,16 @@ protected theorem map_prod [CommMonoid β] [CommMonoid γ] (g : β →* γ) (f :
 #align monoid_hom.map_prod map_prodₓ
 #align add_monoid_hom.map_sum map_sumₓ
 
-#print MulEquiv.map_prod /-
+/- warning: mul_equiv.map_prod clashes with monoid_hom.map_prod -> map_prodₓ
+Case conversion may be inaccurate. Consider using '#align mul_equiv.map_prod map_prodₓₓ'. -/
+#print map_prodₓ /-
 /-- Deprecated: use `_root_.map_prod` instead. -/
 @[to_additive "Deprecated: use `_root_.map_sum` instead."]
-protected theorem MulEquiv.map_prod [CommMonoid β] [CommMonoid γ] (g : β ≃* γ) (f : α → β)
-    (s : Finset α) : g (∏ x in s, f x) = ∏ x in s, g (f x) :=
+protected theorem map_prod [CommMonoid β] [CommMonoid γ] (g : β ≃* γ) (f : α → β) (s : Finset α) :
+    g (∏ x in s, f x) = ∏ x in s, g (f x) :=
   map_prod g f s
-#align mul_equiv.map_prod MulEquiv.map_prod
-#align add_equiv.map_sum AddEquiv.map_sum
+#align mul_equiv.map_prod map_prodₓ
+#align add_monoid_hom.map_sum map_sumₓ
 -/
 
 #print RingHom.map_list_prod /-

Mathbin/Algebra/GroupPower/Order.lean

@@ -109,6 +109,7 @@ theorem pow_lt_one' {a : M} (ha : a < 1) {k : ℕ} (hk : k ≠ 0) : a ^ k < 1 :=
 #align nsmul_neg nsmul_neg
 -/
 
+#print pow_lt_pow' /-
 @[to_additive nsmul_lt_nsmul]
 theorem pow_lt_pow' [CovariantClass M M (· * ·) (· < ·)] {a : M} {n m : ℕ} (ha : 1 < a)
     (h : n < m) : a ^ n < a ^ m :=
@@ -118,6 +119,7 @@ theorem pow_lt_pow' [CovariantClass M M (· * ·) (· < ·)] {a : M} {n m : ℕ}
   exact lt_mul_of_one_lt_right' _ (one_lt_pow' ha k.succ_ne_zero)
 #align pow_lt_pow' pow_lt_pow'
 #align nsmul_lt_nsmul nsmul_lt_nsmul
+-/
 
 #print pow_right_strictMono' /-
 @[to_additive nsmul_left_strictMono]
@@ -176,6 +178,7 @@ section CovariantLtSwap
 variable [Preorder β] [CovariantClass M M (· * ·) (· < ·)]
   [CovariantClass M M (swap (· * ·)) (· < ·)] {f : β → M}
 
+#print StrictMono.pow_right' /-
 @[to_additive StrictMono.nsmul_left]
 theorem StrictMono.pow_right' (hf : StrictMono f) : ∀ {n : ℕ}, n ≠ 0 → StrictMono fun a => f a ^ n
   | 0, hn => (hn rfl).elim
@@ -184,6 +187,7 @@ theorem StrictMono.pow_right' (hf : StrictMono f) : ∀ {n : ℕ}, n ≠ 0 → S
     exact hf.mul' (StrictMono.pow_right' n.succ_ne_zero)
 #align strict_mono.pow_right' StrictMono.pow_right'
 #align strict_mono.nsmul_left StrictMono.nsmul_left
+-/
 
 #print pow_left_strictMono /-
 /-- See also `pow_strict_mono_right` -/
@@ -201,21 +205,21 @@ section CovariantLeSwap
 variable [Preorder β] [CovariantClass M M (· * ·) (· ≤ ·)]
   [CovariantClass M M (swap (· * ·)) (· ≤ ·)]
 
-#print Monotone.pow_right /-
+#print Monotone.pow_const /-
 @[to_additive Monotone.nsmul_left]
-theorem Monotone.pow_right {f : β → M} (hf : Monotone f) : ∀ n : ℕ, Monotone fun a => f a ^ n
+theorem Monotone.pow_const {f : β → M} (hf : Monotone f) : ∀ n : ℕ, Monotone fun a => f a ^ n
   | 0 => by simpa using monotone_const
-  | n + 1 => by simp_rw [pow_succ]; exact hf.mul' (Monotone.pow_right _)
-#align monotone.pow_right Monotone.pow_right
+  | n + 1 => by simp_rw [pow_succ]; exact hf.mul' (Monotone.pow_const _)
+#align monotone.pow_right Monotone.pow_const
 #align monotone.const_nsmul Monotone.const_nsmul
 -/
 
-#print pow_mono_right /-
-@[to_additive nsmul_mono_left]
-theorem pow_mono_right (n : ℕ) : Monotone fun a : M => a ^ n :=
+#print pow_left_mono /-
+@[to_additive nsmul_right_mono]
+theorem pow_left_mono (n : ℕ) : Monotone fun a : M => a ^ n :=
   monotone_id.pow_right _
-#align pow_mono_right pow_mono_right
-#align nsmul_mono_left nsmul_mono_left
+#align pow_mono_right pow_left_mono
+#align nsmul_mono_left nsmul_right_mono
 -/
 
 end CovariantLeSwap
@@ -317,7 +321,7 @@ variable [CovariantClass M M (· * ·) (· ≤ ·)] [CovariantClass M M (swap (
 #print lt_of_pow_lt_pow_left' /-
 @[to_additive lt_of_nsmul_lt_nsmul_right]
 theorem lt_of_pow_lt_pow_left' {a b : M} (n : ℕ) : a ^ n < b ^ n → a < b :=
-  (pow_mono_right _).reflect_lt
+  (pow_left_mono _).reflect_lt
 #align lt_of_pow_lt_pow' lt_of_pow_lt_pow_left'
 #align lt_of_nsmul_lt_nsmul lt_of_nsmul_lt_nsmul_right
 -/
@@ -354,11 +358,11 @@ section CovariantLtSwap
 variable [CovariantClass M M (· * ·) (· < ·)] [CovariantClass M M (swap (· * ·)) (· < ·)]
 
 #print le_of_pow_le_pow_left' /-
-@[to_additive le_of_nsmul_le_nsmul_right']
+@[to_additive le_of_nsmul_le_nsmul_right]
 theorem le_of_pow_le_pow_left' {a b : M} {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ b ^ n → a ≤ b :=
   (pow_left_strictMono hn).le_iff_le.1
 #align le_of_pow_le_pow' le_of_pow_le_pow_left'
-#align le_of_nsmul_le_nsmul le_of_nsmul_le_nsmul_right'
+#align le_of_nsmul_le_nsmul le_of_nsmul_le_nsmul_right
 -/
 
 #print min_le_of_mul_le_sq /-
@@ -557,13 +561,17 @@ theorem pow_right_strictMono (h : 1 < a) : StrictMono fun n : ℕ => a ^ n :=
 #align pow_strict_mono_right pow_right_strictMono
 -/
 
+#print pow_lt_pow /-
 theorem pow_lt_pow (h : 1 < a) (h2 : n < m) : a ^ n < a ^ m :=
   pow_right_strictMono h h2
 #align pow_lt_pow pow_lt_pow
+-/
 
+#print pow_lt_pow_iff /-
 theorem pow_lt_pow_iff (h : 1 < a) : a ^ n < a ^ m ↔ n < m :=
   (pow_right_strictMono h).lt_iff_lt
 #align pow_lt_pow_iff pow_lt_pow_iff
+-/
 
 #print pow_le_pow_iff_right /-
 theorem pow_le_pow_iff_right (h : 1 < a) : a ^ n ≤ a ^ m ↔ n ≤ m :=

Mathbin/Algebra/Order/Floor.lean

@@ -1254,7 +1254,7 @@ variable {k : Type _} [LinearOrderedField k] [FloorRing k] {b : k}
 
 #print Int.fract_div_mul_self_mem_Ico /-
 theorem fract_div_mul_self_mem_Ico (a b : k) (ha : 0 < a) : fract (b / a) * a ∈ Ico 0 a :=
-  ⟨(zero_le_mul_right ha).2 (fract_nonneg (b / a)),
+  ⟨(mul_nonneg_iff_of_pos_right ha).2 (fract_nonneg (b / a)),
     (mul_lt_iff_lt_one_left ha).2 (fract_lt_one (b / a))⟩
 #align int.fract_div_mul_self_mem_Ico Int.fract_div_mul_self_mem_Ico
 -/
@@ -1723,7 +1723,7 @@ theorem abs_sub_round_eq_min (x : α) : |x - round x| = min (fract x) (1 - fract
   · have : 0 < fract x :=
       by
       replace hx : 0 < fract x + fract x := lt_of_lt_of_le zero_lt_one (tsub_le_iff_left.mp hx)
-      simpa only [← two_mul, zero_lt_mul_left, zero_lt_two] using hx
+      simpa only [← two_mul, mul_pos_iff_of_pos_left, zero_lt_two] using hx
     rw [if_neg (not_lt.mpr hx), if_neg (not_lt.mpr hx), abs_sub_comm, ceil_sub_self_eq this.ne.symm,
       abs_one_sub_fract]
 #align abs_sub_round_eq_min abs_sub_round_eq_min