chore(number_theory/padics/padic_integers): golf the comm_ring instan…

…ce (#15590)

This results in nicer definitional equalities that don't involve the application of a recursor.

This also renames `padic_int.coe_coe` to `padic_int.coe_nat_cast` and `padic_int.coe_coe_int` to `padic_int.coe_int_cast` to match other similar lemmas in mathlib.

Finally, this fixes the TODO comment
```lean
-- TODO: define nat_cast/int_cast so that coe_coe and coe_coe_int are rfl
```

src/number_theory/padics/padic_integers.lean

@@ -61,31 +61,37 @@ variables {p : ℕ} [fact p.prime]
 
 instance : has_coe ℤ_[p] ℚ_[p] := ⟨subtype.val⟩
 
-lemma ext {x y : ℤ_[p]} : (x : ℚ_[p]) = y → x = y := subtype.ext_iff_val.2
+lemma ext {x y : ℤ_[p]} : (x : ℚ_[p]) = y → x = y := subtype.ext
+
+variables (p)
+
+/-- The padic integers as a subring of the padics -/
+def subring : subring (ℚ_[p]) :=
+{ carrier := {x : ℚ_[p] | ∥x∥ ≤ 1},
+  zero_mem' := by norm_num,
+  one_mem' := by norm_num,
+  add_mem' := λ x y hx hy, (padic_norm_e.nonarchimedean _ _).trans $ max_le_iff.2 ⟨hx, hy⟩,
+  mul_mem' := λ x y hx hy, (padic_norm_e.mul _ _).trans_le $ mul_le_one hx (norm_nonneg _) hy,
+  neg_mem' := λ x hx, (norm_neg _).trans_le hx }
+
+@[simp] lemma mem_subring_iff {x : ℚ_[p]} : x ∈ subring p ↔ ∥x∥ ≤ 1 := iff.rfl
+
+variables {p}
 
 /-- Addition on ℤ_p is inherited from ℚ_p. -/
-instance : has_add ℤ_[p] :=
-⟨λ ⟨x, hx⟩ ⟨y, hy⟩, ⟨x+y,
-    le_trans (padic_norm_e.nonarchimedean _ _) (max_le_iff.2 ⟨hx,hy⟩)⟩⟩
+instance : has_add ℤ_[p] := (by apply_instance : has_add (subring p))
 
 /-- Multiplication on ℤ_p is inherited from ℚ_p. -/
-instance : has_mul ℤ_[p] :=
-⟨λ ⟨x, hx⟩ ⟨y, hy⟩, ⟨x*y,
-    begin rw padic_norm_e.mul, apply mul_le_one; {assumption <|> apply norm_nonneg} end⟩⟩
+instance : has_mul ℤ_[p] := (by apply_instance : has_mul (subring p))
 
 /-- Negation on ℤ_p is inherited from ℚ_p. -/
-instance : has_neg ℤ_[p] :=
-⟨λ ⟨x, hx⟩, ⟨-x, by simpa⟩⟩
+instance : has_neg ℤ_[p] := (by apply_instance : has_neg (subring p))
 
 /-- Subtraction on ℤ_p is inherited from ℚ_p. -/
-instance : has_sub ℤ_[p] :=
-⟨λ ⟨x, hx⟩ ⟨y, hy⟩, ⟨x - y,
-  by { rw sub_eq_add_neg, rw ← norm_neg at hy,
-       exact le_trans (padic_norm_e.nonarchimedean _ _) (max_le_iff.2 ⟨hx, hy⟩) }⟩⟩
+instance : has_sub ℤ_[p] := (by apply_instance : has_sub (subring p))
 
 /-- Zero on ℤ_p is inherited from ℚ_p. -/
-instance : has_zero ℤ_[p] :=
-⟨⟨0, by norm_num⟩⟩
+instance : has_zero ℤ_[p] := (by apply_instance : has_zero (subring p))
 
 instance : inhabited ℤ_[p] := ⟨0⟩
 
@@ -97,69 +103,28 @@ instance : has_one ℤ_[p] :=
 
 @[simp] lemma val_eq_coe (z : ℤ_[p]) : z.val = z := rfl
 
-@[simp, norm_cast] lemma coe_add : ∀ (z1 z2 : ℤ_[p]), ((z1 + z2 : ℤ_[p]) : ℚ_[p]) = z1 + z2
-| ⟨_, _⟩ ⟨_, _⟩ := rfl
-
-@[simp, norm_cast] lemma coe_mul : ∀ (z1 z2 : ℤ_[p]), ((z1 * z2 : ℤ_[p]) : ℚ_[p]) = z1 * z2
-| ⟨_, _⟩ ⟨_, _⟩ := rfl
-
-@[simp, norm_cast] lemma coe_neg : ∀ (z1 : ℤ_[p]), ((-z1 : ℤ_[p]) : ℚ_[p]) = -z1
-| ⟨_, _⟩ := rfl
-
-@[simp, norm_cast] lemma coe_sub : ∀ (z1 z2 : ℤ_[p]), ((z1 - z2 : ℤ_[p]) : ℚ_[p]) = z1 - z2
-| ⟨_, _⟩ ⟨_, _⟩ := rfl
-
+@[simp, norm_cast] lemma coe_add (z1 z2 : ℤ_[p]) : ((z1 + z2 : ℤ_[p]) : ℚ_[p]) = z1 + z2 := rfl
+@[simp, norm_cast] lemma coe_mul (z1 z2 : ℤ_[p]) : ((z1 * z2 : ℤ_[p]) : ℚ_[p]) = z1 * z2 := rfl
+@[simp, norm_cast] lemma coe_neg (z1 : ℤ_[p]) : ((-z1 : ℤ_[p]) : ℚ_[p]) = -z1 := rfl
+@[simp, norm_cast] lemma coe_sub (z1 z2 : ℤ_[p]) : ((z1 - z2 : ℤ_[p]) : ℚ_[p]) = z1 - z2 := rfl
 @[simp, norm_cast] lemma coe_one : ((1 : ℤ_[p]) : ℚ_[p]) = 1 := rfl
-
 @[simp, norm_cast] lemma coe_zero : ((0 : ℤ_[p]) : ℚ_[p]) = 0 := rfl
 
 instance : add_comm_group ℤ_[p] :=
-by refine_struct
-{ add   := (+),
-  neg   := has_neg.neg,
-  zero  := (0 : ℤ_[p]),
-  sub   := has_sub.sub,
-  nsmul := @nsmul_rec _ ⟨(0 : ℤ_[p])⟩ ⟨(+)⟩,
-  zsmul := @zsmul_rec _ ⟨(0 : ℤ_[p])⟩ ⟨(+)⟩ ⟨has_neg.neg⟩ };
-intros; try { refl }; ext; simp; ring
-
-instance : add_group_with_one ℤ_[p] :=
--- TODO: define nat_cast/int_cast so that coe_coe and coe_coe_int are rfl
-{ one := 1, .. padic_int.add_comm_group }
-
-instance : ring ℤ_[p] :=
-by refine_struct
-{ add   := (+),
-  mul   := (*),
-  neg   := has_neg.neg,
-  zero  := (0 : ℤ_[p]),
-  one   := 1,
-  sub   := has_sub.sub,
-  npow  := @npow_rec _ ⟨(1 : ℤ_[p])⟩ ⟨(*)⟩,
-  .. padic_int.add_group_with_one };
-intros; try { refl }; ext; simp; ring
-
-@[simp, norm_cast] lemma coe_coe : ∀ n : ℕ, ((n : ℤ_[p]) : ℚ_[p]) = n
-| 0 := rfl
-| (k+1) := by simp [coe_coe]
-
-@[simp, norm_cast] lemma coe_coe_int : ∀ (z : ℤ), ((z : ℤ_[p]) : ℚ_[p]) = z
-| (int.of_nat n) := by simp
-| -[1+n] := by simp
+(by apply_instance : add_comm_group (subring p))
+
+instance : comm_ring ℤ_[p] :=
+(by apply_instance : comm_ring (subring p))
+
+@[simp, norm_cast] lemma coe_nat_cast (n : ℕ) : ((n : ℤ_[p]) : ℚ_[p]) = n := rfl
+@[simp, norm_cast] lemma coe_int_cast (z : ℤ) : ((z : ℤ_[p]) : ℚ_[p]) = z := rfl
 
 /-- The coercion from ℤ[p] to ℚ[p] as a ring homomorphism. -/
-def coe.ring_hom : ℤ_[p] →+* ℚ_[p]  :=
-{ to_fun := (coe : ℤ_[p] → ℚ_[p]),
-  map_zero' := rfl,
-  map_one' := rfl,
-  map_mul' := coe_mul,
-  map_add' := coe_add }
+def coe.ring_hom : ℤ_[p] →+* ℚ_[p] := (subring p).subtype
 
-@[simp, norm_cast] lemma coe_pow (x : ℤ_[p]) (n : ℕ) : (↑(x^n) : ℚ_[p]) = (↑x : ℚ_[p])^n :=
-(coe.ring_hom : ℤ_[p] →+* ℚ_[p]).map_pow x n
+@[simp, norm_cast] lemma coe_pow (x : ℤ_[p]) (n : ℕ) : (↑(x^n) : ℚ_[p]) = (↑x : ℚ_[p])^n := rfl
 
-@[simp] lemma mk_coe : ∀ (k : ℤ_[p]), (⟨k, k.2⟩ : ℤ_[p]) = k
-| ⟨_, _⟩ := rfl
+@[simp] lemma mk_coe (k : ℤ_[p]) : (⟨k, k.2⟩ : ℤ_[p]) = k := subtype.coe_eta _ _
 
 /-- The inverse of a p-adic integer with norm equal to 1 is also a p-adic integer. Otherwise, the
 inverse is defined to be 0. -/
@@ -212,29 +177,14 @@ instance : has_norm ℤ_[p] := ⟨λ z, ∥(z : ℚ_[p])∥⟩
 
 variables {p}
 
-protected lemma mul_comm : ∀ z1 z2 : ℤ_[p], z1*z2 = z2*z1
-| ⟨q1, h1⟩ ⟨q2, h2⟩ := show (⟨q1*q2, _⟩ : ℤ_[p]) = ⟨q2*q1, _⟩, by simp [_root_.mul_comm]
-
-protected lemma zero_ne_one : (0 : ℤ_[p]) ≠ 1 :=
-show (⟨(0 : ℚ_[p]), _⟩ : ℤ_[p]) ≠ ⟨(1 : ℚ_[p]), _⟩, from mt subtype.ext_iff_val.1 zero_ne_one
-
-protected lemma eq_zero_or_eq_zero_of_mul_eq_zero :
-          ∀ (a b : ℤ_[p]), a * b = 0 → a = 0 ∨ b = 0
-| ⟨a, ha⟩ ⟨b, hb⟩ := λ h : (⟨a * b, _⟩ : ℤ_[p]) = ⟨0, _⟩,
-have a * b = 0, from subtype.ext_iff_val.1 h,
-(mul_eq_zero.1 this).elim
-  (λ h1, or.inl (by simp [h1]; refl))
-  (λ h2, or.inr (by simp [h2]; refl))
-
 lemma norm_def {z : ℤ_[p]} : ∥z∥ = ∥(z : ℚ_[p])∥ := rfl
 
 variables (p)
 
 instance : normed_comm_ring ℤ_[p] :=
 { dist_eq := λ ⟨_, _⟩ ⟨_, _⟩, rfl,
   norm_mul := by simp [norm_def],
-  mul_comm := padic_int.mul_comm,
-  norm := norm, .. padic_int.ring, .. padic_int.metric_space p }
+  norm := norm, .. padic_int.comm_ring, .. padic_int.metric_space p }
 
 instance : norm_one_class ℤ_[p] := ⟨norm_def.trans norm_one⟩
 
@@ -247,18 +197,15 @@ instance is_absolute_value : is_absolute_value (λ z : ℤ_[p], ∥z∥) :=
 variables {p}
 
 instance : is_domain ℤ_[p] :=
-{ eq_zero_or_eq_zero_of_mul_eq_zero := λ x y, padic_int.eq_zero_or_eq_zero_of_mul_eq_zero x y,
-  exists_pair_ne := ⟨0, 1, padic_int.zero_ne_one⟩,
-  .. padic_int.normed_comm_ring p }
+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
-| ⟨_, h⟩ := h
+lemma norm_le_one (z : ℤ_[p]) : ∥z∥ ≤ 1 := z.2
 
 @[simp] lemma norm_mul (z1 z2 : ℤ_[p]) : ∥z1 * z2∥ = ∥z1∥ * ∥z2∥ :=
 by simp [norm_def]
@@ -267,11 +214,10 @@ by simp [norm_def]
 | 0 := by simp
 | (k+1) := by { rw [pow_succ, pow_succ, norm_mul], congr, apply norm_pow }
 
-theorem nonarchimedean : ∀ (q r : ℤ_[p]), ∥q + r∥ ≤ max (∥q∥) (∥r∥)
-| ⟨_, _⟩ ⟨_, _⟩ := padic_norm_e.nonarchimedean _ _
+theorem nonarchimedean (q r : ℤ_[p]) : ∥q + r∥ ≤ max (∥q∥) (∥r∥) := padic_norm_e.nonarchimedean _ _
 
-theorem norm_add_eq_max_of_ne : ∀ {q r : ℤ_[p]}, ∥q∥ ≠ ∥r∥ → ∥q+r∥ = max (∥q∥) (∥r∥)
-| ⟨_, _⟩ ⟨_, _⟩ := padic_norm_e.add_eq_max_of_ne
+theorem norm_add_eq_max_of_ne {q r : ℤ_[p]} : ∥q∥ ≠ ∥r∥ → ∥q+r∥ = max (∥q∥) (∥r∥) :=
+padic_norm_e.add_eq_max_of_ne
 
 lemma norm_eq_of_norm_add_lt_right {z1 z2 : ℤ_[p]}
   (h : ∥z1 + z2∥ < ∥z2∥) : ∥z1∥ = ∥z2∥ :=
@@ -292,12 +238,9 @@ by simp [norm_def]
 @[simp] lemma norm_eq_padic_norm {q : ℚ_[p]} (hq : ∥q∥ ≤ 1) :
   @norm ℤ_[p] _ ⟨q, hq⟩ = ∥q∥ := rfl
 
-@[simp] lemma norm_p : ∥(p : ℤ_[p])∥ = p⁻¹ :=
-show ∥((p : ℤ_[p]) : ℚ_[p])∥ = p⁻¹, by exact_mod_cast padic_norm_e.norm_p
+@[simp] lemma norm_p : ∥(p : ℤ_[p])∥ = p⁻¹ := padic_norm_e.norm_p
 
-@[simp] lemma norm_p_pow (n : ℕ) : ∥(p : ℤ_[p])^n∥ = p^(-n:ℤ) :=
-show ∥((p^n : ℤ_[p]) : ℚ_[p])∥ = p^(-n:ℤ),
-by { convert padic_norm_e.norm_p_pow n, simp, }
+@[simp] lemma norm_p_pow (n : ℕ) : ∥(p : ℤ_[p])^n∥ = p^(-n:ℤ) := padic_norm_e.norm_p_pow n
 
 private def cau_seq_to_rat_cau_seq (f : cau_seq ℤ_[p] norm) :
   cau_seq ℚ_[p] (λ a, ∥a∥) :=

src/number_theory/padics/ring_homs.lean

@@ -81,7 +81,7 @@ lemma is_unit_denom (r : ℚ) (h : ∥(r : ℚ_[p])∥ ≤ 1) : is_unit (r.denom
 begin
   rw is_unit_iff,
   apply le_antisymm (r.denom : ℤ_[p]).2,
-  rw [← not_lt, val_eq_coe, coe_coe],
+  rw [← not_lt, val_eq_coe, coe_nat_cast],
   intro norm_denom_lt,
   have hr : ∥(r * r.denom : ℚ_[p])∥ = ∥(r.num : ℚ_[p])∥,
   { rw_mod_cast @rat.mul_denom_eq_num r, refl, },
@@ -126,7 +126,7 @@ begin
     simp only [sub_mul, int.cast_coe_nat, ring_hom.eq_int_cast, int.cast_mul,
       sub_left_inj, int.cast_sub],
     apply subtype.coe_injective,
-    simp only [coe_mul, subtype.coe_mk, coe_coe],
+    simp only [coe_mul, subtype.coe_mk, coe_nat_cast],
     rw_mod_cast @rat.mul_denom_eq_num r, refl },
   exact norm_sub_mod_part_aux r h
 end
@@ -182,7 +182,7 @@ begin
   lift n to ℕ using hzn,
   use n,
   split, {exact_mod_cast hnp},
-  simp only [norm_def, coe_sub, subtype.coe_mk, coe_coe] at hn ⊢,
+  simp only [norm_def, coe_sub, subtype.coe_mk, coe_nat_cast] at hn ⊢,
   rw show (x - n : ℚ_[p]) = (x - r) + (r - n), by ring,
   apply lt_of_le_of_lt (padic_norm_e.nonarchimedean _ _),
   apply max_lt hr,
@@ -587,8 +587,7 @@ begin
   apply lt_trans _ hε',
   change ↑(padic_norm_e _) < _,
   norm_cast,
-  convert hN _ hn,
-  simp [nth_hom, lim_nth_hom, nth_hom_seq, of_int_seq],
+  exact hN _ hn,
 end
 
 lemma lim_nth_hom_zero : lim_nth_hom f_compat 0 = 0 :=