chore: backport robustness changes from bump/nightly-2026-04-27 (leanprover-community#38597)

See [#nightly-testing > nightly#213 adaptations for nightly-2026-04-27 @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/nightly.23213.20adaptations.20for.20nightly-2026-04-27/near/591262169).

Author: kim-em

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,29 @@ 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/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,51 @@ 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/Monoidal/Free/Coherence.lean

@@ -104,6 +104,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
@@ -185,14 +189,21 @@ 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
@@ -201,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) :
@@ -252,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)
@@ -267,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

@@ -762,7 +762,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