Merge remote-tracking branch 'nightly-testing/bump/nightly-2026-02-10' into nightly-testing

Author: kim-em

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

@@ -245,7 +245,7 @@ lemma prod_map_erase [DecidableEq α] (f : α → M) {a} :
 @[to_additive] lemma Perm.prod_eq (h : Perm l₁ l₂) : prod l₁ = prod l₂ := h.foldr_op_eq
 
 -- In order to make `to_additive` work, this theorem is adjusted to `List.sum_reverse` from core
-@[to_additive existing]
+@[to_additive existing, simp]
 lemma prod_reverse [One α] [Mul α] [@Std.Associative α (· * ·)] [@Std.Commutative α (· * ·)]
     [@Std.LawfulLeftIdentity α α (· * ·) 1] (l : List α) : prod l.reverse = prod l :=
   @List.sum_reverse α ⟨1⟩ ⟨(· * ·)⟩ _ _ _ l

Mathlib/Data/Multiset/Fintype.lean

@@ -171,7 +171,8 @@ theorem toEmbedding_coeEquiv_trans (m : Multiset α) :
     m.coeEquiv.toEmbedding.trans (Function.Embedding.subtype _) = m.coeEmbedding := by ext <;> rfl
 
 #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/12247
-this was `@[irreducible]`, which is no longer allowed. -/
+this was `@[irreducible]`, which is no longer allowed at the definition site,
+and must be applied afterwards. -/
 instance fintypeCoe : Fintype m :=
   Fintype.ofEquiv m.toEnumFinset m.coeEquiv.symm