chore: adaptations for nightly-2026-04-27

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

@@ -255,7 +255,7 @@ lemma prod_mul_prod_eq_prod_zipWith_mul_prod_drop :
   | [], ys => by simp
   | xs, [] => by simp
   | x :: xs, y :: ys => by
-    simp only [drop, zipWith_cons_cons, prod_cons]
+    simp only [zipWith_cons_cons, prod_cons]
     conv =>
       lhs; rw [mul_assoc]; right; rw [mul_comm, mul_assoc]; right
       rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]

Mathlib/Algebra/Group/Defs.lean

@@ -557,7 +557,8 @@ theorem npowRec'_two_mul {M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) :
     match k' with
     | 0 => rfl
     | 1 => simp [npowRec']
-    | k + 2 => simp [npowRec', ← mul_assoc, ← ih]
+    | k + 2 =>
+      simp [npowRec', ← mul_assoc, ← ih, Nat.mul_succ]
 
 @[to_additive]
 theorem npowRec'_mul_comm {M : Type*} [Semigroup M] [One M] {k : ℕ} (k0 : k ≠ 0) (m : M) :

Mathlib/AlgebraicTopology/SimplexCategory/Augmented/Monoidal.lean

@@ -173,10 +173,12 @@ abbrev inr' (x y : SimplexCategory) : y ⟶ tensorObjOf x y := WithInitial.down
 set_option backward.isDefEq.respectTransparency false in
 lemma inl'_eval (x y : SimplexCategory) (i : Fin (x.len + 1)) :
     (inl' x y).toOrderHom i = (i.castAdd _).cast (Nat.succ_add x.len (y.len + 1)) := by
-  dsimp [inl', inl, MonoidalCategoryStruct.rightUnitor, MonoidalCategoryStruct.whiskerLeft,
-    tensorHom, WithInitial.down, rightUnitor, tensorObj]
   ext
-  simp [OrderEmbedding.toOrderHom]
+  simp [inl', inl, MonoidalCategoryStruct.rightUnitor, MonoidalCategoryStruct.whiskerLeft,
+    MonoidalCategoryStruct.tensorUnit, MonoidalCategoryStruct.tensorObj,
+    tensorUnit, tensorHom, WithInitial.down, rightUnitor, tensorObj, CategoryStruct.id,
+    CategoryStruct.comp, WithInitial.comp, WithInitial.id,
+    OrderEmbedding.toOrderHom]
 
 set_option backward.isDefEq.respectTransparency false in
 lemma inr'_eval (x y : SimplexCategory) (i : Fin (y.len + 1)) :

Mathlib/CategoryTheory/Bicategory/Coherence.lean

@@ -133,6 +133,25 @@ def normalizeIso {a : B} :
   | _, _, p, Hom.comp f g =>
     (α_ _ _ _).symm ≪≫ whiskerRightIso (normalizeIso p f) g ≪≫ normalizeIso (normalizeAux p f) g
 
+-- Equation lemmas for `normalizeIso`/`normalizeAux` matching `≫`/`𝟙`
+-- (i.e., `CategoryStruct.comp`/`CategoryStruct.id` for `FreeBicategory`) instead of
+-- `Hom.comp`/`Hom.id`. Needed because after leanprover/lean4#13363, `canUnfoldAtMatcher`
+-- no longer unfolds class projections in match discriminants.
+@[simp] theorem normalizeAux_comp {a : B} {b c d : FreeBicategory B}
+    (p : Path a b) (f : b ⟶ c) (g : c ⟶ d) :
+    normalizeAux p (f ≫ g) = normalizeAux (normalizeAux p f) g := rfl
+@[simp] theorem normalizeAux_id {a : B} {b : FreeBicategory B} (p : Path a b) :
+    normalizeAux p (𝟙 b) = p := rfl
+@[simp] theorem normalizeIso_comp {a : B} {b c d : FreeBicategory B}
+    (p : Path a b) (f : b ⟶ c) (g : c ⟶ d) :
+    normalizeIso p (f ≫ g) =
+      (α_ _ _ _).symm ≪≫ whiskerRightIso (normalizeIso p f) g ≪≫
+        normalizeIso (normalizeAux p f) g := rfl
+@[simp] theorem normalizeIso_id {a : B} {b : FreeBicategory B} (p : Path a b) :
+    normalizeIso p (𝟙 b) = ρ_ _ := rfl
+@[simp] theorem quot_whisker_left {a b c : FreeBicategory B} (f : a ⟶ b) {g h : b ⟶ c}
+    (η : Hom₂ g h) : Quot.mk Rel (Hom₂.whisker_left f η) = f ◁ (Quot.mk Rel η) := rfl
+
 /-- Given a 2-morphism between `f` and `g` in the free bicategory, we have the equality
 `normalizeAux p f = normalizeAux p g`.
 -/

Mathlib/CategoryTheory/Bicategory/Functor/LocallyDiscrete.lean

@@ -114,7 +114,8 @@ corresponding locally discrete bicategories.
 def Functor.toPseudofunctor : LocallyDiscrete C ⥤ᵖ (LocallyDiscrete D) :=
   pseudofunctorOfIsLocallyDiscrete
     (fun ⟨X⟩ ↦ .mk <| F.obj X) (fun ⟨f⟩ ↦ (F.map f).toLoc)
-    (fun ⟨X⟩ ↦ eqToIso (by simp)) (fun f g ↦ eqToIso (by simp))
+    (fun ⟨X⟩ ↦ eqToIso (by simp [CategoryStruct.id]))
+    (fun ⟨f⟩ ⟨g⟩ ↦ eqToIso (by simp [CategoryStruct.comp]))
 
 @[deprecated (since := "2026-02-08")] alias Functor.toPseudoFunctor := Functor.toPseudofunctor
 
@@ -145,7 +146,8 @@ be promoted to a pseudofunctor from `LocallyDiscrete I` to `B`.
 def Functor.toPseudofunctor' : LocallyDiscrete I ⥤ᵖ B :=
   pseudofunctorOfIsLocallyDiscrete
     (fun ⟨X⟩ ↦ F.obj X) (fun ⟨f⟩ ↦ F.map f)
-    (fun ⟨X⟩ ↦ eqToIso (by simp)) (fun f g ↦ eqToIso (by simp))
+    (fun ⟨X⟩ ↦ eqToIso (by simp [CategoryStruct.id]))
+    (fun f g ↦ eqToIso (by obtain ⟨f⟩ := f; obtain ⟨g⟩ := g; simp [CategoryStruct.comp]))
 
 @[deprecated (since := "2026-02-08")] alias Functor.toPseudoFunctor' := Functor.toPseudofunctor'
 

Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean

@@ -296,11 +296,11 @@ def multiequalizerEquivAux {J : MulticospanShape.{w, w'}} (I : MulticospanIndex
         | WalkingMulticospan.right b => I.fst b (x.1 _)
       property := by
         rintro (a | b) (a' | b') (f | f | f)
-        · simp
+        · simp only [WalkingMulticospan.Hom.id_eq_id, Functor.map_id]; rfl
         · rfl
         · dsimp
           exact (x.2 b').symm
-        · simp }
+        · simp only [WalkingMulticospan.Hom.id_eq_id, Functor.map_id]; rfl }
   left_inv := by
     intro x; ext (a | b)
     · rfl

Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean

@@ -210,24 +210,49 @@ theorem walkingParallelPairOpEquiv_counitIso_inv_app_op_one :
     walkingParallelPairOpEquiv.counitIso.inv.app (op one) = 𝟙 (op one) :=
   rfl
 
-variable {C : Type u} [Category.{v} C]
+variable {C : Type u}
 variable {X Y : C}
 
+namespace parallelPair
+
+/-- Implementation of `parallelPair`, do not use directly. -/
+@[instance_reducible]
+def parallelPairObj (X Y : C) (x : WalkingParallelPair) : C :=
+  match x with
+  | zero => X
+  | one => Y
+
+@[simp] theorem parallelPairObj_zero : parallelPairObj X Y zero = X := rfl
+@[simp] theorem parallelPairObj_one : parallelPairObj X Y one = Y := rfl
+
+variable [Category.{v} C]
+
+/-- Implementation of `parallelPair`, do not use directly. -/
+def parallelPairHom (f g : X ⟶ Y) {x y : WalkingParallelPair} (h : x ⟶ y) :
+    parallelPairObj X Y x ⟶ parallelPairObj X Y y :=
+  match h with
+  | .id _ => 𝟙 _
+  | .left => f
+  | .right => g
+
+@[simp] theorem parallelPairHom_id {f g : X ⟶ Y} {x : WalkingParallelPair} :
+  parallelPairHom f g (𝟙 x) = 𝟙 (parallelPairObj X Y x) := (rfl)
+@[simp] theorem parallelPairHom_left {f g : X ⟶ Y} :
+  parallelPairHom f g .left = f := (rfl)
+@[simp] theorem parallelPairHom_right {f g : X ⟶ Y} :
+  parallelPairHom f g .right = g := (rfl)
+
+end parallelPair
+
+variable [Category.{v} C]
+
+open parallelPair in
 /-- `parallelPair f g` is the diagram in `C` consisting of the two morphisms `f` and `g` with
 common domain and codomain. -/
 def parallelPair (f g : X ⟶ Y) : WalkingParallelPair ⥤ C where
-  obj x :=
-    match x with
-    | zero => X
-    | one => Y
-  map h :=
-    match h with
-    | WalkingParallelPairHom.id _ => 𝟙 _
-    | left => f
-    | right => g
-  -- `sorry` can cope with this, but it's too slow:
-  map_comp := by
-    rintro _ _ _ ⟨⟩ g <;> cases g <;> simp
+  obj x := parallelPairObj X Y x
+  map h := parallelPairHom f g h
+  map_comp := by rintro _ _ _ ⟨⟩ ⟨⟩ <;> simp
 
 @[simp]
 theorem parallelPair_obj_zero (f g : X ⟶ Y) : (parallelPair f g).obj zero = X := rfl

Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean

@@ -540,8 +540,21 @@ def ofι {J : MulticospanShape.{w, w'}} (I : MulticospanIndex J C)
         | WalkingMulticospan.left _ => ι _
         | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b
       naturality := by
+        #adaptation_note /-- Proof repaired after leanprover/lean4#13363.
+        The proof used to finish from this point as
+        ```
         rintro (_ | _) (_ | _) (_ | _ | _) <;>
           dsimp <;> simp only [Category.id_comp, Category.comp_id]
+        apply w
+        ```
+        The replacement proof is a short-term fix, and we request that the authors/maintainers of
+        this file review the proof, and either approve it by removing this note,
+        revise the proof or the prerequisites appropriately, or minimize a problem in lean4 that
+        still needs addressing. -/
+        rintro (_ | _) (_ | _) (_ | _ | _) <;>
+          simp only [WalkingMulticospan.Hom.id_eq_id,
+            Functor.map_id, Functor.const_obj_map, Category.comp_id] <;>
+          dsimp <;> simp only [Category.id_comp]
         apply w }
 
 @[simp]
@@ -658,11 +671,28 @@ def ofPiFork
     | WalkingMulticospan.left _ => a.ι ≫ c.proj _
     | WalkingMulticospan.right _ => a.ι ≫ I.fstPiMapOfIsLimit c hd ≫ d.proj _
   π.naturality := by
+    #adaptation_note /-- Proof repaired after leanprover/lean4#13363.
+    The proof used to finish from this point as
+    ```
     rintro (_ | _) (_ | _) (_ | _ | _)
     · simp
     · simp
     · dsimp; rw [a.condition_assoc]; simp
     · simp
+    ```
+    The replacement proof is a short-term fix, and we request that the authors/maintainers of
+    this file review the proof, and either approve it by removing this note, revise
+    the proof or the prerequisites appropriately, or minimize a problem in lean4 that still
+    needs addressing. -/
+    rintro (_ | _) (_ | _) (_ | _ | _)
+    · simp only [WalkingMulticospan.Hom.id_eq_id, Functor.map_id,
+        Functor.const_obj_map, Category.comp_id]
+      exact Category.id_comp _
+    · simp
+    · dsimp; rw [a.condition_assoc]; simp
+    · simp only [WalkingMulticospan.Hom.id_eq_id, Functor.map_id,
+        Functor.const_obj_map, Category.comp_id]
+      exact Category.id_comp _
 
 @[simp]
 theorem ofPiFork_ι (a : Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd)) (i) :

Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean

@@ -105,6 +105,10 @@ theorem normalizeObj_tensor (X Y : F C) (n : NormalMonoidalObject C) :
 /-- Auxiliary definition for `normalize`. -/
 def normalizeObj' (X : F C) : N C ⥤ N C := Discrete.functor fun n ↦ ⟨normalizeObj X n⟩
 
+@[simp]
+theorem as_obj_normalizeObj' (X : F C) (n : N C) :
+    ((normalizeObj' X).obj n).as = normalizeObj X n.as := rfl
+
 section
 
 open Hom
@@ -186,14 +190,20 @@ def normalizeIsoApp :
 
 /-- Almost non-definitionally equal to `normalizeIsoApp`, but has a better definitional property
 in the proof of `normalize_naturality`. -/
-@[simp]
 def normalizeIsoApp' :
     ∀ (X : F C) (n : NormalMonoidalObject C), inclusionObj n ⊗ X ≅ inclusionObj (normalizeObj X n)
   | of _, _ => Iso.refl _
   | unit, _ => ρ_ _
   | tensor X Y, n =>
     (α_ _ _ _).symm ≪≫ whiskerRightIso (normalizeIsoApp' X n) Y ≪≫ normalizeIsoApp' _ _
 
+@[simp] theorem normalizeIsoApp'_tensor (X Y : F C) (n : NormalMonoidalObject C) :
+    normalizeIsoApp' C (X ⊗ Y) n =
+      (α_ _ _ _).symm ≪≫ whiskerRightIso (normalizeIsoApp' C X n) Y ≪≫
+        normalizeIsoApp' C Y _ := rfl
+@[simp] theorem normalizeIsoApp'_unit (n : NormalMonoidalObject C) :
+    normalizeIsoApp' C (𝟙_ (F C)) n = ρ_ _ := rfl
+
 theorem normalizeIsoApp_eq :
     ∀ (X : F C) (n : N C), normalizeIsoApp C X n = normalizeIsoApp' C X n.as
   | of _, _ => rfl
@@ -202,7 +212,7 @@ theorem normalizeIsoApp_eq :
       rw [normalizeIsoApp, normalizeIsoApp']
       rw [normalizeIsoApp_eq X n]
       rw [normalizeIsoApp_eq Y ⟨normalizeObj X n.as⟩]
-      rfl
+      simp
 
 @[simp]
 theorem normalizeIsoApp_tensor (X Y : F C) (n : N C) :
@@ -253,13 +263,13 @@ theorem normalize_naturality (n : NormalMonoidalObject C) {X Y : F C} (f : X ⟶
   case comp f g ihf ihg => simp [ihg, reassoc_of% (ihf _)]
   case whiskerLeft X' X Y f ih =>
     intro n
-    dsimp only [normalizeObj_tensor, normalizeIsoApp', tensor_eq_tensor, Iso.trans_hom,
+    dsimp only [normalizeObj_tensor, normalizeIsoApp'_tensor, Iso.trans_hom,
       Iso.symm_hom, whiskerRightIso_hom, Function.comp_apply, inclusion_obj]
     rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih]
     simp
   case whiskerRight X Y h η' ih =>
     intro n
-    dsimp only [normalizeObj_tensor, normalizeIsoApp', tensor_eq_tensor, Iso.trans_hom,
+    dsimp only [normalizeObj_tensor, normalizeIsoApp'_tensor, Iso.trans_hom,
       Iso.symm_hom, whiskerRightIso_hom, Function.comp_apply, inclusion_obj]
     rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ih]
     have := dcongr_arg (fun x => (normalizeIsoApp' C η' x).hom) (normalizeObj_congr n h)
@@ -268,7 +278,6 @@ theorem normalize_naturality (n : NormalMonoidalObject C) {X Y : F C} (f : X ⟶
 
 end
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The isomorphism between `n ⊗ X` and `normalize X n` is natural (in both `X` and `n`, but
 naturality in `n` is trivial and was "proved" in `normalizeIsoAux`). This is the real heart
 of our proof of the coherence theorem. -/

Mathlib/CategoryTheory/Sites/DenseSubsite/OneHypercoverDense.lean

@@ -106,8 +106,8 @@ def multicospanMap {P Q : C₀ᵒᵖ ⥤ A} (f : P ⟶ Q) :
     | WalkingMulticospan.left i => f.app _
     | WalkingMulticospan.right j => f.app _
   naturality := by
-    rintro (i₁ | j₁) (i₂ | j₂) (_ | _)
-    all_goals simp
+    rintro (i₁ | j₁) (i₂ | j₂) (_ | _) <;>
+    simp [MulticospanIndex.multicospan]
 
 /-- The natural isomorphism between the diagrams attached to `data : F.PreOneHypercoverDenseData X`
 that are induced by isomorphisms in `C₀ᵒᵖ ⥤ A`. -/

Mathlib/CategoryTheory/Sites/Hypercover/One.lean

@@ -747,7 +747,9 @@ def Hom.mapMulticospan {E : PreOneHypercover.{w} S} {F : PreOneHypercover.{w'} S
     | .id _ => .id _
     | .fst i => WalkingMulticospan.Hom.fst (J := F.multicospanShape) (f.s₁' i)
     | .snd i => WalkingMulticospan.Hom.snd (J := F.multicospanShape) (f.s₁' i)
-  map_id := by simp
+  map_id
+    | .left _ => rfl
+    | .right _ => rfl
   map_comp
     | .id _, _ => by simp
     | .fst _, .id _ => by simp

Mathlib/CategoryTheory/Sites/Whiskering.lean

@@ -117,8 +117,20 @@ def multicospanComp : (S.index (P ⋙ F)).multicospan ≅ (S.index P).multicospa
       | WalkingMulticospan.left _ => Iso.refl _
       | WalkingMulticospan.right _ => Iso.refl _)
     (by
+      #adaptation_note /-- Proof repaired after leanprover/lean4#13363.
+      The body of this `by` block was previously
+      ```
       rintro (a | b) (a | b) (f | f | f)
-      all_goals cat_disch)
+      all_goals cat_disch
+      ```
+      The replacement proof is a short-term fix, and we request that the authors/maintainers of
+      this file review the proof, and either approve it by removing this note,
+      revise the proof or the prerequisites appropriately, or minimize a problem in lean4 that
+      still needs addressing. -/
+      rintro (a | b) (a | b) (f | f | f) <;>
+        simp only [WalkingMulticospan.Hom.id_eq_id, Iso.refl_hom, Category.id_comp,
+          Category.comp_id, Functor.map_id] <;>
+        dsimp [CategoryStruct.comp] <;> simp)
 
 /-- Mapping the multifork associated to a cover `S : J.Cover X` and a presheaf `P` with
 respect to a functor `F` is isomorphic (upto a natural isomorphism of the underlying functors)

Mathlib/Data/List/Permutation.lean

@@ -278,7 +278,7 @@ theorem length_permutationsAux :
   refine permutationsAux.rec (by simp) ?_
   intro t ts is IH1 IH2
   have IH2 : length (permutationsAux is nil) + 1 = is.length ! := by simpa using IH2
-  simp only [factorial, Nat.mul_comm, add_eq] at IH1
+  simp only [List.length_cons, factorial, Nat.mul_comm, add_eq] at IH1
   rw [permutationsAux_cons,
     length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq,
     permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1),

Mathlib/ModelTheory/Order.lean

@@ -135,7 +135,7 @@ language. -/
 @[simps] def orderLHom : Language.order →ᴸ L where
   onRelation | _, .le => leSymb
 
-@[simp]
+@[simp, nolint simpNF]
 theorem orderLHom_leSymb :
     (orderLHom L).onRelation leSymb = (leSymb : L.Relations 2) :=
   rfl

Mathlib/ModelTheory/Semantics.lean

@@ -272,7 +272,7 @@ theorem realize_top : (⊤ : L.BoundedFormula α l).Realize v xs ↔ True := by
 
 @[simp]
 theorem realize_inf : (φ ⊓ ψ).Realize v xs ↔ φ.Realize v xs ∧ ψ.Realize v xs := by
-  simp [Realize]
+  simp [Realize, Min.min]
 
 @[simp]
 theorem realize_foldr_inf (l : List (L.BoundedFormula α n)) (v : α → M) (xs : Fin n → M) :