Skip to content

Commit 2899f15

Browse files
committed
perf(CategoryTheory/Triangulated/TriangleShift): replace cat_disch by faster tactic (#41106)
Replace `cat_disch` with `intros; ext <;> simp` in `Triangle.shiftFunctorAdd'`. See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/116290-rss/topic/Significant.20commits.20to.20mathlib4/near/606901493).
1 parent 0f320b0 commit 2899f15

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/CategoryTheory/Triangulated/TriangleShift.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -111,7 +111,7 @@ noncomputable def Triangle.shiftFunctorAdd' (a b n : ℤ) (h : a + b = n) :
111111
← dsimp% (CategoryTheory.shiftFunctorAdd' C a b (a + b) rfl).hom.naturality_assoc]
112112
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, Int.negOnePow_add,
113113
shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app, add_comm a]))
114-
(by cat_disch)
114+
(by intros; ext <;> simp)
115115

116116
set_option backward.defeqAttrib.useBackward true in
117117
set_option backward.isDefEq.respectTransparency false in

0 commit comments

Comments
 (0)