WIP timeout fixes; should be improved!

leanprover-community · Nov 27, 2023 · 7b66c5d · 7b66c5d
1 parent 59c46b5
commit 7b66c5d
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 1 deletion.
diff --git a/Mathlib/LinearAlgebra/Matrix/Adjugate.lean b/Mathlib/LinearAlgebra/Matrix/Adjugate.lean
@@ -476,6 +476,9 @@ theorem adjugate_mul_distrib_aux (A B : Matrix n n α) (hA : IsLeftRegular A.det
     smul_mul, Matrix.one_mul, mul_smul, mul_adjugate, smul_smul, mul_comm, ← det_mul]
 #align matrix.adjugate_mul_distrib_aux Matrix.adjugate_mul_distrib_aux
 
+-- Reducing this priority fixes a timeout below.
+attribute [instance 50] DistribMulActionHomClass.toAddMonoidHomClass
+
 /-- Proof follows from "The trace Cayley-Hamilton theorem" by Darij Grinberg, Section 5.3
 -/
 theorem adjugate_mul_distrib (A B : Matrix n n α) : adjugate (A * B) = adjugate B * adjugate A := by

diff --git a/Mathlib/RingTheory/IsTensorProduct.lean b/Mathlib/RingTheory/IsTensorProduct.lean
@@ -389,7 +389,9 @@ theorem Algebra.IsPushout.symm (h : Algebra.IsPushout R S R' S') : Algebra.IsPus
     change
       h.1.equiv (TensorProduct.comm R R' S (r • x)) = r • h.1.equiv (TensorProduct.comm R R' S x)
     refine TensorProduct.induction_on x ?_ ?_ ?_
-    · simp only [smul_zero, map_zero]
+    -- Synthesizing the `ZeroHomClass` instances takes a long time, specify them.
+    -- TODO: fix the timeout in a better way!
+    · simp only [smul_zero, AlgEquiv.map_zero, LinearEquiv.map_zero]
     · intro x y
       simp only [smul_tmul', smul_eq_mul, TensorProduct.comm_tmul, smul_def,
         TensorProduct.algebraMap_apply, id.map_eq_id, RingHom.id_apply, TensorProduct.tmul_mul_tmul,

diff --git a/Mathlib/RingTheory/RingHom/Surjective.lean b/Mathlib/RingTheory/RingHom/Surjective.lean
@@ -33,6 +33,9 @@ theorem surjective_respectsIso : RespectsIso surjective := by
   exact e.surjective
 #align ring_hom.surjective_respects_iso RingHom.surjective_respectsIso
 
+-- TODO: this fixes the timeout but is not very principled
+attribute [instance 50] DistribMulActionHomClass.toAddMonoidHomClass
+
 theorem surjective_stableUnderBaseChange : StableUnderBaseChange surjective := by
   refine' StableUnderBaseChange.mk _ surjective_respectsIso _
   classical