remove more stuff

FltRegular/CaseI/Statement.lean

@@ -170,14 +170,13 @@ theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime
   rw [mul_add, mul_comm (↑a : R), ← mul_assoc _ (↑b : R), mul_comm _ (↑b : R), mul_assoc (↑b : R)]
   congr 2
   · ext
-    simp only [Fin.val_mk, map_pow, NumberField.Units.coe_zpow, IsPrimitiveRoot.coe_unit'_coe]
+    simp only [Fin.val_mk, map_pow, NumberField.Units.coe_zpow, ← h]
     refine eq_of_div_eq_one ?_
     rw [← zpow_natCast, ← zpow_sub₀ (hζ'.ne_zero hpri.out.ne_zero), hζ'.zpow_eq_one_iff_dvd]
     simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.intCast_zmod_eq_zero_iff_dvd,
       Int.cast_sub, ZMod.intCast_mod, Int.cast_mul, Int.cast_natCast, sub_self]
   · ext
-    simp only [Fin.val_mk, map_pow, _root_.map_mul, NumberField.Units.coe_zpow,
-      IsPrimitiveRoot.coe_unit'_coe, IsPrimitiveRoot.coe_inv_unit'_coe]
+    simp only [Fin.val_mk, map_pow, _root_.map_mul, NumberField.Units.coe_zpow, map_units_inv, ← h]
     refine eq_of_div_eq_one ?_
     rw [← zpow_natCast, ← zpow_sub_one₀ (hζ'.ne_zero hpri.out.ne_zero), ←
       zpow_sub₀ (hζ'.ne_zero hpri.out.ne_zero), hζ'.zpow_eq_one_iff_dvd]

FltRegular/CaseII/InductionStep.lean

@@ -61,8 +61,8 @@ lemma one_sub_zeta_dvd_zeta_pow_sub : π ∣ x + y * η := by
 lemma div_one_sub_zeta_mem : IsIntegral ℤ ((x + y * η : 𝓞 K) / (ζ - 1)) := by
   obtain ⟨⟨a, ha⟩, e⟩ := one_sub_zeta_dvd_zeta_pow_sub hp hζ e η
   rw [e, mul_comm]
-  simp only [map_mul, NumberField.RingOfIntegers.map_mk, map_sub, IsPrimitiveRoot.coe_unit'_coe,
-    map_one]
+  simp only [map_mul, NumberField.RingOfIntegers.map_mk, map_sub,
+    map_one, show hζ.unit'.1 = ζ from rfl]
   rwa [mul_div_cancel_right₀ _ (hζ.sub_one_ne_zero hpri.out.one_lt)]
 
 /- Make (x+yη)/(ζ-1) into an element of O_K -/
@@ -73,7 +73,8 @@ fun η ↦ ⟨(x + y * η.1) / (ζ - 1), div_one_sub_zeta_mem hp hζ e η⟩
 lemma div_zeta_sub_one_mul_zeta_sub_one (η) :
     div_zeta_sub_one hp hζ e η * (π) = x + y * η := by
   ext
-  simp [div_zeta_sub_one, div_mul_cancel₀ _ (hζ.sub_one_ne_zero hpri.out.one_lt)]
+  simp [show hζ.unit'.1 = ζ from rfl,
+    div_zeta_sub_one, div_mul_cancel₀ _ (hζ.sub_one_ne_zero hpri.out.one_lt)]
 
 /- y is associated to (x+yη₁)/(ζ-1) - (x+yη₂)/(ζ-1) for η₁ ≠ η₂. -/
 lemma div_zeta_sub_one_sub (η₁ η₂) (hη : η₁ ≠ η₂) :

FltRegular/NumberTheory/Cyclotomic/CaseI.lean

@@ -37,8 +37,10 @@ theorem exists_int_sum_eq_zero'_aux (x y i : ℤ) :
     add_right_inj, mul_eq_mul_left_iff, Int.cast_eq_zero]
   simp_rw [NumberField.Units.coe_zpow]
   left
-  push_cast
-  simp only [map_zpow₀, galConj_zeta_runity hζ, inv_zpow', zpow_neg]
+  simp only [map_zpow₀]
+  rw [← inv_zpow]
+  congr
+  exact galConj_zeta_runity hζ
 
 theorem exists_int_sum_eq_zero' (hpodd : p ≠ 2) (hp : (p : ℕ).Prime) (x y i : ℤ) {u : (𝓞 K)ˣ}
     {α : 𝓞 K} (h : (x : 𝓞 K) + y * (hζ.unit' ^ i : (𝓞 K)ˣ) = u * α ^ (p : ℕ)) :

FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean

@@ -31,7 +31,8 @@ lemma norm_Int_zeta_sub_one : Algebra.norm ℤ (↑(IsPrimitiveRoot.unit' hζ) -
   letI := IsCyclotomicExtension.numberField {p} ℚ K
   haveI : Fact (Nat.Prime p) := hpri
   apply RingHom.injective_int (algebraMap ℤ ℚ)
-  simp [Algebra.coe_norm_int, hζ.norm_sub_one_of_prime_ne_two' (cyclotomic.irreducible_rat p.2) hp]
+  simpa [Algebra.coe_norm_int]
+    using hζ.norm_sub_one_of_prime_ne_two' (cyclotomic.irreducible_rat p.2) hp
 
 lemma surjective_of_isCyclotomicExtension_two (R S) [CommRing R] [CommRing S]
     [IsDomain S] [Algebra R S] [IsCyclotomicExtension {2} R S] :
@@ -64,7 +65,7 @@ lemma norm_Int_zeta_sub_one' (hp : p = 2) :
   haveI : Fact (Nat.Prime p) := hpri
   apply RingHom.injective_int (algebraMap ℤ ℚ)
   subst hp
-  simp [Algebra.coe_norm_int, hζ.sub_one_norm_two']
+  simpa [Algebra.coe_norm_int] using hζ.sub_one_norm_two'
 
 lemma associated_zeta_sub_one_pow_prime : Associated ((hζ.unit' - 1 : 𝓞 K) ^ (p - 1 : ℕ)) p := by
   letI := IsCyclotomicExtension.numberField {p} ℚ K

FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean

@@ -27,18 +27,6 @@ def IsPrimitiveRoot.unit' {p : ℕ+} {K : Type _} [Field K] {ζ : K} (hζ : IsPr
   val_inv := Subtype.ext <| mul_inv_cancel <| hζ.ne_zero p.ne_zero
   inv_val := Subtype.ext <| inv_mul_cancel <| hζ.ne_zero p.ne_zero
 
-@[simp, norm_cast]
-theorem IsPrimitiveRoot.coe_unit'_coe {p : ℕ+} {K : Type _} [Field K] {ζ : K}
-  (hζ : IsPrimitiveRoot ζ p) : ↑↑(hζ.unit') = ζ := rfl
-
-@[simp, norm_cast]
-theorem IsPrimitiveRoot.coe_inv_unit'_coe {p : ℕ+} {K : Type _} [Field K] {ζ : K}
-  (hζ : IsPrimitiveRoot ζ p) : ↑↑(hζ.unit'⁻¹) = ζ⁻¹ := rfl
-
-@[simp, norm_cast]
-theorem IsPrimitiveRoot.unit'_val_coe {p : ℕ+} {K : Type u_1} [Field K] {ζ : K}
-  (hζ : IsPrimitiveRoot ζ p) : ↑↑(IsPrimitiveRoot.unit' hζ) = ζ := rfl
-
 set_option quotPrecheck false
 local notation "ζ1" => (hζ.unit' - 1 : 𝓞 K)
 
@@ -249,11 +237,10 @@ theorem roots_of_unity_in_cyclo (hpo : Odd (p : ℕ)) (x : K)
     cases' hxp'' with hxp'' hxp''
     · obtain ⟨i, _, Hi⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one isPrimRoot hxp'' p.prop
       refine' ⟨i, 2, _⟩
-      simp only [IsPrimitiveRoot.unit'_val_coe]
       rw [← Subtype.val_inj] at Hi
-      simp only [SubmonoidClass.coe_pow, IsPrimitiveRoot.unit'_val_coe] at Hi
-      rw [← Hi, show ((2 : ℕ+) : ℕ) = 2 by decide]
-      simp only [even_two, Even.neg_pow, one_pow, one_mul]
+      simp only [SubmonoidClass.coe_pow] at Hi
+      simp only [PNat.val_ofNat, even_two, Even.neg_pow, one_pow, one_mul]
+      rw [← Hi]
       rfl
     · have hone : (-1 : R) ^ (p : ℕ) = (-1 : R) := by apply Odd.neg_one_pow hpo
       have hxp3 : (-1 * ⟨x, hx⟩ : R) ^ (p : ℕ) = 1 := by
@@ -263,10 +250,9 @@ theorem roots_of_unity_in_cyclo (hpo : Odd (p : ℕ)) (x : K)
       refine' ⟨i, 1, _⟩
       simp only [PNat.one_coe, pow_one, neg_mul, one_mul, neg_neg]
       rw [← Subtype.val_inj] at Hi
-      simp only [SubmonoidClass.coe_pow, IsPrimitiveRoot.unit'_val_coe, Submonoid.coe_mul,
+      simp only [SubmonoidClass.coe_pow, Submonoid.coe_mul,
         Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring, InvMemClass.coe_inv,
         OneMemClass.coe_one, neg_mul, one_mul] at Hi
-      simp only [IsPrimitiveRoot.unit'_val_coe]
       exact Iff.mp neg_eq_iff_eq_neg (id (Eq.symm (by simpa using Hi)))
   obtain ⟨m, k, hmk⟩ := H
   refine' ⟨m, k, _⟩
@@ -284,9 +270,10 @@ theorem IsPrimitiveRoot.isPrime_one_sub_zeta [hp : Fact (p : ℕ).Prime] :
   apply_fun (fun x : 𝓞 K => (x : K))
   push_cast
   intro h
-  simp only [map_sub, coe_unit'_coe, map_one, map_zero, sub_eq_zero] at h
   refine hp.1.ne_one (hζ.unique ?_)
-  simp [h]
+  simp only [one_right_iff]
+  simp only [map_sub, map_one, map_zero, sub_eq_zero] at h
+  exact h
 
 theorem IsPrimitiveRoot.two_not_mem_one_sub_zeta [hp : Fact (p : ℕ).Prime] (h : p ≠ 2) :
     (2 : 𝓞 K) ∉ I := by

FltRegular/NumberTheory/Hilbert92.lean

@@ -750,13 +750,6 @@ lemma unit_to_U_map (x : (𝓞 k)ˣ) : mkG (Units.map (algebraMap (𝓞 k) (𝓞
   rw [ofMul_eq_zero, QuotientGroup.eq_one_iff]
   exact ⟨_, rfl⟩
 
-lemma unit_to_U_neg (x) : mkG (-x) = mkG x := by
-  rw [← one_mul x, ← neg_mul, unit_to_U_mul, one_mul, add_left_eq_self]
-  convert unit_to_U_map p hp hKL σ hσ (-1)
-  ext
-  simp only [Units.val_neg, Units.val_one, OneMemClass.coe_one,
-    Units.coe_map, MonoidHom.coe_coe, map_neg, map_one]
-
 instance : CommGroup ((𝓞 k))ˣ := inferInstance
 
 lemma IsPrimitiveRoot.one_left_iff {M} [CommMonoid M] {n : ℕ} :
@@ -857,8 +850,7 @@ lemma Hilbert92ish (hpodd : (p : ℕ) ≠ 2) :
         toMul_ofMul, RingHom.toMonoidHom_eq_coe, zpow_neg, unit_to_U_inv, Function.comp_apply,
         unit_to_U_map, smul_zero, neg_zero, add_zero, add_right_eq_self, NE, η, H2, J, N, H]
       apply_fun mkG at NE_p_pow
-      simp only [RingHom.toMonoidHom_eq_coe, unit_to_U_map,
-        unit_to_U_neg, unit_to_U_pow] at NE_p_pow
+      simp only [RingHom.toMonoidHom_eq_coe, unit_to_U_map, unit_to_U_pow] at NE_p_pow
       rw [eq_comm, smul_eq_zero] at NE_p_pow
       simp only [Nat.cast_eq_zero, PNat.ne_zero, false_or] at NE_p_pow
       rw [NE_p_pow, smul_zero]

FltRegular/NumberTheory/KummersLemma/Field.lean

@@ -77,20 +77,19 @@ lemma map_poly : (poly hp hζ u hcong).map (algebraMap (𝓞 K) K) =
     (((C ((algebraMap ((𝓞 K)) K) ↑hζ.unit') - 1) * X - 1) ^ (p : ℕ)).coeff i +
     (C ((algebraMap ((𝓞 K)) K) ↑u)).coeff i := by
       simp only [map_pow, map_sub, map_one, Polynomial.map_add, Polynomial.map_pow,
-        Polynomial.map_sub, Polynomial.map_mul, map_C, IsPrimitiveRoot.coe_unit'_coe,
+        Polynomial.map_sub, Polynomial.map_mul, map_C,
         Polynomial.map_one, map_X, coeff_add] at this
       convert this
       simp only [NumberField.RingOfIntegers.coe_eq_algebraMap, ← Polynomial.coeff_map]
       simp only [coeff_map, Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_sub, map_C,
-        IsPrimitiveRoot.coe_unit'_coe, Polynomial.map_one]
+        Polynomial.map_one]
       rw [← Polynomial.coeff_map, mul_comm, ← Polynomial.coeff_mul_C, mul_comm]
-      simp
+      simp [show hζ.unit'.1 = ζ from rfl]
   apply mul_right_injective₀ (pow_ne_zero p (hζ.sub_one_ne_zero hpri.out.one_lt))
   simp only [Subalgebra.algebraMap_eq, Algebra.id.map_eq_id, RingHomCompTriple.comp_eq, coeff_map,
     RingHom.coe_coe, Subalgebra.coe_val, one_div, map_sub, map_one, coeff_add, coeff_sub,
-    PNat.pos, pow_eq_zero_iff, this, mul_add, IsPrimitiveRoot.val_unit'_coe,
-    IsPrimitiveRoot.coe_unit'_coe]
-  simp_rw [← smul_eq_mul K, ← coeff_smul]
+    PNat.pos, pow_eq_zero_iff, this, mul_add, IsPrimitiveRoot.val_unit'_coe]
+  simp_rw [← smul_eq_mul K, ← coeff_smul, show hζ.unit'.1 = ζ from rfl]
   rw [smul_C, smul_eq_mul, ← smul_pow, ← mul_div_assoc, mul_div_cancel_left₀, smul_sub, smul_C,
     smul_eq_mul, mul_inv_cancel, map_one, Algebra.smul_def, ← C_eq_algebraMap, map_sub, map_one]
   · exact hζ.sub_one_ne_zero hpri.out.one_lt