Eq pow prime of unit of congruent

theorem eq_pow_prime_of_unit_of_congruent (u : (𝓞 K)ˣ)    (hcong : ∃ n : ℤ, (p : 𝓞 K) ∣ (u - n : 𝓞 K)) :    ∃ v, u = v ^ p := by  obtain ⟨ζ, hζ⟩ := IsCyclotomicExtension.exists_isPrimitiveRoot ℚ (B := K)    (Set.mem_singleton p) (NeZero.ne p)  obtain ⟨x, hx⟩ : (p : 𝓞 K) ∣ (↑(u ^ (p - 1)) : 𝓞 K) - 1 := by    obtain ⟨n, hn⟩ := hcong    have hn' : (p : ℤ) ∣ n ^ (p - 1) - 1 := by      refine Int.modEq_iff_dvd.mp (Int.ModEq.pow_card_sub_one_eq_one hpri.out ?_).symm      rw [isCoprime_comm, (Nat.prime_iff_prime_int.mp hpri.out).coprime_iff_not_dvd]      intro h      replace h := Int.cast_dvd_cast (α := 𝓞 K) _ _ h      simp only [Int.cast_natCast, ← dvd_iff_dvd_of_dvd_sub hn] at h      refine hζ.zeta_sub_one_prime'.not_unit ((isUnit_pow_iff ?_).mp        (isUnit_of_dvd_unit ((associated_zeta_sub_one_pow_prime _ hζ).dvd.trans h) u.isUnit))      simpa only [ne_eq, tsub_eq_zero_iff_le, not_le] using hpri.out.one_lt    replace hn' := Int.cast_dvd_cast (α := 𝓞 K) _ _ hn'    simp only [Int.cast_natCast, Int.cast_sub, Int.cast_pow, Int.cast_one] at hn'    rw [← Ideal.mem_span_singleton, ← Ideal.Quotient.eq_zero_iff_mem,      RingHom.map_sub, sub_eq_zero] at hn hn' ⊢    rw [Units.val_pow_eq_pow_val, RingHom.map_pow, hn, ← RingHom.map_pow, hn']  have : (hζ.toInteger - 1 : 𝓞 K) ^ p ∣ (↑(u ^ (p - 1)) : 𝓞 K) - 1 := by    rw [hx]    rw [sub_eq_iff_eq_add, add_comm] at hx    have H : Algebra.norm ℤ (1 + p • x) = 1 := norm_add_one_smul_of_isUnit hpri.out      hp x (by rw [nsmul_eq_mul, ← hx]; exact Units.isUnit _)    have := H ▸ zeta_sub_one_pow_dvd_norm_sub_pow hζ x    simpa [ge_iff_le, Int.cast_one, sub_self, nsmul_eq_mul, Nat.cast_mul, PNat.pos,      Nat.cast_pred, zero_sub, IsUnit.mul_iff, ne_eq, tsub_eq_zero_iff_le, not_le, dvd_neg,      Units.isUnit, and_true, zero_add] using this  obtain ⟨v, hv⟩ := exists_pow_eq_of_zeta_sub_one_pow_dvd_sub_one hp hreg hζ this  have hv' : IsIntegral ℤ v :=    IsIntegral.of_pow (NeZero.pos p) (hv ▸ NumberField.RingOfIntegers.isIntegral_coe _)  set w : 𝓞 K := ⟨v, hv'⟩  have : IsUnit w := by    rw [← isUnit_pow_iff (NeZero.pos p).ne.symm]; convert (u ^ (p - 1) : (𝓞 K)ˣ).isUnit; ext    exact hv  have hv'' : this.unit ^ p = u ^ (p - 1) := by    ext; simpa using! hv  use u / this.unit  rw [div_pow, hv'', div_eq_mul_inv, ← pow_sub _ tsub_le_self,    tsub_tsub_cancel_of_le (Nat.Prime.one_lt hpri.out).le, pow_one]