more cleanup

FltRegular/CaseII/AuxLemmas.lean

@@ -44,11 +44,6 @@ lemma WfDvdMonoid.multiplicity_finite_iff {M : Type*} [CancelCommMonoidWithZero
   · intro ⟨hx, hy⟩
     exact WfDvdMonoid.multiplicity_finite hx hy
 
-lemma WfDvdMonoid.multiplicity_eq_top_iff {M : Type*} [CancelCommMonoidWithZero M] [WfDvdMonoid M]
-    [DecidableRel (fun a b : M ↦ a ∣ b)] {x y : M} :
-    multiplicity x y = ⊤ ↔ IsUnit x ∨ y = 0 := by
-  rw [multiplicity.eq_top_iff_not_finite, WfDvdMonoid.multiplicity_finite_iff, or_iff_not_and_not]
-
 lemma dvd_iff_multiplicity_le {M : Type*}
     [CancelCommMonoidWithZero M] [DecidableRel (fun a b : M ↦ a ∣ b)] [UniqueFactorizationMonoid M]
     {a b : M} (ha : a ≠ 0) : a ∣ b ↔ ∀ p : M, Prime p → multiplicity p a ≤ multiplicity p b := by

FltRegular/FltThree/Edwards.lean

@@ -260,26 +260,6 @@ theorem prod_map_natAbs {s : Multiset ℤ} :
         map_one' := rfl
         map_mul' := fun x y => Int.natAbs_mul x y } : ℤ →* ℕ)
 
-theorem factors_unique_prod :
-    ∀ {f g : Multiset (ℤ√(-3))},
-      (∀ x ∈ f, OddPrimeOrFour (Zsqrtd.norm x).natAbs) →
-        (∀ x ∈ g, OddPrimeOrFour (Zsqrtd.norm x).natAbs) →
-          Associated f.prod.norm g.prod.norm →
-            (f.map (Int.natAbs ∘ Zsqrtd.norm)) = (g.map (Int.natAbs ∘ Zsqrtd.norm)) :=
-  by
-  intro f g hf hg hassoc
-  refine factors_unique_prod' ?_ ?_ ?_
-  · intro x hx
-    rw [Multiset.mem_map] at hx
-    obtain ⟨y, hy, rfl⟩ := hx
-    exact hf y hy
-  · intro x hx
-    rw [Multiset.mem_map] at hx
-    obtain ⟨y, hy, rfl⟩ := hx
-    exact hg y hy
-  · simp_rw [← Multiset.map_map, prod_map_natAbs, prod_map_norm, ← Int.associated_iff_natAbs]
-    exact hassoc
-
 /-- The multiset of factors. -/
 noncomputable def factorization' {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) :
     Multiset (ℤ√(-3)) :=

FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean

@@ -127,8 +127,6 @@ theorem prime_isUnit_mul {a b : α} (h : IsUnit a) : Prime (a * b) ↔ Prime b :
   let ⟨a, ha⟩ := h
   ha ▸ prime_units_mul a b
 
-theorem prime_mul_units (a : αˣ) (b : α) : Prime (b * ↑a) ↔ Prime b := by simp [Prime]
-
 theorem prime_neg_iff {α} [CommRing α] {a : α} : Prime (-a) ↔ Prime a := by
   rw [← prime_isUnit_mul isUnit_one.neg, neg_mul, one_mul, neg_neg]
 

FltRegular/NumberTheory/Hilbert92.lean

@@ -451,13 +451,6 @@ def unitlifts (S : systemOfUnits p G (NumberField.Units.rank k + 1))  :
     Fin (NumberField.Units.rank k + 1) → Additive (𝓞 K)ˣ :=
   fun i ↦ Additive.ofMul (Additive.toMul (S.units i).out').out'
 
-lemma norm_map_inv (z : K) : Algebra.norm k z⁻¹ = (Algebra.norm k z)⁻¹ := by
-    by_cases h : z = 0
-    rw [h]
-    simp
-    apply eq_inv_of_mul_eq_one_left
-    rw [← map_mul, inv_mul_cancel h, map_one]
-
 lemma unitlifts_spec (S : systemOfUnits p G (NumberField.Units.rank k + 1)) (i) :
     mkG (Additive.toMul <| unitlifts p hp hKL σ hσ S i) = S.units i := by
   delta unit_to_U unitlifts
@@ -680,8 +673,7 @@ lemma Hilbert92ish_aux1 (n : ℕ) (H : Fin n → Additive (𝓞 K)ˣ) (ζ : (
   have hcoe : ((algebraMap (𝓞 K) K) ((algebraMap (𝓞 k) (𝓞 K)) ((ζ ^ a)⁻¹).1)) =
     algebraMap (𝓞 k) (𝓞 K) ((ζ ^ a)⁻¹).1 := rfl
   simp only [toMul_sum, toMul_zsmul, zpow_neg, Units.val_mul, Units.coe_prod, map_mul, map_prod,
-    Units.coe_zpow, map_mul, map_prod, norm_map_inv, norm_map_zpow,
-    Units.coe_map]
+    Units.coe_zpow, map_mul, map_prod, norm_map_zpow, Units.coe_map]
   rw [← map_zpow, Units.coe_map_inv]
   simp only [RingHom.toMonoidHom_eq_coe, MonoidHom.coe_coe]
   have hcoe1 :