diff --git a/Mathlib/Algebra/BigOperators/Group/List/Basic.lean b/Mathlib/Algebra/BigOperators/Group/List/Basic.lean
index 96546ee4f9951f..5fab4fde93634b 100644
--- a/Mathlib/Algebra/BigOperators/Group/List/Basic.lean
+++ b/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]
diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean
index 336bd292f3eb31..784656966179ed 100644
--- a/Mathlib/Algebra/Group/Defs.lean
+++ b/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) :
diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/Augmented/Monoidal.lean b/Mathlib/AlgebraicTopology/SimplexCategory/Augmented/Monoidal.lean
index 76e79afdb35092..37bb7910767159 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/Augmented/Monoidal.lean
+++ b/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)) :
diff --git a/Mathlib/CategoryTheory/Bicategory/Coherence.lean b/Mathlib/CategoryTheory/Bicategory/Coherence.lean
index e816e919a204b5..db4063a746e10a 100644
--- a/Mathlib/CategoryTheory/Bicategory/Coherence.lean
+++ b/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`.
 -/
diff --git a/Mathlib/CategoryTheory/Bicategory/Functor/LocallyDiscrete.lean b/Mathlib/CategoryTheory/Bicategory/Functor/LocallyDiscrete.lean
index bd3385194354e8..64c99a93bb5ccc 100644
--- a/Mathlib/CategoryTheory/Bicategory/Functor/LocallyDiscrete.lean
+++ b/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'
 
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean b/Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
index 6747ce7cb7c1c5..43b0d7cc35f8fb 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
+++ b/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
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
index 1cdad676898b3c..d0e620823bee18 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
+++ b/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
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean b/Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
index 6eab05ecb90c7b..1e74989fbe0043 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
+++ b/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) :
diff --git a/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean b/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
index 006e7944cc975b..198682b4951a66 100644
--- a/Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
+++ b/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,7 +190,6 @@ 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 _
@@ -194,6 +197,13 @@ def normalizeIsoApp' :
   | 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. -/
diff --git a/Mathlib/CategoryTheory/Sites/DenseSubsite/OneHypercoverDense.lean b/Mathlib/CategoryTheory/Sites/DenseSubsite/OneHypercoverDense.lean
index f8304807efa444..d9110e17b9eee1 100644
--- a/Mathlib/CategoryTheory/Sites/DenseSubsite/OneHypercoverDense.lean
+++ b/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`. -/
diff --git a/Mathlib/CategoryTheory/Sites/Hypercover/One.lean b/Mathlib/CategoryTheory/Sites/Hypercover/One.lean
index cf59dca760ca51..cf1ac845094b58 100644
--- a/Mathlib/CategoryTheory/Sites/Hypercover/One.lean
+++ b/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
diff --git a/Mathlib/CategoryTheory/Sites/Whiskering.lean b/Mathlib/CategoryTheory/Sites/Whiskering.lean
index e887b265ab004c..fe31d6e83c88a3 100644
--- a/Mathlib/CategoryTheory/Sites/Whiskering.lean
+++ b/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)
diff --git a/Mathlib/Data/List/Permutation.lean b/Mathlib/Data/List/Permutation.lean
index 324cfbf78b5b3f..fd384a7bbab131 100644
--- a/Mathlib/Data/List/Permutation.lean
+++ b/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),
diff --git a/Mathlib/ModelTheory/Order.lean b/Mathlib/ModelTheory/Order.lean
index fc294f4a38219d..612379dc25b139 100644
--- a/Mathlib/ModelTheory/Order.lean
+++ b/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
diff --git a/Mathlib/ModelTheory/Semantics.lean b/Mathlib/ModelTheory/Semantics.lean
index ea9418de56f9a9..367530edf5ef2f 100644
--- a/Mathlib/ModelTheory/Semantics.lean
+++ b/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) :
diff --git a/Mathlib/SetTheory/Ordinal/Notation.lean b/Mathlib/SetTheory/Ordinal/Notation.lean
index 1db13c525f0771..3e391bb77327dd 100644
--- a/Mathlib/SetTheory/Ordinal/Notation.lean
+++ b/Mathlib/SetTheory/Ordinal/Notation.lean
@@ -437,9 +437,10 @@ theorem repr_add : ∀ (o₁ o₂) [NF o₁] [NF o₂], repr (o₁ + o₂) = rep
         Ordering.compares_eq, repr, gt_iff_lt, PNat.add_coe, Nat.cast_add] at ee ⊢
     · rw [← add_assoc, @add_of_omega0_opow_le _ (repr e') (ω ^ repr e' * (n' : ℕ))]
       · have := (h₁.below_of_lt ee).repr_lt
-        unfold repr at this
-        cases he' : e' <;> simp only [he', zero_def, opow_zero, repr, gt_iff_lt] at this ⊢ <;>
-        exact lt_of_le_of_lt le_self_add this
+        simp only [repr] at this
+        cases he' : e' <;>
+          simp only [he', zero_def, opow_zero, repr, repr_zero, gt_iff_lt] at this ⊢ <;>
+          exact lt_of_le_of_lt le_self_add this
       · simpa using (mul_le_mul_iff_right₀ <| opow_pos (repr e') omega0_pos).2
           (Nat.cast_le.2 n'.pos)
     · rw [ee, ← add_assoc, ← mul_add]
@@ -555,8 +556,9 @@ theorem repr_mul : ∀ (o₁ o₂) [NF o₁] [NF o₂], repr (o₁ * o₂) = rep
       simpa using (mul_le_mul_iff_right₀ <| opow_pos _ omega0_pos).2 (Nat.cast_le.2 n₁.2)
     by_cases e0 : e₂ = 0
     · obtain ⟨x, xe⟩ := Nat.exists_eq_succ_of_ne_zero n₂.ne_zero
-      simp only [Mul.mul, mul, e0, ↓reduceIte, repr, PNat.mul_coe, natCast_mul, opow_zero, one_mul]
-      simp only [xe, h₂.zero_of_zero e0, repr, add_zero]
+      simp only [Mul.mul, mul, e0, ↓reduceIte, repr, repr_zero, PNat.mul_coe, natCast_mul,
+        opow_zero, one_mul]
+      simp only [xe, h₂.zero_of_zero e0, repr_zero, add_zero]
       rw [natCast_succ x, add_mul_succ _ ao, mul_assoc]
     · simp only [repr]
       haveI := h₁.fst
@@ -742,6 +744,9 @@ instance nf_opow (o₁ o₂) [NF o₁] [NF o₂] : NF (o₁ ^ o₂) := by
   rcases e₂ : split' o₂ with ⟨b', k⟩
   haveI := (nf_repr_split' e₂).1
   obtain - | ⟨a0, n, a'⟩ := a
+  #adaptation_note /-- Proof repaired after leanprover/lean4#13363.
+  The next branch was previously
+  ```
   · rcases m with - | m
     · by_cases o₂ = 0 <;> simp only [(· ^ ·), Pow.pow, opow, opowAux2, *] <;> decide
     · by_cases m = 0
@@ -749,6 +754,26 @@ instance nf_opow (o₁ o₂) [NF o₁] [NF o₂] : NF (o₁ ^ o₂) := by
         decide
       · simp only [(· ^ ·), Pow.pow, opow, opowAux2, *]
         infer_instance
+  ```
+  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. -/
+  · rcases m with - | m
+    · by_cases h : o₂ = 0
+      · subst h
+        simp only [(· ^ ·), Pow.pow, opow, opowAux2, e₁, OfNat.ofNat, Zero.zero, One.one]
+        decide
+      · have h' : o₂ ≠ zero := fun he => h (he ▸ zero_def ▸ rfl)
+        simp only [(· ^ ·), Pow.pow, opow, opowAux2, e₁, OfNat.ofNat, Zero.zero, One.one,
+          h', ite_false]
+        exact NF.zero
+    · by_cases h : m = 0
+      · simp only [(· ^ ·), Pow.pow, opow, opowAux2, OfNat.ofNat, Zero.zero, One.one, *]
+        decide
+      · simp only [(· ^ ·), Pow.pow, opow, opowAux2, OfNat.ofNat, Zero.zero, *]
+        change NF (oadd _ _ 0)
+        infer_instance
   · simp only [(· ^ ·), Pow.pow, opow, opowAux2, e₁, split_eq_scale_split' e₂, mulNat_eq_mul]
     have := na.fst
     rcases k with - | k
@@ -809,10 +834,11 @@ theorem repr_opow_aux₂ {a0 a'} [N0 : NF a0] [Na' : NF a'] (m : ℕ) (d : ω 
     = (α' + m) ^ (succ ↑k : Ordinal) at IH
   have RR : R' = ω0 ^ (k : Ordinal) * (α' * m) + R := by
     by_cases h : m = 0
-    · simp only [R, R', h, ONote.ofNat, Nat.cast_zero, ONote.repr, mul_zero,
-        ONote.opowAux, add_zero]
-    · simp only [α', ω0, R, R', ONote.repr_scale, ONote.repr, ONote.mulNat_eq_mul, ONote.opowAux,
-        ONote.repr_ofNat, ONote.repr_mul, ONote.repr_add, Ordinal.opow_mul, ONote.zero_add]
+    · simp only [R, R', h, ONote.ofNat, Nat.cast_zero, ONote.repr_zero,
+        mul_zero, ONote.opowAux, add_zero]
+    · simp only [α', ω0, R, R', ONote.repr_scale, ONote.repr,
+        ONote.mulNat_eq_mul, ONote.opowAux, ONote.repr_ofNat, ONote.repr_mul, ONote.repr_add,
+        Ordinal.opow_mul, ONote.zero_add]
   have α0 : 0 < α' := by simpa [lt_def, repr] using oadd_pos a0 n a'
   have ω00 : 0 < ω0 ^ (k : Ordinal) := opow_pos _ (opow_pos _ omega0_pos)
   have Rl : R < ω ^ (repr a0 * succ ↑k) := by
@@ -878,6 +904,9 @@ theorem repr_opow (o₁ o₂) [NF o₁] [NF o₂] : repr (o₁ ^ o₂) = repr o
   rcases e₁ : split o₁ with ⟨a, m⟩
   obtain ⟨N₁, r₁⟩ := nf_repr_split e₁
   obtain - | ⟨a0, n, a'⟩ := a
+  #adaptation_note /-- Proof repaired after leanprover/lean4#13363.
+  The next block was previously
+  ```
   · rcases m with - | m
     · by_cases h : o₂ = 0 <;> simp [opow_def, opowAux2, e₁, h, r₁]
       have := mt repr_inj.1 h
@@ -889,6 +918,27 @@ theorem repr_opow (o₁ o₂) [NF o₁] [NF o₂] : repr (o₁ ^ o₂) = repr o
       simp only [opow_def, opowAux2, e₁, r₁, e₂, r₂, repr,
           Nat.cast_succ, _root_.zero_add,
           add_zero]
+  ```
+  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. -/
+  · rcases m with - | m
+    · have hzero : (0 : ONote) = zero := rfl
+      by_cases h : o₂ = 0
+      · subst h; simp [-zero_def, opow_def, opowAux2, e₁, r₁, hzero]
+      · have h' := mt repr_inj.1 h
+        have hne : o₂ ≠ zero := fun he => h (he ▸ rfl)
+        simp [-zero_def, opow_def, opowAux2, e₁, r₁, hne, hzero]
+        exact (zero_opow h').symm
+    · rcases e₂ : split' o₂ with ⟨b', k⟩
+      obtain ⟨_, r₂⟩ := nf_repr_split' e₂
+      by_cases h : m = 0
+      · simp only [opowAux2, opow_def, e₁, h, r₁, r₂, OfNat.ofNat, Zero.zero, One.one,
+          repr]
+        simp [opow_add, opow_mul]
+      simp only [opow_def, opowAux2, e₁, r₁, e₂, r₂, repr,
+          Nat.cast_succ, _root_.zero_add, add_zero]
       rw [opow_add, opow_mul, opow_omega0]
       · simp
       · simpa [Nat.one_le_iff_ne_zero]
@@ -905,10 +955,10 @@ theorem repr_opow (o₁ o₂) [NF o₁] [NF o₂] : repr (o₁ ^ o₂) = repr o
     simp only [opow_def, e₁, r₁, split_eq_scale_split' e₂, opowAux2, repr]
     rcases k with - | k
     · simp [r₂, opow_mul, repr_opow_aux₁ a00 al aa, add_assoc]
-    · simp [r₂, opow_add, opow_mul, mul_assoc, add_assoc]
+    · simp [r₂, opow_add, opow_mul, mul_assoc, add_assoc, repr_one]
       rw [repr_opow_aux₁ a00 al aa, scale_opowAux]
-      simp only [repr_mul, repr_scale, repr, opow_zero, PNat.val_ofNat, Nat.cast_one, mul_one,
-        add_zero, opow_one, opow_mul]
+      simp only [repr_mul, repr_scale, repr_one,
+        Nat.cast_one, opow_one, opow_mul]
       rw [← mul_add, ← add_assoc ((ω : Ordinal.{0}) ^ repr a0 * (n : ℕ))]
       congr 1
       rw [← pow_succ, ← opow_natCast, ← opow_natCast]
@@ -998,8 +1048,8 @@ theorem fundamentalSequence_has_prop (o) : FundamentalSequenceProp o (fundamenta
             have := PNat.natPred_add_one m; rw [e'] at this; exact PNat.coe_inj.1 this.symm]) <;>
       (try rw [show m = (m' + 1).succPNat by
               rw [← e', ← PNat.coe_inj, Nat.succPNat_coe, ← Nat.add_one, PNat.natPred_add_one]]) <;>
-      simp only [repr, iha, ihb, opow_lt_opow_iff_right one_lt_omega0, add_lt_add_iff_left,
-        add_zero, lt_add_iff_pos_right, lt_def, mul_one, Nat.cast_zero,
+      simp only [repr, repr_zero, iha, ihb, opow_lt_opow_iff_right one_lt_omega0,
+        add_lt_add_iff_left, add_zero, lt_add_iff_pos_right, lt_def, mul_one, Nat.cast_zero,
         Nat.cast_succ, Nat.succPNat_coe, opow_succ, opow_zero, mul_add_one, PNat.one_coe,
         _root_.zero_add, zero_def]
     · constructor
@@ -1021,7 +1071,7 @@ theorem fundamentalSequence_has_prop (o) : FundamentalSequenceProp o (fundamenta
         gcongr
         apply natCast_lt_omega0
       · refine fun H => H.fst.oadd _ (NF.below_of_lt' ?_ (@NF.oadd_zero _ _ (iha.2 H.fst)))
-        rw [repr, ← zero_def, repr, add_zero, iha.1, opow_succ]
+        rw [repr, repr_zero, add_zero, iha.1, opow_succ]
         gcongr
         apply natCast_lt_omega0
     · rcases iha with ⟨h1, h2, h3⟩
@@ -1035,7 +1085,7 @@ theorem fundamentalSequence_has_prop (o) : FundamentalSequenceProp o (fundamenta
           exists_lt_add (exists_lt_omega0_opow' one_lt_omega0 h1 h3)⟩
       obtain ⟨h4, h5, h6⟩ := h2 i
       refine ⟨h4, h5, fun H => H.fst.oadd _ (NF.below_of_lt' ?_ (@NF.oadd_zero _ _ (h6 H.fst)))⟩
-      rwa [repr, ← zero_def, repr, add_zero, PNat.one_coe, Nat.cast_one, mul_one,
+      rwa [repr, repr_zero, add_zero, PNat.one_coe, Nat.cast_one, mul_one,
         opow_lt_opow_iff_right one_lt_omega0]
   · refine ⟨?_, fun H ↦ H.fst.oadd _ (NF.below_of_lt' ?_ (ihb.2 H.snd))⟩
     · rw [repr, ihb.1, succ_eq_add_one, succ_eq_add_one, ← add_assoc, repr]
diff --git a/lake-manifest.json b/lake-manifest.json
index 73fb3c8a6883ed..315bcfdf5a8a5e 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,14 +1,14 @@
 {"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/Kha/plausible",
+ [{"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "1e454fed5528d2df0f45708f6b9e8e519c47fc5a",
+   "scope": "leanprover-community",
+   "rev": "293af9b2a383eed4d04d66b898d608d0a44b750f",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "push-nuzuuroszpvz",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "667d80cc94e379283e9f0216673fff456692fa5c",
+   "rev": "61bbab8da0e633e855821f1205fbf99874940b0b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
diff --git a/lean-toolchain b/lean-toolchain
index f4ad0908656808..fc7a4e4137e3ef 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2026-04-20
+leanprover/lean4:nightly-2026-04-27