chore(GroupTheory/OreLocalization): golf cardinalMk_le_lift_cardinalMk_of_commute using grind (#31284)

Author: euprunin

Mathlib/GroupTheory/OreLocalization/Cardinality.lean

@@ -99,14 +99,7 @@ theorem cardinalMk_le_lift_cardinalMk_of_commute (hc : ∀ s s' : S, Commute s s
   suffices Injective j by
     have := lift_mk_le_lift_mk_of_injective this
     rwa [lift_umax.{v, u}, lift_id', mk_prod, lift_id, lift_mul, mul_eq_self (by simp)] at this
-  intro y y' heq
-  rw [← hi y, ← hi y']
-  simp_rw [j, comp_apply, Prod.ext_iff] at heq
-  simp_rw [i]
-  set x := surjInv hsurj y
-  set x' := surjInv hsurj y'
-  obtain ⟨h1, h2⟩ := heq
-  rw [← h1] at h2 ⊢
-  exact key x.1 x.2 x'.2 h2 (hc _ _)
+  intro
+  grind
 
 end OreLocalization