From 892c5c60c686073475dc8776547cf5e776ab90c3 Mon Sep 17 00:00:00 2001 From: Jovan Gerbscheid Date: Wed, 6 May 2026 16:52:44 +0100 Subject: [PATCH] feat: set `dsimp := false` in `@[to_app]` --- Mathlib/Tactic/CategoryTheory/ToApp.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Tactic/CategoryTheory/ToApp.lean b/Mathlib/Tactic/CategoryTheory/ToApp.lean index e38eacbf6b93bb..27e6a1c52de4b9 100644 --- a/Mathlib/Tactic/CategoryTheory/ToApp.lean +++ b/Mathlib/Tactic/CategoryTheory/ToApp.lean @@ -43,7 +43,7 @@ def catAppSimp (e : Expr) : MetaM Simp.Result := ``Cat.leftUnitor_hom_app, ``Cat.leftUnitor_inv_app, ``Cat.rightUnitor_hom_app, ``Cat.rightUnitor_inv_app, ``Cat.associator_hom_app, ``Cat.associator_inv_app, ``eqToHom_refl, ``Category.comp_id, ``Category.id_comp] e - (config := { decide := false }) + (config := { decide := false, dsimp := false }) /-- Given a term of type `∀ ..., η = θ`, where `η θ : f ⟶ g` are 2-morphisms in some bicategory