From 6901db6025feb157f9d0ade9bd65609373942c59 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Sat, 27 Aug 2022 18:04:24 +0000 Subject: [PATCH] chore(category_theory/limits/shapes/finite_products): avoid tidy (#16261) --- src/category_theory/limits/shapes/finite_products.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/category_theory/limits/shapes/finite_products.lean b/src/category_theory/limits/shapes/finite_products.lean index 0e6f79c7a08c2..56e23ddd3b4bf 100644 --- a/src/category_theory/limits/shapes/finite_products.lean +++ b/src/category_theory/limits/shapes/finite_products.lean @@ -47,7 +47,7 @@ instance has_fintype_products [has_finite_products C] (ι : Type w) [fintype ι] has_limits_of_shape (discrete ι) C := has_limits_of_shape_of_equivalence (discrete.equivalence - ((show ulift.{0} (fin (fintype.card ι)) ≃ fin (fintype.card ι), by tidy).trans + (equiv.ulift.{0}.trans (fintype.equiv_fin ι).symm)) /-- We can now write this for powers. -/ @@ -83,7 +83,7 @@ instance has_fintype_coproducts [has_finite_coproducts C] (ι : Type w) [fintype has_colimits_of_shape (discrete ι) C := has_colimits_of_shape_of_equivalence (discrete.equivalence - ((show ulift.{0} (fin (fintype.card ι)) ≃ fin (fintype.card ι), by tidy).trans + (equiv.ulift.{0}.trans (fintype.equiv_fin ι).symm)) /--