chore(algebra/*): Fix lint (#16128)

Satisfy the `fintype_finite` and `to_additive_doc` linters.

src/algebra/big_operators/fin.lean

@@ -58,27 +58,24 @@ theorem prod_univ_zero [comm_monoid β] (f : fin 0 → β) : ∏ i, f i = 1 := r
 
 /-- A product of a function `f : fin (n + 1) → β` over all `fin (n + 1)`
 is the product of `f x`, for some `x : fin (n + 1)` times the remaining product -/
-@[to_additive
-/- A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)`
-is the sum of `f x`, for some `x : fin (n + 1)` plus the remaining product -/]
+@[to_additive "A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)` is the sum of `f x`,
+for some `x : fin (n + 1)` plus the remaining product"]
 theorem prod_univ_succ_above [comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) (x : fin (n + 1)) :
   ∏ i, f i = f x * ∏ i : fin n, f (x.succ_above i) :=
 by rw [univ_succ_above, prod_cons, finset.prod_map, rel_embedding.coe_fn_to_embedding]
 
 /-- A product of a function `f : fin (n + 1) → β` over all `fin (n + 1)`
 is the product of `f 0` plus the remaining product -/
-@[to_additive
-/- A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)`
-is the sum of `f 0` plus the remaining product -/]
+@[to_additive "A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)` is the sum of `f 0`
+plus the remaining product"]
 theorem prod_univ_succ [comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) :
   ∏ i, f i = f 0 * ∏ i : fin n, f i.succ :=
 prod_univ_succ_above f 0
 
 /-- A product of a function `f : fin (n + 1) → β` over all `fin (n + 1)`
 is the product of `f (fin.last n)` plus the remaining product -/
-@[to_additive
-/- A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)`
-is the sum of `f (fin.last n)` plus the remaining sum -/]
+@[to_additive "A sum of a function `f : fin (n + 1) → β` over all `fin (n + 1)` is the sum of
+`f (fin.last n)` plus the remaining sum"]
 theorem prod_univ_cast_succ [comm_monoid β] {n : ℕ} (f : fin (n + 1) → β) :
   ∏ i, f i = (∏ i : fin n, f i.cast_succ) * f (last n) :=
 by simpa [mul_comm] using prod_univ_succ_above f (last n)

src/algebra/big_operators/finprod.lean

@@ -776,10 +776,11 @@ finprod_mem_mul_diff' hst (ht.inter_of_left _)
 @[to_additive "Given a family of pairwise disjoint finite sets `t i` indexed by a finite type, the
 sum of `f a` over the union `⋃ i, t i` is equal to the sum over all indexes `i` of the sums of `f a`
 over `a ∈ t i`."]
-lemma finprod_mem_Union [fintype ι] {t : ι → set α} (h : pairwise (disjoint on t))
+lemma finprod_mem_Union [finite ι] {t : ι → set α} (h : pairwise (disjoint on t))
   (ht : ∀ i, (t i).finite) :
   ∏ᶠ a ∈ (⋃ i : ι, t i), f a = ∏ᶠ i, ∏ᶠ a ∈ t i, f a :=
 begin
+  casesI nonempty_fintype ι,
   lift t to ι → finset α using ht,
   classical,
   rw [← bUnion_univ, ← finset.coe_univ, ← finset.coe_bUnion,

src/algebra/big_operators/pi.lean

@@ -60,10 +60,10 @@ lemma finset.univ_sum_single [fintype I] (f : Π i, Z i) :
   ∑ i, pi.single i (f i) = f :=
 by { ext a, simp }
 
-lemma add_monoid_hom.functions_ext [fintype I] (G : Type*)
-  [add_comm_monoid G] (g h : (Π i, Z i) →+ G)
-  (w : ∀ (i : I) (x : Z i), g (pi.single i x) = h (pi.single i x)) : g = h :=
+lemma add_monoid_hom.functions_ext [finite I] (G : Type*) [add_comm_monoid G]
+  (g h : (Π i, Z i) →+ G) (w : ∀ i x, g (pi.single i x) = h (pi.single i x)) :g = h :=
 begin
+  casesI nonempty_fintype I,
   ext k,
   rw [← finset.univ_sum_single k, g.map_sum, h.map_sum],
   simp only [w]
@@ -72,7 +72,7 @@ end
 /-- This is used as the ext lemma instead of `add_monoid_hom.functions_ext` for reasons explained in
 note [partially-applied ext lemmas]. -/
 @[ext]
-lemma add_monoid_hom.functions_ext' [fintype I] (M : Type*) [add_comm_monoid M]
+lemma add_monoid_hom.functions_ext' [finite I] (M : Type*) [add_comm_monoid M]
   (g h : (Π i, Z i) →+ M)
   (H : ∀ i, g.comp (add_monoid_hom.single Z i) = h.comp (add_monoid_hom.single Z i)) :
   g = h :=
@@ -86,7 +86,7 @@ open pi
 variables {I : Type*} [decidable_eq I] {f : I → Type*}
 variables [Π i, non_assoc_semiring (f i)]
 
-@[ext] lemma ring_hom.functions_ext [fintype I] (G : Type*) [non_assoc_semiring G]
+@[ext] lemma ring_hom.functions_ext [finite 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 I _ f _ _ G _ (g : (Π i, f i) →+ G) h w

src/algebra/category/Group/limits.lean

@@ -66,7 +66,8 @@ the existing limit. -/
 
 All we need to do is notice that the limit point has an `add_group` instance available, and then
 reuse the existing limit."]
-instance (F : J ⥤ Group.{max v u}) : creates_limit F (forget₂ Group.{max v u} Mon.{max v u}) :=
+instance forget₂.creates_limit (F : J ⥤ Group.{max v u}) :
+  creates_limit F (forget₂ Group.{max v u} Mon.{max v u}) :=
 creates_limit_of_reflects_iso (λ c' t,
 { lifted_cone :=
   { X := Group.of (types.limit_cone (F ⋙ forget Group)).X,
@@ -159,8 +160,12 @@ We show that the forgetful functor `CommGroup ⥤ Group` creates limits.
 All we need to do is notice that the limit point has a `comm_group` instance available,
 and then reuse the existing limit.
 -/
-@[to_additive]
-instance (F : J ⥤ CommGroup.{max v u}) : creates_limit F (forget₂ CommGroup Group.{max v u}) :=
+@[to_additive "We show that the forgetful functor `AddCommGroup ⥤ AddGroup` creates limits.
+
+All we need to do is notice that the limit point has an `add_comm_group` instance available, and
+then reuse the existing limit."]
+instance forget₂.creates_limit (F : J ⥤ CommGroup.{max v u}) :
+  creates_limit F (forget₂ CommGroup Group.{max v u}) :=
 creates_limit_of_reflects_iso (λ c' t,
 { lifted_cone :=
   { X := CommGroup.of (types.limit_cone (F ⋙ forget CommGroup)).X,

src/algebra/char_p/basic.lean

@@ -329,10 +329,10 @@ theorem frobenius_inj [comm_ring R] [is_reduced R]
 
 /-- If `ring_char R = 2`, where `R` is a finite reduced commutative ring,
 then every `a : R` is a square. -/
-lemma is_square_of_char_two' {R : Type*} [fintype R] [comm_ring R] [is_reduced R] [char_p R 2]
+lemma is_square_of_char_two' {R : Type*} [finite R] [comm_ring R] [is_reduced R] [char_p R 2]
  (a : R) : is_square a :=
-exists_imp_exists (λ b h, pow_two b ▸ eq.symm h) $
-  ((fintype.bijective_iff_injective_and_card _).mpr ⟨frobenius_inj R 2, rfl⟩).surjective a
+by { casesI nonempty_fintype R, exact exists_imp_exists (λ b h, pow_two b ▸ eq.symm h)
+  (((fintype.bijective_iff_injective_and_card _).mpr ⟨frobenius_inj R 2, rfl⟩).surjective a) }
 
 namespace char_p
 

src/algebra/hom/freiman.lean

@@ -121,9 +121,10 @@ instance fun_like : fun_like (A →*[n] β) α (λ _, β) :=
 instance freiman_hom_class : freiman_hom_class (A →*[n] β) A β n :=
 { map_prod_eq_map_prod' := map_prod_eq_map_prod' }
 
-/-- Helper instance for when there's too many metavariables to apply
-`fun_like.has_coe_to_fun` directly. -/
-@[to_additive]
+/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
+directly. -/
+@[to_additive "Helper instance for when there's too many metavariables to apply
+`fun_like.has_coe_to_fun` directly."]
 instance : has_coe_to_fun (A →*[n] β) (λ _, α → β) := ⟨to_fun⟩
 
 initialize_simps_projections freiman_hom (to_fun → apply)

src/algebra/order/group.lean

@@ -87,13 +87,13 @@ section typeclasses_left_le
 variables [has_le α] [covariant_class α α (*) (≤)] {a b c d : α}
 
 /--  Uses `left` co(ntra)variant. -/
-@[simp, to_additive left.neg_nonpos_iff]
+@[simp, to_additive left.neg_nonpos_iff "Uses `left` co(ntra)variant."]
 lemma left.inv_le_one_iff :
   a⁻¹ ≤ 1 ↔ 1 ≤ a :=
 by { rw [← mul_le_mul_iff_left a], simp }
 
 /--  Uses `left` co(ntra)variant. -/
-@[simp, to_additive left.nonneg_neg_iff]
+@[simp, to_additive left.nonneg_neg_iff "Uses `left` co(ntra)variant."]
 lemma left.one_le_inv_iff :
   1 ≤ a⁻¹ ↔ a ≤ 1 :=
 by { rw [← mul_le_mul_iff_left a], simp }
@@ -128,13 +128,13 @@ section typeclasses_left_lt
 variables [has_lt α] [covariant_class α α (*) (<)] {a b c : α}
 
 /--  Uses `left` co(ntra)variant. -/
-@[simp, to_additive left.neg_pos_iff]
+@[simp, to_additive left.neg_pos_iff "Uses `left` co(ntra)variant."]
 lemma left.one_lt_inv_iff :
   1 < a⁻¹ ↔ a < 1 :=
 by rw [← mul_lt_mul_iff_left a, mul_inv_self, mul_one]
 
 /--  Uses `left` co(ntra)variant. -/
-@[simp, to_additive left.neg_neg_iff]
+@[simp, to_additive left.neg_neg_iff "Uses `left` co(ntra)variant."]
 lemma left.inv_lt_one_iff :
   a⁻¹ < 1 ↔ 1 < a :=
 by rw [← mul_lt_mul_iff_left a, mul_inv_self, mul_one]
@@ -169,13 +169,13 @@ section typeclasses_right_le
 variables [has_le α] [covariant_class α α (swap (*)) (≤)] {a b c : α}
 
 /--  Uses `right` co(ntra)variant. -/
-@[simp, to_additive right.neg_nonpos_iff]
+@[simp, to_additive right.neg_nonpos_iff "Uses `right` co(ntra)variant."]
 lemma right.inv_le_one_iff :
   a⁻¹ ≤ 1 ↔ 1 ≤ a :=
 by { rw [← mul_le_mul_iff_right a], simp }
 
 /--  Uses `right` co(ntra)variant. -/
-@[simp, to_additive right.nonneg_neg_iff]
+@[simp, to_additive right.nonneg_neg_iff "Uses `right` co(ntra)variant."]
 lemma right.one_le_inv_iff :
   1 ≤ a⁻¹ ↔ a ≤ 1 :=
 by { rw [← mul_le_mul_iff_right a], simp }

src/algebra/order/lattice_group.lean

@@ -471,7 +471,7 @@ sup_le (mabs_sup_div_sup_le_mabs a b c) (mabs_inf_div_inf_le_mabs a b c)
 /--
 The absolute value satisfies the triangle inequality.
 -/
-@[to_additive abs_add_le]
+@[to_additive abs_add_le "The absolute value satisfies the triangle inequality."]
 lemma mabs_mul_le [covariant_class α α (*) (≤)] (a b : α) : |a * b| ≤ |a| * |b| :=
 begin
   apply sup_le,