better

Author: riccardobrasca

FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean

@@ -374,6 +374,11 @@ theorem unit_inv_conj_not_neg_zeta_runity (h : p ≠ 2) (u : Rˣ) (n : ℕ) (hp
   apply hζ.two_not_mem_one_sub_zeta h
   rw [← Ideal.Quotient.eq_zero_iff_mem, map_two, ← neg_one_eq_one_iff_two_eq_zero, ← hμ', hμ]
 
+-- Add to mathlib
+@[norm_cast]
+lemma NumberField.RingOfIntegers.eq_iff {K : Type*} [Field K] {x y : 𝓞 K} :
+    (x : K) = (y : K) ↔ x = y :=
+  NumberField.RingOfIntegers.ext_iff.symm
 
 -- this proof has mild coe annoyances rn
 theorem unit_inv_conj_is_root_of_unity (h : p ≠ 2) (hp : (p : ℕ).Prime) (u : Rˣ) :
@@ -389,15 +394,14 @@ theorem unit_inv_conj_is_root_of_unity (h : p ≠ 2) (hp : (p : ℕ).Prime) (u :
   have hk := Nat.even_or_odd k
   cases' hk with hk hk
   · simp only [hk.neg_one_pow, one_mul] at hz
-    rw [← map_mul, ← Units.val_mul, ← map_pow, ← Units.val_pow_eq_pow_val,
-      ← NumberField.RingOfIntegers.ext_iff, ← Units.ext_iff] at hz
+    rw [← map_mul, ← Units.val_mul, ← map_pow, ← Units.val_pow_eq_pow_val] at hz
+    norm_cast at hz
     rw [hz]
     refine' (exists_congr fun a => _).mp (zeta_runity_pow_even hζ hpo n)
     · rw [mul_comm]
   · by_contra
     simp only [hk.neg_one_pow, neg_mul, one_mul] at hz
-    rw [← map_mul, ← Units.val_mul, ← map_pow, ←  Units.val_pow_eq_pow_val, ← map_neg,
-      ← NumberField.RingOfIntegers.ext_iff] at hz
+    rw [← map_mul, ← Units.val_mul, ← map_pow, ←  Units.val_pow_eq_pow_val, ← map_neg] at hz
     norm_cast at hz
     simpa [hz] using unit_inv_conj_not_neg_zeta_runity hζ h u n hp
   · apply RingHom.IsIntegralElem.mul