Refactor OddPrimeOrFour to work with Nat

FltRegular/FltThree/Edwards.lean

@@ -15,7 +15,7 @@ theorem Zsqrtd.associated_norm_of_associated {d : ℤ} {f g : ℤ√d} (h : Asso
   exact associated_mul_unit_right (Zsqrtd.norm f) _ this
 #align zsqrtd.associated_norm_of_associated Zsqrtd.associated_norm_of_associated
 
-theorem OddPrimeOrFour.im_ne_zero {p : ℤ√(-3)} (h : OddPrimeOrFour p.norm)
+theorem OddPrimeOrFour.im_ne_zero {p : ℤ√(-3)} (h : OddPrimeOrFour p.norm.natAbs)
     (hcoprime : IsCoprime p.re p.im) : p.im ≠ 0 :=
   by
   intro H
@@ -24,7 +24,8 @@ theorem OddPrimeOrFour.im_ne_zero {p : ℤ√(-3)} (h : OddPrimeOrFour p.norm)
   · rw [H, isCoprime_zero_right, Int.isUnit_iff_abs_eq] at hcoprime
     rw [← sq_abs, hcoprime] at h
     norm_num at h
-  · exact not_prime_pow one_lt_two.ne' hp
+  · rw [Int.natAbs_pow] at hp
+    exact hp.not_prime_pow le_rfl
 #align odd_prime_or_four.im_ne_zero OddPrimeOrFour.im_ne_zero
 
 theorem Zsqrt3.isUnit_iff {z : ℤ√(-3)} : IsUnit z ↔ abs z.re = 1 ∧ z.im = 0 :=
@@ -52,22 +53,26 @@ theorem Zsqrt3.coe_of_isUnit' {z : ℤ√(-3)} (h : IsUnit z) : ∃ u : ℤ, z =
   · exact Int.isUnit_iff_abs_eq.mp u.isUnit
 #align zsqrt3.coe_of_is_unit' Zsqrt3.coe_of_isUnit'
 
+theorem Zsqrt3.norm_natAbs (a : ℤ√(-3)) : a.norm.natAbs = a.norm := by
+  rw [Int.natAbs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) a)]
+
 theorem OddPrimeOrFour.factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime a.re a.im)
-    (hx : OddPrimeOrFour x) (hfactor : x ∣ a.norm) :
+    (hx : OddPrimeOrFour x.natAbs) (hfactor : x ∣ a.norm) :
     ∃ c : ℤ√(-3), |x| = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0 :=
   by
-  obtain rfl | ⟨hprime, hodd⟩ := hx
+  obtain hx | ⟨hprime, hodd⟩ := hx
   · refine' ⟨⟨1, 1⟩, _, zero_le_one, one_ne_zero⟩
-    simp only [Zsqrtd.norm_def, mul_one, abs_of_pos, zero_lt_four, sub_neg_eq_add]
-    decide
-  · obtain ⟨c, hc⟩ := _root_.factors a x hcoprime hodd hfactor
+    simp only [Zsqrtd.norm_def, mul_one, sub_neg_eq_add, Int.abs_eq_natAbs, hx]
+    norm_num
+  · rw [Int.natAbs_odd] at hodd
+    obtain ⟨c, hc⟩ := _root_.factors a x hcoprime hodd hfactor
     rw [hc]
     apply Zsqrtd.exists c
     intro H
-    rw [Zsqrtd.norm_def, H, MulZeroClass.mul_zero, sub_zero, ← pow_two, eq_comm] at hc
-    have := hprime.abs
-    rw [←hc] at this
-    exact not_prime_pow one_lt_two.ne' this
+    rw [Zsqrtd.norm_def, H, MulZeroClass.mul_zero, sub_zero, ← pow_two, eq_comm, Int.abs_eq_natAbs]
+      at hc
+    rw [Nat.prime_iff_prime_int, ← hc] at hprime
+    exact not_prime_pow one_lt_two.ne' hprime
 #align odd_prime_or_four.factors OddPrimeOrFour.factors
 
 theorem step1a {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (heven : Even a.norm) :
@@ -166,54 +171,63 @@ theorem step2 {a p : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (hdvd : p.norm
 #align step2 step2
 
 theorem step1_2 {a p : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (hdvd : p.norm ∣ a.norm)
-    (hp : OddPrimeOrFour p.norm) (hq : p.im ≠ 0) :
+    (hp : OddPrimeOrFour p.norm.natAbs) (hq : p.im ≠ 0) :
     ∃ u : ℤ√(-3), IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧
     a.norm = p.norm * u.norm := by
   obtain hp | ⟨hpprime, -⟩ := hp
-  · rw [hp] at hdvd⊢
+  · replace hp : p.norm = 4 := by
+      rw [← Zsqrt3.norm_natAbs]
+      norm_cast
+    rw [hp] at hdvd⊢
     have heven : Even a.norm :=
       by
       apply even_iff_two_dvd.mpr (dvd_trans _ hdvd)
       norm_num
     exact step1'' hcoprime hp hq heven
-  · apply step2 hcoprime hdvd hpprime
+  · rw [← Int.prime_iff_natAbs_prime] at hpprime
+    apply step2 hcoprime hdvd hpprime
 #align step1_2 step1_2
 
 theorem OddPrimeOrFour.factors' {a : ℤ√(-3)} (h2 : a.norm ≠ 1) (hcoprime : IsCoprime a.re a.im) :
     ∃ u q : ℤ√(-3),
       0 ≤ q.re ∧
-        q.im ≠ 0 ∧ OddPrimeOrFour q.norm ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm := by
-  have h2 : 2 < a.norm := by
+        q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm :=
+  by
+  have h2 : 2 < a.norm.natAbs := by
+    zify
+    rw [abs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) a)]
     apply lt_of_le_of_ne _ (Spts.not_two _).symm
     rw [← one_mul (2 : ℤ), mul_two, Int.add_one_le_iff]
     apply lt_of_le_of_ne _ h2.symm
     rw [← Int.sub_one_lt_iff, sub_self]
     exact Spts.pos_of_coprime' hcoprime
   obtain ⟨p, hpdvd, hp⟩ := OddPrimeOrFour.exists_and_dvd h2
+  rw [← Int.ofNat_dvd_left] at hpdvd
   obtain ⟨q', hcd, hc, hd⟩ := OddPrimeOrFour.factors a p hcoprime hp hpdvd
-  rw [← abs_dvd, hcd] at hpdvd
-  have hp' := hp.abs
-  rw [hcd] at hp'
-  obtain ⟨u, huvcoprime, huv, huvdvd⟩ := step1_2 hcoprime hpdvd hp' hd
+  rw [Nat.abs_cast, ← Zsqrt3.norm_natAbs, Nat.cast_inj] at hcd
+  rw [hcd] at hpdvd hp
+  rw [Int.natAbs_dvd] at hpdvd
+  obtain ⟨u, huvcoprime, huv, huvdvd⟩ := step1_2 hcoprime hpdvd hp hd
   use u
   cases' huv with huv huv <;> [(use q'); (use star q')] <;>
     simp only [IsCoprime, Zsqrtd.star_re, Zsqrtd.star_im, Ne.def, neg_eq_zero, Zsqrtd.norm_conj] <;>
-    use hc, hd, hp', huv, huvcoprime <;>
-    · rw [huvdvd, lt_mul_iff_one_lt_left (Spts.pos_of_coprime' huvcoprime), ← hcd]
-      exact hp.one_lt_abs
+    use hc, hd, hp, huv, huvcoprime <;>
+    · rw [huvdvd, lt_mul_iff_one_lt_left (Spts.pos_of_coprime' huvcoprime), ← Zsqrt3.norm_natAbs,
+        Nat.one_lt_cast]
+      exact hp.one_lt
 #align odd_prime_or_four.factors' OddPrimeOrFour.factors'
 
 theorem step3 {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) :
     ∃ f : Multiset (ℤ√(-3)),
       (a = f.prod ∨ a = -f.prod) ∧
-        ∀ pq : ℤ√(-3), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm :=
+        ∀ pq : ℤ√(-3), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs :=
   by
   suffices
     ∀ n : ℕ,
       a.norm.natAbs = n →
         ∃ f : Multiset (ℤ√(-3)),
           (a = f.prod ∨ a = -f.prod) ∧
-            ∀ pq : ℤ√(-3), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm
+            ∀ pq : ℤ√(-3), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
     by exact this a.norm.natAbs rfl
   intro n hn
   induction' n using Nat.strong_induction_on with n ih generalizing a
@@ -239,7 +253,7 @@ theorem step3 {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) :
 #align step3 step3
 
 theorem step4_3 {p p' : ℤ√(-3)} (hcoprime : IsCoprime p.re p.im) (hcoprime' : IsCoprime p'.re p'.im)
-    (h : OddPrimeOrFour p.norm) (heq : p.norm = p'.norm) :
+    (h : OddPrimeOrFour p.norm.natAbs) (heq : p.norm = p'.norm) :
     abs p.re = abs p'.re ∧ abs p.im = abs p'.im :=
   by
   have hdvd : p'.norm ∣ p.norm := by rw [heq]
@@ -262,15 +276,22 @@ theorem prod_map_norm {d : ℤ} {s : Multiset (ℤ√d)} :
   Multiset.prod_hom s (Zsqrtd.normMonoidHom : ℤ√d →* ℤ)
 #align prod_map_norm prod_map_norm
 
+theorem prod_map_natAbs {s : Multiset ℤ} :
+    (s.map Int.natAbs).prod = Int.natAbs s.prod :=
+  Multiset.prod_hom s <|
+    ({  toFun := Int.natAbs
+        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)) →
-        (∀ x ∈ g, OddPrimeOrFour (Zsqrtd.norm x)) →
+      (∀ x ∈ f, OddPrimeOrFour (Zsqrtd.norm x).natAbs) →
+        (∀ x ∈ g, OddPrimeOrFour (Zsqrtd.norm x).natAbs) →
           Associated f.prod.norm g.prod.norm →
-            Multiset.Rel Associated (f.map Zsqrtd.norm) (g.map Zsqrtd.norm) :=
+            (f.map (Int.natAbs ∘ Zsqrtd.norm)) = (g.map (Int.natAbs ∘ Zsqrtd.norm)) :=
   by
   intro f g hf hg hassoc
-  apply factors_unique_prod'
+  refine factors_unique_prod' ?_ ?_ ?_
   · intro x hx
     rw [Multiset.mem_map] at hx
     obtain ⟨y, hy, rfl⟩ := hx
@@ -279,7 +300,8 @@ theorem factors_unique_prod :
     rw [Multiset.mem_map] at hx
     obtain ⟨y, hy, rfl⟩ := hx
     exact hg y hy
-  · rwa [prod_map_norm, prod_map_norm]
+  · simp_rw [← Multiset.map_map, prod_map_natAbs, prod_map_norm, ← Int.associated_iff_natAbs]
+    exact hassoc
 #align factors_unique_prod factors_unique_prod
 
 /-- The multiset of factors. -/
@@ -291,7 +313,7 @@ noncomputable def factorization' {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.i
 theorem factorization'_prop {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) :
     (a = (factorization' hcoprime).prod ∨ a = -(factorization' hcoprime).prod) ∧
       ∀ pq : ℤ√(-3),
-        pq ∈ factorization' hcoprime → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm :=
+        pq ∈ factorization' hcoprime → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs :=
   Classical.choose_spec (step3 hcoprime)
 #align factorization'_prop factorization'_prop
 
@@ -369,7 +391,7 @@ theorem associated'_of_abs_eq {x y : ℤ√(-3)} (hre : abs x.re = abs y.re)
 
 theorem associated'_of_associated_norm {x y : ℤ√(-3)}
     (h : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)) (hx : IsCoprime x.re x.im)
-    (hy : IsCoprime y.re y.im) (h' : OddPrimeOrFour x.norm) : Associated' x y :=
+    (hy : IsCoprime y.re y.im) (h' : OddPrimeOrFour x.norm.natAbs) : Associated' x y :=
   by
   have heq : x.norm = y.norm :=
     haveI hd : (-3 : ℤ) ≤ 0 := by norm_num
@@ -378,61 +400,66 @@ theorem associated'_of_associated_norm {x y : ℤ√(-3)}
   exact associated'_of_abs_eq hre him
 #align associated'_of_associated_norm associated'_of_associated_norm
 
-theorem factorization'.associated'_of_norm_eq {a b c : ℤ√(-3)} (h : IsCoprime a.re a.im)
-    (hbmem : b ∈ factorization' h) (hcmem : c ∈ factorization' h) (hnorm : b.norm = c.norm) :
-    Associated' b c := by
+theorem factorization'.associated'_of_norm_associated {a b c : ℤ√(-3)} (h : IsCoprime a.re a.im)
+    (hbmem : b ∈ factorization' h) (hcmem : c ∈ factorization' h)
+    (hnorm : Associated b.norm c.norm) : Associated' b c := by
   apply associated'_of_associated_norm
-  · rw [hnorm]
+  · exact hnorm
   · exact factorization'.coprime_of_mem h hbmem
   · exact factorization'.coprime_of_mem h hcmem
   · exact ((factorization'_prop h).2 b hbmem).2.2
-#align factorization'.associated'_of_norm_eq factorization'.associated'_of_norm_eq
+#align factorization'.associated'_of_norm_eq factorization'.associated'_of_norm_associated
 
-theorem factors_unique {f g : Multiset (ℤ√(-3))} (hf : ∀ x ∈ f, OddPrimeOrFour (Zsqrtd.norm x))
+theorem factors_unique {f g : Multiset (ℤ√(-3))} (hf : ∀ x ∈ f, OddPrimeOrFour (Zsqrtd.norm x).natAbs)
     (hf' : ∀ x ∈ f, IsCoprime (Zsqrtd.re x) (Zsqrtd.im x))
-    (hg : ∀ x ∈ g, OddPrimeOrFour (Zsqrtd.norm x))
+    (hg : ∀ x ∈ g, OddPrimeOrFour (Zsqrtd.norm x).natAbs)
     (hg' : ∀ x ∈ g, IsCoprime (Zsqrtd.re x) (Zsqrtd.im x)) (h : Associated f.prod g.prod) :
     Multiset.Rel Associated' f g :=
   by
   have p :
     ∀ (x : ℤ√(-3)) (_ : x ∈ f) (y : ℤ√(-3)) (_ : y ∈ g),
-      Associated x.norm y.norm → Associated' x y :=
+      (Int.natAbs ∘ Zsqrtd.norm) x = (Int.natAbs ∘ Zsqrtd.norm) y → Associated' x y :=
     by
     intro x hx y hy hxy
+    rw [Function.comp_apply, Function.comp_apply, ← Int.associated_iff_natAbs] at hxy
     apply associated'_of_associated_norm hxy
     · exact hf' x hx
     · exact hg' y hy
     · exact hf x hx
   refine' Multiset.Rel.mono _ p
-  rw [← Multiset.rel_map]
-  apply factors_unique_prod hf hg
-  exact Zsqrtd.associated_norm_of_associated h
+  rw [← Multiset.rel_map, factors_unique_prod hf hg <| Zsqrtd.associated_norm_of_associated h,
+    Multiset.rel_eq]
 #align factors_unique factors_unique
 
 theorem factors_2_even' {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) :
-    Even (evenFactorExp a.norm) :=
+    Even (evenFactorExp a.norm.natAbs) :=
   by
   induction' hn : a.norm.natAbs using Nat.strong_induction_on with n ih generalizing a
-  by_cases hparity : Even a.norm
-  · obtain ⟨u, huvcoprime, huvprod⟩ := step1' hcoprime hparity
+  by_cases hparity : Even a.norm.natAbs
+  · obtain ⟨u, huvcoprime, huvprod⟩ := step1' hcoprime (Int.natAbs_even.mp hparity)
     have huv := Spts.ne_zero_of_coprime' _ huvcoprime
-    rw [huvprod, factors_2_even huv, Nat.even_add]
+    have h₄ : Int.natAbs 4 = 4 := by norm_num; decide
+    rw [← hn, huvprod, Int.natAbs_mul, h₄, factors_2_even (by simpa using huv), Nat.even_add]
     apply iff_of_true even_two
     apply ih _ _ huvcoprime rfl
     rw [← hn, huvprod, Int.natAbs_mul, lt_mul_iff_one_lt_left (Int.natAbs_pos.mpr huv)]
     norm_num; decide
   · convert even_zero (α := ℕ)
     simp only [evenFactorExp, Multiset.count_eq_zero, hn]
     contrapose! hparity with hfactor
-    rw [even_iff_two_dvd]
+    rw [hn, even_iff_two_dvd]
     exact UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors hfactor
 #align factors_2_even' factors_2_even'
 
-theorem factorsOddPrimeOrFour.unique {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) {f : Multiset ℤ}
-    (hf : ∀ x ∈ f, OddPrimeOrFour x) (hf' : ∀ x ∈ f, (0 : ℤ) ≤ x)
-    (hassoc : Associated f.prod a.norm) : f = factorsOddPrimeOrFour a.norm :=
-  factorsOddPrimeOrFour.unique' hf hf' (Spts.pos_of_coprime' hcoprime) (factors_2_even' hcoprime)
-    hassoc
+theorem factorsOddPrimeOrFour.unique {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) {f : Multiset ℕ}
+    (hf : ∀ x ∈ f, OddPrimeOrFour x) (hassoc : f.prod = a.norm.natAbs) :
+    factorsOddPrimeOrFour a.norm.natAbs = f := by
+  rw [← hassoc]
+  refine factorsOddPrimeOrFour.unique' hf ?_ ?_
+  · rw [hassoc, Int.natAbs_pos]
+    exact Spts.ne_zero_of_coprime' _ hcoprime
+  · rw [hassoc]
+    exact factors_2_even' hcoprime
 #align factors_odd_prime_or_four.unique factorsOddPrimeOrFour.unique
 
 theorem eq_or_eq_conj_of_associated_of_re_zero {x A : ℤ√(-3)} (hx : x.re = 0) (h : Associated x A) :
@@ -504,14 +531,14 @@ theorem eq_or_eq_conj_iff_associated'_of_nonneg {x A : ℤ√(-3)} (hx : 0 ≤ x
 theorem step5'
     -- lemma page 54
     (a : ℤ√(-3))
-    (r : ℤ) (hcoprime : IsCoprime a.re a.im) (hcube : r ^ 3 = a.norm) :
+    (r : ℕ) (hcoprime : IsCoprime a.re a.im) (hcube : r ^ 3 = a.norm.natAbs) :
     ∃ g : Multiset (ℤ√(-3)), factorization' hcoprime = 3 • g := by
   classical
     obtain ⟨h1, h2⟩ := factorization'_prop hcoprime
     set f := factorization' hcoprime with hf
     apply Multiset.exists_smul_of_dvd_count
     intro x hx
-    convert dvd_mul_right 3 (Multiset.count (Zsqrtd.norm x) (factorsOddPrimeOrFour r))
+    convert dvd_mul_right 3 (Multiset.count x.norm.natAbs (factorsOddPrimeOrFour r))
     have : Even (evenFactorExp r) :=
       by
       suffices Even (3 * evenFactorExp r)
@@ -524,35 +551,32 @@ theorem step5'
     calc
       Multiset.count x f = Multiset.card (Multiset.filter (x = ·) f) := by
         rw [Multiset.count, Multiset.countP_eq_card_filter]
-      _ = Multiset.card (Multiset.filter (fun a : ℤ√(-3) => x.norm = a.norm) f) :=
+      _ = Multiset.card (Multiset.filter (fun a : ℤ√(-3) => x.norm.natAbs = a.norm.natAbs) f) :=
         (congr_arg _ (Multiset.filter_congr fun A HA => ?_))
-      _ = Multiset.countP (x.norm = ·) (Multiset.map Zsqrtd.norm f) :=
-        (Multiset.countP_map Zsqrtd.norm f (x.norm = ·)).symm
-      _ = Multiset.countP (x.norm = ·) (factorsOddPrimeOrFour a.norm) := ?_
-      _ = Multiset.count x.norm (factorsOddPrimeOrFour a.norm) := by rw [Multiset.count]
-      _ = Multiset.count x.norm (factorsOddPrimeOrFour (r ^ 3)) := by rw [hcube]
-      _ = Multiset.count x.norm (3 • _) := (congr_arg _ <| factorsOddPrimeOrFour.pow _ _ this)
-      _ = 3 * _ := Multiset.count_nsmul x.norm _ _
+      _ = Multiset.countP (x.norm.natAbs = ·) (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f) :=
+        (Multiset.countP_map _ f (x.norm.natAbs = ·)).symm
+      _ = Multiset.countP (x.norm.natAbs = ·) ((factorsOddPrimeOrFour a.norm.natAbs)) := ?_
+      _ = Multiset.count x.norm.natAbs ((factorsOddPrimeOrFour a.norm.natAbs)) := by rw [Multiset.count]
+      _ = Multiset.count x.norm.natAbs ((factorsOddPrimeOrFour (r ^ 3))) := by rw [hcube]
+      _ = Multiset.count x.norm.natAbs (3 • _) := by rw [factorsOddPrimeOrFour.pow _ _ this]
+      _ = 3 * _ := Multiset.count_nsmul x.norm.natAbs _ _
 
     swap
     show
-      Multiset.countP (Eq x.norm) (Multiset.map Zsqrtd.norm f) =
-        Multiset.countP (Eq x.norm) (factorsOddPrimeOrFour a.norm)
-    congr
-    · apply factorsOddPrimeOrFour.unique hcoprime
+      Multiset.countP (Eq x.norm.natAbs) (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f) =
+        Multiset.countP (Eq x.norm.natAbs) ((factorsOddPrimeOrFour a.norm.natAbs))
+    congr 1
+    · rw [factorsOddPrimeOrFour.unique hcoprime]
       · intro x hx
         obtain ⟨y, hy, rfl⟩ := Multiset.mem_map.mp hx
         exact (h2 y hy).2.2
-      · intro x hx
-        obtain ⟨y, -, rfl⟩ := Multiset.mem_map.mp hx
-        apply Zsqrtd.norm_nonneg
-        norm_num
-      · rw [prod_map_norm]
+      · rw [← Multiset.map_map, prod_map_natAbs, prod_map_norm]
         cases' h1 with h1 h1 <;> rw [h1]
         rw [Zsqrtd.norm_neg]
     have h2x := h2 x hx
-    refine' ⟨congr_arg _, fun h => _⟩
-    have hassoc := factorization'.associated'_of_norm_eq hcoprime hx HA h
+    refine' ⟨fun h => by rw [h], fun h => _⟩
+    rw [← Int.associated_iff_natAbs] at h
+    have hassoc := factorization'.associated'_of_norm_associated hcoprime hx HA h
     have eq_or_eq_conj := (eq_or_eq_conj_iff_associated'_of_nonneg h2x.1 (h2 A HA).1).mp hassoc
     refine' eq_or_eq_conj.resolve_right fun H => _
     apply no_conj f
@@ -570,7 +594,7 @@ theorem step5'
 theorem step5
     -- lemma page 54
     (a : ℤ√(-3))
-    (r : ℤ) (hcoprime : IsCoprime a.re a.im) (hcube : r ^ 3 = a.norm) : ∃ p : ℤ√(-3), a = p ^ 3 :=
+    (r : ℕ) (hcoprime : IsCoprime a.re a.im) (hcube : r ^ 3 = a.norm.natAbs) : ∃ p : ℤ√(-3), a = p ^ 3 :=
   by
   obtain ⟨f, hf⟩ := step5' a r hcoprime hcube
   obtain ⟨h1, -⟩ := factorization'_prop hcoprime
@@ -588,11 +612,13 @@ theorem step6 (a b r : ℤ) (hcoprime : IsCoprime a b) (hcube : r ^ 3 = a ^ 2 +
     ∃ p q, a = p ^ 3 - 9 * p * q ^ 2 ∧ b = 3 * p ^ 2 * q - 3 * q ^ 3 :=
   by
   set A : ℤ√(-3) := ⟨a, b⟩ with hA
-  have hcube' : r ^ 3 = A.norm :=
+  have hcube' : r.natAbs ^ 3 = A.norm.natAbs :=
     by
+    rw [← Int.natAbs_pow]
+    apply congr_arg
     simp only [hcube, Zsqrtd.norm_def, hA]
     ring
-  obtain ⟨p, hp⟩ := step5 A r hcoprime hcube'
+  obtain ⟨p, hp⟩ := step5 A r.natAbs hcoprime hcube'
   use p.re, p.im
   simp only [Zsqrtd.ext, pow_succ', pow_two, Zsqrtd.mul_re, Zsqrtd.mul_im] at hp
   convert hp using 2 <;> simp <;> ring