Speed up inheritance by deprioritizing a duplicate instance

leanprover-community · Dec 12, 2023 · c9faf41 · c9faf41
1 parent 816edcc
commit c9faf41
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/Counterexamples/HomogeneousPrimeNotPrime.lean b/Counterexamples/HomogeneousPrimeNotPrime.lean
@@ -108,8 +108,7 @@ def grading.decompose : R × R →+ DirectSum Two fun i => grading R i where
         Option.casesOn i _ (fun (i_1 : Unit) => PUnit.casesOn i_1 _)) <;> rfl
   map_add' := by
     rintro ⟨a1, b1⟩ ⟨a2, b2⟩
-    -- HACK because `map_add` caused a timeout:
-    rw [add_add_add_comm, ← AddMonoidHom.map_add, ← AddMonoidHom.map_add]
+    rw [add_add_add_comm, ← map_add, ← map_add]
     dsimp only [Prod.mk_add_mk]
     simp_rw [add_sub_add_comm]
     congr

diff --git a/Mathlib/Algebra/Module/LinearMap.lean b/Mathlib/Algebra/Module/LinearMap.lean
@@ -162,6 +162,9 @@ instance (priority := 100) addMonoidHomClass [SemilinearMapClass F σ M M₃] :
         rw [← zero_smul R (0 : M), map_smulₛₗ]
         simp }
 
+-- The following should go via SemilinearMapClass.addMonoidHomClass instead:
+attribute [instance 0] SemilinearMapClass.toAddHomClass
+
 instance (priority := 100) distribMulActionHomClass [LinearMapClass F R M M₂] :
     DistribMulActionHomClass F R M M₂ :=
   { SemilinearMapClass.addMonoidHomClass F with