diff --git a/src/number_theory/padics/padic_integers.lean b/src/number_theory/padics/padic_integers.lean
index 7543b9e3de9c3..3a151d38e601a 100644
--- a/src/number_theory/padics/padic_integers.lean
+++ b/src/number_theory/padics/padic_integers.lean
@@ -56,7 +56,9 @@ def padic_int (p : ℕ) [fact p.prime] := {x : ℚ_[p] // ∥x∥ ≤ 1}
 notation `ℤ_[`p`]` := padic_int p
 
 namespace padic_int
+
 /-! ### Ring structure and coercion to `ℚ_[p]` -/
+
 variables {p : ℕ} [fact p.prime]
 
 instance : has_coe ℤ_[p] ℚ_[p] := ⟨subtype.val⟩
@@ -156,8 +158,8 @@ def of_int_seq (seq : ℕ → ℤ) (h : is_cau_seq (padic_norm p) (λ n, seq n))
 end padic_int
 
 namespace padic_int
-/-!
-### Instances
+
+/-! ### Instances
 
 We now show that `ℤ_[p]` is a
 * complete metric space
@@ -202,7 +204,9 @@ function.injective.is_domain (subring p).subtype subtype.coe_injective
 end padic_int
 
 namespace padic_int
+
 /-! ### Norm -/
+
 variables {p : ℕ} [fact p.prime]
 
 lemma norm_le_one (z : ℤ_[p]) : ∥z∥ ≤ 1 := z.2
@@ -260,8 +264,8 @@ end padic_int
 
 namespace padic_int
 
-variables (p : ℕ) [hp_prime : fact p.prime]
-include hp_prime
+variables (p : ℕ) [hp : fact p.prime]
+include hp
 
 lemma exists_pow_neg_lt {ε : ℝ} (hε : 0 < ε) :
   ∃ (k : ℕ), ↑p ^ -((k : ℕ) : ℤ) < ε :=
@@ -274,8 +278,8 @@ begin
     norm_cast,
     apply le_of_lt,
     convert nat.lt_pow_self _ _ using 1,
-    exact hp_prime.1.one_lt },
-  { exact_mod_cast hp_prime.1.pos }
+    exact hp.1.one_lt },
+  { exact_mod_cast hp.1.pos }
 end
 
 lemma exists_pow_neg_lt_rat {ε : ℚ} (hε : 0 < ε) :
@@ -289,13 +293,13 @@ end
 
 variable {p}
 
-lemma norm_int_lt_one_iff_dvd (k : ℤ) : ∥(k : ℤ_[p])∥ < 1 ↔ ↑p ∣ k :=
+lemma norm_int_lt_one_iff_dvd (k : ℤ) : ∥(k : ℤ_[p])∥ < 1 ↔ (p : ℤ) ∣ k :=
 suffices ∥(k : ℚ_[p])∥ < 1 ↔ ↑p ∣ k, by rwa norm_int_cast_eq_padic_norm,
 padic_norm_e.norm_int_lt_one_iff_dvd k
 
-lemma norm_int_le_pow_iff_dvd {k : ℤ} {n : ℕ} : ∥(k : ℤ_[p])∥ ≤ ((↑p)^(-n : ℤ)) ↔ ↑p^n ∣ k :=
-suffices ∥(k : ℚ_[p])∥ ≤ ((↑p)^(-n : ℤ)) ↔ ↑(p^n) ∣ k, by simpa [norm_int_cast_eq_padic_norm],
-padic_norm_e.norm_int_le_pow_iff_dvd _ _
+lemma norm_int_le_pow_iff_dvd {k : ℤ} {n : ℕ} : ∥(k : ℤ_[p])∥ ≤ p ^ (-n : ℤ) ↔ (p^n : ℤ) ∣ k :=
+suffices ∥(k : ℚ_[p])∥ ≤ ((↑p)^(-n : ℤ)) ↔ ↑(p^n) ∣ k,
+by simpa [norm_int_cast_eq_padic_norm], padic_norm_e.norm_int_le_pow_iff_dvd _ _
 
 /-! ### Valuation on `ℤ_[p]` -/
 
@@ -323,31 +327,32 @@ lemma valuation_nonneg (x : ℤ_[p]) : 0 ≤ x.valuation :=
 begin
   by_cases hx : x = 0,
   { simp [hx] },
-  have h : (1 : ℝ) < p := by exact_mod_cast hp_prime.1.one_lt,
+  have h : (1 : ℝ) < p := by exact_mod_cast hp.1.one_lt,
   rw [← neg_nonpos, ← (zpow_strict_mono h).le_iff_le],
   show (p : ℝ) ^ -valuation x ≤ p ^ 0,
   rw [← norm_eq_pow_val hx],
-  simpa using x.property,
+  simpa using x.property
 end
 
 @[simp] lemma valuation_p_pow_mul (n : ℕ) (c : ℤ_[p]) (hc : c ≠ 0) :
   (↑p ^ n * c).valuation = n + c.valuation :=
 begin
-  have : ∥↑p ^ n * c∥ = ∥(p ^ n : ℤ_[p])∥ * ∥c∥,
+  have : ∥(↑p ^ n * c)∥ = ∥(p ^ n : ℤ_[p])∥ * ∥c∥,
   { exact norm_mul _ _ },
-  have aux : ↑p ^ n * c ≠ 0,
+  have aux : (↑p ^ n * c) ≠ 0,
   { contrapose! hc, rw mul_eq_zero at hc, cases hc,
-    { refine (hp_prime.1.ne_zero _).elim,
+    { refine (hp.1.ne_zero _).elim,
       exact_mod_cast (pow_eq_zero hc) },
     { exact hc } },
   rwa [norm_eq_pow_val aux, norm_p_pow, norm_eq_pow_val hc,
       ← zpow_add₀, ← neg_add, zpow_inj, neg_inj] at this,
-  { exact_mod_cast hp_prime.1.pos },
-  { exact_mod_cast hp_prime.1.ne_one },
-  { exact_mod_cast hp_prime.1.ne_zero },
+  { exact_mod_cast hp.1.pos },
+  { exact_mod_cast hp.1.ne_one },
+  { exact_mod_cast hp.1.ne_zero }
 end
 
 section units
+
 /-! ### Units of `ℤ_[p]` -/
 
 local attribute [reducible] padic_int
@@ -360,7 +365,7 @@ lemma mul_inv : ∀ {z : ℤ_[p]}, ∥z∥ = 1 → z * z.inv = 1
     rw [norm_eq_padic_norm] at h,
     rw dif_pos h,
     apply subtype.ext_iff_val.2,
-    simp [mul_inv_cancel hk],
+    simp [mul_inv_cancel hk]
   end
 
 lemma inv_mul {z : ℤ_[p]} (hz : ∥z∥ = 1) : z.inv * z = 1 :=
@@ -400,7 +405,7 @@ See `unit_coeff_spec`. -/
 def unit_coeff {x : ℤ_[p]} (hx : x ≠ 0) : ℤ_[p]ˣ :=
 let u : ℚ_[p] := x*p^(-x.valuation) in
 have hu : ∥u∥ = 1,
-by simp [hx, nat.zpow_ne_zero_of_pos (by exact_mod_cast hp_prime.1.pos) x.valuation,
+by simp [hx, nat.zpow_ne_zero_of_pos (by exact_mod_cast hp.1.pos) x.valuation,
          norm_eq_pow_val, zpow_neg, inv_mul_cancel],
 mk_units hu
 
@@ -415,14 +420,15 @@ begin
   have repr : (x : ℚ_[p]) = (unit_coeff hx) * p ^ x.valuation,
   { rw [unit_coeff_coe, mul_assoc, ← zpow_add₀],
     { simp },
-    { exact_mod_cast hp_prime.1.ne_zero } },
+    { exact_mod_cast hp.1.ne_zero } },
   convert repr using 2,
-  rw [← zpow_coe_nat, int.nat_abs_of_nonneg (valuation_nonneg x)],
+  rw [← zpow_coe_nat, int.nat_abs_of_nonneg (valuation_nonneg x)]
 end
 
 end units
 
 section norm_le_iff
+
 /-! ### Various characterizations of open unit balls -/
 
 lemma norm_le_pow_iff_le_valuation (x : ℤ_[p]) (hx : x ≠ 0) (n : ℕ) :
@@ -432,11 +438,11 @@ begin
   lift x.valuation to ℕ using x.valuation_nonneg with k hk,
   simp only [int.coe_nat_le, zpow_neg, zpow_coe_nat],
   have aux : ∀ n : ℕ, 0 < (p ^ n : ℝ),
-  { apply pow_pos, exact_mod_cast hp_prime.1.pos },
+  { apply pow_pos, exact_mod_cast hp.1.pos },
   rw [inv_le_inv (aux _) (aux _)],
-  have : p ^ n ≤ p ^ k ↔ n ≤ k := (strict_mono_pow hp_prime.1.one_lt).le_iff_le,
+  have : p ^ n ≤ p ^ k ↔ n ≤ k := (strict_mono_pow hp.1.one_lt).le_iff_le,
   rw [← this],
-  norm_cast,
+  norm_cast
 end
 
 lemma mem_span_pow_iff_le_valuation (x : ℤ_[p]) (hx : x ≠ 0) (n : ℕ) :
@@ -446,14 +452,14 @@ begin
   split,
   { rintro ⟨c, rfl⟩,
     suffices : c ≠ 0,
-    { rw [valuation_p_pow_mul _ _ this, le_add_iff_nonneg_right], apply valuation_nonneg, },
-    contrapose! hx, rw [hx, mul_zero], },
+    { rw [valuation_p_pow_mul _ _ this, le_add_iff_nonneg_right], apply valuation_nonneg },
+    contrapose! hx, rw [hx, mul_zero] },
   { rw [unit_coeff_spec hx] { occs := occurrences.pos [2] },
     lift x.valuation to ℕ using x.valuation_nonneg with k hk,
     simp only [int.nat_abs_of_nat, units.is_unit, is_unit.dvd_mul_left, int.coe_nat_le],
     intro H,
     obtain ⟨k, rfl⟩ := nat.exists_eq_add_of_le H,
-    simp only [pow_add, dvd_mul_right], }
+    simp only [pow_add, dvd_mul_right] }
 end
 
 lemma norm_le_pow_iff_mem_span_pow (x : ℤ_[p]) (n : ℕ) :
@@ -463,7 +469,7 @@ begin
   { subst hx,
     simp only [norm_zero, zpow_neg, zpow_coe_nat, inv_nonneg, iff_true, submodule.zero_mem],
     exact_mod_cast nat.zero_le _ },
-  rw [norm_le_pow_iff_le_valuation x hx, mem_span_pow_iff_le_valuation x hx],
+  rw [norm_le_pow_iff_le_valuation x hx, mem_span_pow_iff_le_valuation x hx]
 end
 
 lemma norm_le_pow_iff_norm_lt_pow_add_one (x : ℤ_[p]) (n : ℤ) :
@@ -481,7 +487,7 @@ begin
   have := norm_le_pow_iff_mem_span_pow x 1,
   rw [ideal.mem_span_singleton, pow_one] at this,
   rw [← this, norm_le_pow_iff_norm_lt_pow_add_one],
-  simp only [zpow_zero, int.coe_nat_zero, int.coe_nat_succ, add_left_neg, zero_add],
+  simp only [zpow_zero, int.coe_nat_zero, int.coe_nat_succ, add_left_neg, zero_add]
 end
 
 @[simp] lemma pow_p_dvd_int_iff (n : ℕ) (a : ℤ) : (p ^ n : ℤ_[p]) ∣ a ↔ ↑p ^ n ∣ a :=
@@ -490,13 +496,14 @@ by rw [← norm_int_le_pow_iff_dvd, norm_le_pow_iff_mem_span_pow, ideal.mem_span
 end norm_le_iff
 
 section dvr
+
 /-! ### Discrete valuation ring -/
 
 instance : local_ring ℤ_[p] :=
 local_ring.of_nonunits_add $ by simp only [mem_nonunits]; exact λ x y, norm_lt_one_add
 
 lemma p_nonnunit : (p : ℤ_[p]) ∈ nonunits ℤ_[p] :=
-have (p : ℝ)⁻¹ < 1, from inv_lt_one $ by exact_mod_cast hp_prime.1.one_lt,
+have (p : ℝ)⁻¹ < 1, from inv_lt_one $ by exact_mod_cast hp.1.one_lt,
 by simp [this]
 
 lemma maximal_ideal_eq_span_p : maximal_ideal ℤ_[p] = ideal.span {p} :=
@@ -505,7 +512,7 @@ begin
   { intros x hx,
     rw ideal.mem_span_singleton,
     simp only [local_ring.mem_maximal_ideal, mem_nonunits] at hx,
-    rwa ← norm_lt_one_iff_dvd, },
+    rwa ← norm_lt_one_iff_dvd },
   { rw [ideal.span_le, set.singleton_subset_iff], exact p_nonnunit }
 end
 
@@ -513,7 +520,7 @@ lemma prime_p : prime (p : ℤ_[p]) :=
 begin
   rw [← ideal.span_singleton_prime, ← maximal_ideal_eq_span_p],
   { apply_instance },
-  { exact_mod_cast hp_prime.1.ne_zero }
+  { exact_mod_cast hp.1.ne_zero }
 end
 
 lemma irreducible_p : irreducible (p : ℤ_[p]) :=
@@ -539,14 +546,14 @@ instance : is_adic_complete (maximal_ideal ℤ_[p]) ℤ_[p] :=
     { intros ε hε, obtain ⟨m, hm⟩ := exists_pow_neg_lt p hε,
       refine ⟨m, λ n hn, lt_of_le_of_lt _ hm⟩, rw [← neg_sub, norm_neg], exact hx hn },
     { refine ⟨x'.lim, λ n, _⟩,
-      have : (0:ℝ) < p ^ (-n : ℤ), { apply zpow_pos_of_pos, exact_mod_cast hp_prime.1.pos },
+      have : (0:ℝ) < p ^ (-n : ℤ), { apply zpow_pos_of_pos, exact_mod_cast hp.1.pos },
       obtain ⟨i, hi⟩ := equiv_def₃ (equiv_lim x') this,
       by_cases hin : i ≤ n,
-      { exact (hi i le_rfl n hin).le, },
+      { exact (hi i le_rfl n hin).le },
       { push_neg at hin, specialize hi i le_rfl i le_rfl, specialize hx hin.le,
         have := nonarchimedean (x n - x i) (x i - x'.lim),
         rw [sub_add_sub_cancel] at this,
-        refine this.trans (max_le_iff.mpr ⟨hx, hi.le⟩), } },
+        refine this.trans (max_le_iff.mpr ⟨hx, hi.le⟩) } }
   end }
 
 end dvr
diff --git a/src/number_theory/padics/padic_norm.lean b/src/number_theory/padics/padic_norm.lean
index 818567dbd0e01..e44df9e92c04e 100644
--- a/src/number_theory/padics/padic_norm.lean
+++ b/src/number_theory/padics/padic_norm.lean
@@ -47,7 +47,7 @@ if q = 0 then 0 else (↑p : ℚ) ^ (-(padic_val_rat p q))
 namespace padic_norm
 
 open padic_val_rat
-variables (p : ℕ)
+variables {p : ℕ}
 
 /-- Unfolds the definition of the p-adic norm of `q` when `q ≠ 0`. -/
 @[simp] protected lemma eq_zpow_of_nonzero {q : ℚ} (hq : q ≠ 0) :
@@ -75,7 +75,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 :=
+lemma padic_norm_p (hp : 1 < p) : padic_norm p p = 1 / p :=
 by simp [padic_norm, (pos_of_gt hp).ne', padic_val_nat.self hp]
 
 /--
@@ -83,11 +83,11 @@ The p-adic norm of `p` is `1/p` if `p` is prime.
 
 See also `padic_norm.padic_norm_p` for a version that assumes `1 < p`.
 -/
-@[simp] lemma padic_norm_p_of_prime (p : ℕ) [fact p.prime] : padic_norm p p = 1 / p :=
+@[simp] lemma padic_norm_p_of_prime [fact p.prime] : padic_norm p p = 1 / p :=
 padic_norm_p $ nat.prime.one_lt (fact.out _)
 
 /-- The p-adic norm of `q` is `1` if `q` is prime and not equal to `p`. -/
-lemma padic_norm_of_prime_of_ne {p q : ℕ} [p_prime : fact p.prime] [q_prime : fact q.prime]
+lemma padic_norm_of_prime_of_ne {q : ℕ} [p_prime : fact p.prime] [q_prime : fact q.prime]
   (neq : p ≠ q) : padic_norm p q = 1 :=
 begin
   have p : padic_val_rat p q = 0,
@@ -100,7 +100,7 @@ The p-adic norm of `p` is less than 1 if `1 < p`.
 
 See also `padic_norm.padic_norm_p_lt_one_of_prime` for a version assuming `prime p`.
 -/
-lemma padic_norm_p_lt_one {p : ℕ} (hp : 1 < p) : padic_norm p p < 1 :=
+lemma padic_norm_p_lt_one (hp : 1 < p) : padic_norm p p < 1 :=
 begin
   rw [padic_norm_p hp, div_lt_iff, one_mul],
   { exact_mod_cast hp },
@@ -112,7 +112,7 @@ The p-adic norm of `p` is less than 1 if `p` is prime.
 
 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 :=
+lemma padic_norm_p_lt_one_of_prime [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 : ℤ`. -/
@@ -130,7 +130,7 @@ include hp
 /-- 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,
+  rw padic_norm.eq_zpow_of_nonzero hq,
   apply zpow_ne_zero_of_ne_zero,
   exact_mod_cast ne_of_gt hp.1.pos
 end
@@ -153,13 +153,13 @@ else if hr : r = 0 then
   by simp [hr]
 else
   have q*r ≠ 0, from mul_ne_zero hq hr,
-  have (↑p : ℚ) ≠ 0, by simp [hp.1.ne_zero],
+  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. -/
 @[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])
+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. -/
 protected theorem of_int (z : ℤ) : padic_norm p ↑z ≤ 1 :=
@@ -168,7 +168,7 @@ begin
   unfold padic_norm,
   rw [if_neg _],
   { refine zpow_le_one_of_nonpos _ _,
-    { exact_mod_cast le_of_lt hp.1.one_lt, },
+    { exact_mod_cast le_of_lt hp.1.one_lt },
     { rw [padic_val_rat.of_int, neg_nonpos],
       norm_cast, simp }},
   exact_mod_cast hz,
@@ -176,8 +176,8 @@ end
 
 private lemma nonarchimedean_aux {q r : ℚ} (h : padic_val_rat p q ≤ padic_val_rat p r) :
   padic_norm p (q + r) ≤ max (padic_norm p q) (padic_norm p r) :=
-have hnqp : padic_norm p q ≥ 0, from padic_norm.nonneg _ _,
-have hnrp : padic_norm p r ≥ 0, from padic_norm.nonneg _ _,
+have hnqp : padic_norm p q ≥ 0, from padic_norm.nonneg _,
+have hnrp : padic_norm p r ≥ 0, from padic_norm.nonneg _,
 if hq : q = 0 then
   by simp [hq, max_eq_right hnrp, le_max_right]
 else if hr : r = 0 then
@@ -206,8 +206,8 @@ the norm of `q`.
 protected theorem nonarchimedean {q r : ℚ} :
   padic_norm p (q + r) ≤ max (padic_norm p q) (padic_norm p r) :=
 begin
-    wlog hle := le_total (padic_val_rat p q) (padic_val_rat p r) using [q r],
-    exact nonarchimedean_aux p hle
+  wlog hle := le_total (padic_val_rat p q) (padic_val_rat p r) using [q r],
+  exact nonarchimedean_aux hle
 end
 
 /--
@@ -215,16 +215,16 @@ The p-adic norm respects the triangle inequality: the norm of `p + q` is at most
 plus the norm of `q`.
 -/
 theorem triangle_ineq (q r : ℚ) : padic_norm p (q + r) ≤ padic_norm p q + padic_norm p r :=
-calc padic_norm p (q + r) ≤ max (padic_norm p q) (padic_norm p r) : padic_norm.nonarchimedean p
+calc padic_norm p (q + r) ≤ max (padic_norm p q) (padic_norm p r) : padic_norm.nonarchimedean
                        ... ≤ padic_norm p q + padic_norm p r :
-                         max_le_add_of_nonneg (padic_norm.nonneg p _) (padic_norm.nonneg p _)
+                         max_le_add_of_nonneg (padic_norm.nonneg _) (padic_norm.nonneg _)
 
 /--
 The p-adic norm of a difference is at most the max of each component. Restates the archimedean
 property of the p-adic norm.
 -/
 protected theorem sub {q r : ℚ} : padic_norm p (q - r) ≤ max (padic_norm p q) (padic_norm p r) :=
-by rw [sub_eq_add_neg, ←padic_norm.neg p r]; apply padic_norm.nonarchimedean
+by rw [sub_eq_add_neg, ←padic_norm.neg r]; apply padic_norm.nonarchimedean
 
 /--
 If the p-adic norms of `q` and `r` are different, then the norm of `q + r` is equal to the max of
@@ -237,7 +237,7 @@ begin
   have hlt : padic_norm p r < padic_norm p q, from lt_of_le_of_ne hle hne.symm,
   have : padic_norm p q ≤ max (padic_norm p (q + r)) (padic_norm p r), from calc
    padic_norm p q = padic_norm p (q + r - r) : by congr; ring
-               ... ≤ max (padic_norm p (q + r)) (padic_norm p (-r)) : padic_norm.nonarchimedean p
+               ... ≤ max (padic_norm p (q + r)) (padic_norm p (-r)) : padic_norm.nonarchimedean
                ... = max (padic_norm p (q + r)) (padic_norm p r) : by simp,
   have hnge : padic_norm p r ≤ padic_norm p (q + r),
   { apply le_of_not_gt,
@@ -247,9 +247,8 @@ begin
     assumption },
   have : padic_norm p q ≤ padic_norm p (q + r), by rwa [max_eq_left hnge] at this,
   apply _root_.le_antisymm,
-  { apply padic_norm.nonarchimedean p },
-  { rw max_eq_left_of_lt hlt,
-    assumption }
+  { apply padic_norm.nonarchimedean },
+  { rwa max_eq_left_of_lt hlt }
 end
 
 /--
@@ -257,20 +256,12 @@ The p-adic norm is an absolute value: positive-definite and multiplicative, sati
 inequality.
 -/
 instance : is_absolute_value (padic_norm p) :=
-{ abv_nonneg := padic_norm.nonneg p,
-  abv_eq_zero :=
-    begin
-      intros,
-      constructor; intro,
-      { apply zero_of_padic_norm_eq_zero p, assumption },
-      { simp [*] }
-    end,
-  abv_add := padic_norm.triangle_ineq p,
-  abv_mul := padic_norm.mul p }
-
-variable {p}
-
-lemma dvd_iff_norm_le {n : ℕ} {z : ℤ} : ↑(p^n) ∣ z ↔ padic_norm p z ≤ ↑p ^ (-n : ℤ) :=
+{ abv_nonneg := padic_norm.nonneg,
+  abv_eq_zero := λ _, ⟨zero_of_padic_norm_eq_zero, λ hx, by simpa only [hx]⟩,
+  abv_add := padic_norm.triangle_ineq,
+  abv_mul := padic_norm.mul }
+
+lemma dvd_iff_norm_le {n : ℕ} {z : ℤ} : ↑(p ^ n) ∣ z ↔ padic_norm p z ≤ p ^ (-n : ℤ) :=
 begin
   unfold padic_norm, split_ifs with hz,
   { norm_cast at hz,
@@ -314,8 +305,7 @@ begin
   simp only [padic_norm.of_int, true_and],
 end
 
-lemma of_nat (m : ℕ) : padic_norm p m ≤ 1 :=
-padic_norm.of_int p (m : ℤ)
+lemma of_nat (m : ℕ) : padic_norm p m ≤ 1 := padic_norm.of_int (m : ℤ)
 
 /-- The `p`-adic norm of a natural `m` is one iff `p` doesn't divide `m`. -/
 lemma nat_eq_one_iff (m : ℕ) : padic_norm p m = 1 ↔ ¬ p ∣ m :=
@@ -327,47 +317,43 @@ by simp only [←int.coe_nat_dvd, ←int_lt_one_iff, int.cast_coe_nat]
 open_locale big_operators
 
 lemma sum_lt {α : Type*} {F : α → ℚ} {t : ℚ} {s : finset α} :
-  s.nonempty → (∀ i ∈ s, padic_norm p (F i) < t) →
-  padic_norm p (∑ i in s, F i) < t :=
+  s.nonempty → (∀ i ∈ s, padic_norm p (F i) < t) → padic_norm p (∑ i in s, F i) < t :=
 begin
   classical,
   refine s.induction_on (by { rintro ⟨-, ⟨⟩⟩, }) _,
   rintro a S haS IH - ht,
   by_cases hs : S.nonempty,
   { rw finset.sum_insert haS,
-    exact lt_of_le_of_lt (padic_norm.nonarchimedean p) (max_lt
+    exact lt_of_le_of_lt padic_norm.nonarchimedean (max_lt
       (ht a (finset.mem_insert_self a S))
       (IH hs (λ b hb, ht b (finset.mem_insert_of_mem hb)))), },
   { simp * at *, },
 end
 
 lemma sum_le {α : Type*} {F : α → ℚ} {t : ℚ} {s : finset α} :
-  s.nonempty → (∀ i ∈ s, padic_norm p (F i) ≤ t) →
-  padic_norm p (∑ i in s, F i) ≤ t :=
+  s.nonempty → (∀ i ∈ s, padic_norm p (F i) ≤ t) → padic_norm p (∑ i in s, F i) ≤ t :=
 begin
   classical,
   refine s.induction_on (by { rintro ⟨-, ⟨⟩⟩, }) _,
   rintro a S haS IH - ht,
   by_cases hs : S.nonempty,
   { rw finset.sum_insert haS,
-    exact (padic_norm.nonarchimedean p).trans (max_le
+    exact padic_norm.nonarchimedean.trans (max_le
       (ht a (finset.mem_insert_self a S))
       (IH hs (λ b hb, ht b (finset.mem_insert_of_mem hb)))), },
   { simp * at *, },
 end
 
-lemma sum_lt' {α : Type*} {F : α → ℚ} {t : ℚ} {s : finset α}
-  (hF : ∀ i ∈ s, padic_norm p (F i) < t) (ht : 0 < t) :
-  padic_norm p (∑ i in s, F i) < t :=
+lemma sum_lt' {α : Type*} {F : α → ℚ} {t : ℚ} {s : finset α} (hF : ∀ i ∈ s, padic_norm p (F i) < t)
+  (ht : 0 < t) : padic_norm p (∑ i in s, F i) < t :=
 begin
   obtain rfl | hs := finset.eq_empty_or_nonempty s,
   { simp [ht], },
   { exact sum_lt hs hF, },
 end
 
-lemma sum_le' {α : Type*} {F : α → ℚ} {t : ℚ} {s : finset α}
-  (hF : ∀ i ∈ s, padic_norm p (F i) ≤ t) (ht : 0 ≤ t) :
-  padic_norm p (∑ i in s, F i) ≤ t :=
+lemma sum_le' {α : Type*} {F : α → ℚ} {t : ℚ} {s : finset α} (hF : ∀ i ∈ s, padic_norm p (F i) ≤ t)
+  (ht : 0 ≤ t) : padic_norm p (∑ i in s, F i) ≤ t :=
 begin
   obtain rfl | hs := finset.eq_empty_or_nonempty s,
   { simp [ht], },
diff --git a/src/number_theory/padics/padic_numbers.lean b/src/number_theory/padics/padic_numbers.lean
index 83f1fca5f7df0..830a6142985b7 100644
--- a/src/number_theory/padics/padic_numbers.lean
+++ b/src/number_theory/padics/padic_numbers.lean
@@ -88,10 +88,10 @@ let ⟨ε, hε, N1, hN1⟩ := this,
     from lt_max_iff.2 (or.inl this),
   begin
     by_contradiction hne,
-    rw ←padic_norm.neg p (f m) at hne,
-    have hnam := add_eq_max_of_ne p hne,
+    rw ← padic_norm.neg (f m) at hne,
+    have hnam := add_eq_max_of_ne hne,
     rw [padic_norm.neg, max_comm] at hnam,
-    rw [←hnam, sub_eq_add_neg, add_comm] at this,
+    rw [← hnam, sub_eq_add_neg, add_comm] at this,
     apply _root_.lt_irrefl _ this
   end ⟩
 
@@ -215,7 +215,7 @@ begin
   use (stationary_point hf),
   intros n hn,
   rw stationary_point_spec hf le_rfl hn,
-  simpa [H] using hε,
+  simpa [H] using hε
 end
 
 lemma val_eq_iff_norm_eq {f g : padic_seq p} (hf : ¬ f ≈ 0) (hg : ¬ g ≈ 0) :
@@ -223,7 +223,7 @@ lemma val_eq_iff_norm_eq {f g : padic_seq p} (hf : ¬ f ≈ 0) (hg : ¬ g ≈ 0)
 begin
   rw [norm_eq_pow_val hf, norm_eq_pow_val hg, ← neg_inj, zpow_inj],
   { exact_mod_cast (fact.out p.prime).pos },
-  { exact_mod_cast (fact.out p.prime).ne_one },
+  { exact_mod_cast (fact.out p.prime).ne_one }
 end
 
 end valuation
@@ -295,7 +295,7 @@ else
 lemma norm_values_discrete (a : padic_seq p) (ha : ¬ a ≈ 0) :
   (∃ (z : ℤ), a.norm = ↑p ^ (-z)) :=
 let ⟨k, hk, hk'⟩ := norm_eq_norm_app_of_nonzero ha in
-by simpa [hk] using padic_norm.values_discrete p hk'
+by simpa [hk] using padic_norm.values_discrete hk'
 
 lemma norm_one : norm (1 : padic_seq p) = 1 :=
 have h1 : ¬ (1 : padic_seq p) ≈ 0, from one_not_equiv_zero _,
@@ -314,8 +314,8 @@ begin
   have hN' := hN _ hi,
   padic_index_simp [N, hf, hg] at hN' h hlt,
   have hpne : padic_norm p (f i) ≠ padic_norm p (-(g i)),
-    by rwa [ ←padic_norm.neg p (g i)] at h,
-  let hpnem := add_eq_max_of_ne p hpne,
+    by rwa [← padic_norm.neg (g i)] at h,
+  let hpnem := add_eq_max_of_ne hpne,
   have hpeq : padic_norm p ((f - g) i) = max (padic_norm p (f i)) (padic_norm p (g i)),
   { rwa padic_norm.neg at hpnem },
   rw [hpeq, max_eq_left_of_lt hlt] at hN',
@@ -423,7 +423,7 @@ else
 begin
   unfold norm at ⊢ hfgne, split_ifs at ⊢ hfgne,
   padic_index_simp [hfg, hf, hg] at ⊢ hfgne,
-  exact padic_norm.add_eq_max_of_ne p hfgne
+  exact padic_norm.add_eq_max_of_ne hfgne
 end
 
 end embedding
@@ -438,7 +438,6 @@ namespace padic
 section completion
 variables {p : ℕ} [fact p.prime]
 
-/-- The discrete field structure on `ℚ_p` is inherited from the Cauchy completion construction. -/
 instance : field (ℚ_[p]) := Cauchy.field
 
 instance : inhabited ℚ_[p] := ⟨0⟩
@@ -458,17 +457,13 @@ instance : add_comm_group ℚ_[p] := by apply_instance
 
 /-- Builds the equivalence class of a Cauchy sequence of rationals. -/
 def mk : padic_seq p → ℚ_[p] := quotient.mk
-end completion
 
-section completion
-variables (p : ℕ) [fact p.prime]
+variables (p)
 
 lemma mk_eq {f g : padic_seq p} : mk f = mk g ↔ f ≈ g := quotient.eq
 
 lemma const_equiv {q r : ℚ} : const (padic_norm p) q ≈ const (padic_norm p) r ↔ q = r :=
-⟨ λ heq : lim_zero (const (padic_norm p) (q - r)),
-    eq_of_sub_eq_zero $ const_lim_zero.1 heq,
-  λ heq, by rw heq; apply setoid.refl _ ⟩
+⟨ λ heq, eq_of_sub_eq_zero $ const_lim_zero.1 heq, λ heq, by rw heq; apply setoid.refl _ ⟩
 
 @[norm_cast] lemma coe_inj {q r : ℚ} : (↑q : ℚ_[p]) = ↑r ↔ q = r :=
 ⟨(const_equiv p).1 ∘ quotient.eq.1, λ h, by rw h⟩
@@ -510,8 +505,8 @@ begin
   cases em (N ≤ stationary_point hne) with hgen hngen,
   { apply hN _ hgen _ hi },
   { have := stationary_point_spec hne le_rfl (le_of_not_le hngen),
-    rw ←this,
-    exact hN _ le_rfl _ hi },
+    rw ← this,
+    exact hN _ le_rfl _ hi }
 end
 
 protected lemma nonneg (q : ℚ_[p]) : 0 ≤ padic_norm_e q :=
@@ -618,7 +613,7 @@ is a sequence of rationals with the same limit point as `f`. -/
 def lim_seq : ℕ → ℚ := λ n, classical.some (rat_dense' (f n) (div_nat_pos n))
 
 lemma exi_rat_seq_conv {ε : ℚ} (hε : 0 < ε) :
-  ∃ N, ∀ i ≥ N, padic_norm_e (f i - ((lim_seq f) i : ℚ_[p])) < ε :=
+  ∃ N, ∀ i ≥ N, padic_norm_e (f i - (lim_seq f i : ℚ_[p])) < ε :=
 begin
   refine (exists_nat_gt (1/ε)).imp (λ N hN i hi, _),
   have h := classical.some_spec (rat_dense' (f i) (div_nat_pos i)),
@@ -638,7 +633,7 @@ begin
   existsi max N N2,
   intros j hj,
   suffices :
-    padic_norm_e ((↑(lim_seq f j) - f (max N N2)) + (f (max N N2) - lim_seq f (max N N2))) < ε,
+    padic_norm_e ((lim_seq f j - f (max N N2)) + (f (max N N2) - lim_seq f (max N N2))) < ε,
   { ring_nf at this ⊢,
     rw [← padic_norm_e.eq_padic_norm'],
     exact_mod_cast this },
@@ -697,7 +692,7 @@ instance : has_dist ℚ_[p] := ⟨λ x y, padic_norm_e (x - y)⟩
 instance : metric_space ℚ_[p] :=
 { dist_self := by simp [dist],
   dist := dist,
-  dist_comm := λ x y, by unfold dist; rw ←padic_norm_e.neg (x - y); simp,
+  dist_comm := λ x y, by unfold dist; rw ← padic_norm_e.neg (x - y); simp,
   dist_triangle :=
     begin
       intros, unfold dist,
@@ -820,14 +815,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', padic_val_rat, neg_sub,
+      rw [padic_norm.eq_zpow_of_nonzero hnz', padic_val_rat, neg_sub,
         padic_val_nat.eq_zero_of_not_dvd hq],
       norm_cast,
       rw [zero_sub, zpow_neg, zpow_coe_nat],
       apply inv_le_one,
       { norm_cast,
         apply one_le_pow,
-        exact hp.1.pos, },
+        exact hp.1.pos }
     end
 
 theorem norm_int_le_one (z : ℤ) : ∥(z : ℚ_[p])∥ ≤ 1 :=
@@ -855,7 +850,7 @@ begin
       convert zpow_zero _,
       rw [neg_eq_zero, padic_val_rat.of_int],
       norm_cast,
-      apply padic_val_int.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,
@@ -864,15 +859,15 @@ begin
     ... < 1 : _,
     { rw [mul_one, padic_norm_e.norm_p],
       apply inv_lt_one,
-      exact_mod_cast hp.1.one_lt }, },
+      exact_mod_cast hp.1.one_lt } }
 end
 
-lemma norm_int_le_pow_iff_dvd (k : ℤ) (n : ℕ) : ∥(k : ℚ_[p])∥ ≤ ((↑p)^(-n : ℤ)) ↔ ↑(p^n) ∣ k :=
+lemma norm_int_le_pow_iff_dvd (k : ℤ) (n : ℕ) : ∥(k : ℚ_[p])∥ ≤ (↑p)^(-n : ℤ) ↔ ↑(p^n) ∣ k :=
 begin
   have : (p : ℝ) ^ (-n : ℤ) = ↑((p ^ (-n : ℤ) : ℚ)), {simp},
   rw [show (k : ℚ_[p]) = ((k : ℚ) : ℚ_[p]), by norm_cast, eq_padic_norm, this],
   norm_cast,
-  rw padic_norm.dvd_iff_norm_le,
+  rw ← padic_norm.dvd_iff_norm_le
 end
 
 lemma eq_of_norm_add_lt_right {p : ℕ} {hp : fact p.prime} {z1 z2 : ℚ_[p]}
@@ -889,8 +884,8 @@ end normed_space
 end padic_norm_e
 
 namespace padic
-variables {p : ℕ} [hp_prime : fact p.prime]
-include hp_prime
+variables {p : ℕ} [hp : fact p.prime]
+include hp
 
 set_option eqn_compiler.zeta true
 instance complete : cau_seq.is_complete ℚ_[p] norm :=
@@ -935,9 +930,7 @@ begin
   exact this.imp (λ N hN n hn, hε (hN n hn))
 end
 
-/-!
-### Valuation on `ℚ_[p]`
--/
+/-! ### Valuation on `ℚ_[p]` -/
 
 /--
 `padic.valuation` lifts the p-adic valuation on rationals to `ℚ_[p]`.
@@ -950,7 +943,7 @@ begin
     simp [hf, hg, padic_seq.valuation] },
   { have hg : ¬ g ≈ 0, from (λ hg, hf (setoid.trans h hg)),
     rw padic_seq.val_eq_iff_norm_eq hf hg,
-    exact padic_seq.norm_equiv h },
+    exact padic_seq.norm_equiv h }
 end)
 
 @[simp] lemma valuation_zero : valuation (0 : ℚ_[p]) = 0 :=
@@ -962,7 +955,7 @@ begin
   have h : ¬ cau_seq.const (padic_norm p) 1 ≈ 0,
   { assume H, erw const_equiv p at H, exact one_ne_zero H },
   rw dif_neg h,
-  simp,
+  simp
 end
 
 lemma norm_eq_pow_val {x : ℚ_[p]} : x ≠ 0 → ∥x∥ = p^(-x.valuation) :=
@@ -976,7 +969,7 @@ begin
   { apply cau_seq.not_lim_zero_of_not_congr_zero,
     contrapose! hf,
     apply quotient.sound,
-    simpa using hf, }
+    simpa using hf }
 end
 
 @[simp] lemma valuation_p : valuation (p : ℚ_[p]) = 1 :=
@@ -999,7 +992,7 @@ begin
     { have h_norm : ∥x + y∥ ≤ (max ∥x∥ ∥y∥) := padic_norm_e.nonarchimedean x y,
       have hp_one : (1 : ℝ) < p,
       { rw [← nat.cast_one, nat.cast_lt],
-        exact nat.prime.one_lt hp_prime.elim, },
+        exact nat.prime.one_lt hp.elim },
       rw [norm_eq_pow_val hx, norm_eq_pow_val hy, norm_eq_pow_val hxy] at h_norm,
       exact min_le_of_zpow_le_max hp_one h_norm }}
 end
@@ -1010,13 +1003,13 @@ begin
   have h_norm : ∥x * y∥ = ∥x∥ * ∥y∥ := norm_mul x y,
   have hp_ne_one : (p : ℝ) ≠ 1,
   { rw [← nat.cast_one, ne.def, nat.cast_inj],
-    exact nat.prime.ne_one hp_prime.elim, },
+    exact nat.prime.ne_one hp.elim },
   have hp_pos : (0 : ℝ) < p,
   { rw [← nat.cast_zero, nat.cast_lt],
-    exact nat.prime.pos hp_prime.elim },
+    exact nat.prime.pos hp.elim },
   rw [norm_eq_pow_val hx, norm_eq_pow_val hy, norm_eq_pow_val (mul_ne_zero hx hy),
     ← zpow_add₀ (ne_of_gt hp_pos), zpow_inj hp_pos hp_ne_one, ← neg_add, neg_inj] at h_norm,
-  exact h_norm,
+  exact h_norm
 end
 
 /-- The additive p-adic valuation on `ℚ_p`, with values in `with_top ℤ`. -/
@@ -1027,7 +1020,7 @@ def add_valuation_def : ℚ_[p] → (with_top ℤ) :=
 by simp only [add_valuation_def, if_pos (eq.refl _)]
 
 @[simp] lemma add_valuation.map_one : add_valuation_def (1 : ℚ_[p]) = 0 :=
-by simp only [add_valuation_def, if_neg (one_ne_zero), valuation_one,
+by simp only [add_valuation_def, if_neg one_ne_zero, valuation_one,
   with_top.coe_zero]
 
 lemma add_valuation.map_mul (x y : ℚ_[p]) :
@@ -1048,11 +1041,11 @@ begin
   simp only [add_valuation_def],
   by_cases hxy : x + y = 0,
   { rw [hxy, if_pos (eq.refl _)],
-    exact le_top, },
+    exact le_top },
   { by_cases hx : x = 0,
     { simp only [hx, if_pos (eq.refl _), min_eq_right, le_top, zero_add, le_refl] },
     { by_cases hy : y = 0,
-      { simp only [hy, if_pos (eq.refl _), min_eq_left, le_top, add_zero, le_refl], },
+      { simp only [hy, if_pos (eq.refl _), min_eq_left, le_top, add_zero, le_refl] },
       { rw [if_neg hx, if_neg hy, if_neg hxy, ← with_top.coe_min, with_top.coe_le_coe],
         exact valuation_map_add hxy }}}
 end
@@ -1067,17 +1060,19 @@ add_valuation.of add_valuation_def add_valuation.map_zero add_valuation.map_one
 by simp only [add_valuation, add_valuation.of_apply, add_valuation_def, if_neg hx]
 
 section norm_le_iff
+
 /-! ### Various characterizations of open unit balls -/
+
 lemma norm_le_pow_iff_norm_lt_pow_add_one (x : ℚ_[p]) (n : ℤ) :
   ∥x∥ ≤ p ^ n ↔ ∥x∥ < p ^ (n + 1) :=
 begin
   have aux : ∀ n : ℤ, 0 < (p ^ n : ℝ),
-  { apply nat.zpow_pos_of_pos, exact hp_prime.1.pos },
-  by_cases hx0 : x = 0, { simp [hx0, norm_zero, aux, le_of_lt (aux _)], },
+  { apply nat.zpow_pos_of_pos, exact hp.1.pos },
+  by_cases hx0 : x = 0, { simp [hx0, norm_zero, aux, le_of_lt (aux _)] },
   rw norm_eq_pow_val hx0,
-  have h1p : 1 < (p : ℝ), { exact_mod_cast hp_prime.1.one_lt },
+  have h1p : 1 < (p : ℝ), { exact_mod_cast hp.1.one_lt },
   have H := zpow_strict_mono h1p,
-  rw [H.le_iff_le, H.lt_iff_lt, int.lt_add_one_iff],
+  rw [H.le_iff_le, H.lt_iff_lt, int.lt_add_one_iff]
 end
 
 lemma norm_lt_pow_iff_norm_le_pow_sub_one (x : ℚ_[p]) (n : ℤ) :
diff --git a/src/number_theory/padics/padic_val.lean b/src/number_theory/padics/padic_val.lean
index e89f21ed2e3c2..b32672aca4be5 100644
--- a/src/number_theory/padics/padic_val.lean
+++ b/src/number_theory/padics/padic_val.lean
@@ -69,25 +69,20 @@ by simp [padic_val_nat]
 
 /-- `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 *
+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 :=
 begin
   have neq_one : (¬ p = 1) ↔ true,
-  { exact iff_of_true ((ne_of_lt hp).symm) trivial, },
+  { 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],
+  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
+by { rw padic_val_nat, split_ifs; simp [multiplicity_eq_zero_of_not_dvd h] }
 
 end padic_val_nat
 
@@ -107,8 +102,8 @@ 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 (and.intro hp (int.nat_abs_pos_of_ne_zero hz))],
-  simp_rw multiplicity.int.nat_abs p z,
-  refl,
+  simp only [multiplicity.int.nat_abs p z],
+  refl
 end
 
 /-- `padic_val_int p 0` is 0 for any `p`. -/
@@ -130,10 +125,7 @@ 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],
-  split_ifs,
-  { simp_rw multiplicity.int.nat_abs,
-    simp [multiplicity_eq_zero_of_not_dvd h], },
-  refl,
+  split_ifs; simp [multiplicity.int.nat_abs, multiplicity_eq_zero_of_not_dvd h],
 end
 
 end padic_val_int
@@ -147,7 +139,9 @@ def padic_val_rat (p : ℕ) (q : ℚ) : ℤ :=
 padic_val_int p q.num - padic_val_nat p q.denom
 
 namespace padic_val_rat
+
 open multiplicity
+
 variables {p : ℕ}
 
 /-- `padic_val_rat p q` is symmetric in `q`. -/
@@ -155,37 +149,33 @@ variables {p : ℕ}
 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 := by simp [padic_val_rat, padic_val_int]
+@[simp] protected lemma zero : padic_val_rat p 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]
+@[simp] protected lemma one : padic_val_rat p 1 = 0 := 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]
+@[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) :
+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, 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 =
+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], exact ⟨hp, q.pos⟩ }) :=
 begin
   rw [padic_val_rat, padic_val_int.of_ne_one_ne_zero hp, padic_val_nat, dif_pos],
   { refl },
   { exact ⟨hp, q.pos⟩ },
-  { exact rat.num_ne_zero_of_ne_zero hq },
+  { 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 -/
-@[simp] lemma of_nat {n : ℕ} : padic_val_rat p (n : ℚ) = padic_val_nat p n :=
-by simp [padic_val_rat, padic_val_int]
+@[simp] lemma of_nat {n : ℕ} : padic_val_rat p n = padic_val_nat p n := by simp [padic_val_rat]
 
 /-- For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1. -/
 lemma self (hp : 1 < p) : padic_val_rat p p = 1 := by simp [of_nat, hp]
@@ -194,46 +184,48 @@ end padic_val_rat
 
 section padic_val_nat
 
-lemma zero_le_padic_val_rat_of_nat (p n : ℕ) : 0 ≤ padic_val_rat p n := by simp
+variables {p : ℕ}
+
+lemma zero_le_padic_val_rat_of_nat (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 : ℕ) :
+/-- `padic_val_rat` coincides with `padic_val_nat`. -/
+@[norm_cast] lemma padic_val_rat_of_nat (n : ℕ) :
   ↑(padic_val_nat p n) = padic_val_rat p n :=
-by simp [padic_val_rat, padic_val_int]
+by simp
 
 /--
 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 : 0 < n) :
+lemma padic_val_nat_def [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⟩) :=
 begin
   simp [padic_val_nat],
   split_ifs,
-  { refl, },
+  { refl },
   { exfalso,
-    apply h ⟨(hp.out).ne_one, hn⟩, }
+    exact h ⟨hp.out.ne_one, hn⟩ }
 end
 
-lemma padic_val_nat_def' {n p : ℕ} (hp : p ≠ 1) (hn : 0 < n) :
+lemma padic_val_nat_def' {n : ℕ} (hp : p ≠ 1) (hn : 0 < n) :
   ↑(padic_val_nat p n) = multiplicity p n :=
 by simp [padic_val_nat, hp, hn]
 
-@[simp] lemma padic_val_nat_self (p : ℕ) [fact p.prime] : padic_val_nat p p = 1 :=
+@[simp] lemma padic_val_nat_self [fact p.prime] : padic_val_nat p p = 1 :=
 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] (n_pos : 0 < n) (div : p ∣ n) :
+lemma one_le_padic_val_nat_of_dvd {n : ℕ} [hp : fact p.prime] (hn : 0 < n) (div : p ∣ n) :
   1 ≤ padic_val_nat p n :=
 begin
-  rw @padic_val_nat_def _ prime _ n_pos,
+  rw padic_val_nat_def hn,
   let one_le_mul : _ ≤ multiplicity p n :=
-    @multiplicity.le_multiplicity_of_pow_dvd _ _ _ p n 1 (begin norm_num, exact div end),
+    multiplicity.le_multiplicity_of_pow_dvd (by { rw [pow_one], exact div }),
   simp only [nat.cast_one] at one_le_mul,
   rcases one_le_mul with ⟨_, q⟩,
   dsimp at q,
   solve_by_elim,
+  exact hp
 end
 
 lemma dvd_iff_padic_val_nat_ne_zero {p n : ℕ} [fact p.prime] (hn0 : n ≠ 0) :
@@ -244,36 +236,39 @@ lemma dvd_iff_padic_val_nat_ne_zero {p n : ℕ} [fact p.prime] (hn0 : n ≠ 0) :
 end padic_val_nat
 
 namespace padic_val_rat
+
 open multiplicity
-variables (p : ℕ) [p_prime : fact p.prime]
-include p_prime
+
+variables {p : ℕ} [hp : fact p.prime]
+
+include hp
 
 /-- 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))]
+lemma finite_int_prime_iff {a : ℤ} : finite (p : ℤ) a ↔ a ≠ 0 :=
+by simp [finite_int_iff, ne.symm (ne_of_lt hp.1.one_lt)]
 
 /-- 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 *⟩) -
-  (multiplicity (p : ℤ) d).get (finite_int_iff.2 ⟨ne.symm $ ne_of_lt p_prime.1.one_lt,
-    λ hd, by simp * at *⟩) :=
+protected lemma defn (p : ℕ) [hp : fact p.prime] {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 hp.1.one_lt, λ hn, by simp * at *⟩)
+    - (multiplicity (p : ℤ) d).get
+      (finite_int_iff.2 ⟨ne.symm $ ne_of_lt hp.1.one_lt, λ 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
 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],
+  simp [hc1, hc2, multiplicity.mul' (nat.prime_iff_prime_int.1 hp.1),
+    ne.symm (ne_of_lt hp.1.one_lt), hqz, pos_iff_ne_zero, int.coe_nat_multiplicity p q.denom]
 end
 
 /-- 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,
+have q*r = (q.num * r.num) /. (q.denom * r.denom), by rw_mod_cast rat.mul_num_denom,
 have hq' : q.num /. q.denom ≠ 0, by rw rat.num_denom; exact hq,
 have hr' : r.num /. r.denom ≠ 0, by rw rat.num_denom; exact hr,
-have hp' : _root_.prime (p : ℤ), from nat.prime_iff_prime_int.1 p_prime.1,
+have hp' : _root_.prime (p : ℤ), from nat.prime_iff_prime_int.1 hp.1,
 begin
   rw [padic_val_rat.defn p (mul_ne_zero hq hr) this],
   conv_rhs { rw [←(@rat.num_denom q), padic_val_rat.defn p hq',
@@ -284,8 +279,7 @@ end
 /-- 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]
+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`.
@@ -294,16 +288,19 @@ protected lemma inv (q : ℚ) :
   padic_val_rat p (q⁻¹) = -padic_val_rat p q :=
 begin
   by_cases hq : q = 0,
-  { simp [hq], },
-  { 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] },
+  { simp [hq] },
+  { rw [eq_neg_iff_add_eq_zero, ← padic_val_rat.mul (inv_ne_zero hq) hq,
+      inv_mul_cancel hq, padic_val_rat.one],
+    exact hp },
 end
 
 /-- 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),
-    padic_val_rat.inv p r, sub_eq_add_neg]
+begin
+  rw [div_eq_mul_inv, padic_val_rat.mul hq (inv_ne_zero hr), padic_val_rat.inv r, sub_eq_add_neg],
+  all_goals { exact hp }
+end
 
 /--
 A condition for `padic_val_rat p (n₁ / d₁) ≤ padic_val_rat p (n₂ / d₂),
@@ -325,8 +322,8 @@ have hf2 : finite (p : ℤ) (n₂ * d₁),
       ← add_sub_assoc,
       le_sub_iff_add_le],
     norm_cast,
-    rw [← multiplicity.mul' (nat.prime_iff_prime_int.1 p_prime.1) hf1, add_comm,
-      ← multiplicity.mul' (nat.prime_iff_prime_int.1 p_prime.1) hf2,
+    rw [← multiplicity.mul' (nat.prime_iff_prime_int.1 hp.1) hf1, add_comm,
+      ← multiplicity.mul' (nat.prime_iff_prime_int.1 hp.1) hf2,
       part_enat.get_le_get, multiplicity_le_multiplicity_iff] }
 
 /--
@@ -349,18 +346,18 @@ have hqrd : q.num * ↑(r.denom) + ↑(q.denom) * r.num ≠ 0,
   from rat.mk_num_ne_zero_of_ne_zero hqr hqreq,
 begin
   conv_lhs { rw ←(@rat.num_denom q) },
-  rw [hqreq, padic_val_rat_le_padic_val_rat_iff p hqn hqrd hqd (mul_ne_zero hqd hrd),
+  rw [hqreq, padic_val_rat_le_padic_val_rat_iff hqn hqrd hqd (mul_ne_zero hqd hrd),
     ← multiplicity_le_multiplicity_iff, mul_left_comm,
-    multiplicity.mul (nat.prime_iff_prime_int.1 p_prime.1), add_mul],
+    multiplicity.mul (nat.prime_iff_prime_int.1 hp.1), add_mul],
   rw [←(@rat.num_denom q), ←(@rat.num_denom r),
-    padic_val_rat_le_padic_val_rat_iff p hqn hrn hqd hrd, ← multiplicity_le_multiplicity_iff] at h,
+    padic_val_rat_le_padic_val_rat_iff hqn hrn hqd hrd, ← multiplicity_le_multiplicity_iff] at h,
   calc _ ≤ min (multiplicity ↑p (q.num * ↑(r.denom) * ↑(q.denom)))
     (multiplicity ↑p (↑(q.denom) * r.num * ↑(q.denom))) : (le_min
-    (by rw [@multiplicity.mul _ _ _ _ (_ * _) _ (nat.prime_iff_prime_int.1 p_prime.1), add_comm])
+    (by rw [@multiplicity.mul _ _ _ _ (_ * _) _ (nat.prime_iff_prime_int.1 hp.1), add_comm])
     (by rw [mul_assoc, @multiplicity.mul _ _ _ _ (q.denom : ℤ)
-        (_ * _) (nat.prime_iff_prime_int.1 p_prime.1)];
-      exact add_le_add_left h _))
-    ... ≤ _ : min_le_multiplicity_add
+        (_ * _) (nat.prime_iff_prime_int.1 hp.1)]; exact add_le_add_left h _))
+    ... ≤ _ : min_le_multiplicity_add,
+  all_goals { exact hp }
 end
 
 /--
@@ -369,8 +366,8 @@ The minimum of the valuations of `q` and `r` is less than or equal to the valuat
 theorem min_le_padic_val_rat_add {q r : ℚ} (hqr : q + r ≠ 0) :
   min (padic_val_rat p q) (padic_val_rat p r) ≤ padic_val_rat p (q + r) :=
 (le_total (padic_val_rat p q) (padic_val_rat p r)).elim
-  (λ h, by rw [min_eq_left h]; exact le_padic_val_rat_add_of_le _ hqr h)
-  (λ h, by rw [min_eq_right h, add_comm]; exact le_padic_val_rat_add_of_le _
+  (λ h, by rw [min_eq_left h]; exact le_padic_val_rat_add_of_le hqr h)
+  (λ h, by rw [min_eq_right h, add_comm]; exact le_padic_val_rat_add_of_le
     (by rwa add_comm) h)
 
 open_locale big_operators
@@ -387,81 +384,82 @@ begin
     by_cases h : ∑ (x : ℕ) in finset.range d, F x = 0,
     { rw [h, zero_add],
       exact hF d (lt_add_one _) },
-    { refine lt_of_lt_of_le _ (min_le_padic_val_rat_add p hn0),
+    { refine lt_of_lt_of_le _ (min_le_padic_val_rat_add hn0),
       { refine lt_min (hd (λ i hi, _) h) (hF d (lt_add_one _)),
-        exact hF _ (lt_trans hi (lt_add_one _)) }, } }
+        exact hF _ (lt_trans hi (lt_add_one _)) } } }
 end
 
 end padic_val_rat
 
 namespace padic_val_nat
 
-/-- 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 :=
+variables {p a b : ℕ} [hp : fact p.prime]
+
+include hp
+
+/-- A rewrite lemma for `padic_val_nat p (a * b)` with conditions `a ≠ 0`, `b ≠ 0`. -/
+protected lemma mul (ha : a ≠ 0) (hb : b ≠ 0) :
+  padic_val_nat p (a * b) = padic_val_nat p a + padic_val_nat p b :=
 begin
   apply int.coe_nat_inj,
   simp only [padic_val_rat_of_nat, nat.cast_mul],
   rw padic_val_rat.mul,
   norm_cast,
-  exact cast_ne_zero.mpr hq,
-  exact cast_ne_zero.mpr hr,
+  exact cast_ne_zero.mpr ha,
+  exact cast_ne_zero.mpr hb
 end
 
-protected lemma div_of_dvd (p : ℕ) [hp : fact p.prime] {a b : ℕ} (h : b ∣ a) :
+protected lemma div_of_dvd (h : b ∣ a) :
   padic_val_nat p (a / b) = padic_val_nat p a - padic_val_nat p b :=
 begin
   rcases eq_or_ne a 0 with rfl | ha,
   { simp },
   obtain ⟨k, rfl⟩ := h,
   obtain ⟨hb, hk⟩ := mul_ne_zero_iff.mp ha,
-  rw [mul_comm, k.mul_div_cancel hb.bot_lt, padic_val_nat.mul p hk hb, nat.add_sub_cancel]
+  rw [mul_comm, k.mul_div_cancel hb.bot_lt, padic_val_nat.mul hk hb, nat.add_sub_cancel],
+  exact hp
 end
 
 /-- 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 :=
+protected lemma div (dvd : p ∣ b) : padic_val_nat p (b / p) = (padic_val_nat p b) - 1 :=
 begin
-  convert padic_val_nat.div_of_dvd p dvd,
-  rw padic_val_nat_self p
+  convert padic_val_nat.div_of_dvd dvd,
+  rw padic_val_nat_self,
+  exact hp
 end
 
 /-- A version of `padic_val_rat.pow` for `padic_val_nat` -/
-protected lemma pow (p q n : ℕ) [fact p.prime] (hq : q ≠ 0) :
-  padic_val_nat p (q ^ n) = n * padic_val_nat p q :=
-begin
-  apply @nat.cast_injective ℤ,
-  push_cast,
-  exact padic_val_rat.pow _ (cast_ne_zero.mpr hq),
-end
+protected lemma pow (n : ℕ) (ha : a ≠ 0) :
+  padic_val_nat p (a ^ n) = n * padic_val_nat p a :=
+by simpa only [← @nat.cast_inj ℤ] with push_cast using padic_val_rat.pow (cast_ne_zero.mpr ha)
 
-@[simp] protected lemma prime_pow (p n : ℕ) [fact p.prime] : padic_val_nat p (p ^ n) = n :=
-by rw [padic_val_nat.pow p _ _ (fact.out p.prime).ne_zero, padic_val_nat_self p, mul_one]
+@[simp] protected lemma prime_pow (n : ℕ) : padic_val_nat p (p ^ n) = n :=
+by rwa [padic_val_nat.pow _ (fact.out p.prime).ne_zero, padic_val_nat_self, mul_one]
 
-protected lemma div_pow {p : ℕ} [p_prime : fact p.prime] {b k : ℕ} (dvd : p ^ k ∣ b) :
-  (padic_val_nat p (b / p ^ k)) = (padic_val_nat p b) - k :=
+protected lemma div_pow (dvd : p ^ a ∣ b) : padic_val_nat p (b / p ^ a) = (padic_val_nat p b) - a :=
 begin
-  convert padic_val_nat.div_of_dvd p dvd,
-  rw padic_val_nat.prime_pow
+  convert padic_val_nat.div_of_dvd dvd,
+  rw padic_val_nat.prime_pow,
+  exact hp
 end
 
 end padic_val_nat
 
 section padic_val_nat
 
-lemma dvd_of_one_le_padic_val_nat {n p : nat} (hp : 1 ≤ padic_val_nat p n) :
+lemma dvd_of_one_le_padic_val_nat {p n : ℕ} (hp : 1 ≤ padic_val_nat p n) :
   p ∣ n :=
 begin
   by_contra h,
   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),
+  exact lt_irrefl 0 (lt_of_lt_of_le zero_lt_one hp)
 end
 
 lemma pow_padic_val_nat_dvd {p n : ℕ} : p ^ (padic_val_nat p n) ∣ n :=
 begin
   rcases n.eq_zero_or_pos with rfl | hn, { simp },
   rcases eq_or_ne p 1 with rfl | hp, { simp },
-  rw [multiplicity.pow_dvd_iff_le_multiplicity, padic_val_nat_def']; assumption,
+  rw [multiplicity.pow_dvd_iff_le_multiplicity, padic_val_nat_def']; assumption
 end
 
 lemma pow_succ_padic_val_nat_not_dvd {p n : ℕ} [hp : fact (nat.prime p)] (hn : 0 < n) :
@@ -476,7 +474,7 @@ begin
   { apply_instance }
 end
 
-lemma padic_val_nat_dvd_iff (p : ℕ) [hp :fact p.prime] (n : ℕ) (a : ℕ) :
+lemma padic_val_nat_dvd_iff {p : ℕ} (n : ℕ) [hp : fact p.prime] (a : ℕ) :
   p^n ∣ a ↔ a = 0 ∨ n ≤ padic_val_nat p a :=
 begin
   split,
@@ -488,17 +486,17 @@ begin
       exact λ hn, or.inl h } },
   { rintro (rfl|h),
     { exact dvd_zero (p ^ n) },
-    { exact dvd_trans (pow_dvd_pow p h) pow_padic_val_nat_dvd } },
+    { 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]
+lemma padic_val_nat_primes {p q : ℕ} [hp : fact p.prime] [hq : fact q.prime]
   (neq : p ≠ q) : padic_val_nat p q = 0 :=
 @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
+  (not_congr (iff.symm (prime_dvd_prime_iff_eq hp.1 hq.1))).mp neq
 
-protected lemma padic_val_nat.div' {p : ℕ} [p_prime : fact p.prime] :
+protected lemma padic_val_nat.div' {p : ℕ} [hp : fact p.prime] :
   ∀ {m : ℕ} (cpm : coprime p m) {b : ℕ} (dvd : m ∣ b), padic_val_nat p (b / m) = padic_val_nat p b
-| 0 := λ cpm b dvd, by { rw zero_dvd_iff at dvd, rw [dvd, nat.zero_div], }
+| 0 := λ cpm b dvd, by { rw zero_dvd_iff at dvd, rw [dvd, nat.zero_div] }
 | (n + 1) :=
   λ cpm b dvd,
   begin
@@ -509,9 +507,9 @@ protected lemma padic_val_nat.div' {p : ℕ} [p_prime : fact p.prime] :
       { suffices : ¬ p ∣ (n+1),
         { 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 hp.1.dvd_iff_not_coprime.mp cpm },
       { exact nat.succ_ne_zero _ },
-      { exact hc } },
+      { exact hc } }
   end
 
 open_locale big_operators
@@ -526,7 +524,7 @@ begin
   exact ⟨(pow_dvd_pow p $ by linarith).trans pow_padic_val_nat_dvd, hn⟩
 end
 
-lemma range_pow_padic_val_nat_subset_divisors' {n : ℕ} (p : ℕ) [h : fact p.prime] :
+lemma range_pow_padic_val_nat_subset_divisors' {p n : ℕ} [hp : fact p.prime] :
   (finset.range (padic_val_nat p n)).image (λ t, p ^ (t + 1)) ⊆ (n.divisors \ {1}) :=
 begin
   rcases eq_or_ne n 0 with rfl | hn,
@@ -537,42 +535,44 @@ begin
   rw [finset.mem_sdiff, nat.mem_divisors],
   refine ⟨⟨(pow_dvd_pow p $ by linarith).trans pow_padic_val_nat_dvd, hn⟩, _⟩,
   rw [finset.mem_singleton],
-  nth_rewrite 1 ←one_pow (k + 1),
-  exact (nat.pow_lt_pow_of_lt_left h.1.one_lt $ nat.succ_pos k).ne',
+  nth_rewrite 1 ← one_pow (k + 1),
+  exact (nat.pow_lt_pow_of_lt_left hp.1.one_lt $ nat.succ_pos k).ne'
 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 :=
-by rw [padic_val_int, ←int.nat_abs_eq_zero, ←padic_val_nat_dvd_iff, ←int.coe_nat_dvd_left,
-       int.coe_nat_pow]
+variables {p : ℕ} [hp : fact p.prime]
+
+include hp
+
+lemma padic_val_int_dvd_iff (n : ℕ) (a : ℤ) : (p : ℤ) ^ n ∣ a ↔ a = 0 ∨ n ≤ padic_val_int p a :=
+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 :=
+lemma padic_val_int_dvd (a : ℤ) : (p : ℤ) ^ padic_val_int p a ∣ a :=
 begin
   rw padic_val_int_dvd_iff,
-  exact or.inr le_rfl,
+  exact or.inr le_rfl
 end
 
-lemma padic_val_int_self (p : ℕ) [pp : fact p.prime] : padic_val_int p p = 1 :=
-padic_val_int.self pp.out.one_lt
+lemma padic_val_int_self : padic_val_int p p = 1 := padic_val_int.self hp.out.one_lt
 
-lemma padic_val_int.mul (p : ℕ) [fact p.prime] {a b : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) :
+lemma padic_val_int.mul {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,
   rw [int.nat_abs_mul, padic_val_nat.mul];
-  rwa int.nat_abs_ne_zero,
+  rwa int.nat_abs_ne_zero
 end
 
-lemma padic_val_int_mul_eq_succ (p : ℕ) [pp : fact p.prime] (a : ℤ) (ha : a ≠ 0) :
+lemma padic_val_int_mul_eq_succ (a : ℤ) (ha : a ≠ 0) :
   padic_val_int p (a * p) = (padic_val_int p a) + 1 :=
 begin
-  rw padic_val_int.mul p ha (int.coe_nat_ne_zero.mpr (pp.out).ne_zero),
+  rw padic_val_int.mul ha (int.coe_nat_ne_zero.mpr hp.out.ne_zero),
   simp only [eq_self_iff_true, padic_val_int.of_nat, padic_val_nat_self],
+  exact hp
 end
 
 end padic_val_int
diff --git a/src/ring_theory/polynomial/cyclotomic/eval.lean b/src/ring_theory/polynomial/cyclotomic/eval.lean
index 63d26e79b4296..79c5b3ed040c4 100644
--- a/src/ring_theory/polynomial/cyclotomic/eval.lean
+++ b/src/ring_theory/polynomial/cyclotomic/eval.lean
@@ -162,8 +162,8 @@ begin
 
   have := prod_cyclotomic_eq_geom_sum hn' ℤ,
   apply_fun eval 1 at this,
-  rw [eval_geom_sum, one_geom_sum, eval_prod, eq_comm,
-      ←finset.prod_sdiff $ range_pow_padic_val_nat_subset_divisors' p, finset.prod_image] at this,
+  rw [eval_geom_sum, one_geom_sum, eval_prod, eq_comm, ←finset.prod_sdiff $
+        @range_pow_padic_val_nat_subset_divisors' p _ _, finset.prod_image] at this,
   simp_rw [eval_one_cyclotomic_prime_pow, finset.prod_const, finset.card_range, mul_comm] at this,
   rw [←finset.prod_sdiff $ show {n} ⊆ _, from _] at this,
   any_goals {apply_instance},