refactor(algebra/char_zero): use function.injective (#1894)

No need to require `↔` in the definition.

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/algebra/char_zero.lean

@@ -5,25 +5,27 @@ Authors: Mario Carneiro
 
 Natural homomorphism from the natural numbers into a monoid with one.
 -/
-import data.nat.cast algebra.group algebra.field
+import data.nat.cast algebra.group algebra.field tactic.wlog
 
 /-- Typeclass for monoids with characteristic zero.
   (This is usually stated on fields but it makes sense for any additive monoid with 1.) -/
 class char_zero (α : Type*) [add_monoid α] [has_one α] : Prop :=
-(cast_inj : ∀ {m n : ℕ}, (m : α) = n ↔ m = n)
+(cast_injective : function.injective (coe : ℕ → α))
 
 theorem char_zero_of_inj_zero {α : Type*} [add_monoid α] [has_one α]
   (add_left_cancel : ∀ a b c : α, a + b = a + c → b = c)
   (H : ∀ n:ℕ, (n:α) = 0 → n = 0) : char_zero α :=
-⟨λ m n, ⟨suffices ∀ {m n : ℕ}, (m:α) = n → m ≤ n,
-  from λ h, le_antisymm (this h) (this h.symm),
-  λ m n h, (le_total m n).elim id $ λ h2, le_of_eq $ begin
-    cases nat.le.dest h2 with k e,
-    suffices : k = 0, {rw [← e, this, add_zero]},
-    apply H, apply add_left_cancel n,
-    rw [← nat.cast_add, e, add_zero, h]
-  end,
-congr_arg _⟩⟩
+⟨λ m n, begin
+   assume h,
+   wlog hle : m ≤ n,
+   cases nat.le.dest hle with k e,
+   suffices : k = 0, by rw [← e, this, add_zero],
+   apply H, apply add_left_cancel n,
+   rw [← h, ← nat.cast_add, e, add_zero, h]
+ end⟩
+
+-- We have no `left_cancel_add_monoid`, so we restate it for `add_group`
+-- and `ordered_cancel_comm_monoid`.
 
 theorem add_group.char_zero_of_inj_zero {α : Type*} [add_group α] [has_one α]
   (H : ∀ n:ℕ, (n:α) = 0 → n = 0) : char_zero α :=
@@ -44,16 +46,16 @@ ordered_cancel_comm_monoid.char_zero_of_inj_zero $
 namespace nat
 variables {α : Type*} [add_monoid α] [has_one α] [char_zero α]
 
-@[simp, elim_cast] theorem cast_inj {m n : ℕ} : (m : α) = n ↔ m = n :=
-char_zero.cast_inj _
+theorem cast_injective : function.injective (coe : ℕ → α) :=
+char_zero.cast_injective α
 
-theorem cast_injective : function.injective (coe : ℕ → α)
-| m n := cast_inj.1
+@[simp, elim_cast] theorem cast_inj {m n : ℕ} : (m : α) = n ↔ m = n :=
+cast_injective.eq_iff
 
-@[simp] theorem cast_eq_zero {n : ℕ} : (n : α) = 0 ↔ n = 0 :=
+@[simp, elim_cast] theorem cast_eq_zero {n : ℕ} : (n : α) = 0 ↔ n = 0 :=
 by rw [← cast_zero, cast_inj]
 
-@[simp] theorem cast_ne_zero {n : ℕ} : (n : α) ≠ 0 ↔ n ≠ 0 :=
+@[simp, elim_cast] theorem cast_ne_zero {n : ℕ} : (n : α) ≠ 0 ↔ n ≠ 0 :=
 not_congr cast_eq_zero
 
 end nat

src/data/padics/padic_numbers.lean

@@ -487,7 +487,7 @@ lemma of_rat_eq {q r : ℚ} : of_rat p q = of_rat p r ↔ q = r :=
 by simp [cast_eq_of_rat, of_rat_eq]
 
 instance : char_zero ℚ_[p] :=
-⟨λ m n, by { rw ← rat.cast_coe_nat, norm_cast }⟩
+⟨λ m n, by { rw ← rat.cast_coe_nat, norm_cast, exact id }⟩
 
 end completion
 end padic

src/data/real/ennreal.lean

@@ -272,9 +272,14 @@ lemma lt_iff_exists_real_btwn :
 
 lemma coe_nat_lt_coe {n : ℕ} : (n : ennreal) < r ↔ ↑n < r := ennreal.coe_nat n ▸ coe_lt_coe
 lemma coe_lt_coe_nat {n : ℕ} : (r : ennreal) < n ↔ r < n := ennreal.coe_nat n ▸ coe_lt_coe
-lemma coe_nat_lt_coe_nat {m n : ℕ} : (m : ennreal) < n ↔ m < n :=
+@[elim_cast] lemma coe_nat_lt_coe_nat {m n : ℕ} : (m : ennreal) < n ↔ m < n :=
 ennreal.coe_nat n ▸ coe_nat_lt_coe.trans nat.cast_lt
 lemma coe_nat_ne_top {n : ℕ} : (n : ennreal) ≠ ∞ := ennreal.coe_nat n ▸ coe_ne_top
+lemma coe_nat_mono : strict_mono (coe : ℕ → ennreal) := λ _ _, coe_nat_lt_coe_nat.2
+@[elim_cast] lemma coe_nat_le_coe_nat {m n : ℕ} : (m : ennreal) ≤ n ↔ m ≤ n :=
+coe_nat_mono.le_iff_le
+
+instance : char_zero ennreal := ⟨coe_nat_mono.injective⟩
 
 protected lemma exists_nat_gt {r : ennreal} (h : r ≠ ⊤) : ∃n:ℕ, r < n :=
 begin

src/data/zsqrtd/basic.lean

@@ -133,7 +133,7 @@ section
   by simp [ext]
 
   instance : char_zero ℤ√d :=
-  { cast_inj := λ m n, ⟨by simp [zsqrtd.ext], congr_arg _⟩ }
+  { cast_injective := λ m n, by simp [ext] }
 
   @[simp] theorem of_int_eq_coe (n : ℤ) : (of_int n : ℤ√d) = n :=
   by simp [ext]