chore(*): revert #17048 (#17733)

This had merge conflicts which I've been rather reckless about resolving. Let's see what CI says.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

Author: kim-em

counterexamples/zero_divisors_in_add_monoid_algebras.lean

@@ -196,7 +196,7 @@ begin
   rintro ⟨h⟩,
   refine not_lt.mpr (h (single (0 : F) (1 : F)) (_ : single 1 1 ≤ single 0 1)) ⟨1, _⟩,
   { exact or.inr ⟨0, by simp [(by boom : ∀ j : F, j < 0 ↔ false)]⟩ },
-  { simp only [(by boom : ∀ j : F, j < 1 ↔ j = 0), of_lex_add, finsupp.coe_add, pi.to_lex_apply,
+  { simp only [(by boom : ∀ j : F, j < 1 ↔ j = 0), of_lex_add, coe_add, pi.to_lex_apply,
       pi.add_apply, forall_eq, f010, f1, eq_self_iff_true, f011, f111, zero_add, and_self] },
 end
 

src/algebra/group/opposite.lean

@@ -41,7 +41,7 @@ unop_injective.add_monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)
 
 instance [add_monoid_with_one α] : add_monoid_with_one αᵐᵒᵖ :=
 { nat_cast := λ n, op n,
-  nat_cast_zero := show op ((0 : ℕ) : α) = 0, by simp [nat.cast_zero],
+  nat_cast_zero := show op ((0 : ℕ) : α) = 0, by simp,
   nat_cast_succ := show ∀ n, op ((n + 1 : ℕ) : α) = op (n : ℕ) + 1, by simp,
   .. mul_opposite.add_monoid α, .. mul_opposite.has_one α }
 

src/algebra/group_power/lemmas.lean

@@ -358,14 +358,14 @@ instance non_unital_non_assoc_semiring.nat_is_scalar_tower [non_unital_non_assoc
   | (n + 1) := by simp_rw [succ_nsmul, ←_match n, smul_eq_mul, add_mul]
   end⟩
 
-@[norm_cast] theorem nat.cast_pow [semiring R] (n m : ℕ) : (↑(n ^ m) : R) = ↑n ^ m :=
+@[simp, norm_cast] theorem nat.cast_pow [semiring R] (n m : ℕ) : (↑(n ^ m) : R) = ↑n ^ m :=
 begin
   induction m with m ih,
   { rw [pow_zero, pow_zero], exact nat.cast_one },
   { rw [pow_succ', pow_succ', nat.cast_mul, ih] }
 end
 
-@[norm_cast] theorem int.coe_nat_pow (n m : ℕ) : ((n ^ m : ℕ) : ℤ) = n ^ m :=
+@[simp, norm_cast] theorem int.coe_nat_pow (n m : ℕ) : ((n ^ m : ℕ) : ℤ) = n ^ m :=
 by induction m with m ih; [exact int.coe_nat_one, rw [pow_succ', pow_succ', int.coe_nat_mul, ih]]
 
 theorem int.nat_abs_pow (n : ℤ) (k : ℕ) : int.nat_abs (n ^ k) = (int.nat_abs n) ^ k :=
@@ -413,7 +413,7 @@ lemma zsmul_int_int (a b : ℤ) : a • b = a * b := by simp
 
 lemma zsmul_int_one (n : ℤ) : n • 1 = n := by simp
 
-@[norm_cast] theorem int.cast_pow [ring R] (n : ℤ) (m : ℕ) : (↑(n ^ m) : R) = ↑n ^ m :=
+@[simp, norm_cast] theorem int.cast_pow [ring R] (n : ℤ) (m : ℕ) : (↑(n ^ m) : R) = ↑n ^ m :=
 begin
   induction m with m ih,
   { rw [pow_zero, pow_zero, int.cast_one] },

src/algebra/group_with_zero/units/lemmas.lean

@@ -155,16 +155,6 @@ end
 
 @[simp] lemma map_div₀ : f (a / b) = f a / f b := map_div' f (map_inv₀ f) a b
 
-@[simp]
-lemma coe_inv₀ [has_lift_t G₀ G₀'] [coe_is_monoid_with_zero_hom G₀ G₀']
-  (a : G₀) : ↑(a⁻¹) = (↑a : G₀')⁻¹ :=
-map_inv₀ (monoid_with_zero_hom.coe G₀ G₀') a
-
-@[simp]
-lemma coe_div₀ [has_lift_t G₀ G₀'] [coe_is_monoid_with_zero_hom G₀ G₀']
-  (a b : G₀) : ↑(a / b) = (↑a : G₀') / ↑b :=
-map_div₀ (monoid_with_zero_hom.coe G₀ G₀') a b
-
 end group_with_zero
 
 /-- We define the inverse as a `monoid_with_zero_hom` by extending the inverse map by zero

src/algebra/hom/group.lean

@@ -28,15 +28,6 @@ building blocks for other homomorphisms:
 * `mul_hom`
 * `monoid_with_zero_hom`
 
-Finally, we define classes that state the coercion operator `↑` (a.k.a. `coe`) is a homomorphism:
- * `coe_is_one_hom`/`coe_is_zero_hom`
- * `coe_is_mul_hom`/`coe_is_add_monoid_hom`
- * `coe_is_monoid_hom`/`coe_is_add_monoid_hom`
- * `coe_is_monoid_with_zero_hom`
-These come with a selection of `simp` lemmas stating that `↑` preserves the corresponding operation:
-`coe_add`, `coe_mul`, `coe_zero`, `coe_one`, `coe_pow`, `coe_nsmul`, `coe_zpow`, `coe_zsmul`,
-`coe_bit0`, `coe_bit1`, `coe_sub`, `coe_neg`, ..., etc.
-
 ## Notations
 
 * `→+`: Bundled `add_monoid` homs. Also use for `add_group` homs.
@@ -1255,151 +1246,3 @@ instance {M N} {hM : mul_zero_one_class M} [comm_monoid_with_zero N] : has_mul (
   { to_fun := λ a, f a * g a,
     map_zero' := by rw [map_zero, zero_mul],
     ..(f * g : M →* N) }⟩
-
-section coe
-
-/-! ### Coercions as bundled morphisms
-
-The classes `coe_is_mul_hom`, `coe_is_monoid_hom`, etc. state that the coercion map `↑`
-(a.k.a. `coe`) is a homomorphism.
-
-These classes are unbundled (they take an instance of `has_lift_t R S` as a parameter, rather than
-extending `has_lift_t` or one of its subclasses) for two reasons:
- * We wouldn't have to introduce new classes that handle transitivity (and probably cause diamonds)
- * It doesn't matter whether a coercion is written with `has_coe` or `has_lift`, you can give it
-   a homomorphism structure in exactly the same way.
--/
-
-variables (M N) [has_lift_t M N]
-
-/-- `coe_is_zero_hom M N` is a class stating that the coercion map `↑ : M → N` (a.k.a. `coe`)
-is an zero-preserving homomorphism.
--/
-class coe_is_zero_hom [has_zero M] [has_zero N] : Prop :=
-(coe_zero : (↑(0 : M) : N) = 0)
-export coe_is_zero_hom (coe_zero)
-
-attribute [simp, norm_cast] coe_zero
-
-/-- `coe_is_one_hom M N` is a class stating that the coercion map `↑ : M → N` (a.k.a. `coe`)
-is a one-preserving homomorphism.
--/
-@[to_additive]
-class coe_is_one_hom [has_one M] [has_one N] : Prop :=
-(coe_one : (↑(1 : M) : N) = 1)
-export coe_is_one_hom (coe_one)
-
-attribute [simp, norm_cast] coe_one
-
-/-- `one_hom.coe M N` is the map `↑ : M → N` (a.k.a. `coe`),
-bundled as a one-preserving homomorphism. -/
-@[to_additive "`zero_hom.coe M N` is the map `↑ : M → N` (a.k.a. `coe`),
-bundled as a zero-preserving homomorphism.", simps { fully_applied := ff }]
-protected def one_hom.coe [has_one M] [has_one N] [coe_is_one_hom M N] : one_hom M N :=
-{ to_fun := coe,
-  map_one' := coe_one }
-
-/-- `coe_is_add_hom M N` is a class stating that the coercion map `↑ : M → N` (a.k.a. `coe`)
-is an additive homomorphism.
--/
-class coe_is_add_hom [has_add M] [has_add N] : Prop :=
-(coe_add : ∀ (x y : M), (↑(x + y) : N) = ↑x + ↑y)
-export coe_is_add_hom (coe_add)
-
-attribute [simp, norm_cast] coe_add
-
-/-- `coe_is_mul_hom M N` is a class stating that the coercion map `↑ : M → N` (a.k.a. `coe`)
-is a multiplicative homomorphism.
--/
-@[to_additive]
-class coe_is_mul_hom [has_mul M] [has_mul N] : Prop :=
-(coe_mul : ∀ (x y : M), (↑(x * y) : N) = ↑x * ↑y)
-export coe_is_mul_hom (coe_mul)
-
-attribute [simp, norm_cast] coe_mul
-
-/-- `mul_hom.coe M N` is the map `↑ : M → N` (a.k.a. `coe`),
-bundled as a multiplicative homomorphism. -/
-@[to_additive "`add_hom.coe M N` is the map `↑ : M → N` (a.k.a. `coe`),
-bundled as an additive homomorphism.", simps { fully_applied := ff }]
-protected def mul_hom.coe [has_mul M] [has_mul N] [coe_is_mul_hom M N] : mul_hom M N :=
-{ to_fun := coe,
-  map_mul' := coe_mul }
-
-@[simp, norm_cast]
-lemma coe_bit0 [has_add M] [has_add N] [coe_is_add_hom M N]
-  (x : M) : ↑(bit0 x) = bit0 (↑x : N) :=
-coe_add _ _
-
-@[simp, norm_cast]
-lemma coe_bit1 [has_one M] [has_add M] [has_one N] [has_add N] [coe_is_one_hom M N]
-  [coe_is_add_hom M N] (x : M) :
-  ↑(bit1 x) = bit1 (↑x : N) :=
-by simp [bit1]
-
-/-- `coe_is_add_monoid_hom M N` is a class stating that the coercion map `↑ : M → N` (a.k.a. `coe`)
-is an additive monoid homomorphism.
--/
-class coe_is_add_monoid_hom [add_zero_class M] [add_zero_class N]
-  extends coe_is_zero_hom M N, coe_is_add_hom M N
-
-/-- `coe_is_monoid_hom M N` is a class stating that the coercion map `↑ : M → N` (a.k.a. `coe`)
-is a monoid homomorphism.
--/
-@[to_additive]
-class coe_is_monoid_hom [mul_one_class M] [mul_one_class N]
-  extends coe_is_one_hom M N, coe_is_mul_hom M N
-
--- `to_additive` doesn't seem to map these correctly...
-attribute [to_additive coe_is_add_monoid_hom.to_coe_is_zero_hom] coe_is_monoid_hom.to_coe_is_one_hom
-attribute [to_additive coe_is_add_monoid_hom.to_coe_is_add_hom] coe_is_monoid_hom.to_coe_is_mul_hom
-
-/-- `monoid_hom.coe M N` is the map `↑ : M → N` (a.k.a. `coe`),
-bundled as a monoid homomorphism. -/
-@[to_additive "`add_monoid_hom.coe M N` is the map `↑ : M → N` (a.k.a. `coe`),
-bundled as an additive monoid homomorphism.", simps { fully_applied := ff }]
-protected def monoid_hom.coe [mul_one_class M] [mul_one_class N] [coe_is_monoid_hom M N] : M →* N :=
-{ to_fun := coe,
-  .. one_hom.coe M N,
-  .. mul_hom.coe M N }
-
-variables {M N}
-
-@[simp, norm_cast, to_additive]
-lemma coe_pow [monoid M] [monoid N] [coe_is_monoid_hom M N]
-  (a : M) (n : ℕ) : ↑(a ^ n) = (↑a : N) ^ n :=
-map_pow (monoid_hom.coe M N) a n
-
-@[simp, norm_cast, to_additive]
-lemma coe_zpow [group M] [group N] [coe_is_monoid_hom M N]
-  (a : M) (n : ℤ) : ↑(a ^ n) = (↑a : N) ^ n :=
-map_zpow (monoid_hom.coe M N) a n
-
-@[simp, norm_cast, to_additive]
-lemma coe_inv [group G] [division_monoid H] [has_lift_t G H] [coe_is_monoid_hom G H]
-  (a : G) : ↑(a⁻¹) = (↑a : H)⁻¹ :=
-map_inv (monoid_hom.coe G H) a
-
-@[simp, norm_cast, to_additive]
-lemma coe_div [group G] [division_monoid H] [has_lift_t G H] [coe_is_monoid_hom G H]
-  (a b : G) : ↑(a / b) = (↑a : H) / ↑b :=
-map_div (monoid_hom.coe G H) a b
-
-variables (M N)
-
-/-- `coe_monoid_with-zero_hom M N` is a class stating that the coercion map `↑ : M → N`
-(a.k.a. `coe`) is a monoid with zero homomorphism.
--/
-class coe_is_monoid_with_zero_hom [monoid_with_zero M] [monoid_with_zero N]
-  extends coe_is_monoid_hom M N, coe_is_zero_hom M N
-
-/-- `monoid_with_zero_hom.coe M N` is the map `↑ : M → N` (a.k.a. `coe`),
-bundled as a monoid with zero homomorphism. -/
-@[simps { fully_applied := ff }]
-protected def monoid_with_zero_hom.coe [monoid_with_zero M] [monoid_with_zero N]
-  [coe_is_monoid_with_zero_hom M N] : M →*₀ N :=
-{ to_fun := coe,
-  .. monoid_hom.coe M N,
-  .. zero_hom.coe M N }
-
-end coe

src/algebra/hom/group_action.lean

@@ -354,55 +354,3 @@ def is_invariant_subring.subtype_hom : U →+*[M] R' :=
   (is_invariant_subring.subtype_hom M U : U →+* R') = U.subtype := rfl
 
 end
-
-section coe
-
-variables (M' X Y)
-
-/-- `coe_is_smul_hom M X Y` is a class stating that the coercion map `↑ : X → Y`
-(a.k.a. `coe`) preserves scalar multiplication by `M`.
-
-Note that there is no class corresponding to `mul_action`, `distrib_mul_action` or
-`mul_semiring_action`: instead we assume `coe_is_smul_hom` and `coe_is_add_monoid_hom` or
-`coe_is_ring_hom` in separate parameters.
-This is because `coe_is_smul_hom` has a different set of parameters from those other classes,
-so extending both classes at once wouldn't work.
--/
-class coe_is_smul_hom [has_lift_t X Y] :=
-(coe_smul : ∀ (c : M') (x : X), ↑(c • x) = c • (↑x : Y))
-
-export coe_is_smul_hom (coe_smul)
-
-attribute [simp, norm_cast] coe_smul
-
-/-- `mul_action_hom.coe X Y` is the map `↑ : M → N` (a.k.a. `coe`),
-bundled as a scalar-multiplication preserving map. -/
-@[simps { fully_applied := ff }]
-protected def mul_action_hom.coe [has_lift_t X Y] [coe_is_smul_hom M' X Y] : X →[M'] Y :=
-{ to_fun := coe,
-  map_smul' := coe_smul }
-
-variables (M A B)
-
-/-- `distrib_mul_action_hom.coe X Y` is the map `↑ : M → N` (a.k.a. `coe`),
-bundled as an equivariant additive monoid homomorphism. -/
-@[simps { fully_applied := ff }]
-protected def distrib_mul_action_hom.coe [has_lift_t A B] [coe_is_add_monoid_hom A B]
-  [coe_is_smul_hom M A B] : A →+[M] B :=
-{ to_fun := coe,
-  .. mul_action_hom.coe M A B,
-  .. add_monoid_hom.coe A B }
-
-variables (M X Y)
-
-/-- `mul_semiring_action_hom.coe X Y` is the map `↑ : M → N` (a.k.a. `coe`),
-bundled as an equivariant semiring homomorphism. -/
-@[simps { fully_applied := ff }]
-protected def mul_semiring_action_hom.coe [has_lift_t R S] [coe_is_ring_hom R S]
-  [coe_is_smul_hom M R S] :
-  R →+*[M] S :=
-{ to_fun := coe,
-  .. distrib_mul_action_hom.coe M R S,
-  .. ring_hom.coe R S }
-
-end coe

src/algebra/hom/group_instances.lean

@@ -233,7 +233,7 @@ def add_monoid_hom.mul : R →+ R →+ R :=
 lemma add_monoid_hom.mul_apply (x y : R) : add_monoid_hom.mul x y = x * y := rfl
 
 @[simp]
-protected lemma add_monoid_hom.coe_mul :
+lemma add_monoid_hom.coe_mul :
   ⇑(add_monoid_hom.mul : R →+ R →+ R) = add_monoid_hom.mul_left := rfl
 
 @[simp]

src/algebra/hom/ring.lean

@@ -561,49 +561,3 @@ def mk_ring_hom_of_mul_self_of_two_ne_zero (h : ∀ x, f (x * x) = f x * f x) (h
 by { ext, refl }
 
 end add_monoid_hom
-
-section coe
-
-variables (R S : Type*) [has_lift_t R S]
-
-/-- `coe_is_non_unital_ring_hom R S` is a class stating that the coercion map `↑ : R → S`
-(a.k.a. `coe`) is a non-unital ring homomorphism.
--/
-class coe_is_non_unital_ring_hom [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S]
-  extends coe_is_mul_hom R S, coe_is_add_monoid_hom R S
-
-/-- `non_unital_ring_hom.coe M N` is the map `↑ : M → N` (a.k.a. `coe`),
-bundled as a non-unital ring homomorphism. -/
-@[simps { fully_applied := ff }]
-protected def non_unital_ring_hom.coe [non_unital_non_assoc_semiring R]
-  [non_unital_non_assoc_semiring S] [coe_is_non_unital_ring_hom R S] : R →ₙ+* S :=
-{ to_fun := coe,
-  .. mul_hom.coe R S,
-  .. add_monoid_hom.coe R S }
-
-/-- `coe_is_ring_hom R S` is a class stating that the coercion map `↑ : R → S` (a.k.a. `coe`)
-is a ring homomorphism.
--/
-class coe_is_ring_hom [non_assoc_semiring R] [non_assoc_semiring S]
-  extends coe_is_monoid_hom R S, coe_is_add_monoid_hom R S
-
-@[priority 100] -- See note [lower instance priority]
-instance coe_is_ring_hom.to_coe_is_non_unital_ring_hom [non_assoc_semiring R] [non_assoc_semiring S]
-  [inst : coe_is_ring_hom R S] : coe_is_non_unital_ring_hom R S :=
-{ .. inst }
-
-@[priority 100] -- See note [lower instance priority]
-instance coe_is_ring_hom.to_coe_is_monoid_with_zero_hom [semiring R] [semiring S]
-  [inst : coe_is_ring_hom R S] : coe_is_monoid_with_zero_hom R S :=
-{ .. inst }
-
-/-- `ring_hom.coe M N` is the map `↑ : M → N` (a.k.a. `coe`),
-bundled as a ring homomorphism. -/
-@[simps { fully_applied := ff }]
-protected def ring_hom.coe [non_assoc_semiring R] [non_assoc_semiring S] [coe_is_ring_hom R S] :
-  R →+* S :=
-{ to_fun := coe,
-  .. monoid_hom.coe R S,
-  .. add_monoid_hom.coe R S }
-
-end coe