perf: change to CommGroup instance on units (#6398)

Fixes a slowdown issue [reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Quotient.20slowdowns/near/382006676). The first declaration in that example (the `Basis` example) takes 268578 to elaborate on master but only 11541 (an order of magnitude better) on this branch, and heartbeats no longer need to be bumped.

Mathlib/Algebra/Group/Units.lean

@@ -198,8 +198,9 @@ attribute [instance] AddUnits.instAddGroupAddUnits
 @[to_additive "Additive units of an additive commutative monoid form
 an additive commutative group."]
 instance {α} [CommMonoid α] : CommGroup αˣ :=
-  { (inferInstance : Group αˣ) with
-    mul_comm := fun _ _ => ext <| mul_comm _ _ }
+  -- note: the original ported file had `{ (inferInstance : Group αˣ) with ... }`
+  -- and this was removed because it was causing slowdowns: see lean4#2387
+  { mul_comm := fun _ _ => ext <| mul_comm _ _ }
 attribute [instance] AddUnits.instAddCommGroupAddUnitsToAddMonoid
 #align units.comm_group Units.instCommGroupUnitsToMonoid
 #align add_units.add_comm_group AddUnits.instAddCommGroupAddUnitsToAddMonoid

Mathlib/RingTheory/ClassGroup.lean

@@ -180,8 +180,6 @@ theorem ClassGroup.induction {P : ClassGroup R → Prop}
     exact h _
 #align class_group.induction ClassGroup.induction
 
--- Porting note: This definition needs a lot of heartbeats to complete even with some help
-set_option maxHeartbeats 600000 in
 /-- The definition of the class group does not depend on the choice of field of fractions. -/
 noncomputable def ClassGroup.equiv :
     ClassGroup R ≃* (FractionalIdeal R⁰ K)ˣ ⧸ (toPrincipalIdeal R K).range := by
@@ -210,8 +208,6 @@ noncomputable def ClassGroup.equiv :
     (Units.mapEquiv (FractionalIdeal.canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv) this
 #align class_group.equiv ClassGroup.equiv
 
--- Porting note: This proof needs a lot of heartbeats to complete
-set_option maxHeartbeats 600000 in
 @[simp]
 theorem ClassGroup.equiv_mk (K' : Type _) [Field K'] [Algebra R K'] [IsFractionRing R K']
     (I : (FractionalIdeal R⁰ K)ˣ) :