perf(group_theory/torsion): Speedup torsion_mul_equiv (#18614)

YaelDillies · YaelDillies · commit 1f4705ccdfe1 · 2023-03-18T18:29:34.000Z
From 17s to 0.1s on my gitpod.
diff --git a/src/group_theory/torsion.lean b/src/group_theory/torsion.lean
@@ -239,9 +239,15 @@ variable {G}
 lemma torsion_eq_top (tG : is_torsion G) : torsion G = ⊤ := by ext; tauto
 
 /-- A torsion monoid is isomorphic to its torsion submonoid. -/
-@[to_additive "An additive torsion monoid is isomorphic to its torsion submonoid.", simps]
+@[to_additive "An additive torsion monoid is isomorphic to its torsion submonoid."]
 def torsion_mul_equiv (tG : is_torsion G) : torsion G ≃* G :=
- (mul_equiv.submonoid_congr tG.torsion_eq_top).trans submonoid.top_equiv
+(mul_equiv.submonoid_congr tG.torsion_eq_top).trans submonoid.top_equiv
+
+@[to_additive] lemma torsion_mul_equiv_apply (tG : is_torsion G) (a : torsion G) :
+  tG.torsion_mul_equiv a = mul_equiv.submonoid_congr tG.torsion_eq_top a := rfl
+
+@[to_additive] lemma torsion_mul_equiv_symm_apply_coe (tG : is_torsion G) (a : G) :
+  tG.torsion_mul_equiv.symm a = ⟨submonoid.top_equiv.symm a, tG _⟩ := rfl
 
 end monoid.is_torsion
 
