chore(mv_polynomial/equiv): speed up elaboration by adjusting priorit…

…ies (#7840)

`option_equiv_left` timed out several times in bors, since the introduction of non-unital rings. We fix this by adjusting the priority to make sure that the problematic instance is found right away.

Also speed up circumcenter file (which also just timed out in bors) by squeezing simps.

src/data/mv_polynomial/equiv.lean

@@ -259,6 +259,11 @@ def sum_alg_equiv : mv_polynomial (S₁ ⊕ S₂) R ≃ₐ[R]
   end,
   ..sum_ring_equiv R S₁ S₂ }
 
+section
+
+-- this speeds up typeclass search in the lemma below
+local attribute [instance, priority 2000] is_scalar_tower.right
+
 /--
 The algebra isomorphism between multivariable polynomials in `option S₁` and
 polynomials with coefficients in `mv_polynomial S₁ R`.
@@ -269,6 +274,8 @@ def option_equiv_left : mv_polynomial (option S₁) R ≃ₐ[R] polynomial (mv_p
 (sum_alg_equiv R _ _).trans $
 (punit_alg_equiv (mv_polynomial S₁ R)).restrict_scalars R
 
+end
+
 /--
 The algebra isomorphism between multivariable polynomials in `option S₁` and
 multivariable polynomials with coefficients in polynomials.

src/geometry/euclidean/circumcenter.lean

@@ -839,21 +839,21 @@ begin
     r * r - s.circumradius * s.circumradius,
   { rw [dist_comm, ←h₁ 0,
       dist_sq_eq_dist_orthogonal_projection_sq_add_dist_orthogonal_projection_sq p₁ h],
-    simp [h₁', dist_comm p₁] },
+    simp only [h₁', dist_comm p₁, add_sub_cancel', simplex.dist_circumcenter_eq_circumradius] },
   have hd₂ : dist p₂ s.circumcenter * dist p₂ s.circumcenter =
     r * r - s.circumradius * s.circumradius,
   { rw [dist_comm, ←h₂ 0,
       dist_sq_eq_dist_orthogonal_projection_sq_add_dist_orthogonal_projection_sq p₂ h],
-    simp [h₂', dist_comm p₂] },
+    simp only [h₂', dist_comm p₂, add_sub_cancel', simplex.dist_circumcenter_eq_circumradius] },
   rw [←hd₂, hp₁, hp₂, dist_eq_norm_vsub V _ s.circumcenter,
       dist_eq_norm_vsub V _ s.circumcenter, vadd_vsub, vadd_vsub, ←real_inner_self_eq_norm_sq,
       ←real_inner_self_eq_norm_sq, real_inner_smul_left, real_inner_smul_left,
       real_inner_smul_right, real_inner_smul_right, ←mul_assoc, ←mul_assoc] at hd₁,
   by_cases hp : p = orthogonal_projection span_s p,
   { rw [hp₁, hp₂, ←hp],
-    simp },
+    simp only [true_or, eq_self_iff_true, smul_zero, vsub_self] },
   { have hz : ⟪p -ᵥ orthogonal_projection span_s p, p -ᵥ orthogonal_projection span_s p⟫ ≠ 0,
-    { simpa using hp },
+      by simpa only [ne.def, vsub_eq_zero_iff_eq, inner_self_eq_zero] using hp,
     rw [mul_left_inj' hz, mul_self_eq_mul_self_iff] at hd₁,
     rw [hp₁, hp₂],
     cases hd₁,