feat: add_monoid_with_one, add_group_with_one (#12182)

Adds two type classes `add_monoid_with_one R` and `add_group_with_one R` with operations for `ℕ → R` and `ℤ → R`, resp.  The type classes extend `add_monoid` and `add_group` because those seem to be the weakest type classes where such a `+₀₁`-homomorphism is guaranteed to exist.  The `nat.cast` function as well as `coe : ℕ → R` are implemented in terms of `add_monoid_with_one R`, removing the infamous `nat.cast` diamond.  Fixes #946.

Some lemmas are less general now because the algebraic hierarchy is not fine-grained enough, or because the lawful coercion only exists for monoids and above.  This generality was not used in mathlib as far as I could tell.  For example:
 - `char_p.char_p_to_char_zero` now requires a group instead of a left-cancellative monoid, because we don't have the `add_left_cancel_monoid_with_one` class
 - `nat.norm_cast_le` now requires a seminormed ring instead of a seminormed group, because we don't have `semi_normed_group_with_one`

archive/100-theorems-list/16_abel_ruffini.lean

@@ -78,11 +78,11 @@ begin
     interval_cases n with hn;
     simp only [Φ, coeff_X_pow, coeff_C, int.coe_nat_dvd.mpr, hpb, if_true, coeff_C_mul, if_false,
       nat.zero_ne_bit1, eq_self_iff_true, coeff_X_zero, hpa, coeff_add, zero_add, mul_zero,
-      int.nat_cast_eq_coe_nat, coeff_sub, sub_self, nat.one_ne_zero, add_zero, coeff_X_one, mul_one,
+      coeff_sub, sub_self, nat.one_ne_zero, add_zero, coeff_X_one, mul_one,
       zero_sub, dvd_neg, nat.one_eq_bit1, bit0_eq_zero, neg_zero, nat.bit0_ne_bit1,
       dvd_mul_of_dvd_left, nat.bit1_eq_bit1, nat.one_ne_bit0, nat.bit1_ne_zero], },
   { simp only [degree_Phi, ←with_bot.coe_zero, with_bot.coe_lt_coe, nat.succ_pos'] },
-  { rw [coeff_zero_Phi, span_singleton_pow, mem_span_singleton, int.nat_cast_eq_coe_nat],
+  { rw [coeff_zero_Phi, span_singleton_pow, mem_span_singleton],
     exact mt int.coe_nat_dvd.mp hp2b },
   all_goals { exact monic.is_primitive (monic_Phi a b) },
 end

archive/100-theorems-list/30_ballot_problem.lean

@@ -502,7 +502,7 @@ begin
       { apply ne_of_gt,
         norm_cast,
         linarith },
-      field_simp [h₄, h₅, h₆],
+      field_simp [h₄, h₅, h₆] at *,
       ring },
     all_goals { refine (ennreal.mul_lt_top (measure_lt_top _ _).ne _).ne,
       simp [ne.def, ennreal.div_eq_top] } }

archive/imo/imo2013_q5.lean

@@ -209,15 +209,17 @@ begin
     { exact (lt_irrefl 0 hn).elim },
     induction n with pn hpn,
     { simp only [one_mul, nat.cast_one] },
-    calc (↑pn + 1 + 1) * f x
-          = ((pn : ℝ) + 1) * f x + 1 * f x : add_mul (↑pn + 1) 1 (f x)
+    calc    ↑(pn + 2) * f x
+          = (↑pn + 1 + 1) * f x            : by norm_cast
+      ... = ((pn : ℝ) + 1) * f x + 1 * f x : add_mul (↑pn + 1) 1 (f x)
       ... = (↑pn + 1) * f x + f x          : by rw one_mul
       ... ≤ f ((↑pn.succ) * x) + f x       : by exact_mod_cast add_le_add_right
                                                   (hpn pn.succ_pos) (f x)
       ... ≤ f ((↑pn + 1) * x + x)          : by exact_mod_cast H2 _ _
                                                   (mul_pos pn.cast_add_one_pos hx) hx
       ... = f ((↑pn + 1) * x + 1 * x)      : by rw one_mul
-      ... = f ((↑pn + 1 + 1) * x)          : congr_arg f (add_mul (↑pn + 1) 1 x).symm },
+      ... = f ((↑pn + 1 + 1) * x)          : congr_arg f (add_mul (↑pn + 1) 1 x).symm
+      ... = f (↑(pn + 2) * x)              : by norm_cast },
   have H4 : ∀ n : ℕ, 0 < n → (n : ℝ) ≤ f n,
   { intros n hn,
     have hf1 : 1 ≤ f 1,

archive/imo/imo2019_q4.lean

@@ -80,7 +80,7 @@ begin
   have := imo2019_q4_upper_bound hk h,
   interval_cases n,
   /- n = 1 -/
-  { left, congr, norm_num at h, norm_cast at h, rw [factorial_eq_one] at h, apply antisymm h,
+  { left, congr, norm_num at h, rw [factorial_eq_one] at h, apply antisymm h,
     apply succ_le_of_lt hk },
   /- n = 2 -/
   { right, congr, norm_num [prod_range_succ] at h, norm_cast at h, rw [← factorial_inj],

counterexamples/phillips.lean

@@ -281,8 +281,8 @@ begin
           union_diff_left],
       rw [nat.succ_eq_add_one, this, f.additive],
       swap, { rw disjoint.comm, apply disjoint_diff },
-      calc ((n + 1) : ℝ) * (ε / 2) = ε / 2 + n * (ε / 2) : by ring
-      ... ≤ f ((s (n + 1)) \ (s n)) + f (s n) : add_le_add (I1 n) IH } },
+      calc ((n + 1 : ℕ) : ℝ) * (ε / 2) = ε / 2 + n * (ε / 2) : by simp only [nat.cast_succ]; ring
+      ... ≤ f ((s (n + 1 : ℕ)) \ (s n)) + f (s n) : add_le_add (I1 n) IH } },
   rcases exists_nat_gt (f.C / (ε / 2)) with ⟨n, hn⟩,
   have : (n : ℝ) ≤ f.C / (ε / 2),
     by { rw le_div_iff (half_pos ε_pos), exact (I2 n).trans (f.le_bound _) },

src/algebra/algebra/operations.lean

@@ -304,6 +304,7 @@ instance : semiring (submodule R A) :=
   mul_zero      := mul_bot,
   left_distrib  := mul_sup,
   right_distrib := sup_mul,
+  ..add_monoid_with_one.unary,
   ..submodule.pointwise_add_comm_monoid,
   ..submodule.has_one,
   ..submodule.has_mul }

src/algebra/algebra/subalgebra/basic.lean

@@ -1078,8 +1078,8 @@ variables {R : Type*} [ring R]
 
 /-- A subring is a `ℤ`-subalgebra. -/
 def subalgebra_of_subring (S : subring R) : subalgebra ℤ R :=
-{ algebra_map_mem' := λ i, int.induction_on i S.zero_mem
-  (λ i ih, S.add_mem ih S.one_mem)
+{ algebra_map_mem' := λ i, int.induction_on i (by simpa using S.zero_mem)
+  (λ i ih, by simpa using S.add_mem ih S.one_mem)
   (λ i ih, show ((-i - 1 : ℤ) : R) ∈ S, by { rw [int.cast_sub, int.cast_one],
     exact S.sub_mem ih S.one_mem }),
   .. S }

src/algebra/big_operators/basic.lean

@@ -1722,23 +1722,23 @@ end multiset
 
 namespace nat
 
-@[simp, norm_cast] lemma cast_list_sum [add_monoid β] [has_one β] (s : list ℕ) :
+@[simp, norm_cast] lemma cast_list_sum [add_monoid_with_one β] (s : list ℕ) :
   (↑(s.sum) : β) = (s.map coe).sum :=
 map_list_sum (cast_add_monoid_hom β) _
 
 @[simp, norm_cast] lemma cast_list_prod [semiring β] (s : list ℕ) :
   (↑(s.prod) : β) = (s.map coe).prod :=
 map_list_prod (cast_ring_hom β) _
 
-@[simp, norm_cast] lemma cast_multiset_sum [add_comm_monoid β] [has_one β] (s : multiset ℕ) :
+@[simp, norm_cast] lemma cast_multiset_sum [add_comm_monoid_with_one β] (s : multiset ℕ) :
   (↑(s.sum) : β) = (s.map coe).sum :=
 map_multiset_sum (cast_add_monoid_hom β) _
 
 @[simp, norm_cast] lemma cast_multiset_prod [comm_semiring β] (s : multiset ℕ) :
   (↑(s.prod) : β) = (s.map coe).prod :=
 map_multiset_prod (cast_ring_hom β) _
 
-@[simp, norm_cast] lemma cast_sum [add_comm_monoid β] [has_one β] (s : finset α) (f : α → ℕ) :
+@[simp, norm_cast] lemma cast_sum [add_comm_monoid_with_one β] (s : finset α) (f : α → ℕ) :
   ↑(∑ x in s, f x : ℕ) = (∑ x in s, (f x : β)) :=
 map_sum (cast_add_monoid_hom β) _ _
 
@@ -1750,23 +1750,23 @@ end nat
 
 namespace int
 
-@[simp, norm_cast] lemma cast_list_sum [add_group β] [has_one β] (s : list ℤ) :
+@[simp, norm_cast] lemma cast_list_sum [add_group_with_one β] (s : list ℤ) :
   (↑(s.sum) : β) = (s.map coe).sum :=
 map_list_sum (cast_add_hom β) _
 
 @[simp, norm_cast] lemma cast_list_prod [ring β] (s : list ℤ) :
   (↑(s.prod) : β) = (s.map coe).prod :=
 map_list_prod (cast_ring_hom β) _
 
-@[simp, norm_cast] lemma cast_multiset_sum [add_comm_group β] [has_one β] (s : multiset ℤ) :
+@[simp, norm_cast] lemma cast_multiset_sum [add_comm_group_with_one β] (s : multiset ℤ) :
   (↑(s.sum) : β) = (s.map coe).sum :=
 map_multiset_sum (cast_add_hom β) _
 
 @[simp, norm_cast] lemma cast_multiset_prod {R : Type*} [comm_ring R] (s : multiset ℤ) :
   (↑(s.prod) : R) = (s.map coe).prod :=
 map_multiset_prod (cast_ring_hom R) _
 
-@[simp, norm_cast] lemma cast_sum [add_comm_group β] [has_one β] (s : finset α) (f : α → ℤ) :
+@[simp, norm_cast] lemma cast_sum [add_comm_group_with_one β] (s : finset α) (f : α → ℤ) :
   ↑(∑ x in s, f x : ℤ) = (∑ x in s, (f x : β)) :=
 map_sum (cast_add_hom β) _ _
 

src/algebra/big_operators/pi.lean

@@ -89,7 +89,7 @@ variables [Π i, non_assoc_semiring (f i)]
 @[ext] lemma ring_hom.functions_ext [fintype I] (G : Type*) [non_assoc_semiring G]
   (g h : (Π i, f i) →+* G) (w : ∀ (i : I) (x : f i), g (single i x) = h (single i x)) : g = h :=
 ring_hom.coe_add_monoid_hom_injective $
- add_monoid_hom.functions_ext G (g : (Π i, f i) →+ G) h w
+  @add_monoid_hom.functions_ext I _ f _ _ G _ (g : (Π i, f i) →+ G) h w
 
 end ring_hom
 

src/algebra/category/Ring/colimits.lean

@@ -127,15 +127,11 @@ The underlying type of the colimit of a diagram in `CommRing`.
 @[derive inhabited]
 def colimit_type : Type v := quotient (colimit_setoid F)
 
-instance : comm_ring (colimit_type F) :=
+instance : add_group (colimit_type F) :=
 { zero :=
   begin
     exact quot.mk _ zero
   end,
-  one :=
-  begin
-    exact quot.mk _ one
-  end,
   neg :=
   begin
     fapply @quot.lift,
@@ -163,24 +159,6 @@ instance : comm_ring (colimit_type F) :=
       { exact relation.add_1 _ _ _ r },
       { refl } },
   end,
-  mul :=
-  begin
-    fapply @quot.lift _ _ ((colimit_type F) → (colimit_type F)),
-    { intro x,
-      fapply @quot.lift,
-      { intro y,
-        exact quot.mk _ (mul x y) },
-      { intros y y' r,
-        apply quot.sound,
-        exact relation.mul_2 _ _ _ r } },
-    { intros x x' r,
-      funext y,
-      induction y,
-      dsimp,
-      apply quot.sound,
-      { exact relation.mul_1 _ _ _ r },
-      { refl } },
-  end,
   zero_add := λ x,
   begin
     induction x,
@@ -197,28 +175,71 @@ instance : comm_ring (colimit_type F) :=
     apply relation.add_zero,
     refl,
   end,
-  one_mul := λ x,
+  add_left_neg := λ x,
   begin
     induction x,
     dsimp,
     apply quot.sound,
-    apply relation.one_mul,
+    apply relation.add_left_neg,
     refl,
   end,
-  mul_one := λ x,
+  add_assoc := λ x y z,
   begin
     induction x,
+    induction y,
+    induction z,
     dsimp,
     apply quot.sound,
-    apply relation.mul_one,
+    apply relation.add_assoc,
+    refl,
     refl,
+    refl,
+  end }
+
+instance : add_group_with_one (colimit_type F) :=
+{ one :=
+  begin
+    exact quot.mk _ one
   end,
-  add_left_neg := λ x,
+  .. colimit_type.add_group F }
+
+instance : comm_ring (colimit_type F) :=
+{ one :=
+  begin
+    exact quot.mk _ one
+  end,
+  mul :=
+  begin
+    fapply @quot.lift _ _ ((colimit_type F) → (colimit_type F)),
+    { intro x,
+      fapply @quot.lift,
+      { intro y,
+        exact quot.mk _ (mul x y) },
+      { intros y y' r,
+        apply quot.sound,
+        exact relation.mul_2 _ _ _ r } },
+    { intros x x' r,
+      funext y,
+      induction y,
+      dsimp,
+      apply quot.sound,
+      { exact relation.mul_1 _ _ _ r },
+      { refl } },
+  end,
+  one_mul := λ x,
   begin
     induction x,
     dsimp,
     apply quot.sound,
-    apply relation.add_left_neg,
+    apply relation.one_mul,
+    refl,
+  end,
+  mul_one := λ x,
+  begin
+    induction x,
+    dsimp,
+    apply quot.sound,
+    apply relation.mul_one,
     refl,
   end,
   add_comm := λ x y,
@@ -288,7 +309,8 @@ instance : comm_ring (colimit_type F) :=
     refl,
     refl,
     refl,
-  end, }
+  end,
+  .. colimit_type.add_group_with_one F }
 
 @[simp] lemma quot_zero : quot.mk setoid.r zero = (0 : colimit_type F) := rfl
 @[simp] lemma quot_one : quot.mk setoid.r one = (1 : colimit_type F) := rfl

src/algebra/char_p/algebra.lean

@@ -93,7 +93,7 @@ char_p_of_injective_algebra_map (is_fraction_ring.injective R K) p
 
 /-- If `R` has characteristic `0`, then so does Frac(R). -/
 lemma char_zero_of_is_fraction_ring [char_zero R] : char_zero K :=
-@char_p.char_p_to_char_zero K _ _ (char_p_of_is_fraction_ring R 0)
+@char_p.char_p_to_char_zero K _ (char_p_of_is_fraction_ring R 0)
 
 variables [is_domain R]
 

src/algebra/char_p/basic.lean

@@ -28,18 +28,19 @@ For instance, endowing `{0, 1}` with addition given by `max` (i.e. `1` is absorb
 `char_zero {0, 1}` does not hold and yet `char_p {0, 1} 0` does.
 This example is formalized in `counterexamples/char_p_zero_ne_char_zero`.
  -/
-class char_p [add_monoid R] [has_one R] (p : ℕ) : Prop :=
+@[mk_iff]
+class char_p [add_monoid_with_one R] (p : ℕ) : Prop :=
 (cast_eq_zero_iff [] : ∀ x:ℕ, (x:R) = 0 ↔ p ∣ x)
 
-theorem char_p.cast_eq_zero [add_monoid R] [has_one R] (p : ℕ) [char_p R p] :
+theorem char_p.cast_eq_zero [add_monoid_with_one R] (p : ℕ) [char_p R p] :
   (p:R) = 0 :=
 (char_p.cast_eq_zero_iff R p p).2 (dvd_refl p)
 
-@[simp] lemma char_p.cast_card_eq_zero [add_group R] [has_one R] [fintype R] :
+@[simp] lemma char_p.cast_card_eq_zero [add_group_with_one R] [fintype R] :
   (fintype.card R : R) = 0 :=
 by rw [← nsmul_one, card_nsmul_eq_zero]
 
-lemma char_p.int_cast_eq_zero_iff [add_group R] [has_one R] (p : ℕ) [char_p R p]
+lemma char_p.int_cast_eq_zero_iff [add_group_with_one R] (p : ℕ) [char_p R p]
   (a : ℤ) :
   (a : R) = 0 ↔ (p:ℤ) ∣ a :=
 begin
@@ -52,25 +53,25 @@ begin
     rw [int.cast_coe_nat, char_p.cast_eq_zero_iff R p, int.coe_nat_dvd] }
 end
 
-lemma char_p.int_coe_eq_int_coe_iff [add_group R] [has_one R] (p : ℕ) [char_p R p] (a b : ℤ) :
+lemma char_p.int_coe_eq_int_coe_iff [add_group_with_one R] (p : ℕ) [char_p R p] (a b : ℤ) :
   (a : R) = (b : R) ↔ a ≡ b [ZMOD p] :=
 by rw [eq_comm, ←sub_eq_zero, ←int.cast_sub,
        char_p.int_cast_eq_zero_iff R p, int.modeq_iff_dvd]
 
-theorem char_p.eq [add_monoid R] [has_one R] {p q : ℕ} (c1 : char_p R p) (c2 : char_p R q) :
+theorem char_p.eq [add_monoid_with_one R] {p q : ℕ} (c1 : char_p R p) (c2 : char_p R q) :
   p = q :=
 nat.dvd_antisymm
   ((char_p.cast_eq_zero_iff R p q).1 (char_p.cast_eq_zero _ _))
   ((char_p.cast_eq_zero_iff R q p).1 (char_p.cast_eq_zero _ _))
 
-instance char_p.of_char_zero [add_monoid R] [has_one R] [char_zero R] : char_p R 0 :=
+instance char_p.of_char_zero [add_monoid_with_one R] [char_zero R] : char_p R 0 :=
 ⟨λ x, by rw [zero_dvd_iff, ← nat.cast_zero, nat.cast_inj]⟩
 
 theorem char_p.exists [non_assoc_semiring R] : ∃ p, char_p R p :=
 by letI := classical.dec_eq R; exact
 classical.by_cases
   (assume H : ∀ p:ℕ, (p:R) = 0 → p = 0, ⟨0,
-    ⟨λ x, by rw [zero_dvd_iff]; exact ⟨H x, by rintro rfl; refl⟩⟩⟩)
+    ⟨λ x, by rw [zero_dvd_iff]; exact ⟨H x, by rintro rfl; simp⟩⟩⟩)
   (λ H, ⟨nat.find (not_forall.1 H), ⟨λ x,
     ⟨λ H1, nat.dvd_of_mod_eq_zero (by_contradiction $ λ H2,
       nat.find_min (not_forall.1 H)
@@ -86,7 +87,7 @@ classical.by_cases
 theorem char_p.exists_unique [non_assoc_semiring R] : ∃! p, char_p R p :=
 let ⟨c, H⟩ := char_p.exists R in ⟨c, H, λ y H2, char_p.eq R H2 H⟩
 
-theorem char_p.congr {R : Type u} [add_monoid R] [has_one R] {p : ℕ} (q : ℕ) [hq : char_p R q]
+theorem char_p.congr {R : Type u} [add_monoid_with_one R] {p : ℕ} (q : ℕ) [hq : char_p R q]
   (h : q = p) :
   char_p R p :=
 h ▸ hq
@@ -227,11 +228,7 @@ end
 lemma ring_hom.char_p_iff_char_p {K L : Type*} [division_ring K] [semiring L] [nontrivial L]
   (f : K →+* L) (p : ℕ) :
   char_p K p ↔ char_p L p :=
-begin
-  split;
-  { introI _c, constructor, intro n,
-    rw [← @char_p.cast_eq_zero_iff _ _ _ p _c n, ← f.injective.eq_iff, map_nat_cast f, f.map_zero] }
-end
+by simp only [char_p_iff, ← f.injective.eq_iff, map_nat_cast f, f.map_zero]
 
 section frobenius
 
@@ -340,7 +337,7 @@ namespace char_p
 section
 variables [non_assoc_ring R]
 
-lemma char_p_to_char_zero (R : Type*) [add_left_cancel_monoid R] [has_one R] [char_p R 0] :
+lemma char_p_to_char_zero (R : Type*) [add_group_with_one R] [char_p R 0] :
   char_zero R :=
 char_zero_of_inj_zero $
   λ n h0, eq_zero_of_zero_dvd ((cast_eq_zero_iff R 0 n).mp h0)
@@ -352,8 +349,8 @@ calc (k : R) = ↑(k % p + p * (k / p)) : by rw [nat.mod_add_div]
 /-- The characteristic of a finite ring cannot be zero. -/
 theorem char_ne_zero_of_fintype (p : ℕ) [hc : char_p R p] [fintype R] : p ≠ 0 :=
 assume h : p = 0,
-have char_zero R := @char_p_to_char_zero R _ _ (h ▸ hc),
-absurd (@nat.cast_injective R _ _ this) (not_injective_infinite_fintype coe)
+have char_zero R := @char_p_to_char_zero R _ (h ▸ hc),
+absurd (@nat.cast_injective R _ this) (not_injective_infinite_fintype coe)
 
 lemma ring_char_ne_zero_of_fintype [fintype R] : ring_char R ≠ 0 :=
 char_ne_zero_of_fintype R (ring_char R)

src/algebra/char_p/char_and_card.lean

@@ -53,7 +53,7 @@ lemma prime_dvd_char_iff_dvd_card {R : Type*} [comm_ring R] [fintype R] (p : ℕ
   p ∣ ring_char R ↔ p ∣ fintype.card R :=
 begin
   refine ⟨λ h, h.trans $ int.coe_nat_dvd.mp $ (char_p.int_cast_eq_zero_iff R (ring_char R)
-    (fintype.card R)).mp $ char_p.cast_card_eq_zero R, λ h, _⟩,
+    (fintype.card R)).mp $ by exact_mod_cast char_p.cast_card_eq_zero R, λ h, _⟩,
   by_contra h₀,
   rcases exists_prime_add_order_of_dvd_card p h with ⟨r, hr⟩,
   have hr₁ := add_order_of_nsmul_eq_zero r,