feat: ringOfIntegersEquiv_symm_coe (#31300)

This is upstreamed from the FLT project.

Co-authored-by: bwangpj <70694994+bwangpj@users.noreply.github.com>

Author: bwangpj

Mathlib/NumberTheory/NumberField/Basic.lean

@@ -419,11 +419,15 @@ noncomputable def ringOfIntegersEquiv : 𝓞 ℚ ≃+* ℤ :=
   RingOfIntegers.equiv ℤ
 
 @[simp]
-theorem coe_ringOfIntegersEquiv (z : 𝓞 ℚ) :
+theorem ringOfIntegersEquiv_apply_coe (z : 𝓞 ℚ) :
     (Rat.ringOfIntegersEquiv z : ℚ) = algebraMap (𝓞 ℚ) ℚ z := by
   obtain ⟨z, rfl⟩ := Rat.ringOfIntegersEquiv.symm.surjective z
   simp
 
+theorem ringOfIntegersEquiv_symm_apply_coe (x : ℤ) :
+    (ringOfIntegersEquiv.symm x : ℚ) = ↑x :=
+  eq_intCast ringOfIntegersEquiv.symm _ ▸ rfl
+
 end Rat
 
 namespace AdjoinRoot