From 65a410c37d5ea9bbe7f4316253268e301ef6644d Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 4 Mar 2022 23:42:08 -0600
Subject: [PATCH 01/54] initial commit

---
 src/number_theory/padics/padic_norm.lean | 186 ++++++++++++++++-------
 src/ring_theory/int/basic.lean           |   2 +-
 src/ring_theory/multiplicity.lean        |  22 ++-
 3 files changed, 150 insertions(+), 60 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index b1f8c636bc860..381d686f5bbe1 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -51,6 +51,84 @@ open_locale rat
 
 open multiplicity
 
+def padic_val_nat (p : ℕ) (n : ℕ) : ℕ :=
+if h : p ≠ 1 ∧ n ≠ 0
+then (multiplicity p n).get (multiplicity.finite_nat_iff.2 h)
+else 0
+
+namespace padic_val_nat
+open multiplicity
+variables {p : ℕ}
+
+/--
+`padic_val_nat p 0` is 0 for any `p`.
+-/
+@[simp]
+protected lemma zero : padic_val_nat p 0 = 0 :=
+begin
+  unfold padic_val_nat,
+  simp,
+end
+
+/--
+`padic_val_nat p 1` is 0 for any `p`.
+-/
+@[simp] protected lemma one : padic_val_nat p 1 = 0 :=
+by unfold padic_val_nat; split_ifs; simp *
+
+/--
+For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1.
+-/
+@[simp] lemma self (hp : 1 < p) : padic_val_nat p p = 1 :=
+by {
+  have h := (ne_of_lt hp).symm,
+  have h2 : (¬ p = 1) ↔ true, exact iff_of_true h trivial,
+  have : 0 < p := trans zero_lt_one hp,
+  have h3 := (ne_of_lt this).symm,
+  have h4 : (p = 0) ↔ false, exact iff_false_intro h3,
+  simp [padic_val_nat],
+  rw [h2, h4],
+  simp,
+  }
+
+end padic_val_nat
+
+def padic_val_int (p : ℕ) (z : ℤ) : ℕ :=
+padic_val_nat p (z.nat_abs)
+
+namespace padic_val_int
+open multiplicity
+variables {p : ℕ}
+
+/--
+`padic_val_int p 0` is 0 for any `p`.
+-/
+@[simp]
+protected lemma zero : padic_val_int p 0 = 0 :=
+begin
+  unfold padic_val_int,
+  simp,
+end
+
+/--
+`padic_val_int p 1` is 0 for any `p`.
+-/
+@[simp] protected lemma one : padic_val_int p 1 = 0 :=
+by simp [padic_val_int]
+
+-- @[simp] lemma nat_abs (z : ℤ) : padic_val_nat p z.nat_abs = padic_val_int p z :=
+-- by simp [padic_val_int]
+
+/--
+For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1.
+-/
+@[simp] lemma self (hp : 1 < p) : padic_val_int p p = 1 :=
+by {simp [padic_val_int, padic_val_nat.self hp], }
+
+
+
+end padic_val_int
+
 /--
 For `p ≠ 1`, the p-adic valuation of an integer `z ≠ 0` is the largest natural number `n` such that
 p^n divides z.
@@ -60,21 +138,16 @@ valuation of `q.denom`.
 If `q = 0` or `p = 1`, then `padic_val_rat p q` defaults to 0.
 -/
 def padic_val_rat (p : ℕ) (q : ℚ) : ℤ :=
-if h : q ≠ 0 ∧ p ≠ 1
-then (multiplicity (p : ℤ) q.num).get
-    (multiplicity.finite_int_iff.2 ⟨h.2, rat.num_ne_zero_of_ne_zero h.1⟩) -
-  (multiplicity (p : ℤ) q.denom).get
-    (multiplicity.finite_int_iff.2 ⟨h.2, by exact_mod_cast rat.denom_ne_zero _⟩)
-else 0
+padic_val_int p q.num - padic_val_nat p q.denom
 
-/--
-A simplification of the definition of `padic_val_rat p q` when `q ≠ 0` and `p` is prime.
--/
-lemma padic_val_rat_def (p : ℕ) [hp : fact p.prime] {q : ℚ} (hq : q ≠ 0) : padic_val_rat p q =
-  (multiplicity (p : ℤ) q.num).get (finite_int_iff.2 ⟨hp.1.ne_one, rat.num_ne_zero_of_ne_zero hq⟩) -
-  (multiplicity (p : ℤ) q.denom).get
-    (finite_int_iff.2 ⟨hp.1.ne_one, by exact_mod_cast rat.denom_ne_zero _⟩) :=
-dif_pos ⟨hq, hp.1.ne_one⟩
+-- /--
+-- A simplification of the definition of `padic_val_rat p q` when `q ≠ 0` and `p` is prime.
+-- -/
+-- lemma padic_val_rat_def (p : ℕ) [hp : fact p.prime] {q : ℚ} (hq : q ≠ 0) : padic_val_rat p q =
+--   (multiplicity (p : ℤ) q.num).get (finite_int_iff.2 ⟨hp.1.ne_one, rat.num_ne_zero_of_ne_zero hq⟩) -
+--   (multiplicity (p : ℤ) q.denom).get
+--     (finite_int_iff.2 ⟨hp.1.ne_one, by exact_mod_cast rat.denom_ne_zero _⟩) :=
+-- dif_pos ⟨hq, hp.1.ne_one⟩
 
 namespace padic_val_rat
 open multiplicity
@@ -84,32 +157,28 @@ variables {p : ℕ}
 `padic_val_rat p q` is symmetric in `q`.
 -/
 @[simp] protected lemma neg (q : ℚ) : padic_val_rat p (-q) = padic_val_rat p q :=
-begin
-  unfold padic_val_rat,
-  split_ifs,
-  { simp [-add_comm]; refl },
-  { exfalso, simp * at * },
-  { exfalso, simp * at * },
-  { refl }
-end
+by simp [padic_val_rat, padic_val_int]
 
 /--
 `padic_val_rat p 0` is 0 for any `p`.
 -/
 @[simp]
-protected lemma zero (m : nat) : padic_val_rat m 0 = 0 := rfl
+protected lemma zero (m : nat) : padic_val_rat m 0 = 0 := by simp [padic_val_rat, padic_val_int]
 
 /--
 `padic_val_rat p 1` is 0 for any `p`.
 -/
-@[simp] protected lemma one : padic_val_rat p 1 = 0 :=
-by unfold padic_val_rat; split_ifs; simp *
+@[simp] protected lemma one : padic_val_rat p 1 = 0 := by simp [padic_val_rat, padic_val_int]
 
 /--
 For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1.
 -/
 @[simp] lemma padic_val_rat_self (hp : 1 < p) : padic_val_rat p p = 1 :=
-by unfold padic_val_rat; split_ifs; simp [*, nat.one_lt_iff_ne_zero_and_ne_one] at *
+by {simp [padic_val_rat, padic_val_int],
+    rw padic_val_nat.self hp, -- why doesn't this simp trigger
+    dec_trivial, }
+
+lemma nat_abs_or (z : ℤ) : (z.nat_abs : ℤ) = z ∨ (z.nat_abs : ℤ) = (-z) := by sorry
 
 /--
 The p-adic value of an integer `z ≠ 0` is the multiplicity of `p` in `z`.
@@ -117,16 +186,22 @@ The p-adic value of an integer `z ≠ 0` is the multiplicity of `p` in `z`.
 lemma padic_val_rat_of_int (z : ℤ) (hp : p ≠ 1) (hz : z ≠ 0) :
   padic_val_rat p (z : ℚ) = (multiplicity (p : ℤ) z).get
     (finite_int_iff.2 ⟨hp, hz⟩) :=
-by rw [padic_val_rat, dif_pos]; simp *; refl
+by {
+  rw [padic_val_rat, padic_val_int, padic_val_nat, padic_val_nat, dif_pos, dif_pos],
+  simp_rw multiplicity.int.nat_abs,
+  simp only [rat.coe_int_denom,
+ int.coe_nat_zero,
+ rat.coe_int_num,
+ int.coe_nat_inj',
+ sub_zero,
+ multiplicity.get_one_right],
+ refl,
+ simp [hp],
+ simp [hp, hz],
+  }
 
 end padic_val_rat
 
-/--
-A convenience function for the case of `padic_val_rat` when both inputs are natural numbers.
--/
-def padic_val_nat (p : ℕ) (n : ℕ) : ℕ :=
-int.to_nat (padic_val_rat p n)
-
 section padic_val_nat
 
 /--
@@ -135,10 +210,8 @@ this lemma ensures that the cast is well-behaved.
 -/
 lemma zero_le_padic_val_rat_of_nat (p n : ℕ) : 0 ≤ padic_val_rat p n :=
 begin
-  unfold padic_val_rat,
-  split_ifs,
-  { simp, },
-  { trivial, },
+  unfold padic_val_rat padic_val_int padic_val_nat,
+  split_ifs; simp,
 end
 
 /--
@@ -147,8 +220,8 @@ end
 @[simp, norm_cast] lemma padic_val_rat_of_nat (p n : ℕ) :
   ↑(padic_val_nat p n) = padic_val_rat p n :=
 begin
-  unfold padic_val_nat,
-  rw int.to_nat_of_nonneg (zero_le_padic_val_rat_of_nat p n),
+  unfold padic_val_rat padic_val_int,
+  simp,
 end
 
 /--
@@ -157,16 +230,13 @@ A simplification of `padic_val_nat` when one input is prime, by analogy with `pa
 lemma padic_val_nat_def {p : ℕ} [hp : fact p.prime] {n : ℕ} (hn : n ≠ 0) :
   padic_val_nat p n =
   (multiplicity p n).get
-    (multiplicity.finite_nat_iff.2 ⟨nat.prime.ne_one hp.1, bot_lt_iff_ne_bot.mpr hn⟩) :=
+    (multiplicity.finite_nat_iff.2 ⟨nat.prime.ne_one hp.1, hn⟩) :=
 begin
-  have n_nonzero : (n : ℚ) ≠ 0, by simpa only [cast_eq_zero, ne.def],
-  -- Infinite loop with @simp padic_val_rat_of_nat unless we restrict the available lemmas here,
-  -- hence the very long list
-  simpa only
-    [ int.coe_nat_multiplicity p n, rat.coe_nat_denom n, (padic_val_rat_of_nat p n).symm,
-      int.coe_nat_zero, int.coe_nat_inj', sub_zero, get_one_right, int.coe_nat_succ, zero_add,
-      rat.coe_nat_num ]
-    using padic_val_rat_def p n_nonzero,
+  simp [padic_val_nat],
+  split_ifs,
+  refl,
+  exfalso,
+  apply h ⟨(hp.out).ne_one, hn⟩,
 end
 
 @[simp] lemma padic_val_nat_self (p : ℕ) [fact p.prime] : padic_val_nat p p = 1 :=
@@ -185,12 +255,6 @@ begin
   solve_by_elim,
 end
 
-@[simp]
-lemma padic_val_nat_zero (m : nat) : padic_val_nat m 0 = 0 := rfl
-
-@[simp]
-lemma padic_val_nat_one (m : nat) : padic_val_nat m 1 = 0 := by simp [padic_val_nat]
-
 end padic_val_nat
 
 namespace padic_val_rat
@@ -215,9 +279,16 @@ protected lemma defn {q : ℚ} {n d : ℤ} (hqz : q ≠ 0) (qdf : q = n /. d) :
 have hn : n ≠ 0, from rat.mk_num_ne_zero_of_ne_zero hqz qdf,
 have hd : d ≠ 0, from rat.mk_denom_ne_zero_of_ne_zero hqz qdf,
 let ⟨c, hc1, hc2⟩ := rat.num_denom_mk hn hd qdf in
-by rw [padic_val_rat, dif_pos];
+begin
   simp [hc1, hc2, multiplicity.mul' (nat.prime_iff_prime_int.1 p_prime.1),
-    (ne.symm (ne_of_lt p_prime.1.one_lt)), hqz]
+    (ne.symm (ne_of_lt p_prime.1.one_lt)), hqz],
+  rw [padic_val_rat, padic_val_int, padic_val_nat, padic_val_nat, dif_pos, dif_pos],
+  simp_rw [int.coe_nat_multiplicity p q.denom],
+  simp_rw multiplicity.int.nat_abs,
+  refl,
+  sorry,
+  sorry,
+end
 
 /--
 A rewrite lemma for `padic_val_rat p (q * r)` with conditions `q ≠ 0`, `r ≠ 0`.
@@ -446,7 +517,8 @@ begin
     rw padic_val_nat_def (ne_of_gt hn),
     { rw [nat.cast_add, enat.coe_get],
       simp only [nat.cast_one, not_le],
-      apply enat.lt_add_one (ne_top_iff_finite.2 (finite_nat_iff.2 ⟨hp.elim.ne_one, hn⟩)) },
+      exact enat.lt_add_one (ne_top_iff_finite.mpr
+        (finite_nat_iff.mpr ⟨(fact.elim hp).ne_one, (ne_of_lt hn).symm⟩)), },
     { apply_instance } }
 end
 
diff --git a/src/ring_theory/int/basic.lean b/src/ring_theory/int/basic.lean
index fbd3891627807..82f2a1e3e020e 100644
--- a/src/ring_theory/int/basic.lean
+++ b/src/ring_theory/int/basic.lean
@@ -294,7 +294,7 @@ lemma finite_int_iff_nat_abs_finite {a b : ℤ} : finite a b ↔ finite a.nat_ab
 by simp only [finite_def, ← int.nat_abs_dvd_iff_dvd, int.nat_abs_pow]
 
 lemma finite_int_iff {a b : ℤ} : finite a b ↔ (a.nat_abs ≠ 1 ∧ b ≠ 0) :=
-by rw [finite_int_iff_nat_abs_finite, finite_nat_iff, pos_iff_ne_zero, int.nat_abs_ne_zero]
+by rw [finite_int_iff_nat_abs_finite, finite_nat_iff, int.nat_abs_ne_zero]
 
 instance decidable_nat : decidable_rel (λ a b : ℕ, (multiplicity a b).dom) :=
 λ a b, decidable_of_iff _ finite_nat_iff.symm
diff --git a/src/ring_theory/multiplicity.lean b/src/ring_theory/multiplicity.lean
index 382a633783e6f..54247066b6e67 100644
--- a/src/ring_theory/multiplicity.lean
+++ b/src/ring_theory/multiplicity.lean
@@ -57,6 +57,24 @@ begin
     apply _root_.le_antisymm; { apply nat.find_mono, norm_cast, simp } }
 end
 
+example (a b : ℤ) : a ∣ b ↔ a ∣ b.nat_abs := int.dvd_nat_abs.symm
+
+theorem quoi (a b : ℕ) :
+    multiplicity a (b : ℤ).nat_abs = multiplicity (a : ℤ) (b : ℤ) :=
+begin
+  apply part.ext',
+  { repeat { rw [← finite_iff_dom, finite_def] },
+    norm_cast },
+  { intros h1 h2,
+    apply _root_.le_antisymm; { apply nat.find_mono, norm_cast, simp } }
+end
+
+theorem int.nat_abs (a : ℕ) (b : ℤ) :
+    multiplicity a b.nat_abs = multiplicity (a : ℤ) b :=
+begin
+  sorry,
+end
+
 lemma not_finite_iff_forall {a b : α} : (¬ finite a b) ↔ ∀ n : ℕ, a ^ n ∣ b :=
 ⟨λ h n, nat.cases_on n (by { rw pow_zero, exact one_dvd _ }) (by simpa [finite, not_not] using h),
   by simp [finite, multiplicity, not_not]; tauto⟩
@@ -224,9 +242,9 @@ lemma dvd_iff_multiplicity_pos {a b : α} : (0 : enat) < multiplicity a b ↔ a
       by simpa only [heq, nat.cast_zero] using enat.coe_lt_coe.mpr zero_lt_one)
     (by rwa pow_one a))⟩
 
-lemma finite_nat_iff {a b : ℕ} : finite a b ↔ (a ≠ 1 ∧ 0 < b) :=
+lemma finite_nat_iff {a b : ℕ} : finite a b ↔ (a ≠ 1 ∧ b ≠ 0) :=
 begin
-  rw [← not_iff_not, not_finite_iff_forall, not_and_distrib, ne.def,
+  rw [←pos_iff_ne_zero, ← not_iff_not, not_finite_iff_forall, not_and_distrib, ne.def,
     not_not, not_lt, nat.le_zero_iff],
   exact ⟨λ h, or_iff_not_imp_right.2 (λ hb,
     have ha : a ≠ 0, from λ ha, by simpa [ha] using h 1,

From 3b759114c8c02ad6cafe5e2c0b7c8d5aa467f0bf Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Wed, 9 Mar 2022 19:41:04 -0600
Subject: [PATCH 02/54] remove unused lemma

---
 src/number_theory/padics/padic_norm.lean | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 381d686f5bbe1..45de2ea454a47 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -178,8 +178,6 @@ by {simp [padic_val_rat, padic_val_int],
     rw padic_val_nat.self hp, -- why doesn't this simp trigger
     dec_trivial, }
 
-lemma nat_abs_or (z : ℤ) : (z.nat_abs : ℤ) = z ∨ (z.nat_abs : ℤ) = (-z) := by sorry
-
 /--
 The p-adic value of an integer `z ≠ 0` is the multiplicity of `p` in `z`.
 -/
@@ -286,8 +284,19 @@ begin
   simp_rw [int.coe_nat_multiplicity p q.denom],
   simp_rw multiplicity.int.nat_abs,
   refl,
-  sorry,
-  sorry,
+  split,
+  { exact nat.prime.ne_one p_prime.out, },
+  { intro hq,
+    rw hq at hc2,
+    simp at hc2,
+    exact hd hc2, },
+  split,
+  { exact nat.prime.ne_one p_prime.out, },
+  { intro hq,
+    simp at hq,
+    rw hq at hc1,
+    simp at hc1,
+    exact hn hc1, },
 end
 
 /--

From c578361e1b83bdd7d62247ea4da385a50528769e Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Wed, 9 Mar 2022 19:57:55 -0600
Subject: [PATCH 03/54] fix lemma

---
 src/ring_theory/multiplicity.lean | 21 ++++++++++++++-------
 1 file changed, 14 insertions(+), 7 deletions(-)

diff --git a/src/ring_theory/multiplicity.lean b/src/ring_theory/multiplicity.lean
index 54247066b6e67..bb2bcf1709679 100644
--- a/src/ring_theory/multiplicity.lean
+++ b/src/ring_theory/multiplicity.lean
@@ -59,7 +59,7 @@ end
 
 example (a b : ℤ) : a ∣ b ↔ a ∣ b.nat_abs := int.dvd_nat_abs.symm
 
-theorem quoi (a b : ℕ) :
+theorem nat_cast_nat_abs (a b : ℕ) :
     multiplicity a (b : ℤ).nat_abs = multiplicity (a : ℤ) (b : ℤ) :=
 begin
   apply part.ext',
@@ -69,12 +69,6 @@ begin
     apply _root_.le_antisymm; { apply nat.find_mono, norm_cast, simp } }
 end
 
-theorem int.nat_abs (a : ℕ) (b : ℤ) :
-    multiplicity a b.nat_abs = multiplicity (a : ℤ) b :=
-begin
-  sorry,
-end
-
 lemma not_finite_iff_forall {a b : α} : (¬ finite a b) ↔ ∀ n : ℕ, a ^ n ∣ b :=
 ⟨λ h n, nat.cases_on n (by { rw pow_zero, exact one_dvd _ }) (by simpa [finite, not_not] using h),
   by simp [finite, multiplicity, not_not]; tauto⟩
@@ -305,6 +299,19 @@ part.ext' (by simp only [multiplicity, enat.find, dvd_neg])
     eq.symm (unique ((dvd_neg _ _).2 (pow_multiplicity_dvd _))
       (mt (dvd_neg _ _).1 (is_greatest' _ (lt_succ_self _))))))
 
+theorem int.nat_abs (a : ℕ) (b : ℤ) :
+    multiplicity a b.nat_abs = multiplicity (a : ℤ) b :=
+begin
+  have h := @int.nat_abs_eq_iff b b.nat_abs,
+  simp only [true_iff, eq_self_iff_true] at h,
+  cases h,
+  { conv_rhs { rw h },
+   apply nat_cast_nat_abs, },
+  { conv_rhs { rw h },
+    rw multiplicity.neg,
+    apply nat_cast_nat_abs, },
+end
+
 lemma multiplicity_add_of_gt {p a b : α} (h : multiplicity p b < multiplicity p a) :
   multiplicity p (a + b) = multiplicity p b :=
 begin

From 24fe9a64854553b50f24d4f97be2e5f603506516 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Wed, 9 Mar 2022 20:10:12 -0600
Subject: [PATCH 04/54] golfing

---
 src/number_theory/padics/padic_norm.lean | 47 ++++++++----------------
 1 file changed, 16 insertions(+), 31 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 45de2ea454a47..fdad70291b959 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -80,16 +80,13 @@ by unfold padic_val_nat; split_ifs; simp *
 For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1.
 -/
 @[simp] lemma self (hp : 1 < p) : padic_val_nat p p = 1 :=
-by {
-  have h := (ne_of_lt hp).symm,
-  have h2 : (¬ p = 1) ↔ true, exact iff_of_true h trivial,
-  have : 0 < p := trans zero_lt_one hp,
-  have h3 := (ne_of_lt this).symm,
-  have h4 : (p = 0) ↔ false, exact iff_false_intro h3,
-  simp [padic_val_nat],
-  rw [h2, h4],
-  simp,
-  }
+begin
+  have neq_one : (¬ p = 1) ↔ true,
+  { exact iff_of_true ((ne_of_lt hp).symm) trivial, },
+  have eq_zero_false : (p = 0) ↔ false,
+  { exact iff_false_intro ((ne_of_lt (trans zero_lt_one hp)).symm) },
+  simp [padic_val_nat, neq_one, eq_zero_false],
+end
 
 end padic_val_nat
 
@@ -105,10 +102,7 @@ variables {p : ℕ}
 -/
 @[simp]
 protected lemma zero : padic_val_int p 0 = 0 :=
-begin
-  unfold padic_val_int,
-  simp,
-end
+by simp [padic_val_int]
 
 /--
 `padic_val_int p 1` is 0 for any `p`.
@@ -116,16 +110,11 @@ end
 @[simp] protected lemma one : padic_val_int p 1 = 0 :=
 by simp [padic_val_int]
 
--- @[simp] lemma nat_abs (z : ℤ) : padic_val_nat p z.nat_abs = padic_val_int p z :=
--- by simp [padic_val_int]
-
 /--
 For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1.
 -/
 @[simp] lemma self (hp : 1 < p) : padic_val_int p p = 1 :=
-by {simp [padic_val_int, padic_val_nat.self hp], }
-
-
+by simp [padic_val_int, padic_val_nat.self hp]
 
 end padic_val_int
 
@@ -184,19 +173,15 @@ The p-adic value of an integer `z ≠ 0` is the multiplicity of `p` in `z`.
 lemma padic_val_rat_of_int (z : ℤ) (hp : p ≠ 1) (hz : z ≠ 0) :
   padic_val_rat p (z : ℚ) = (multiplicity (p : ℤ) z).get
     (finite_int_iff.2 ⟨hp, hz⟩) :=
-by {
+begin
   rw [padic_val_rat, padic_val_int, padic_val_nat, padic_val_nat, dif_pos, dif_pos],
   simp_rw multiplicity.int.nat_abs,
-  simp only [rat.coe_int_denom,
- int.coe_nat_zero,
- rat.coe_int_num,
- int.coe_nat_inj',
- sub_zero,
- multiplicity.get_one_right],
- refl,
- simp [hp],
- simp [hp, hz],
-  }
+  simp only [rat.coe_int_denom, int.coe_nat_zero, rat.coe_int_num, int.coe_nat_inj',
+    sub_zero, multiplicity.get_one_right],
+  refl,
+  simp [hp],
+  simp [hp, hz],
+end
 
 end padic_val_rat
 

From 27b5af4e599181f24434a97711fe0dcab17917bd Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Wed, 9 Mar 2022 20:23:35 -0600
Subject: [PATCH 05/54] revert change

---
 src/ring_theory/int/basic.lean    | 2 +-
 src/ring_theory/multiplicity.lean | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/ring_theory/int/basic.lean b/src/ring_theory/int/basic.lean
index 82f2a1e3e020e..fbd3891627807 100644
--- a/src/ring_theory/int/basic.lean
+++ b/src/ring_theory/int/basic.lean
@@ -294,7 +294,7 @@ lemma finite_int_iff_nat_abs_finite {a b : ℤ} : finite a b ↔ finite a.nat_ab
 by simp only [finite_def, ← int.nat_abs_dvd_iff_dvd, int.nat_abs_pow]
 
 lemma finite_int_iff {a b : ℤ} : finite a b ↔ (a.nat_abs ≠ 1 ∧ b ≠ 0) :=
-by rw [finite_int_iff_nat_abs_finite, finite_nat_iff, int.nat_abs_ne_zero]
+by rw [finite_int_iff_nat_abs_finite, finite_nat_iff, pos_iff_ne_zero, int.nat_abs_ne_zero]
 
 instance decidable_nat : decidable_rel (λ a b : ℕ, (multiplicity a b).dom) :=
 λ a b, decidable_of_iff _ finite_nat_iff.symm
diff --git a/src/ring_theory/multiplicity.lean b/src/ring_theory/multiplicity.lean
index bb2bcf1709679..7ade4ff52a1b6 100644
--- a/src/ring_theory/multiplicity.lean
+++ b/src/ring_theory/multiplicity.lean
@@ -236,9 +236,9 @@ lemma dvd_iff_multiplicity_pos {a b : α} : (0 : enat) < multiplicity a b ↔ a
       by simpa only [heq, nat.cast_zero] using enat.coe_lt_coe.mpr zero_lt_one)
     (by rwa pow_one a))⟩
 
-lemma finite_nat_iff {a b : ℕ} : finite a b ↔ (a ≠ 1 ∧ b ≠ 0) :=
+lemma finite_nat_iff {a b : ℕ} : finite a b ↔ (a ≠ 1 ∧ 0 < b) :=
 begin
-  rw [←pos_iff_ne_zero, ← not_iff_not, not_finite_iff_forall, not_and_distrib, ne.def,
+  rw [← not_iff_not, not_finite_iff_forall, not_and_distrib, ne.def,
     not_not, not_lt, nat.le_zero_iff],
   exact ⟨λ h, or_iff_not_imp_right.2 (λ hb,
     have ha : a ≠ 0, from λ ha, by simpa [ha] using h 1,

From bb7bb903f9c37bec54e2e9d99264bab7ac9d244f Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Wed, 9 Mar 2022 20:23:39 -0600
Subject: [PATCH 06/54] golf

---
 src/number_theory/padics/padic_norm.lean | 27 +++++++++++-------------
 1 file changed, 12 insertions(+), 15 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index fdad70291b959..ea9a9774d5684 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -163,9 +163,11 @@ protected lemma zero (m : nat) : padic_val_rat m 0 = 0 := by simp [padic_val_rat
 For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1.
 -/
 @[simp] lemma padic_val_rat_self (hp : 1 < p) : padic_val_rat p p = 1 :=
-by {simp [padic_val_rat, padic_val_int],
-    rw padic_val_nat.self hp, -- why doesn't this simp trigger
-    dec_trivial, }
+begin
+  simp only [padic_val_rat, padic_val_int, rat.coe_nat_num, int.nat_abs_of_nat, rat.coe_nat_denom,
+    padic_val_nat.one, int.coe_nat_zero, sub_zero, padic_val_nat.self hp],
+  refl,
+end
 
 /--
 The p-adic value of an integer `z ≠ 0` is the multiplicity of `p` in `z`.
@@ -202,10 +204,7 @@ end
 -/
 @[simp, norm_cast] lemma padic_val_rat_of_nat (p n : ℕ) :
   ↑(padic_val_nat p n) = padic_val_rat p n :=
-begin
-  unfold padic_val_rat padic_val_int,
-  simp,
-end
+by simp [padic_val_rat, padic_val_int]
 
 /--
 A simplification of `padic_val_nat` when one input is prime, by analogy with `padic_val_rat_def`.
@@ -217,9 +216,9 @@ lemma padic_val_nat_def {p : ℕ} [hp : fact p.prime] {n : ℕ} (hn : n ≠ 0) :
 begin
   simp [padic_val_nat],
   split_ifs,
-  refl,
-  exfalso,
-  apply h ⟨(hp.out).ne_one, hn⟩,
+  { refl, },
+  { exfalso,
+    apply h ⟨(hp.out).ne_one, hn⟩, }
 end
 
 @[simp] lemma padic_val_nat_self (p : ℕ) [fact p.prime] : padic_val_nat p p = 1 :=
@@ -272,15 +271,13 @@ begin
   split,
   { exact nat.prime.ne_one p_prime.out, },
   { intro hq,
-    rw hq at hc2,
-    simp at hc2,
+    simp [hq] at hc2,
     exact hd hc2, },
   split,
   { exact nat.prime.ne_one p_prime.out, },
   { intro hq,
-    simp at hq,
-    rw hq at hc1,
-    simp at hc1,
+    simp only [int.nat_abs_eq_zero] at hq,
+    simp [hq] at hc1,
     exact hn hc1, },
 end
 

From 14882a1ea03b942011d4cb5a8abf2833f6c4cabf Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Wed, 9 Mar 2022 20:42:36 -0600
Subject: [PATCH 07/54] revert to pos

---
 src/number_theory/padics/padic_norm.lean | 35 ++++++++++++++----------
 1 file changed, 20 insertions(+), 15 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index ea9a9774d5684..5991c6a5d6a93 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -52,7 +52,7 @@ open_locale rat
 open multiplicity
 
 def padic_val_nat (p : ℕ) (n : ℕ) : ℕ :=
-if h : p ≠ 1 ∧ n ≠ 0
+if h : p ≠ 1 ∧ 0 < n
 then (multiplicity p n).get (multiplicity.finite_nat_iff.2 h)
 else 0
 
@@ -182,7 +182,9 @@ begin
     sub_zero, multiplicity.get_one_right],
   refl,
   simp [hp],
-  simp [hp, hz],
+  simp [hp],
+  apply nat.pos_of_ne_zero,
+  simp [hz],
 end
 
 end padic_val_rat
@@ -209,7 +211,7 @@ by simp [padic_val_rat, padic_val_int]
 /--
 A simplification of `padic_val_nat` when one input is prime, by analogy with `padic_val_rat_def`.
 -/
-lemma padic_val_nat_def {p : ℕ} [hp : fact p.prime] {n : ℕ} (hn : n ≠ 0) :
+lemma padic_val_nat_def {p : ℕ} [hp : fact p.prime] {n : ℕ} (hn : 0 < n) :
   padic_val_nat p n =
   (multiplicity p n).get
     (multiplicity.finite_nat_iff.2 ⟨nat.prime.ne_one hp.1, hn⟩) :=
@@ -222,13 +224,13 @@ begin
 end
 
 @[simp] lemma padic_val_nat_self (p : ℕ) [fact p.prime] : padic_val_nat p p = 1 :=
-by simp [padic_val_nat_def (fact.out p.prime).ne_zero]
+by simp [padic_val_nat_def (fact.out p.prime).pos]
 
 lemma one_le_padic_val_nat_of_dvd
-  {n p : nat} [prime : fact p.prime] (nonzero : n ≠ 0) (div : p ∣ n) :
+  {n p : nat} [prime : fact p.prime] (n_pos : 0 < n) (div : p ∣ n) :
   1 ≤ padic_val_nat p n :=
 begin
-  rw @padic_val_nat_def _ prime _ nonzero,
+  rw @padic_val_nat_def _ prime _ n_pos,
   let one_le_mul : _ ≤ multiplicity p n :=
     @multiplicity.le_multiplicity_of_pow_dvd _ _ _ p n 1 (begin norm_num, exact div end),
   simp only [nat.cast_one] at one_le_mul,
@@ -270,12 +272,14 @@ begin
   refl,
   split,
   { exact nat.prime.ne_one p_prime.out, },
-  { intro hq,
+  { apply nat.pos_of_ne_zero,
+    intro hq,
     simp [hq] at hc2,
     exact hd hc2, },
   split,
   { exact nat.prime.ne_one p_prime.out, },
-  { intro hq,
+  { apply nat.pos_of_ne_zero,
+    intro hq,
     simp only [int.nat_abs_eq_zero] at hq,
     simp [hq] at hc1,
     exact hn hc1, },
@@ -477,7 +481,7 @@ lemma padic_val_nat_of_not_dvd {p : ℕ} [fact p.prime] {n : ℕ} (not_dvd : ¬(
 begin
   by_cases hn : n = 0,
   { subst hn, simp at not_dvd, trivial, },
-  { rw padic_val_nat_def hn,
+  { rw padic_val_nat_def (nat.pos_of_ne_zero hn),
     exact (@multiplicity.unique' _ _ _ p n 0 (by simp) (by simpa using not_dvd)).symm,
     assumption, },
 end
@@ -496,7 +500,7 @@ begin
   { rw hn, exact dvd_zero (p ^ padic_val_nat p 0) },
   { rw multiplicity.pow_dvd_iff_le_multiplicity,
     apply le_of_eq,
-    rw padic_val_nat_def (ne_of_gt hn),
+    rw padic_val_nat_def hn,
     { apply enat.coe_get },
     { apply_instance } }
 end
@@ -505,11 +509,11 @@ lemma pow_succ_padic_val_nat_not_dvd {p n : ℕ} [hp : fact (nat.prime p)] (hn :
   ¬ p ^ (padic_val_nat p n + 1) ∣ n :=
 begin
   { rw multiplicity.pow_dvd_iff_le_multiplicity,
-    rw padic_val_nat_def (ne_of_gt hn),
+    rw padic_val_nat_def hn,
     { rw [nat.cast_add, enat.coe_get],
       simp only [nat.cast_one, not_le],
       exact enat.lt_add_one (ne_top_iff_finite.mpr
-        (finite_nat_iff.mpr ⟨(fact.elim hp).ne_one, (ne_of_lt hn).symm⟩)), },
+        (finite_nat_iff.mpr ⟨(fact.elim hp).ne_one, hn⟩)), },
     { apply_instance } }
 end
 
@@ -540,7 +544,7 @@ lemma padic_val_nat_eq_factorization (p n : ℕ) [hp : fact p.prime] :
   padic_val_nat p n = n.factorization p :=
 begin
   by_cases hn : n = 0, { subst hn, simp },
-  rw @padic_val_nat_def p _ n hn,
+  rw @padic_val_nat_def p _ n (nat.pos_of_ne_zero hn),
   simp [@multiplicity_eq_factorization n p hp.elim hn],
 end
 
@@ -747,8 +751,9 @@ begin
   rw [if_neg _],
   { refine zpow_le_one_of_nonpos _ _,
     { exact_mod_cast le_of_lt hp.1.one_lt, },
-    { rw [padic_val_rat_of_int _ hp.1.ne_one hz, neg_nonpos],
-      norm_cast, simp }},
+    { have : z ≠ 0, exact hz,
+      rw [neg_nonpos, padic_val_rat_of_int], -- _ hp.1.ne_one (sorry)],
+      norm_cast, simp, }},
   exact_mod_cast hz
 end
 

From 5fed609b7089a883570f5bfa34b8637427ced8bc Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Wed, 9 Mar 2022 20:42:45 -0600
Subject: [PATCH 08/54] revert

---
 src/number_theory/padics/padic_norm.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 5991c6a5d6a93..d1fb80e3da583 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -751,9 +751,8 @@ begin
   rw [if_neg _],
   { refine zpow_le_one_of_nonpos _ _,
     { exact_mod_cast le_of_lt hp.1.one_lt, },
-    { have : z ≠ 0, exact hz,
-      rw [neg_nonpos, padic_val_rat_of_int], -- _ hp.1.ne_one (sorry)],
-      norm_cast, simp, }},
+    { rw [padic_val_rat_of_int _ hp.1.ne_one hz, neg_nonpos],
+      norm_cast, simp }},
   exact_mod_cast hz
 end
 

From 1a17933c0de37b8c7c3c9c34a9f91b6fe022fddf Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Wed, 9 Mar 2022 20:46:45 -0600
Subject: [PATCH 09/54] remove old simplification

---
 src/number_theory/padics/padic_norm.lean | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index d1fb80e3da583..4d5221c4954ab 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -129,15 +129,6 @@ If `q = 0` or `p = 1`, then `padic_val_rat p q` defaults to 0.
 def padic_val_rat (p : ℕ) (q : ℚ) : ℤ :=
 padic_val_int p q.num - padic_val_nat p q.denom
 
--- /--
--- A simplification of the definition of `padic_val_rat p q` when `q ≠ 0` and `p` is prime.
--- -/
--- lemma padic_val_rat_def (p : ℕ) [hp : fact p.prime] {q : ℚ} (hq : q ≠ 0) : padic_val_rat p q =
---   (multiplicity (p : ℤ) q.num).get (finite_int_iff.2 ⟨hp.1.ne_one, rat.num_ne_zero_of_ne_zero hq⟩) -
---   (multiplicity (p : ℤ) q.denom).get
---     (finite_int_iff.2 ⟨hp.1.ne_one, by exact_mod_cast rat.denom_ne_zero _⟩) :=
--- dif_pos ⟨hq, hp.1.ne_one⟩
-
 namespace padic_val_rat
 open multiplicity
 variables {p : ℕ}

From ad6c6d7657aabce569c1edc56d31d038f919ac1f Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Wed, 9 Mar 2022 20:50:54 -0600
Subject: [PATCH 10/54] golf

---
 src/number_theory/padics/padic_norm.lean | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 4d5221c4954ab..8ae2f6e93503e 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -65,10 +65,7 @@ variables {p : ℕ}
 -/
 @[simp]
 protected lemma zero : padic_val_nat p 0 = 0 :=
-begin
-  unfold padic_val_nat,
-  simp,
-end
+by simp [padic_val_nat]
 
 /--
 `padic_val_nat p 1` is 0 for any `p`.

From 9b3ba9fa08c12e0f6242da223a873f9976b1acb2 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Thu, 10 Mar 2022 13:11:18 -0600
Subject: [PATCH 11/54] Update src/number_theory/padics/padic_norm.lean

Co-authored-by: Johan Commelin <johan@commelin.net>
---
 src/number_theory/padics/padic_norm.lean | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 8ae2f6e93503e..58abd31c51d7e 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -60,11 +60,8 @@ namespace padic_val_nat
 open multiplicity
 variables {p : ℕ}
 
-/--
-`padic_val_nat p 0` is 0 for any `p`.
--/
-@[simp]
-protected lemma zero : padic_val_nat p 0 = 0 :=
+/-- `padic_val_nat p 0` is 0 for any `p`. -/
+@[simp] protected lemma zero : padic_val_nat p 0 = 0 :=
 by simp [padic_val_nat]
 
 /--

From 3b8f6d566a17f86fea3a0025d46d988fcf11d5a5 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Thu, 10 Mar 2022 13:11:25 -0600
Subject: [PATCH 12/54] Update src/number_theory/padics/padic_norm.lean

Co-authored-by: Johan Commelin <johan@commelin.net>
---
 src/number_theory/padics/padic_norm.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 58abd31c51d7e..0c133fea0f072 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -64,9 +64,7 @@ variables {p : ℕ}
 @[simp] protected lemma zero : padic_val_nat p 0 = 0 :=
 by simp [padic_val_nat]
 
-/--
-`padic_val_nat p 1` is 0 for any `p`.
--/
+/-- `padic_val_nat p 1` is 0 for any `p`. -/
 @[simp] protected lemma one : padic_val_nat p 1 = 0 :=
 by unfold padic_val_nat; split_ifs; simp *
 

From f3be9eb1c60cf8180476903982a5a022c73a4617 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Thu, 10 Mar 2022 13:11:31 -0600
Subject: [PATCH 13/54] Update src/number_theory/padics/padic_norm.lean

Co-authored-by: Johan Commelin <johan@commelin.net>
---
 src/number_theory/padics/padic_norm.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 0c133fea0f072..9dde3fa9b7c6e 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -68,9 +68,7 @@ by simp [padic_val_nat]
 @[simp] protected lemma one : padic_val_nat p 1 = 0 :=
 by unfold padic_val_nat; split_ifs; simp *
 
-/--
-For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1.
--/
+/-- For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1. -/
 @[simp] lemma self (hp : 1 < p) : padic_val_nat p p = 1 :=
 begin
   have neq_one : (¬ p = 1) ↔ true,

From 85b0e8d1b15abc1586aa539ee6fb5d6eb066cf68 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Thu, 10 Mar 2022 13:11:43 -0600
Subject: [PATCH 14/54] Update src/number_theory/padics/padic_norm.lean

Co-authored-by: Johan Commelin <johan@commelin.net>
---
 src/number_theory/padics/padic_norm.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 9dde3fa9b7c6e..c93929819fc7d 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -87,9 +87,7 @@ namespace padic_val_int
 open multiplicity
 variables {p : ℕ}
 
-/--
-`padic_val_int p 0` is 0 for any `p`.
--/
+/-- `padic_val_int p 0` is 0 for any `p`. -/
 @[simp]
 protected lemma zero : padic_val_int p 0 = 0 :=
 by simp [padic_val_int]

From ae586d5de749ac5bb4c0b3fd6175150f9404a7c5 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Thu, 10 Mar 2022 13:11:49 -0600
Subject: [PATCH 15/54] Update src/number_theory/padics/padic_norm.lean

Co-authored-by: Johan Commelin <johan@commelin.net>
---
 src/number_theory/padics/padic_norm.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index c93929819fc7d..8bde5c042f22d 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -92,9 +92,7 @@ variables {p : ℕ}
 protected lemma zero : padic_val_int p 0 = 0 :=
 by simp [padic_val_int]
 
-/--
-`padic_val_int p 1` is 0 for any `p`.
--/
+/-- `padic_val_int p 1` is 0 for any `p`. -/
 @[simp] protected lemma one : padic_val_int p 1 = 0 :=
 by simp [padic_val_int]
 

From b0387aae2962681efbd4e1f8d02ea5f0be2d31a2 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Thu, 10 Mar 2022 13:11:55 -0600
Subject: [PATCH 16/54] Update src/number_theory/padics/padic_norm.lean

Co-authored-by: Johan Commelin <johan@commelin.net>
---
 src/number_theory/padics/padic_norm.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 8bde5c042f22d..021d6876f8ff8 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -96,9 +96,7 @@ by simp [padic_val_int]
 @[simp] protected lemma one : padic_val_int p 1 = 0 :=
 by simp [padic_val_int]
 
-/--
-For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1.
--/
+/-- For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1. -/
 @[simp] lemma self (hp : 1 < p) : padic_val_int p p = 1 :=
 by simp [padic_val_int, padic_val_nat.self hp]
 

From 9ded751a287f692c139f80871bb289446c4d0e22 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Thu, 10 Mar 2022 13:46:59 -0600
Subject: [PATCH 17/54] fix proof

---
 src/number_theory/padics/padic_numbers.lean | 22 ++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

diff --git a/src/number_theory/padics/padic_numbers.lean b/src/number_theory/padics/padic_numbers.lean
index b78056a456626..f3b0d4713ac8d 100644
--- a/src/number_theory/padics/padic_numbers.lean
+++ b/src/number_theory/padics/padic_numbers.lean
@@ -816,7 +816,8 @@ end
 begin
   have p₀ : p ≠ 0 := hp.1.ne_zero,
   have p₁ : p ≠ 1 := hp.1.ne_one,
-  simp [p₀, p₁, norm, padic_norm, padic_val_rat, zpow_neg, padic.cast_eq_of_rat_of_nat],
+  simp [p₀, p₁, norm, padic_norm, padic_val_rat, padic_val_int, zpow_neg,
+    padic.cast_eq_of_rat_of_nat],
 end
 
 lemma norm_p_lt_one : ∥(p : ℚ_[p])∥ < 1 :=
@@ -864,13 +865,20 @@ theorem norm_rat_le_one : ∀ {q : ℚ} (hq : ¬ p ∣ q.denom), ∥(q : ℚ_[p]
         from mt rat.zero_iff_num_zero.1 hnz,
       rw [padic_norm_e.eq_padic_norm],
       norm_cast,
-      rw [padic_norm.eq_zpow_of_nonzero p hnz', padic_val_rat_def p hnz'],
-      have h : (multiplicity p d).get _ = 0, by simp [multiplicity_eq_zero_of_not_dvd, hq],
-      simp only, norm_cast,
-      rw_mod_cast [h, sub_zero],
+      rw [padic_norm.eq_zpow_of_nonzero p hnz'],
+      simp only [padic_val_rat, padic_val_int, padic_val_nat, ne.def, neg_sub],
+      rw [dif_pos, dif_pos],
+      simp only [multiplicity_eq_zero_of_not_dvd, hq, not_false_iff, enat.get_zero,
+        int.coe_nat_zero, zero_sub, zpow_neg₀, zpow_coe_nat],
+      norm_cast,
+      rw ←zpow_neg_one,
       apply zpow_le_one_of_nonpos,
-      { exact_mod_cast le_of_lt hp.1.one_lt, },
-      { apply neg_nonpos_of_nonneg, norm_cast, simp, }
+      { norm_cast,
+        apply one_le_pow,
+        exact hp.1.pos, },
+      { dec_trivial, },
+      exact ⟨ne_of_gt (hp.out).one_lt, int.nat_abs_pos_of_ne_zero hnz⟩,
+      exact ⟨ne_of_gt (hp.out).one_lt, hn⟩,
     end
 
 theorem norm_int_le_one (z : ℤ) : ∥(z : ℚ_[p])∥ ≤ 1 :=

From b58ee9a56589b53e32e023708a98d06538c926c0 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Thu, 10 Mar 2022 16:39:11 -0600
Subject: [PATCH 18/54] docs

---
 src/number_theory/padics/padic_norm.lean | 123 +++++++----------------
 1 file changed, 38 insertions(+), 85 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 021d6876f8ff8..994564079ecdd 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -51,6 +51,12 @@ open_locale rat
 
 open multiplicity
 
+/--
+For `p ≠ 1`, the p-adic valuation of a natural `n ≠ 0` is the largest natural number `k` such that
+p^k divides z.
+
+If `n = 0` or `p = 1`, then `padic_val_nat p q` defaults to 0.
+-/
 def padic_val_nat (p : ℕ) (n : ℕ) : ℕ :=
 if h : p ≠ 1 ∧ 0 < n
 then (multiplicity p n).get (multiplicity.finite_nat_iff.2 h)
@@ -80,6 +86,12 @@ end
 
 end padic_val_nat
 
+/--
+For `p ≠ 1`, the p-adic valuation of an integer `z ≠ 0` is the largest natural number `k` such that
+p^k divides z.
+
+If `x = 0` or `p = 1`, then `padic_val_int p q` defaults to 0.
+-/
 def padic_val_int (p : ℕ) (z : ℤ) : ℕ :=
 padic_val_nat p (z.nat_abs)
 
@@ -103,9 +115,6 @@ by simp [padic_val_int, padic_val_nat.self hp]
 end padic_val_int
 
 /--
-For `p ≠ 1`, the p-adic valuation of an integer `z ≠ 0` is the largest natural number `n` such that
-p^n divides z.
-
 `padic_val_rat` defines the valuation of a rational `q` to be the valuation of `q.num` minus the
 valuation of `q.denom`.
 If `q = 0` or `p = 1`, then `padic_val_rat p q` defaults to 0.
@@ -117,26 +126,18 @@ namespace padic_val_rat
 open multiplicity
 variables {p : ℕ}
 
-/--
-`padic_val_rat p q` is symmetric in `q`.
--/
+/-- `padic_val_rat p q` is symmetric in `q`. -/
 @[simp] protected lemma neg (q : ℚ) : padic_val_rat p (-q) = padic_val_rat p q :=
 by simp [padic_val_rat, padic_val_int]
 
-/--
-`padic_val_rat p 0` is 0 for any `p`.
--/
+/-- `padic_val_rat p 0` is 0 for any `p`. -/
 @[simp]
 protected lemma zero (m : nat) : padic_val_rat m 0 = 0 := by simp [padic_val_rat, padic_val_int]
 
-/--
-`padic_val_rat p 1` is 0 for any `p`.
--/
+/-- `padic_val_rat p 1` is 0 for any `p`. -/
 @[simp] protected lemma one : padic_val_rat p 1 = 0 := by simp [padic_val_rat, padic_val_int]
 
-/--
-For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1.
--/
+/-- For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1. -/
 @[simp] lemma padic_val_rat_self (hp : 1 < p) : padic_val_rat p p = 1 :=
 begin
   simp only [padic_val_rat, padic_val_int, rat.coe_nat_num, int.nat_abs_of_nat, rat.coe_nat_denom,
@@ -144,9 +145,7 @@ begin
   refl,
 end
 
-/--
-The p-adic value of an integer `z ≠ 0` is the multiplicity of `p` in `z`.
--/
+/-- The p-adic value of an integer `z ≠ 0` is the multiplicity of `p` in `z`. -/
 lemma padic_val_rat_of_int (z : ℤ) (hp : p ≠ 1) (hz : z ≠ 0) :
   padic_val_rat p (z : ℚ) = (multiplicity (p : ℤ) z).get
     (finite_int_iff.2 ⟨hp, hz⟩) :=
@@ -166,19 +165,13 @@ end padic_val_rat
 
 section padic_val_nat
 
-/--
-`padic_val_nat` is defined as an `int.to_nat` cast;
-this lemma ensures that the cast is well-behaved.
--/
 lemma zero_le_padic_val_rat_of_nat (p n : ℕ) : 0 ≤ padic_val_rat p n :=
 begin
   unfold padic_val_rat padic_val_int padic_val_nat,
   split_ifs; simp,
 end
 
-/--
-`padic_val_rat` coincides with `padic_val_nat`.
--/
+/-- `padic_val_rat` coincides with `padic_val_nat`. -/
 @[simp, norm_cast] lemma padic_val_rat_of_nat (p n : ℕ) :
   ↑(padic_val_nat p n) = padic_val_rat p n :=
 by simp [padic_val_rat, padic_val_int]
@@ -221,15 +214,11 @@ open multiplicity
 variables (p : ℕ) [p_prime : fact p.prime]
 include p_prime
 
-/--
-The multiplicity of `p : ℕ` in `a : ℤ` is finite exactly when `a ≠ 0`.
--/
+/-- The multiplicity of `p : ℕ` in `a : ℤ` is finite exactly when `a ≠ 0`. -/
 lemma finite_int_prime_iff {p : ℕ} [p_prime : fact p.prime] {a : ℤ} : finite (p : ℤ) a ↔ a ≠ 0 :=
 by simp [finite_int_iff, ne.symm (ne_of_lt (p_prime.1.one_lt))]
 
-/--
-A rewrite lemma for `padic_val_rat p q` when `q` is expressed in terms of `rat.mk`.
--/
+/-- A rewrite lemma for `padic_val_rat p q` when `q` is expressed in terms of `rat.mk`. -/
 protected lemma defn {q : ℚ} {n d : ℤ} (hqz : q ≠ 0) (qdf : q = n /. d) :
   padic_val_rat p q = (multiplicity (p : ℤ) n).get (finite_int_iff.2
     ⟨ne.symm $ ne_of_lt p_prime.1.one_lt, λ hn, by simp * at *⟩) -
@@ -260,9 +249,7 @@ begin
     exact hn hc1, },
 end
 
-/--
-A rewrite lemma for `padic_val_rat p (q * r)` with conditions `q ≠ 0`, `r ≠ 0`.
--/
+/-- A rewrite lemma for `padic_val_rat p (q * r)` with conditions `q ≠ 0`, `r ≠ 0`. -/
 protected lemma mul {q r : ℚ} (hq : q ≠ 0) (hr : r ≠ 0) :
   padic_val_rat p (q * r) = padic_val_rat p q + padic_val_rat p r :=
 have q*r = (q.num * r.num) /. (↑q.denom * ↑r.denom), by rw_mod_cast rat.mul_num_denom,
@@ -276,25 +263,19 @@ begin
   rw [multiplicity.mul' hp', multiplicity.mul' hp']; simp [add_comm, add_left_comm, sub_eq_add_neg]
 end
 
-/--
-A rewrite lemma for `padic_val_rat p (q^k)` with condition `q ≠ 0`.
--/
+/-- A rewrite lemma for `padic_val_rat p (q^k)` with condition `q ≠ 0`. -/
 protected lemma pow {q : ℚ} (hq : q ≠ 0) {k : ℕ} :
     padic_val_rat p (q ^ k) = k * padic_val_rat p q :=
 by induction k; simp [*, padic_val_rat.mul _ hq (pow_ne_zero _ hq),
   pow_succ, add_mul, add_comm]
 
-/--
-A rewrite lemma for `padic_val_rat p (q⁻¹)` with condition `q ≠ 0`.
--/
+/-- A rewrite lemma for `padic_val_rat p (q⁻¹)` with condition `q ≠ 0`. -/
 protected lemma inv {q : ℚ} (hq : q ≠ 0) :
   padic_val_rat p (q⁻¹) = -padic_val_rat p q :=
 by rw [eq_neg_iff_add_eq_zero, ← padic_val_rat.mul p (inv_ne_zero hq) hq,
     inv_mul_cancel hq, padic_val_rat.one]
 
-/--
-A rewrite lemma for `padic_val_rat p (q / r)` with conditions `q ≠ 0`, `r ≠ 0`.
--/
+/-- A rewrite lemma for `padic_val_rat p (q / r)` with conditions `q ≠ 0`, `r ≠ 0`. -/
 protected lemma div {q r : ℚ} (hq : q ≠ 0) (hr : r ≠ 0) :
   padic_val_rat p (q / r) = padic_val_rat p q - padic_val_rat p r :=
 by rw [div_eq_mul_inv, padic_val_rat.mul p hq (inv_ne_zero hr),
@@ -391,9 +372,7 @@ end padic_val_rat
 
 namespace padic_val_nat
 
-/--
-A rewrite lemma for `padic_val_nat p (q * r)` with conditions `q ≠ 0`, `r ≠ 0`.
--/
+/-- A rewrite lemma for `padic_val_nat p (q * r)` with conditions `q ≠ 0`, `r ≠ 0`. -/
 protected lemma mul (p : ℕ) [p_prime : fact p.prime] {q r : ℕ} (hq : q ≠ 0) (hr : r ≠ 0) :
   padic_val_nat p (q * r) = padic_val_nat p q + padic_val_nat p r :=
 begin
@@ -415,9 +394,7 @@ begin
   rw [mul_comm, k.mul_div_cancel hb.bot_lt, padic_val_nat.mul p hk hb, nat.add_sub_cancel]
 end
 
-/--
-Dividing out by a prime factor reduces the padic_val_nat by 1.
--/
+/-- Dividing out by a prime factor reduces the padic_val_nat by 1. -/
 protected lemma div {p : ℕ} [p_prime : fact p.prime] {b : ℕ} (dvd : p ∣ b) :
   (padic_val_nat p (b / p)) = (padic_val_nat p b) - 1 :=
 begin
@@ -448,9 +425,7 @@ end padic_val_nat
 
 section padic_val_nat
 
-/--
-If a prime doesn't appear in `n`, `padic_val_nat p n` is `0`.
--/
+/-- If a prime doesn't appear in `n`, `padic_val_nat p n` is `0`. -/
 lemma padic_val_nat_of_not_dvd {p : ℕ} [fact p.prime] {n : ℕ} (not_dvd : ¬(p ∣ n)) :
   padic_val_nat p n = 0 :=
 begin
@@ -584,16 +559,12 @@ section padic_norm
 open padic_val_rat
 variables (p : ℕ)
 
-/--
-Unfolds the definition of the p-adic norm of `q` when `q ≠ 0`.
--/
+/-- Unfolds the definition of the p-adic norm of `q` when `q ≠ 0`. -/
 @[simp] protected lemma eq_zpow_of_nonzero {q : ℚ} (hq : q ≠ 0) :
   padic_norm p q = p ^ (-(padic_val_rat p q)) :=
 by simp [hq, padic_norm]
 
-/--
-The p-adic norm is nonnegative.
--/
+/-- The p-adic norm is nonnegative. -/
 protected lemma nonneg (q : ℚ) : 0 ≤ padic_norm p q :=
 if hq : q = 0 then by simp [hq, padic_norm]
 else
@@ -603,14 +574,10 @@ else
     exact_mod_cast nat.zero_le _
   end
 
-/--
-The p-adic norm of 0 is 0.
--/
+/-- The p-adic norm of 0 is 0. -/
 @[simp] protected lemma zero : padic_norm p 0 = 0 := by simp [padic_norm]
 
-/--
-The p-adic norm of 1 is 1.
--/
+/-- The p-adic norm of 1 is 1. -/
 @[simp] protected lemma one : padic_norm p 1 = 1 := by simp [padic_norm]
 
 /--
@@ -658,15 +625,11 @@ See also `padic_norm.padic_norm_p_lt_one` for a version assuming `1 < p`.
 lemma padic_norm_p_lt_one_of_prime (p : ℕ) [fact p.prime] : padic_norm p p < 1 :=
 padic_norm_p_lt_one $ nat.prime.one_lt (fact.out _)
 
-/--
-`padic_norm p q` takes discrete values `p ^ -z` for `z : ℤ`.
--/
+/-- `padic_norm p q` takes discrete values `p ^ -z` for `z : ℤ`. -/
 protected theorem values_discrete {q : ℚ} (hq : q ≠ 0) : ∃ z : ℤ, padic_norm p q = p ^ (-z) :=
 ⟨ (padic_val_rat p q), by simp [padic_norm, hq] ⟩
 
-/--
-`padic_norm p` is symmetric.
--/
+/-- `padic_norm p` is symmetric. -/
 @[simp] protected lemma neg (q : ℚ) : padic_norm p (-q) = padic_norm p q :=
 if hq : q = 0 then by simp [hq]
 else by simp [padic_norm, hq]
@@ -674,9 +637,7 @@ else by simp [padic_norm, hq]
 variable [hp : fact p.prime]
 include hp
 
-/--
-If `q ≠ 0`, then `padic_norm p q ≠ 0`.
--/
+/-- If `q ≠ 0`, then `padic_norm p q ≠ 0`. -/
 protected lemma nonzero {q : ℚ} (hq : q ≠ 0) : padic_norm p q ≠ 0 :=
 begin
   rw padic_norm.eq_zpow_of_nonzero p hq,
@@ -684,9 +645,7 @@ begin
   exact_mod_cast ne_of_gt hp.1.pos
 end
 
-/--
-If the p-adic norm of `q` is 0, then `q` is 0.
--/
+/-- If the p-adic norm of `q` is 0, then `q` is 0. -/
 lemma zero_of_padic_norm_eq_zero {q : ℚ} (h : padic_norm p q = 0) : q = 0 :=
 begin
   apply by_contradiction, intro hq,
@@ -696,9 +655,7 @@ begin
   exact_mod_cast hp.1.ne_zero
 end
 
-/--
-The p-adic norm is multiplicative.
--/
+/-- The p-adic norm is multiplicative. -/
 @[simp] protected theorem mul (q r : ℚ) : padic_norm p (q*r) = padic_norm p q * padic_norm p r :=
 if hq : q = 0 then
   by simp [hq]
@@ -709,16 +666,12 @@ else
   have (↑p : ℚ) ≠ 0, by simp [hp.1.ne_zero],
   by simp [padic_norm, *, padic_val_rat.mul, zpow_add₀ this, mul_comm]
 
-/--
-The p-adic norm respects division.
--/
+/-- The p-adic norm respects division. -/
 @[simp] protected theorem div (q r : ℚ) : padic_norm p (q / r) = padic_norm p q / padic_norm p r :=
 if hr : r = 0 then by simp [hr] else
 eq_div_of_mul_eq (padic_norm.nonzero _ hr) (by rw [←padic_norm.mul, div_mul_cancel _ hr])
 
-/--
-The p-adic norm of an integer is at most 1.
--/
+/-- The p-adic norm of an integer is at most 1. -/
 protected theorem of_int (z : ℤ) : padic_norm p ↑z ≤ 1 :=
 if hz : z = 0 then by simp [hz, zero_le_one] else
 begin

From e26cf1cb4ce9edd3d0ae50812c281491a0143873 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Thu, 10 Mar 2022 22:47:32 -0600
Subject: [PATCH 19/54] delete old version

---
 src/number_theory/padics/padic_norm.lean | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 3608f6a323d88..994564079ecdd 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -465,12 +465,6 @@ begin
       exact enat.lt_add_one (ne_top_iff_finite.mpr
         (finite_nat_iff.mpr ⟨(fact.elim hp).ne_one, hn⟩)), },
     { apply_instance } }
-  -- rw multiplicity.pow_dvd_iff_le_multiplicity,
-  -- rw padic_val_nat_def (ne_of_gt hn),
-  -- { rw [nat.cast_add, enat.coe_get],
-  --   simp only [nat.cast_one, not_le],
-  --   apply enat.lt_add_one (ne_top_iff_finite.2 (finite_nat_iff.2 ⟨hp.elim.ne_one, hn⟩)) },
-  -- { apply_instance }
 end
 
 lemma padic_val_nat_primes {p q : ℕ} [p_prime : fact p.prime] [q_prime : fact q.prime]

From a0759e5ef1879899a1eeae4aa1a8d7b809bb8d96 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Thu, 10 Mar 2022 22:48:28 -0600
Subject: [PATCH 20/54] fix indent

---
 src/ring_theory/multiplicity.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ring_theory/multiplicity.lean b/src/ring_theory/multiplicity.lean
index 7ade4ff52a1b6..b8c4b5daecb89 100644
--- a/src/ring_theory/multiplicity.lean
+++ b/src/ring_theory/multiplicity.lean
@@ -306,7 +306,7 @@ begin
   simp only [true_iff, eq_self_iff_true] at h,
   cases h,
   { conv_rhs { rw h },
-   apply nat_cast_nat_abs, },
+    apply nat_cast_nat_abs, },
   { conv_rhs { rw h },
     rw multiplicity.neg,
     apply nat_cast_nat_abs, },

From 61e69b97f96a501fd7b7eca83c23933d142d168c Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Thu, 10 Mar 2022 23:19:58 -0600
Subject: [PATCH 21/54] golfs

---
 src/number_theory/padics/padic_norm.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 994564079ecdd..f41b257f1b42a 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -156,7 +156,7 @@ begin
     sub_zero, multiplicity.get_one_right],
   refl,
   simp [hp],
-  simp [hp],
+  simp only [hp, ne.def, not_false_iff, rat.coe_int_num, true_and],
   apply nat.pos_of_ne_zero,
   simp [hz],
 end
@@ -231,8 +231,7 @@ begin
   simp [hc1, hc2, multiplicity.mul' (nat.prime_iff_prime_int.1 p_prime.1),
     (ne.symm (ne_of_lt p_prime.1.one_lt)), hqz],
   rw [padic_val_rat, padic_val_int, padic_val_nat, padic_val_nat, dif_pos, dif_pos],
-  simp_rw [int.coe_nat_multiplicity p q.denom],
-  simp_rw multiplicity.int.nat_abs,
+  simp_rw [int.coe_nat_multiplicity p q.denom, multiplicity.int.nat_abs],
   refl,
   split,
   { exact nat.prime.ne_one p_prime.out, },

From ab16b3d0c061c6e942af05fe9f0654d22f1ee791 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 11 Mar 2022 12:21:53 -0600
Subject: [PATCH 22/54] remove example

---
 src/ring_theory/multiplicity.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/ring_theory/multiplicity.lean b/src/ring_theory/multiplicity.lean
index b8c4b5daecb89..f058e375cc955 100644
--- a/src/ring_theory/multiplicity.lean
+++ b/src/ring_theory/multiplicity.lean
@@ -57,8 +57,6 @@ begin
     apply _root_.le_antisymm; { apply nat.find_mono, norm_cast, simp } }
 end
 
-example (a b : ℤ) : a ∣ b ↔ a ∣ b.nat_abs := int.dvd_nat_abs.symm
-
 theorem nat_cast_nat_abs (a b : ℕ) :
     multiplicity a (b : ℤ).nat_abs = multiplicity (a : ℤ) (b : ℤ) :=
 begin

From 9525be1ae003eb3369431bf3705fe9150c7f204a Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 11 Mar 2022 14:04:00 -0600
Subject: [PATCH 23/54] add johan's suggestion

---
 src/number_theory/padics/padic_norm.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index f41b257f1b42a..440a60fc47e37 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -99,6 +99,17 @@ namespace padic_val_int
 open multiplicity
 variables {p : ℕ}
 
+lemma defn {z : ℤ} (hp : p ≠ 1) (hz : z ≠ 0) : padic_val_int p z =
+  (multiplicity (p : ℤ) z).get (by {apply multiplicity.finite_int_iff.2, simp [hp, hz]}) :=
+begin
+  rw [padic_val_int, padic_val_nat, dif_pos],
+  simp_rw  multiplicity.int.nat_abs p z,
+  refl,
+  simp [hp, hz],
+  exact int.nat_abs_pos_of_ne_zero hz, -- TODO make simp lemma
+  -- see nat_abs_ne_zero (and make that a simp lemma too)
+end
+
 /-- `padic_val_int p 0` is 0 for any `p`. -/
 @[simp]
 protected lemma zero : padic_val_int p 0 = 0 :=

From a776c8cc0a9f0f277a768cad3c753bfe2e387492 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 11 Mar 2022 14:08:08 -0600
Subject: [PATCH 24/54] golf

---
 src/number_theory/padics/padic_norm.lean | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 440a60fc47e37..89c60d1d14363 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -161,15 +161,14 @@ lemma padic_val_rat_of_int (z : ℤ) (hp : p ≠ 1) (hz : z ≠ 0) :
   padic_val_rat p (z : ℚ) = (multiplicity (p : ℤ) z).get
     (finite_int_iff.2 ⟨hp, hz⟩) :=
 begin
-  rw [padic_val_rat, padic_val_int, padic_val_nat, padic_val_nat, dif_pos, dif_pos],
-  simp_rw multiplicity.int.nat_abs,
+  rw [padic_val_rat, padic_val_int.defn, padic_val_nat, dif_pos],
+  -- simp_rw multiplicity.int.nat_abs,
   simp only [rat.coe_int_denom, int.coe_nat_zero, rat.coe_int_num, int.coe_nat_inj',
     sub_zero, multiplicity.get_one_right],
   refl,
   simp [hp],
-  simp only [hp, ne.def, not_false_iff, rat.coe_int_num, true_and],
-  apply nat.pos_of_ne_zero,
-  simp [hz],
+  exact hp,
+  simp only [hp, ne.def, not_false_iff, rat.coe_int_num, true_and, hz],
 end
 
 end padic_val_rat

From a4642e13a1e69669b4f3b6690fdc193526cb5573 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 11 Mar 2022 14:08:23 -0600
Subject: [PATCH 25/54] delete comment

---
 src/number_theory/padics/padic_norm.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 89c60d1d14363..b2c973724a85e 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -162,7 +162,6 @@ lemma padic_val_rat_of_int (z : ℤ) (hp : p ≠ 1) (hz : z ≠ 0) :
     (finite_int_iff.2 ⟨hp, hz⟩) :=
 begin
   rw [padic_val_rat, padic_val_int.defn, padic_val_nat, dif_pos],
-  -- simp_rw multiplicity.int.nat_abs,
   simp only [rat.coe_int_denom, int.coe_nat_zero, rat.coe_int_num, int.coe_nat_inj',
     sub_zero, multiplicity.get_one_right],
   refl,

From dfe0bb59a577476d4a5e590f269bda156f2adffa Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 11 Mar 2022 14:42:38 -0600
Subject: [PATCH 26/54] golf defn

---
 src/number_theory/padics/padic_norm.lean | 19 ++++++++-----------
 1 file changed, 8 insertions(+), 11 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index b2c973724a85e..7935cabe26c3d 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -237,24 +237,21 @@ have hn : n ≠ 0, from rat.mk_num_ne_zero_of_ne_zero hqz qdf,
 have hd : d ≠ 0, from rat.mk_denom_ne_zero_of_ne_zero hqz qdf,
 let ⟨c, hc1, hc2⟩ := rat.num_denom_mk hn hd qdf in
 begin
+  rw [padic_val_rat, padic_val_int.defn, padic_val_nat, dif_pos];
   simp [hc1, hc2, multiplicity.mul' (nat.prime_iff_prime_int.1 p_prime.1),
     (ne.symm (ne_of_lt p_prime.1.one_lt)), hqz],
-  rw [padic_val_rat, padic_val_int, padic_val_nat, padic_val_nat, dif_pos, dif_pos],
-  simp_rw [int.coe_nat_multiplicity p q.denom, multiplicity.int.nat_abs],
+  simp_rw [int.coe_nat_multiplicity p q.denom],
   refl,
-  split,
-  { exact nat.prime.ne_one p_prime.out, },
-  { apply nat.pos_of_ne_zero,
-    intro hq,
+  rw pos_iff_ne_zero,
+  -- split,
+  -- repeat { exact nat.prime.ne_one p_prime.out, },
+  { intro hq,
     simp [hq] at hc2,
     exact hd hc2, },
-  split,
-  { exact nat.prime.ne_one p_prime.out, },
-  { apply nat.pos_of_ne_zero,
-    intro hq,
-    simp only [int.nat_abs_eq_zero] at hq,
+  { intro hq,
     simp [hq] at hc1,
     exact hn hc1, },
+    -- multiplicity.mul
 end
 
 /-- A rewrite lemma for `padic_val_rat p (q * r)` with conditions `q ≠ 0`, `r ≠ 0`. -/

From 2cc1eedfd7a1dbb93ee6194b5c3fc379de893d9e Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 11 Mar 2022 16:15:03 -0600
Subject: [PATCH 27/54] golf

---
 src/number_theory/padics/padic_norm.lean | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 7935cabe26c3d..212c5b9234d1f 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -145,6 +145,13 @@ by simp [padic_val_rat, padic_val_int]
 @[simp]
 protected lemma zero (m : nat) : padic_val_rat m 0 = 0 := by simp [padic_val_rat, padic_val_int]
 
+/--
+`padic_val_rat p q` for nonzero `q` is the difference in valuations of the numerator and
+denominator.
+-/
+lemma nonzero {q : ℚ} (hq : q ≠ 0) : padic_val_rat p q =
+  (padic_val_int p q.num : ℤ) - (padic_val_nat p q.denom : ℤ) := by rw padic_val_rat
+
 /-- `padic_val_rat p 1` is 0 for any `p`. -/
 @[simp] protected lemma one : padic_val_rat p 1 = 0 := by simp [padic_val_rat, padic_val_int]
 
@@ -237,21 +244,18 @@ have hn : n ≠ 0, from rat.mk_num_ne_zero_of_ne_zero hqz qdf,
 have hd : d ≠ 0, from rat.mk_denom_ne_zero_of_ne_zero hqz qdf,
 let ⟨c, hc1, hc2⟩ := rat.num_denom_mk hn hd qdf in
 begin
-  rw [padic_val_rat, padic_val_int.defn, padic_val_nat, dif_pos];
+  rw [padic_val_rat.nonzero hqz, padic_val_int.defn, padic_val_nat, dif_pos];
   simp [hc1, hc2, multiplicity.mul' (nat.prime_iff_prime_int.1 p_prime.1),
     (ne.symm (ne_of_lt p_prime.1.one_lt)), hqz],
   simp_rw [int.coe_nat_multiplicity p q.denom],
   refl,
-  rw pos_iff_ne_zero,
-  -- split,
-  -- repeat { exact nat.prime.ne_one p_prime.out, },
-  { intro hq,
+  { rw pos_iff_ne_zero,
+    intro hq,
     simp [hq] at hc2,
     exact hd hc2, },
   { intro hq,
     simp [hq] at hc1,
     exact hn hc1, },
-    -- multiplicity.mul
 end
 
 /-- A rewrite lemma for `padic_val_rat p (q * r)` with conditions `q ≠ 0`, `r ≠ 0`. -/

From b238113bd77f7606dc63b7d09beee7eb44ffd00d Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 11 Mar 2022 16:25:05 -0600
Subject: [PATCH 28/54] more changes

---
 src/number_theory/padics/padic_norm.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 212c5b9234d1f..0840ef0dd84c8 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -99,7 +99,7 @@ namespace padic_val_int
 open multiplicity
 variables {p : ℕ}
 
-lemma defn {z : ℤ} (hp : p ≠ 1) (hz : z ≠ 0) : padic_val_int p z =
+lemma of_ne_one_ne_zero {z : ℤ} (hp : p ≠ 1) (hz : z ≠ 0) : padic_val_int p z =
   (multiplicity (p : ℤ) z).get (by {apply multiplicity.finite_int_iff.2, simp [hp, hz]}) :=
 begin
   rw [padic_val_int, padic_val_nat, dif_pos],
@@ -149,7 +149,7 @@ protected lemma zero (m : nat) : padic_val_rat m 0 = 0 := by simp [padic_val_rat
 `padic_val_rat p q` for nonzero `q` is the difference in valuations of the numerator and
 denominator.
 -/
-lemma nonzero {q : ℚ} (hq : q ≠ 0) : padic_val_rat p q =
+lemma of_ne_zero {q : ℚ} (hq : q ≠ 0) : padic_val_rat p q =
   (padic_val_int p q.num : ℤ) - (padic_val_nat p q.denom : ℤ) := by rw padic_val_rat
 
 /-- `padic_val_rat p 1` is 0 for any `p`. -/
@@ -168,7 +168,7 @@ lemma padic_val_rat_of_int (z : ℤ) (hp : p ≠ 1) (hz : z ≠ 0) :
   padic_val_rat p (z : ℚ) = (multiplicity (p : ℤ) z).get
     (finite_int_iff.2 ⟨hp, hz⟩) :=
 begin
-  rw [padic_val_rat, padic_val_int.defn, padic_val_nat, dif_pos],
+  rw [padic_val_rat, padic_val_int.of_ne_one_ne_zero, padic_val_nat, dif_pos],
   simp only [rat.coe_int_denom, int.coe_nat_zero, rat.coe_int_num, int.coe_nat_inj',
     sub_zero, multiplicity.get_one_right],
   refl,
@@ -244,13 +244,13 @@ have hn : n ≠ 0, from rat.mk_num_ne_zero_of_ne_zero hqz qdf,
 have hd : d ≠ 0, from rat.mk_denom_ne_zero_of_ne_zero hqz qdf,
 let ⟨c, hc1, hc2⟩ := rat.num_denom_mk hn hd qdf in
 begin
-  rw [padic_val_rat.nonzero hqz, padic_val_int.defn, padic_val_nat, dif_pos];
+  rw [padic_val_rat.of_ne_zero hqz, padic_val_int.of_ne_one_ne_zero, padic_val_nat,
+    dif_pos];
   simp [hc1, hc2, multiplicity.mul' (nat.prime_iff_prime_int.1 p_prime.1),
-    (ne.symm (ne_of_lt p_prime.1.one_lt)), hqz],
+    (ne.symm (ne_of_lt p_prime.1.one_lt)), hqz, pos_iff_ne_zero],
   simp_rw [int.coe_nat_multiplicity p q.denom],
   refl,
-  { rw pos_iff_ne_zero,
-    intro hq,
+  { intro hq,
     simp [hq] at hc2,
     exact hd hc2, },
   { intro hq,

From 3ed868ae8255da0df6a5e813193061eeda5be777 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 11 Mar 2022 17:13:12 -0600
Subject: [PATCH 29/54] added API lemmas and golfed long proof

---
 src/number_theory/padics/padic_norm.lean | 41 +++++++++++++-----------
 1 file changed, 22 insertions(+), 19 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 0840ef0dd84c8..74655e3a81422 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -156,7 +156,7 @@ lemma of_ne_zero {q : ℚ} (hq : q ≠ 0) : padic_val_rat p q =
 @[simp] protected lemma one : padic_val_rat p 1 = 0 := by simp [padic_val_rat, padic_val_int]
 
 /-- For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1. -/
-@[simp] lemma padic_val_rat_self (hp : 1 < p) : padic_val_rat p p = 1 :=
+@[simp] lemma self (hp : 1 < p) : padic_val_rat p p = 1 :=
 begin
   simp only [padic_val_rat, padic_val_int, rat.coe_nat_num, int.nat_abs_of_nat, rat.coe_nat_denom,
     padic_val_nat.one, int.coe_nat_zero, sub_zero, padic_val_nat.self hp],
@@ -164,17 +164,28 @@ begin
 end
 
 /-- The p-adic value of an integer `z ≠ 0` is the multiplicity of `p` in `z`. -/
-lemma padic_val_rat_of_int (z : ℤ) (hp : p ≠ 1) (hz : z ≠ 0) :
+lemma of_int {z : ℤ} (hp : p ≠ 1) :
+  padic_val_rat p (z : ℚ) = padic_val_int p z := by simp [padic_val_rat]
+
+/-- The p-adic value of an integer `z ≠ 0` is the multiplicity of `p` in `z`. -/
+lemma of_int_multiplicity (z : ℤ) (hp : p ≠ 1) (hz : z ≠ 0) :
   padic_val_rat p (z : ℚ) = (multiplicity (p : ℤ) z).get
     (finite_int_iff.2 ⟨hp, hz⟩) :=
+by rw [of_int hp, padic_val_int.of_ne_one_ne_zero hp hz]
+
+/-- The p-adic value of a rational `z ≠ 0` is the multiplicity of `p` in `z`. -/
+lemma multiplicity_sub_multiplicity {q : ℚ} (hp : p ≠ 1) (hq : q ≠ 0) :
+  padic_val_rat p q =
+  (multiplicity (p : ℤ) q.num).get (finite_int_iff.2 ⟨hp, rat.num_ne_zero_of_ne_zero hq⟩) -
+  (multiplicity p q.denom).get (by {rw <-finite_iff_dom, rw finite_nat_iff, refine (and_iff_left _).mpr hp, exact q.pos,}) :=
 begin
-  rw [padic_val_rat, padic_val_int.of_ne_one_ne_zero, padic_val_nat, dif_pos],
-  simp only [rat.coe_int_denom, int.coe_nat_zero, rat.coe_int_num, int.coe_nat_inj',
-    sub_zero, multiplicity.get_one_right],
+  rw [padic_val_rat.of_ne_zero hq, padic_val_int.of_ne_one_ne_zero hp, padic_val_nat, dif_pos],
   refl,
   simp [hp],
-  exact hp,
-  simp only [hp, ne.def, not_false_iff, rat.coe_int_num, true_and, hz],
+  exact q.pos,
+  -- library_search, -- fails, but shouldn't
+  intro h, apply hq,
+  exact rat.zero_of_num_zero h,
 end
 
 end padic_val_rat
@@ -244,18 +255,10 @@ have hn : n ≠ 0, from rat.mk_num_ne_zero_of_ne_zero hqz qdf,
 have hd : d ≠ 0, from rat.mk_denom_ne_zero_of_ne_zero hqz qdf,
 let ⟨c, hc1, hc2⟩ := rat.num_denom_mk hn hd qdf in
 begin
-  rw [padic_val_rat.of_ne_zero hqz, padic_val_int.of_ne_one_ne_zero, padic_val_nat,
-    dif_pos];
+  rw [padic_val_rat.multiplicity_sub_multiplicity];
   simp [hc1, hc2, multiplicity.mul' (nat.prime_iff_prime_int.1 p_prime.1),
     (ne.symm (ne_of_lt p_prime.1.one_lt)), hqz, pos_iff_ne_zero],
   simp_rw [int.coe_nat_multiplicity p q.denom],
-  refl,
-  { intro hq,
-    simp [hq] at hc2,
-    exact hd hc2, },
-  { intro hq,
-    simp [hq] at hc1,
-    exact hn hc1, },
 end
 
 /-- A rewrite lemma for `padic_val_rat p (q * r)` with conditions `q ≠ 0`, `r ≠ 0`. -/
@@ -595,7 +598,7 @@ The p-adic norm of `p` is `1/p` if `p > 1`.
 See also `padic_norm.padic_norm_p_of_prime` for a version that assumes `p` is prime.
 -/
 lemma padic_norm_p {p : ℕ} (hp : 1 < p) : padic_norm p p = 1 / p :=
-by simp [padic_norm, (show p ≠ 0, by linarith), padic_val_rat.padic_val_rat_self hp]
+by simp [padic_norm, (show p ≠ 0, by linarith), padic_val_rat.self hp]
 
 /--
 The p-adic norm of `p` is `1/p` if `p` is prime.
@@ -688,7 +691,7 @@ begin
   rw [if_neg _],
   { refine zpow_le_one_of_nonpos _ _,
     { exact_mod_cast le_of_lt hp.1.one_lt, },
-    { rw [padic_val_rat_of_int _ hp.1.ne_one hz, neg_nonpos],
+    { rw [padic_val_rat.of_int_multiplicity _ hp.1.ne_one hz, neg_nonpos],
       norm_cast, simp }},
   exact_mod_cast hz
 end
@@ -795,7 +798,7 @@ begin
   { norm_cast at hz,
     have : 0 ≤ (p^n : ℚ), {apply pow_nonneg, exact_mod_cast le_of_lt hp.1.pos },
     simp [hz, this] },
-  { rw [zpow_le_iff_le, neg_le_neg_iff, padic_val_rat_of_int _ hp.1.ne_one _],
+  { rw [zpow_le_iff_le, neg_le_neg_iff, padic_val_rat.of_int_multiplicity _ hp.1.ne_one _],
     { norm_cast,
       rw [← enat.coe_le_coe, enat.coe_get, ← multiplicity.pow_dvd_iff_le_multiplicity],
       simp },

From a656b63814e42122c0316c5f06253bcdade7d89e Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 11 Mar 2022 18:34:27 -0600
Subject: [PATCH 30/54] golfing

---
 src/number_theory/padics/padic_norm.lean    | 48 ++++++++++++++++-----
 src/number_theory/padics/padic_numbers.lean | 22 +++-------
 2 files changed, 44 insertions(+), 26 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 74655e3a81422..c7188f9b1a755 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -84,6 +84,14 @@ begin
   simp [padic_val_nat, neq_one, eq_zero_false],
 end
 
+lemma eq_zero_of_not_dvd {n : ℕ} (h : ¬ p ∣ n) : padic_val_nat p n = 0 :=
+begin
+  rw padic_val_nat,
+  split_ifs,
+  { simp [multiplicity_eq_zero_of_not_dvd h], },
+  refl,
+end
+
 end padic_val_nat
 
 /--
@@ -103,7 +111,7 @@ lemma of_ne_one_ne_zero {z : ℤ} (hp : p ≠ 1) (hz : z ≠ 0) : padic_val_int
   (multiplicity (p : ℤ) z).get (by {apply multiplicity.finite_int_iff.2, simp [hp, hz]}) :=
 begin
   rw [padic_val_int, padic_val_nat, dif_pos],
-  simp_rw  multiplicity.int.nat_abs p z,
+  simp_rw multiplicity.int.nat_abs p z,
   refl,
   simp [hp, hz],
   exact int.nat_abs_pos_of_ne_zero hz, -- TODO make simp lemma
@@ -123,6 +131,19 @@ by simp [padic_val_int]
 @[simp] lemma self (hp : 1 < p) : padic_val_int p p = 1 :=
 by simp [padic_val_int, padic_val_nat.self hp]
 
+/-- The p-adic value of an natural is its p-adic_value as an integer -/
+@[simp] lemma of_nat {n : ℕ} : padic_val_int p (n : ℤ) = padic_val_nat p n :=
+by simp [padic_val_int]
+
+lemma eq_zero_of_not_dvd {z : ℤ} (h : ¬ (p : ℤ) ∣ z) : padic_val_int p z = 0 :=
+begin
+  rw [padic_val_int, padic_val_nat],
+  split_ifs,
+  { simp_rw multiplicity.int.nat_abs,
+    simp [multiplicity_eq_zero_of_not_dvd h], },
+  refl,
+end
+
 end padic_val_int
 
 /--
@@ -163,17 +184,16 @@ begin
   refl,
 end
 
-/-- The p-adic value of an integer `z ≠ 0` is the multiplicity of `p` in `z`. -/
-lemma of_int {z : ℤ} (hp : p ≠ 1) :
-  padic_val_rat p (z : ℚ) = padic_val_int p z := by simp [padic_val_rat]
+/-- The p-adic value of an integer `z ≠ 0` is its p-adic_value as a rational -/
+@[simp] lemma of_int {z : ℤ} : padic_val_rat p (z : ℚ) = padic_val_int p z :=
+by simp [padic_val_rat]
 
 /-- The p-adic value of an integer `z ≠ 0` is the multiplicity of `p` in `z`. -/
 lemma of_int_multiplicity (z : ℤ) (hp : p ≠ 1) (hz : z ≠ 0) :
   padic_val_rat p (z : ℚ) = (multiplicity (p : ℤ) z).get
     (finite_int_iff.2 ⟨hp, hz⟩) :=
-by rw [of_int hp, padic_val_int.of_ne_one_ne_zero hp hz]
+by rw [of_int, padic_val_int.of_ne_one_ne_zero hp hz]
 
-/-- The p-adic value of a rational `z ≠ 0` is the multiplicity of `p` in `z`. -/
 lemma multiplicity_sub_multiplicity {q : ℚ} (hp : p ≠ 1) (hq : q ≠ 0) :
   padic_val_rat p q =
   (multiplicity (p : ℤ) q.num).get (finite_int_iff.2 ⟨hp, rat.num_ne_zero_of_ne_zero hq⟩) -
@@ -188,6 +208,11 @@ begin
   exact rat.zero_of_num_zero h,
 end
 
+/-- The p-adic value of an integer `z ≠ 0` is its p-adic_value as a rational -/
+@[simp] lemma of_nat {n : ℕ} : padic_val_rat p (n : ℚ) = padic_val_nat p n :=
+by simp [padic_val_rat, padic_val_int]
+
+
 end padic_val_rat
 
 section padic_val_nat
@@ -198,8 +223,8 @@ begin
   split_ifs; simp,
 end
 
-/-- `padic_val_rat` coincides with `padic_val_nat`. -/
-@[simp, norm_cast] lemma padic_val_rat_of_nat (p n : ℕ) :
+-- /-- `padic_val_rat` coincides with `padic_val_nat`. -/
+@[norm_cast] lemma padic_val_rat_of_nat (p n : ℕ) :
   ↑(padic_val_nat p n) = padic_val_rat p n :=
 by simp [padic_val_rat, padic_val_int]
 
@@ -691,9 +716,9 @@ begin
   rw [if_neg _],
   { refine zpow_le_one_of_nonpos _ _,
     { exact_mod_cast le_of_lt hp.1.one_lt, },
-    { rw [padic_val_rat.of_int_multiplicity _ hp.1.ne_one hz, neg_nonpos],
+    { rw [padic_val_rat.of_int, neg_nonpos],
       norm_cast, simp }},
-  exact_mod_cast hz
+  exact_mod_cast hz,
 end
 
 private lemma nonarchimedean_aux {q r : ℚ} (h : padic_val_rat p q ≤ padic_val_rat p r) :
@@ -798,7 +823,8 @@ begin
   { norm_cast at hz,
     have : 0 ≤ (p^n : ℚ), {apply pow_nonneg, exact_mod_cast le_of_lt hp.1.pos },
     simp [hz, this] },
-  { rw [zpow_le_iff_le, neg_le_neg_iff, padic_val_rat.of_int_multiplicity _ hp.1.ne_one _],
+  { rw [zpow_le_iff_le, neg_le_neg_iff, padic_val_rat.of_int,
+      padic_val_int.of_ne_one_ne_zero hp.1.ne_one _],
     { norm_cast,
       rw [← enat.coe_le_coe, enat.coe_get, ← multiplicity.pow_dvd_iff_le_multiplicity],
       simp },
diff --git a/src/number_theory/padics/padic_numbers.lean b/src/number_theory/padics/padic_numbers.lean
index f3b0d4713ac8d..4e0e929f056c9 100644
--- a/src/number_theory/padics/padic_numbers.lean
+++ b/src/number_theory/padics/padic_numbers.lean
@@ -556,7 +556,7 @@ begin
   { have := stationary_point_spec hne le_rfl (le_of_not_le hngen),
     rw ←this,
     apply hN,
-    exact le_rfl, assumption }
+    exact le_rfl, assumption },
 end
 
 protected lemma nonneg (q : ℚ_[p]) : 0 ≤ padic_norm_e q :=
@@ -865,20 +865,14 @@ theorem norm_rat_le_one : ∀ {q : ℚ} (hq : ¬ p ∣ q.denom), ∥(q : ℚ_[p]
         from mt rat.zero_iff_num_zero.1 hnz,
       rw [padic_norm_e.eq_padic_norm],
       norm_cast,
-      rw [padic_norm.eq_zpow_of_nonzero p hnz'],
-      simp only [padic_val_rat, padic_val_int, padic_val_nat, ne.def, neg_sub],
-      rw [dif_pos, dif_pos],
-      simp only [multiplicity_eq_zero_of_not_dvd, hq, not_false_iff, enat.get_zero,
-        int.coe_nat_zero, zero_sub, zpow_neg₀, zpow_coe_nat],
+      rw [padic_norm.eq_zpow_of_nonzero p hnz', padic_val_rat, neg_sub,
+        padic_val_nat.eq_zero_of_not_dvd hq],
       norm_cast,
-      rw ←zpow_neg_one,
-      apply zpow_le_one_of_nonpos,
+      rw [zero_sub, zpow_neg₀, zpow_coe_nat],
+      apply inv_le_one,
       { norm_cast,
         apply one_le_pow,
         exact hp.1.pos, },
-      { dec_trivial, },
-      exact ⟨ne_of_gt (hp.out).one_lt, int.nat_abs_pos_of_ne_zero hnz⟩,
-      exact ⟨ne_of_gt (hp.out).one_lt, hn⟩,
     end
 
 theorem norm_int_le_one (z : ℤ) : ∥(z : ℚ_[p])∥ ≤ 1 :=
@@ -904,11 +898,9 @@ begin
       apply dvd_zero },
     { norm_cast at H ⊢,
       convert zpow_zero _,
-      simp only [neg_eq_zero],
-      rw padic_val_rat.padic_val_rat_of_int _ hp.1.ne_one H,
+      rw [neg_eq_zero, padic_val_rat.of_int],
       norm_cast,
-      rw [← enat.coe_inj, enat.coe_get, nat.cast_zero],
-      apply multiplicity.multiplicity_eq_zero_of_not_dvd h } },
+      apply padic_val_int.eq_zero_of_not_dvd h, } },
   { rintro ⟨x, rfl⟩,
     push_cast,
     rw padic_norm_e.mul,

From 6870e233f3a6f3b89b5410c05f8c6852051f13b0 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 11 Mar 2022 18:36:29 -0600
Subject: [PATCH 31/54] delete nat_cast_nat_abs

Co-authored-by: Johan Commelin <johan@commelin.net>
---
 src/ring_theory/multiplicity.lean | 10 ----------
 1 file changed, 10 deletions(-)

diff --git a/src/ring_theory/multiplicity.lean b/src/ring_theory/multiplicity.lean
index f058e375cc955..d4d6f366382d9 100644
--- a/src/ring_theory/multiplicity.lean
+++ b/src/ring_theory/multiplicity.lean
@@ -57,16 +57,6 @@ begin
     apply _root_.le_antisymm; { apply nat.find_mono, norm_cast, simp } }
 end
 
-theorem nat_cast_nat_abs (a b : ℕ) :
-    multiplicity a (b : ℤ).nat_abs = multiplicity (a : ℤ) (b : ℤ) :=
-begin
-  apply part.ext',
-  { repeat { rw [← finite_iff_dom, finite_def] },
-    norm_cast },
-  { intros h1 h2,
-    apply _root_.le_antisymm; { apply nat.find_mono, norm_cast, simp } }
-end
-
 lemma not_finite_iff_forall {a b : α} : (¬ finite a b) ↔ ∀ n : ℕ, a ^ n ∣ b :=
 ⟨λ h n, nat.cases_on n (by { rw pow_zero, exact one_dvd _ }) (by simpa [finite, not_not] using h),
   by simp [finite, multiplicity, not_not]; tauto⟩

From 149184aa2890d5a31029a0f08b0c47266ada9850 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 11 Mar 2022 18:37:20 -0600
Subject: [PATCH 32/54] Update src/ring_theory/multiplicity.lean

Co-authored-by: Johan Commelin <johan@commelin.net>
---
 src/ring_theory/multiplicity.lean | 11 +++--------
 1 file changed, 3 insertions(+), 8 deletions(-)

diff --git a/src/ring_theory/multiplicity.lean b/src/ring_theory/multiplicity.lean
index d4d6f366382d9..59840ba943eb3 100644
--- a/src/ring_theory/multiplicity.lean
+++ b/src/ring_theory/multiplicity.lean
@@ -290,14 +290,9 @@ part.ext' (by simp only [multiplicity, enat.find, dvd_neg])
 theorem int.nat_abs (a : ℕ) (b : ℤ) :
     multiplicity a b.nat_abs = multiplicity (a : ℤ) b :=
 begin
-  have h := @int.nat_abs_eq_iff b b.nat_abs,
-  simp only [true_iff, eq_self_iff_true] at h,
-  cases h,
-  { conv_rhs { rw h },
-    apply nat_cast_nat_abs, },
-  { conv_rhs { rw h },
-    rw multiplicity.neg,
-    apply nat_cast_nat_abs, },
+  cases int.nat_abs_eq b with h h; conv_rhs { rw h },
+  { rw [int.coe_nat_multiplicity], },
+  { rw [multiplicity.neg, int.coe_nat_multiplicity], },
 end
 
 lemma multiplicity_add_of_gt {p a b : α} (h : multiplicity p b < multiplicity p a) :

From 52450867f97e74d2f55c1dcfb73996b854ae59a1 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 11 Mar 2022 18:40:36 -0600
Subject: [PATCH 33/54] fix line too long

---
 src/number_theory/padics/padic_norm.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index c7188f9b1a755..9baa41da5b788 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -197,7 +197,8 @@ by rw [of_int, padic_val_int.of_ne_one_ne_zero hp hz]
 lemma multiplicity_sub_multiplicity {q : ℚ} (hp : p ≠ 1) (hq : q ≠ 0) :
   padic_val_rat p q =
   (multiplicity (p : ℤ) q.num).get (finite_int_iff.2 ⟨hp, rat.num_ne_zero_of_ne_zero hq⟩) -
-  (multiplicity p q.denom).get (by {rw <-finite_iff_dom, rw finite_nat_iff, refine (and_iff_left _).mpr hp, exact q.pos,}) :=
+  (multiplicity p q.denom).get
+    (by {rw [←finite_iff_dom, finite_nat_iff, and_iff_right hp], exact q.pos,}) :=
 begin
   rw [padic_val_rat.of_ne_zero hq, padic_val_int.of_ne_one_ne_zero hp, padic_val_nat, dif_pos],
   refl,

From abf21f556facf1082f5116054b729c264e6e285b Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Fri, 11 Mar 2022 18:41:41 -0600
Subject: [PATCH 34/54] fix spaces

---
 src/number_theory/padics/padic_norm.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 9baa41da5b788..b72c6143d34a6 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -198,7 +198,7 @@ lemma multiplicity_sub_multiplicity {q : ℚ} (hp : p ≠ 1) (hq : q ≠ 0) :
   padic_val_rat p q =
   (multiplicity (p : ℤ) q.num).get (finite_int_iff.2 ⟨hp, rat.num_ne_zero_of_ne_zero hq⟩) -
   (multiplicity p q.denom).get
-    (by {rw [←finite_iff_dom, finite_nat_iff, and_iff_right hp], exact q.pos,}) :=
+    (by { rw [←finite_iff_dom, finite_nat_iff, and_iff_right hp], exact q.pos }) :=
 begin
   rw [padic_val_rat.of_ne_zero hq, padic_val_int.of_ne_one_ne_zero hp, padic_val_nat, dif_pos],
   refl,

From 6af58813f6e4185951626f93c3bf1762dc2c6554 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 12 Mar 2022 14:57:10 -0600
Subject: [PATCH 35/54] delete extraneous lemma

---
 src/number_theory/padics/padic_norm.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index b72c6143d34a6..533e441dda97f 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -166,12 +166,12 @@ by simp [padic_val_rat, padic_val_int]
 @[simp]
 protected lemma zero (m : nat) : padic_val_rat m 0 = 0 := by simp [padic_val_rat, padic_val_int]
 
-/--
-`padic_val_rat p q` for nonzero `q` is the difference in valuations of the numerator and
-denominator.
--/
-lemma of_ne_zero {q : ℚ} (hq : q ≠ 0) : padic_val_rat p q =
-  (padic_val_int p q.num : ℤ) - (padic_val_nat p q.denom : ℤ) := by rw padic_val_rat
+-- /--
+-- `padic_val_rat p q` for nonzero `q` is the difference in valuations of the numerator and
+-- denominator.
+-- -/
+-- lemma of_ne_zero {q : ℚ} (hq : q ≠ 0) : padic_val_rat p q =
+--   (padic_val_int p q.num : ℤ) - (padic_val_nat p q.denom : ℤ) := by rw padic_val_rat
 
 /-- `padic_val_rat p 1` is 0 for any `p`. -/
 @[simp] protected lemma one : padic_val_rat p 1 = 0 := by simp [padic_val_rat, padic_val_int]
@@ -200,7 +200,7 @@ lemma multiplicity_sub_multiplicity {q : ℚ} (hp : p ≠ 1) (hq : q ≠ 0) :
   (multiplicity p q.denom).get
     (by { rw [←finite_iff_dom, finite_nat_iff, and_iff_right hp], exact q.pos }) :=
 begin
-  rw [padic_val_rat.of_ne_zero hq, padic_val_int.of_ne_one_ne_zero hp, padic_val_nat, dif_pos],
+  rw [padic_val_rat, padic_val_int.of_ne_one_ne_zero hp, padic_val_nat, dif_pos],
   refl,
   simp [hp],
   exact q.pos,

From f9b0bfc587239f5d35dd4f3b1c61f9feb55edc77 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 12 Mar 2022 15:09:58 -0600
Subject: [PATCH 36/54] trying to please simp linter

---
 src/number_theory/padics/padic_norm.lean | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 533e441dda97f..e4bb8dc7944d4 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -128,7 +128,7 @@ by simp [padic_val_int]
 by simp [padic_val_int]
 
 /-- For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1. -/
-@[simp] lemma self (hp : 1 < p) : padic_val_int p p = 1 :=
+lemma self (hp : 1 < p) : padic_val_int p p = 1 :=
 by simp [padic_val_int, padic_val_nat.self hp]
 
 /-- The p-adic value of an natural is its p-adic_value as an integer -/
@@ -176,14 +176,6 @@ protected lemma zero (m : nat) : padic_val_rat m 0 = 0 := by simp [padic_val_rat
 /-- `padic_val_rat p 1` is 0 for any `p`. -/
 @[simp] protected lemma one : padic_val_rat p 1 = 0 := by simp [padic_val_rat, padic_val_int]
 
-/-- For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1. -/
-@[simp] lemma self (hp : 1 < p) : padic_val_rat p p = 1 :=
-begin
-  simp only [padic_val_rat, padic_val_int, rat.coe_nat_num, int.nat_abs_of_nat, rat.coe_nat_denom,
-    padic_val_nat.one, int.coe_nat_zero, sub_zero, padic_val_nat.self hp],
-  refl,
-end
-
 /-- The p-adic value of an integer `z ≠ 0` is its p-adic_value as a rational -/
 @[simp] lemma of_int {z : ℤ} : padic_val_rat p (z : ℚ) = padic_val_int p z :=
 by simp [padic_val_rat]
@@ -202,7 +194,7 @@ lemma multiplicity_sub_multiplicity {q : ℚ} (hp : p ≠ 1) (hq : q ≠ 0) :
 begin
   rw [padic_val_rat, padic_val_int.of_ne_one_ne_zero hp, padic_val_nat, dif_pos],
   refl,
-  simp [hp],
+  simp only [hp, ne.def, not_false_iff, true_and],
   exact q.pos,
   -- library_search, -- fails, but shouldn't
   intro h, apply hq,
@@ -213,6 +205,13 @@ end
 @[simp] lemma of_nat {n : ℕ} : padic_val_rat p (n : ℚ) = padic_val_nat p n :=
 by simp [padic_val_rat, padic_val_int]
 
+-- /-- For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1. -/
+-- @[simp] lemma self (hp : 1 < p) : padic_val_rat p p = 1 :=
+-- begin
+--   simp,
+--   rw padic_val_nat.self hp, -- Why does this fail to fire with simp?
+--   refl,
+-- end
 
 end padic_val_rat
 

From 079931466cab1c73273cdeaaff642f021643015e Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 12 Mar 2022 15:20:54 -0600
Subject: [PATCH 37/54] remove fixed todo about library_search

---
 src/number_theory/padics/padic_norm.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index e4bb8dc7944d4..558bd6365017b 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -196,9 +196,7 @@ begin
   refl,
   simp only [hp, ne.def, not_false_iff, true_and],
   exact q.pos,
-  -- library_search, -- fails, but shouldn't
-  intro h, apply hq,
-  exact rat.zero_of_num_zero h,
+  exact rat.num_ne_zero_of_ne_zero hq,
 end
 
 /-- The p-adic value of an integer `z ≠ 0` is its p-adic_value as a rational -/

From df02270f73c57b86dc6b7b814edba60eb115f6d6 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 12 Mar 2022 15:24:44 -0600
Subject: [PATCH 38/54] experimenting with self

---
 src/number_theory/padics/padic_norm.lean | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 558bd6365017b..1a285e0563154 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -203,13 +203,13 @@ end
 @[simp] lemma of_nat {n : ℕ} : padic_val_rat p (n : ℚ) = padic_val_nat p n :=
 by simp [padic_val_rat, padic_val_int]
 
--- /-- For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1. -/
--- @[simp] lemma self (hp : 1 < p) : padic_val_rat p p = 1 :=
--- begin
---   simp,
---   rw padic_val_nat.self hp, -- Why does this fail to fire with simp?
---   refl,
--- end
+/-- For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1. -/
+lemma self (hp : 1 < p) : padic_val_rat p p = 1 :=
+begin
+  simp only [of_nat],
+  rw padic_val_nat.self hp, -- Why does this fail to fire with simp above?
+  refl,
+end
 
 end padic_val_rat
 
@@ -621,7 +621,7 @@ The p-adic norm of `p` is `1/p` if `p > 1`.
 See also `padic_norm.padic_norm_p_of_prime` for a version that assumes `p` is prime.
 -/
 lemma padic_norm_p {p : ℕ} (hp : 1 < p) : padic_norm p p = 1 / p :=
-by simp [padic_norm, (show p ≠ 0, by linarith), padic_val_rat.self hp]
+by simp [padic_norm, (show p ≠ 0, by linarith), padic_val_nat.self hp]
 
 /--
 The p-adic norm of `p` is `1/p` if `p` is prime.

From 283718bc29e7d18ddb3402716b4ae48c1486fe69 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 12 Mar 2022 15:26:39 -0600
Subject: [PATCH 39/54] simp only

---
 src/number_theory/padics/padic_norm.lean | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 1a285e0563154..55d0869376e3d 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -166,13 +166,6 @@ by simp [padic_val_rat, padic_val_int]
 @[simp]
 protected lemma zero (m : nat) : padic_val_rat m 0 = 0 := by simp [padic_val_rat, padic_val_int]
 
--- /--
--- `padic_val_rat p q` for nonzero `q` is the difference in valuations of the numerator and
--- denominator.
--- -/
--- lemma of_ne_zero {q : ℚ} (hq : q ≠ 0) : padic_val_rat p q =
---   (padic_val_int p q.num : ℤ) - (padic_val_nat p q.denom : ℤ) := by rw padic_val_rat
-
 /-- `padic_val_rat p 1` is 0 for any `p`. -/
 @[simp] protected lemma one : padic_val_rat p 1 = 0 := by simp [padic_val_rat, padic_val_int]
 
@@ -207,7 +200,7 @@ by simp [padic_val_rat, padic_val_int]
 lemma self (hp : 1 < p) : padic_val_rat p p = 1 :=
 begin
   simp only [of_nat],
-  rw padic_val_nat.self hp, -- Why does this fail to fire with simp above?
+  rw padic_val_nat.self hp, -- Why does simp fail to fire this here?
   refl,
 end
 

From a5fae2fa896058251d347565f8eedff0b3630ca7 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 12 Mar 2022 16:05:55 -0600
Subject: [PATCH 40/54] golf

---
 src/number_theory/padics/padic_norm.lean | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 55d0869376e3d..56dcdbbdfe8ef 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -197,12 +197,7 @@ end
 by simp [padic_val_rat, padic_val_int]
 
 /-- For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1. -/
-lemma self (hp : 1 < p) : padic_val_rat p p = 1 :=
-begin
-  simp only [of_nat],
-  rw padic_val_nat.self hp, -- Why does simp fail to fire this here?
-  refl,
-end
+lemma self (hp : 1 < p) : padic_val_rat p p = 1 := by simp [of_nat, hp]
 
 end padic_val_rat
 

From 281308b4172489fb47128973c7c7f000e1795d02 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 12 Mar 2022 16:11:29 -0600
Subject: [PATCH 41/54] golf

---
 src/number_theory/padics/padic_norm.lean | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 56dcdbbdfe8ef..2c597fae8d84d 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -203,11 +203,7 @@ end padic_val_rat
 
 section padic_val_nat
 
-lemma zero_le_padic_val_rat_of_nat (p n : ℕ) : 0 ≤ padic_val_rat p n :=
-begin
-  unfold padic_val_rat padic_val_int padic_val_nat,
-  split_ifs; simp,
-end
+lemma zero_le_padic_val_rat_of_nat (p n : ℕ) : 0 ≤ padic_val_rat p n := by simp
 
 -- /-- `padic_val_rat` coincides with `padic_val_nat`. -/
 @[norm_cast] lemma padic_val_rat_of_nat (p n : ℕ) :

From 807122dba54789658f12e0863be9c97f4ae8d8a4 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 19 Mar 2022 17:09:46 -0500
Subject: [PATCH 42/54] minor cleanup

---
 src/number_theory/padics/padic_norm.lean | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 2c597fae8d84d..03ce63182269f 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -114,13 +114,11 @@ begin
   simp_rw multiplicity.int.nat_abs p z,
   refl,
   simp [hp, hz],
-  exact int.nat_abs_pos_of_ne_zero hz, -- TODO make simp lemma
-  -- see nat_abs_ne_zero (and make that a simp lemma too)
+  exact int.nat_abs_pos_of_ne_zero hz,
 end
 
 /-- `padic_val_int p 0` is 0 for any `p`. -/
-@[simp]
-protected lemma zero : padic_val_int p 0 = 0 :=
+@[simp] protected lemma zero : padic_val_int p 0 = 0 :=
 by simp [padic_val_int]
 
 /-- `padic_val_int p 1` is 0 for any `p`. -/
@@ -128,7 +126,7 @@ by simp [padic_val_int]
 by simp [padic_val_int]
 
 /-- For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1. -/
-lemma self (hp : 1 < p) : padic_val_int p p = 1 :=
+@[simp] lemma self (hp : 1 < p) : padic_val_int p p = 1 :=
 by simp [padic_val_int, padic_val_nat.self hp]
 
 /-- The p-adic value of an natural is its p-adic_value as an integer -/

From b45e3551d9458437f6e7c010cdb408f41d165a55 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sat, 19 Mar 2022 17:13:50 -0500
Subject: [PATCH 43/54] undo weird change

---
 src/number_theory/padics/padic_norm.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 03ce63182269f..f0c90c61163e5 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -475,13 +475,13 @@ end
 lemma pow_succ_padic_val_nat_not_dvd {p n : ℕ} [hp : fact (nat.prime p)] (hn : 0 < n) :
   ¬ p ^ (padic_val_nat p n + 1) ∣ n :=
 begin
-  { rw multiplicity.pow_dvd_iff_le_multiplicity,
-    rw padic_val_nat_def hn,
-    { rw [nat.cast_add, enat.coe_get],
-      simp only [nat.cast_one, not_le],
-      exact enat.lt_add_one (ne_top_iff_finite.mpr
-        (finite_nat_iff.mpr ⟨(fact.elim hp).ne_one, hn⟩)), },
-    { apply_instance } }
+  rw multiplicity.pow_dvd_iff_le_multiplicity,
+  rw padic_val_nat_def hn,
+  { rw [nat.cast_add, enat.coe_get],
+    simp only [nat.cast_one, not_le],
+    exact enat.lt_add_one (ne_top_iff_finite.mpr
+      (finite_nat_iff.mpr ⟨(fact.elim hp).ne_one, hn⟩)), },
+  { apply_instance }
 end
 
 lemma padic_val_nat_primes {p q : ℕ} [p_prime : fact p.prime] [q_prime : fact q.prime]

From 5af66d392c04d20ab7d17ca4b5c2ad786641cc77 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Mon, 21 Mar 2022 00:14:29 -0500
Subject: [PATCH 44/54] undo simp

---
 src/number_theory/padics/padic_norm.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index f0c90c61163e5..8cb78460ff419 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -126,7 +126,7 @@ by simp [padic_val_int]
 by simp [padic_val_int]
 
 /-- For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1. -/
-@[simp] lemma self (hp : 1 < p) : padic_val_int p p = 1 :=
+lemma self (hp : 1 < p) : padic_val_int p p = 1 :=
 by simp [padic_val_int, padic_val_nat.self hp]
 
 /-- The p-adic value of an natural is its p-adic_value as an integer -/

From 947e15f43d4850d8d72be8dd316e7ff43e35f814 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Mon, 21 Mar 2022 00:18:01 -0500
Subject: [PATCH 45/54] rearrange lemma

---
 src/number_theory/padics/padic_norm.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 8cb78460ff419..a9eef8463646a 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -125,14 +125,14 @@ by simp [padic_val_int]
 @[simp] protected lemma one : padic_val_int p 1 = 0 :=
 by simp [padic_val_int]
 
-/-- For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1. -/
-lemma self (hp : 1 < p) : padic_val_int p p = 1 :=
-by simp [padic_val_int, padic_val_nat.self hp]
-
 /-- The p-adic value of an natural is its p-adic_value as an integer -/
 @[simp] lemma of_nat {n : ℕ} : padic_val_int p (n : ℤ) = padic_val_nat p n :=
 by simp [padic_val_int]
 
+/-- For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1. -/
+lemma self (hp : 1 < p) : padic_val_int p p = 1 :=
+by simp [padic_val_nat.self hp]
+
 lemma eq_zero_of_not_dvd {z : ℤ} (h : ¬ (p : ℤ) ∣ z) : padic_val_int p z = 0 :=
 begin
   rw [padic_val_int, padic_val_nat],

From 132766731d9d085af07b5a3c1a0da215209ebbdd Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 3 Apr 2022 13:39:39 -0500
Subject: [PATCH 46/54] fix docstring

---
 src/number_theory/padics/padic_norm.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index a9eef8463646a..cae4fce3e1249 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -129,7 +129,7 @@ by simp [padic_val_int]
 @[simp] lemma of_nat {n : ℕ} : padic_val_int p (n : ℤ) = padic_val_nat p n :=
 by simp [padic_val_int]
 
-/-- For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1. -/
+/-- For `p ≠ 0, p ≠ 1, `padic_val_int p p` is 1. -/
 lemma self (hp : 1 < p) : padic_val_int p p = 1 :=
 by simp [padic_val_nat.self hp]
 

From a93bb746a82c717673daa5e626dbbe44ef8255e9 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 3 Apr 2022 13:46:06 -0500
Subject: [PATCH 47/54] delete duplicate lemma

---
 src/number_theory/padics/padic_norm.lean | 17 +++--------------
 1 file changed, 3 insertions(+), 14 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index cae4fce3e1249..75a33ead73b5c 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -442,22 +442,11 @@ end padic_val_nat
 
 section padic_val_nat
 
-/-- If a prime doesn't appear in `n`, `padic_val_nat p n` is `0`. -/
-lemma padic_val_nat_of_not_dvd {p : ℕ} [fact p.prime] {n : ℕ} (not_dvd : ¬(p ∣ n)) :
-  padic_val_nat p n = 0 :=
-begin
-  by_cases hn : n = 0,
-  { subst hn, simp at not_dvd, trivial, },
-  { rw padic_val_nat_def (nat.pos_of_ne_zero hn),
-    exact (@multiplicity.unique' _ _ _ p n 0 (by simp) (by simpa using not_dvd)).symm,
-    assumption, },
-end
-
 lemma dvd_of_one_le_padic_val_nat {n p : nat} [prime : fact p.prime] (hp : 1 ≤ padic_val_nat p n) :
   p ∣ n :=
 begin
   by_contra h,
-  rw padic_val_nat_of_not_dvd h at hp,
+  rw padic_val_nat.eq_zero_of_not_dvd h at hp,
   exact lt_irrefl 0 (lt_of_lt_of_le zero_lt_one hp),
 end
 
@@ -486,7 +475,7 @@ end
 
 lemma padic_val_nat_primes {p q : ℕ} [p_prime : fact p.prime] [q_prime : fact q.prime]
   (neq : p ≠ q) : padic_val_nat p q = 0 :=
-@padic_val_nat_of_not_dvd p p_prime q $
+@padic_val_nat.eq_zero_of_not_dvd p q $
 (not_congr (iff.symm (prime_dvd_prime_iff_eq p_prime.1 q_prime.1))).mp neq
 
 protected lemma padic_val_nat.div' {p : ℕ} [p_prime : fact p.prime] :
@@ -500,7 +489,7 @@ protected lemma padic_val_nat.div' {p : ℕ} [p_prime : fact p.prime] :
     { rw [hc, mul_zero] },
     { rw padic_val_nat.mul,
       { suffices : ¬ p ∣ (n+1),
-        { rw [padic_val_nat_of_not_dvd this, zero_add] },
+        { rw [padic_val_nat.eq_zero_of_not_dvd this, zero_add] },
         contrapose! cpm,
         exact p_prime.1.dvd_iff_not_coprime.mp cpm },
       { exact nat.succ_ne_zero _ },

From a55921d406afc05eebcc607b11dc063bcac0c98b Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 3 Apr 2022 14:01:01 -0500
Subject: [PATCH 48/54] add todos

---
 src/number_theory/padics/padic_norm.lean | 35 ++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 75a33ead73b5c..7447dae85b395 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -552,6 +552,41 @@ end
 
 end padic_val_nat
 
+section padic_val_int
+variables (p : ℕ) [p_prime : fact p.prime]
+
+lemma padic_val_int_dvd_iff (p : ℕ) [fact p.prime] (n : ℕ) (a : ℤ) :
+  ↑p^n ∣ a ↔ a = 0 ∨ n ≤ padic_val_int p a :=
+begin
+  sorry,
+end
+
+lemma padic_val_int_dvd (p : ℕ) [fact p.prime] (a : ℤ) : ↑p^(padic_val_int p a) ∣ a :=
+begin
+  sorry,
+end
+
+lemma padic_val_int_eq_one (p : ℕ) [fact p.prime] : padic_val_int p p = 1 :=
+begin
+  apply padic_val_int.self,
+  exact _inst_1.out.one_lt,
+end
+
+lemma padic_val_int_add_of_mul (p : ℕ) [fact p.prime] {a b : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) :
+  padic_val_int p (a*b) = padic_val_int p a + padic_val_int p b :=
+begin
+  sorry,
+end
+
+lemma padic_val_int_succ_mul_p (p : ℕ) [fact p.prime] (a : ℤ) (ha : a ≠ 0) :
+  padic_val_int p (a * p) = (padic_val_int p a) + 1 :=
+begin
+  sorry,
+end
+
+end padic_val_int
+
+
 /--
 If `q ≠ 0`, the p-adic norm of a rational `q` is `p ^ (-(padic_val_rat p q))`.
 If `q = 0`, the p-adic norm of `q` is 0.

From 193a8b7ac081f029e1befb625e59de17059660cb Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Wed, 13 Apr 2022 09:45:28 -0500
Subject: [PATCH 49/54] fix bug

---
 src/number_theory/padics/padic_norm.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 9d1f8364867a5..049c170604196 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -258,7 +258,8 @@ protected lemma defn {q : ℚ} {n d : ℤ} (hqz : q ≠ 0) (qdf : q = n /. d) :
     λ hd, by simp * at *⟩) :=
 have hd : d ≠ 0, from rat.mk_denom_ne_zero_of_ne_zero hqz qdf,
 let ⟨c, hc1, hc2⟩ := rat.num_denom_mk hd qdf in
-by rw [padic_val_rat, dif_pos];
+begin
+  rw [padic_val_rat.multiplicity_sub_multiplicity];
   simp [hc1, hc2, multiplicity.mul' (nat.prime_iff_prime_int.1 p_prime.1),
     (ne.symm (ne_of_lt p_prime.1.one_lt)), hqz, pos_iff_ne_zero],
   simp_rw [int.coe_nat_multiplicity p q.denom],

From 5ff0158d2759de9d468e70250dd6e5d457fc4cfe Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Wed, 13 Apr 2022 10:54:44 -0500
Subject: [PATCH 50/54] solve todos

---
 src/number_theory/padics/padic_norm.lean | 43 ++++++++++++++++++++----
 1 file changed, 37 insertions(+), 6 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 049c170604196..0b4175b1e0275 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -478,6 +478,28 @@ begin
   { apply_instance }
 end
 
+lemma padic_val_nat_dvd_iff (p : ℕ) [fact p.prime] (n : ℕ) (a : ℕ) :
+  p^n ∣ a ↔ a = 0 ∨ n ≤ padic_val_nat p a :=
+begin
+  split,
+  { rw pow_dvd_iff_le_multiplicity,
+    rw padic_val_nat,
+    split_ifs,
+    rw enat.coe_le_iff,
+    intro hn,
+    right,
+    apply hn,
+    have : p ≠ 1, exact _inst_1.out.ne_one,
+    simp [this] at h,
+    rw h,
+    simp, },
+  { intro h,
+    cases h,
+    rw h,
+    exact dvd_zero (p ^ n),
+    exact dvd_trans (pow_dvd_pow p h) pow_padic_val_nat_dvd, },
+end
+
 lemma padic_val_nat_primes {p q : ℕ} [p_prime : fact p.prime] [q_prime : fact q.prime]
   (neq : p ≠ q) : padic_val_nat p q = 0 :=
 @padic_val_nat.eq_zero_of_not_dvd p q $
@@ -562,13 +584,13 @@ variables (p : ℕ) [p_prime : fact p.prime]
 
 lemma padic_val_int_dvd_iff (p : ℕ) [fact p.prime] (n : ℕ) (a : ℤ) :
   ↑p^n ∣ a ↔ a = 0 ∨ n ≤ padic_val_int p a :=
-begin
-  sorry,
-end
+by rw [padic_val_int, ←int.nat_abs_eq_zero, ←padic_val_nat_dvd_iff, ←int.coe_nat_dvd_left,
+       int.coe_nat_pow]
 
 lemma padic_val_int_dvd (p : ℕ) [fact p.prime] (a : ℤ) : ↑p^(padic_val_int p a) ∣ a :=
 begin
-  sorry,
+  rw padic_val_int_dvd_iff,
+  simp only [le_refl, or_true],
 end
 
 lemma padic_val_int_eq_one (p : ℕ) [fact p.prime] : padic_val_int p p = 1 :=
@@ -580,13 +602,22 @@ end
 lemma padic_val_int_add_of_mul (p : ℕ) [fact p.prime] {a b : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) :
   padic_val_int p (a*b) = padic_val_int p a + padic_val_int p b :=
 begin
-  sorry,
+  simp_rw padic_val_int,
+  rw int.nat_abs_mul,
+  rw padic_val_nat.mul,
+  exact int.nat_abs_ne_zero.mpr ha,
+  exact int.nat_abs_ne_zero.mpr hb,
 end
 
 lemma padic_val_int_succ_mul_p (p : ℕ) [fact p.prime] (a : ℤ) (ha : a ≠ 0) :
   padic_val_int p (a * p) = (padic_val_int p a) + 1 :=
 begin
-  sorry,
+  rw padic_val_int_add_of_mul,
+  congr,
+  simp only [eq_self_iff_true, padic_val_int.of_nat, padic_val_nat_self],
+  assumption,
+  simp only [int.coe_nat_eq_zero, ne.def],
+  exact (_inst_1.out).ne_zero,
 end
 
 end padic_val_int

From c3e1c59347ff8b82d6e7325f972579fe1ba773fb Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Wed, 13 Apr 2022 11:15:11 -0500
Subject: [PATCH 51/54] no auto vars

---
 src/number_theory/padics/padic_norm.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 0b4175b1e0275..aef65a21a669b 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -593,13 +593,13 @@ begin
   simp only [le_refl, or_true],
 end
 
-lemma padic_val_int_eq_one (p : ℕ) [fact p.prime] : padic_val_int p p = 1 :=
+lemma padic_val_int_self (p : ℕ) [pp : fact p.prime] : padic_val_int p p = 1 :=
 begin
   apply padic_val_int.self,
-  exact _inst_1.out.one_lt,
+  exact pp.out.one_lt,
 end
 
-lemma padic_val_int_add_of_mul (p : ℕ) [fact p.prime] {a b : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) :
+lemma padic_val_int.mul (p : ℕ) [fact p.prime] {a b : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) :
   padic_val_int p (a*b) = padic_val_int p a + padic_val_int p b :=
 begin
   simp_rw padic_val_int,
@@ -609,15 +609,15 @@ begin
   exact int.nat_abs_ne_zero.mpr hb,
 end
 
-lemma padic_val_int_succ_mul_p (p : ℕ) [fact p.prime] (a : ℤ) (ha : a ≠ 0) :
+lemma padic_val_int_mul_eq_succ (p : ℕ) [pp : fact p.prime] (a : ℤ) (ha : a ≠ 0) :
   padic_val_int p (a * p) = (padic_val_int p a) + 1 :=
 begin
-  rw padic_val_int_add_of_mul,
+  rw padic_val_int.mul,
   congr,
   simp only [eq_self_iff_true, padic_val_int.of_nat, padic_val_nat_self],
   assumption,
   simp only [int.coe_nat_eq_zero, ne.def],
-  exact (_inst_1.out).ne_zero,
+  exact (pp.out).ne_zero,
 end
 
 end padic_val_int

From 59514ab7413f5cbb0dde7fb047ac50a901bce1d6 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Thu, 14 Apr 2022 05:04:36 -0500
Subject: [PATCH 52/54] remove unnecessary argument

---
 src/number_theory/padics/padic_norm.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index aef65a21a669b..dc00f69ea9a1e 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -447,7 +447,7 @@ end padic_val_nat
 
 section padic_val_nat
 
-lemma dvd_of_one_le_padic_val_nat {n p : nat} [prime : fact p.prime] (hp : 1 ≤ padic_val_nat p n) :
+lemma dvd_of_one_le_padic_val_nat {n p : nat} (hp : 1 ≤ padic_val_nat p n) :
   p ∣ n :=
 begin
   by_contra h,

From 987b7ea098566e4c01eedb05a61caf7988c1c2f6 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Thu, 14 Apr 2022 07:38:32 -0500
Subject: [PATCH 53/54] golf

---
 src/number_theory/padics/padic_norm.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index dc00f69ea9a1e..8e0d016ac35df 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -478,7 +478,7 @@ begin
   { apply_instance }
 end
 
-lemma padic_val_nat_dvd_iff (p : ℕ) [fact p.prime] (n : ℕ) (a : ℕ) :
+lemma padic_val_nat_dvd_iff (p : ℕ) [hp :fact p.prime] (n : ℕ) (a : ℕ) :
   p^n ∣ a ↔ a = 0 ∨ n ≤ padic_val_nat p a :=
 begin
   split,
@@ -489,8 +489,7 @@ begin
     intro hn,
     right,
     apply hn,
-    have : p ≠ 1, exact _inst_1.out.ne_one,
-    simp [this] at h,
+    simp [hp.out.ne_one] at h,
     rw h,
     simp, },
   { intro h,

From f05482ba44ad2f5c6d220c08a5c98d344e360f19 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Thu, 14 Apr 2022 07:39:47 -0500
Subject: [PATCH 54/54] golf

---
 src/number_theory/padics/padic_norm.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 8e0d016ac35df..2f2e56389113a 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -603,9 +603,8 @@ lemma padic_val_int.mul (p : ℕ) [fact p.prime] {a b : ℤ} (ha : a ≠ 0) (hb
 begin
   simp_rw padic_val_int,
   rw int.nat_abs_mul,
-  rw padic_val_nat.mul,
-  exact int.nat_abs_ne_zero.mpr ha,
-  exact int.nat_abs_ne_zero.mpr hb,
+  rw padic_val_nat.mul;
+  rwa int.nat_abs_ne_zero,
 end
 
 lemma padic_val_int_mul_eq_succ (p : ℕ) [pp : fact p.prime] (a : ℤ) (ha : a ≠ 0) :