chore: fix casing errors per naming scheme (#1670)

Mathlib/Algebra/BigOperators/Basic.lean

@@ -630,7 +630,7 @@ theorem prod_product {s : Finset γ} {t : Finset α} {f : γ × α → β} :
 #align finset.sum_product Finset.sum_product
 
 /-- An uncurried version of `Finset.prod_product`. -/
-@[to_additive "An uncurried version of `finset.sum_product`"]
+@[to_additive "An uncurried version of `Finset.sum_product`"]
 theorem prod_product' {s : Finset γ} {t : Finset α} {f : γ → α → β} :
     (∏ x in s ×ᶠ t, f x.1 x.2) = ∏ x in s, ∏ y in t, f x y :=
   prod_product
@@ -645,7 +645,7 @@ theorem prod_product_right {s : Finset γ} {t : Finset α} {f : γ × α → β}
 #align finset.sum_product_right Finset.sum_product_right
 
 /-- An uncurried version of `Finset.prod_product_right`. -/
-@[to_additive "An uncurried version of `finset.prod_product_right`"]
+@[to_additive "An uncurried version of `Finset.prod_product_right`"]
 theorem prod_product_right' {s : Finset γ} {t : Finset α} {f : γ → α → β} :
     (∏ x in s ×ᶠ t, f x.1 x.2) = ∏ y in t, ∏ x in s, f x y :=
   prod_product_right
@@ -1057,11 +1057,11 @@ theorem prod_ite_eq [DecidableEq α] (s : Finset α) (a : α) (b : α → β) :
 /-- A product taken over a conditional whose condition is an equality test on the index and whose
 alternative is `1` has value either the term at that index or `1`.
 
-The difference with `finset.prod_ite_eq` is that the arguments to `eq` are swapped. -/
+The difference with `Finset.prod_ite_eq` is that the arguments to `eq` are swapped. -/
 @[to_additive (attr := simp) "A sum taken over a conditional whose condition is an equality
 test on the index and whose alternative is `0` has value either the term at that index or `0`.
 
-The difference with `finset.sum_ite_eq` is that the arguments to `eq` are swapped."]
+The difference with `Finset.sum_ite_eq` is that the arguments to `eq` are swapped."]
 theorem prod_ite_eq' [DecidableEq α] (s : Finset α) (a : α) (b : α → β) :
     (∏ x in s, ite (x = a) (b x) 1) = ite (a ∈ s) (b a) 1 :=
   prod_dite_eq' s a fun x _ => b x
@@ -1474,9 +1474,9 @@ theorem prod_involution {s : Finset α} {f : α → β} :
 #align finset.sum_involution Finset.sum_involution
 
 /-- The product of the composition of functions `f` and `g`, is the product over `b ∈ s.image g` of
-`f b` to the power of the cardinality of the fibre of `b`. See also `finset.prod_image`. -/
+`f b` to the power of the cardinality of the fibre of `b`. See also `Finset.prod_image`. -/
 @[to_additive "The sum of the composition of functions `f` and `g`, is the sum over `b ∈ s.image g`
-of `f b` times of the cardinality of the fibre of `b`. See also `finset.sum_image`."]
+of `f b` times of the cardinality of the fibre of `b`. See also `Finset.sum_image`."]
 theorem prod_comp [DecidableEq γ] (f : γ → β) (g : α → γ) :
     (∏ a in s, f (g a)) = ∏ b in s.image g, f b ^ (s.filter fun a => g a = b).card :=
   calc
@@ -1607,22 +1607,22 @@ theorem eq_of_card_le_one_of_prod_eq {s : Finset α} (hc : s.card ≤ 1) {f : α
 #align finset.eq_of_card_le_one_of_prod_eq Finset.eq_of_card_le_one_of_prod_eq
 #align finset.eq_of_card_le_one_of_sum_eq Finset.eq_of_card_le_one_of_sum_eq
 
-/-- Taking a product over `s : finset α` is the same as multiplying the value on a single element
+/-- Taking a product over `s : Finset α` is the same as multiplying the value on a single element
 `f a` by the product of `s.erase a`.
 
-See `multiset.prod_map_erase` for the `multiset` version. -/
-@[to_additive "Taking a sum over `s : finset α` is the same as adding the value on a single element
+See `Multiset.prod_map_erase` for the `Multiset` version. -/
+@[to_additive "Taking a sum over `s : Finset α` is the same as adding the value on a single element
 `f a` to the sum over `s.erase a`.
 
-See `multiset.sum_map_erase` for the `multiset` version."]
+See `Multiset.sum_map_erase` for the `Multiset` version."]
 theorem mul_prod_erase [DecidableEq α] (s : Finset α) (f : α → β) {a : α} (h : a ∈ s) :
     (f a * ∏ x in s.erase a, f x) = ∏ x in s, f x := by
   rw [← prod_insert (not_mem_erase a s), insert_erase h]
 #align finset.mul_prod_erase Finset.mul_prod_erase
 #align finset.add_sum_erase Finset.add_sum_erase
 
-/-- A variant of `finset.mul_prod_erase` with the multiplication swapped. -/
-@[to_additive "A variant of `finset.add_sum_erase` with the addition swapped."]
+/-- A variant of `Finset.mul_prod_erase` with the multiplication swapped. -/
+@[to_additive "A variant of `Finset.add_sum_erase` with the addition swapped."]
 theorem prod_erase_mul [DecidableEq α] (s : Finset α) (f : α → β) {a : α} (h : a ∈ s) :
     (∏ x in s.erase a, f x) * f a = ∏ x in s, f x := by rw [mul_comm, mul_prod_erase s f h]
 #align finset.prod_erase_mul Finset.prod_erase_mul
@@ -1641,8 +1641,8 @@ theorem prod_erase [DecidableEq α] (s : Finset α) {f : α → β} {a : α} (h
 #align finset.prod_erase Finset.prod_erase
 #align finset.sum_erase Finset.sum_erase
 
-/-- See also `finset.prod_boole`. -/
-@[to_additive "See also `finset.sum_boole`."]
+/-- See also `Finset.prod_boole`. -/
+@[to_additive "See also `Finset.sum_boole`."]
 theorem prod_ite_one {f : α → Prop} [DecidablePred f] (hf : (s : Set α).PairwiseDisjoint f)
     (a : β) : (∏ i in s, ite (f i) a 1) = ite (∃ i ∈ s, f i) a 1 := by
   split_ifs with h
@@ -1911,13 +1911,13 @@ namespace Fintype
 
 open Finset
 
-/-- `fintype.prod_bijective` is a variant of `finset.prod_bij` that accepts `function.bijective`.
+/-- `Fintype.prod_bijective` is a variant of `Finset.prod_bij` that accepts `Function.bijective`.
 
-See `function.bijective.prod_comp` for a version without `h`. -/
-@[to_additive "`fintype.sum_equiv` is a variant of `finset.sum_bij` that accepts
-`function.bijective`.
+See `Function.bijective.prod_comp` for a version without `h`. -/
+@[to_additive "`Fintype.sum_equiv` is a variant of `Finset.sum_bij` that accepts
+`Function.bijective`.
 
-See `function.bijective.sum_comp` for a version without `h`. "]
+See `Function.bijective.sum_comp` for a version without `h`. "]
 theorem prod_bijective {α β M : Type _} [Fintype α] [Fintype β] [CommMonoid M] (e : α → β)
     (he : Function.Bijective e) (f : α → M) (g : β → M) (h : ∀ x, f x = g (e x)) :
     (∏ x : α, f x) = ∏ x : β, g x :=
@@ -1927,15 +1927,15 @@ theorem prod_bijective {α β M : Type _} [Fintype α] [Fintype β] [CommMonoid
 #align fintype.prod_bijective Fintype.prod_bijective
 #align fintype.sum_bijective Fintype.sum_bijective
 
-/-- `fintype.prod_equiv` is a specialization of `finset.prod_bij` that
+/-- `Fintype.prod_equiv` is a specialization of `Finset.prod_bij` that
 automatically fills in most arguments.
 
-See `equiv.prod_comp` for a version without `h`.
+See `Equiv.prod_comp` for a version without `h`.
 -/
-@[to_additive "`fintype.sum_equiv` is a specialization of `finset.sum_bij` that
+@[to_additive "`Fintype.sum_equiv` is a specialization of `Finset.sum_bij` that
 automatically fills in most arguments.
 
-See `equiv.sum_comp` for a version without `h`."]
+See `Equiv.sum_comp` for a version without `h`."]
 theorem prod_equiv {α β M : Type _} [Fintype α] [Fintype β] [CommMonoid M] (e : α ≃ β) (f : α → M)
     (g : β → M) (h : ∀ x, f x = g (e x)) : (∏ x : α, f x) = ∏ x : β, g x :=
   prod_bijective e e.bijective f g h

Mathlib/Algebra/CovariantAndContravariant.lean

@@ -237,23 +237,23 @@ theorem Covariant.monotone_of_const [CovariantClass M N μ (· ≤ ·)] (m : M)
   fun _ _ ha ↦ CovariantClass.elim m ha
 
 /-- A monotone function remains monotone when composed with the partial application
-of a covariant operator. E.g., `∀ (m : ℕ), monotone f → monotone (λ n, f (m + n))`. -/
+of a covariant operator. E.g., `∀ (m : ℕ), Monotone f → Monotone (λ n, f (m + n))`. -/
 theorem Monotone.covariant_of_const [CovariantClass M N μ (· ≤ ·)] (hf : Monotone f) (m : M) :
     Monotone fun n ↦ f (μ m n) :=
   fun _ _ x ↦ hf (Covariant.monotone_of_const m x)
 
-/-- Same as `monotone.covariant_of_const`, but with the constant on the other side of
+/-- Same as `Monotone.covariant_of_const`, but with the constant on the other side of
 the operator.  E.g., `∀ (m : ℕ), monotone f → monotone (λ n, f (n + m))`. -/
 theorem Monotone.covariant_of_const' {μ : N → N → N} [CovariantClass N N (swap μ) (· ≤ ·)]
     (hf : Monotone f) (m : N) : Monotone fun n ↦ f (μ n m) :=
   fun _ _ x ↦ hf (@Covariant.monotone_of_const _ _ (swap μ) _ _ m _ _ x)
 
-/-- Dual of `monotone.covariant_of_const` -/
+/-- Dual of `Monotone.covariant_of_const` -/
 theorem Antitone.covariant_of_const [CovariantClass M N μ (· ≤ ·)] (hf : Antitone f) (m : M) :
     Antitone fun n ↦ f (μ m n) :=
   hf.comp_monotone <| Covariant.monotone_of_const m
 
-/-- Dual of `monotone.covariant_of_const'` -/
+/-- Dual of `Monotone.covariant_of_const'` -/
 theorem Antitone.covariant_of_const' {μ : N → N → N} [CovariantClass N N (swap μ) (· ≤ ·)]
     (hf : Antitone f) (m : N) : Antitone fun n ↦ f (μ n m) :=
   hf.comp_monotone <| @Covariant.monotone_of_const _ _ (swap μ) _ _ m

Mathlib/Algebra/GCDMonoid/Finset.lean

@@ -43,7 +43,7 @@ variable [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α]
 /-! ### lcm -/
 
 
-section Lcm
+section lcm
 
 /-- Least common multiple of a finite set -/
 def lcm (s : Finset β) (f : β → α) : α :=
@@ -127,12 +127,12 @@ theorem lcm_eq_zero_iff [Nontrivial α] : s.lcm f = 0 ↔ 0 ∈ f '' s := by
     Finset.mem_def]
 #align finset.lcm_eq_zero_iff Finset.lcm_eq_zero_iff
 
-end Lcm
+end lcm
 
 /-! ### gcd -/
 
 
-section Gcd
+section gcd
 
 /-- Greatest common divisor of a finite set -/
 def gcd (s : Finset β) (f : β → α) : α :=
@@ -283,7 +283,7 @@ theorem extract_gcd (f : β → α) (hs : s.Nonempty) :
       rw [dif_pos hb, hg hb]
 #align finset.extract_gcd Finset.extract_gcd
 
-end Gcd
+end gcd
 
 end Finset
 

Mathlib/Algebra/GCDMonoid/Multiset.lean

@@ -33,10 +33,10 @@ namespace Multiset
 
 variable {α : Type _} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α]
 
-/-! ### lcm -/
+/-! ### LCM -/
 
 
-section Lcm
+section lcm
 
 /-- Least common multiple of a multiset -/
 def lcm (s : Multiset α) : α :=
@@ -78,7 +78,7 @@ theorem lcm_mono {s₁ s₂ : Multiset α} (h : s₁ ⊆ s₂) : s₁.lcm ∣ s
 
 /- Porting note: Following `Algebra.GCDMonoid.Basic`'s version of `normalize_gcd`, I'm giving
 this lower priority to avoid linter complaints about simp-normal form -/
-/- Porting note: Mathport seems to be replacing `multiset.induction_on s $` with
+/- Porting note: Mathport seems to be replacing `Multiset.induction_on s $` with
 `(Multiset.induction_on s)`, when it should be `Multiset.induction_on s <|`. -/
 @[simp 1100]
 theorem normalize_lcm (s : Multiset α) : normalize s.lcm = s.lcm :=
@@ -121,12 +121,12 @@ theorem lcm_ndinsert (a : α) (s : Multiset α) : (ndinsert a s).lcm = GCDMonoid
   simp
 #align multiset.lcm_ndinsert Multiset.lcm_ndinsert
 
-end Lcm
+end lcm
 
-/-! ### gcd -/
+/-! ### GCD -/
 
 
-section Gcd
+section gcd
 
 /-- Greatest common divisor of a multiset -/
 def gcd (s : Multiset α) : α :=
@@ -260,6 +260,6 @@ theorem extract_gcd (s : Multiset α) (hs : s ≠ 0) :
         rw [← hf hx]
 #align multiset.extract_gcd Multiset.extract_gcd
 
-end Gcd
+end gcd
 
 end Multiset

Mathlib/Algebra/Group/Prod.lean

@@ -705,8 +705,8 @@ theorem coe_prodComm_symm : ⇑(prodComm : M × N ≃* N × M).symm = Prod.swap
 
 variable {M' N' : Type _} [MulOneClass M'] [MulOneClass N']
 
-/-- Product of multiplicative isomorphisms; the maps come from `equiv.prodCongr`.-/
-@[to_additive prodCongr "Product of additive isomorphisms; the maps come from `equiv.prodCongr`."]
+/-- Product of multiplicative isomorphisms; the maps come from `Equiv.prodCongr`.-/
+@[to_additive prodCongr "Product of additive isomorphisms; the maps come from `Equiv.prodCongr`."]
 def prodCongr (f : M ≃* M') (g : N ≃* N') : M × N ≃* M' × N' :=
   { f.toEquiv.prodCongr g.toEquiv with
     map_mul' := fun _ _ => Prod.ext (f.map_mul _ _) (g.map_mul _ _) }

Mathlib/Algebra/Hom/Centroid.lean

@@ -60,7 +60,7 @@ attribute [nolint docBlame] CentroidHom.toAddMonoidHom
 
 /-- `CentroidHomClass F α` states that `F` is a type of centroid homomorphisms.
 
-You should extend this class when you extend `centroid_hom`. -/
+You should extend this class when you extend `CentroidHom`. -/
 class CentroidHomClass (F : Type _) (α : outParam <| Type _) [NonUnitalNonAssocSemiring α] extends
   AddMonoidHomClass F α α where
   /-- Commutativity of centroid homomorphims with left multiplication. -/
@@ -102,7 +102,7 @@ instance : CentroidHomClass (CentroidHom α) α
   map_mul_right f := f.map_mul_right'
 
 
-/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
+/-- Helper instance for when there's too many metavariables to apply `FunLike.CoeFun`
 directly. -/
 /- Porting note: Lean gave me `unknown constant 'FunLike.CoeFun'` and says `CoeFun` is a type
 mismatch, so I used `library_search`. -/
@@ -119,31 +119,31 @@ theorem ext {f g : CentroidHom α} (h : ∀ a, f a = g a) : f = g :=
 #align centroid_hom.ext CentroidHom.ext
 
 @[simp, norm_cast]
-theorem coe_to_add_monoid_hom (f : CentroidHom α) : ⇑(f : α →+ α) = f :=
+theorem coe_toAddMonoidHom (f : CentroidHom α) : ⇑(f : α →+ α) = f :=
   rfl
-#align centroid_hom.coe_to_add_monoid_hom CentroidHom.coe_to_add_monoid_hom
+#align centroid_hom.coe_to_add_monoid_hom CentroidHom.coe_toAddMonoidHom
 
 @[simp]
-theorem to_add_monoid_hom_eq_coe (f : CentroidHom α) : f.toAddMonoidHom = f :=
+theorem toAddMonoidHom_eq_coe (f : CentroidHom α) : f.toAddMonoidHom = f :=
   rfl
-#align centroid_hom.to_add_monoid_hom_eq_coe CentroidHom.to_add_monoid_hom_eq_coe
+#align centroid_hom.to_add_monoid_hom_eq_coe CentroidHom.toAddMonoidHom_eq_coe
 
-theorem coe_to_add_monoid_hom_injective : Injective ((↑) : CentroidHom α → α →+ α) :=
+theorem coe_toAddMonoidHom_injective : Injective ((↑) : CentroidHom α → α →+ α) :=
   fun _f _g h => ext fun a ↦
     haveI := FunLike.congr_fun h a
     this
-#align centroid_hom.coe_to_add_monoid_hom_injective CentroidHom.coe_to_add_monoid_hom_injective
+#align centroid_hom.coe_to_add_monoid_hom_injective CentroidHom.coe_toAddMonoidHom_injective
 
 /-- Turn a centroid homomorphism into an additive monoid endomorphism. -/
 def toEnd (f : CentroidHom α) : AddMonoid.End α :=
   (f : α →+ α)
 #align centroid_hom.to_End CentroidHom.toEnd
 
 theorem toEnd_injective : Injective (CentroidHom.toEnd : CentroidHom α → AddMonoid.End α) :=
-  coe_to_add_monoid_hom_injective
+  coe_toAddMonoidHom_injective
 #align centroid_hom.to_End_injective CentroidHom.toEnd_injective
 
-/-- Copy of a `centroid_hom` with a new `to_fun` equal to the old one. Useful to fix
+/-- Copy of a `CentroidHom` with a new `toFun` equal to the old one. Useful to fix
 definitional equalities. -/
 protected def copy (f : CentroidHom α) (f' : α → α) (h : f' = f) : CentroidHom α :=
   { f.toAddMonoidHom.copy f' <| h with
@@ -163,7 +163,7 @@ theorem copy_eq (f : CentroidHom α) (f' : α → α) (h : f' = f) : f.copy f' h
 
 variable (α)
 
-/-- `id` as a `centroid_hom`. -/
+/-- `id` as a `CentroidHom`. -/
 protected def id : CentroidHom α :=
   { AddMonoidHom.id α with
     map_mul_left' := fun _ _ ↦ rfl
@@ -190,7 +190,7 @@ theorem id_apply (a : α) : CentroidHom.id α a = a :=
   rfl
 #align centroid_hom.id_apply CentroidHom.id_apply
 
-/-- Composition of `centroid_hom`s as a `centroid_hom`. -/
+/-- Composition of `CentroidHom`s as a `CentroidHom`. -/
 def comp (g f : CentroidHom α) : CentroidHom α :=
   { g.toAddMonoidHom.comp f.toAddMonoidHom with
     map_mul_left' := fun _a _b ↦ (congr_arg g <| f.map_mul_left' _ _).trans <| g.map_mul_left' _ _
@@ -358,7 +358,7 @@ theorem toEnd_nsmul (x : CentroidHom α) (n : ℕ) : (n • x).toEnd = n • x.t
 -- Porting note: I guess the porter has naming issues still
 -- cf.`add_monoid_hom.add_comm_monoid`
 instance : AddCommMonoid (CentroidHom α) :=
-  coe_to_add_monoid_hom_injective.addCommMonoid _ toEnd_zero toEnd_add toEnd_nsmul
+  coe_toAddMonoidHom_injective.addCommMonoid _ toEnd_zero toEnd_add toEnd_nsmul
 
 instance : NatCast (CentroidHom α) where natCast n := n • (1 : CentroidHom α)
 
@@ -408,7 +408,7 @@ section NonUnitalNonAssocRing
 
 variable [NonUnitalNonAssocRing α]
 
-/-- Negation of `centroid_hom`s as a `centroid_hom`. -/
+/-- Negation of `CentroidHom`s as a `CentroidHom`. -/
 instance : Neg (CentroidHom α) :=
   ⟨fun f ↦
     { (-f : α →+ α) with

Mathlib/Algebra/Hom/Equiv/Units/Basic.lean

@@ -181,7 +181,7 @@ theorem _root_.Group.mulRight_bijective (a : G) : Function.Bijective (· * a) :=
 #align add_group.add_right_bijective AddGroup.addRight_bijective
 
 /-- A version of `Equiv.mulLeft a b⁻¹` that is defeq to `a / b`. -/
-@[to_additive " A version of `equiv.add_left a (-b)` that is defeq to `a - b`. ", simps]
+@[to_additive " A version of `Equiv.addLeft a (-b)` that is defeq to `a - b`. ", simps]
 protected def divLeft (a : G) : G ≃ G where
   toFun b := a / b
   invFun b := b⁻¹ * a
@@ -198,7 +198,7 @@ theorem divLeft_eq_inv_trans_mulLeft (a : G) :
 #align equiv.sub_left_eq_neg_trans_add_left Equiv.subLeft_eq_neg_trans_addLeft
 
 /-- A version of `Equiv.mulRight a⁻¹ b` that is defeq to `b / a`. -/
-@[to_additive " A version of `equiv.add_right (-a) b` that is defeq to `b - a`. ", simps]
+@[to_additive " A version of `Equiv.addRight (-a) b` that is defeq to `b - a`. ", simps]
 protected def divRight (a : G) : G ≃
       G where
   toFun b := b / a

Mathlib/Algebra/Module/Basic.lean

@@ -195,9 +195,9 @@ def smulAddHom : R →+ M →+ M :=
 variable {R M}
 
 @[simp]
-theorem smul_add_hom_apply (r : R) (x : M) : smulAddHom R M r x = r • x :=
+theorem smulAddHom_apply (r : R) (x : M) : smulAddHom R M r x = r • x :=
   rfl
-#align smul_add_hom_apply smul_add_hom_apply
+#align smul_add_hom_apply smulAddHom_apply
 
 theorem Module.eq_zero_of_zero_eq_one (zero_eq_one : (0 : R) = 1) : x = 0 := by
   rw [← one_smul R x, ← zero_eq_one, zero_smul]

Mathlib/Algebra/Parity.lean

@@ -96,7 +96,7 @@ alias isSquare_iff_exists_sq ↔ IsSquare.exists_sq isSquare_of_exists_sq
 
 attribute
   [to_additive Even.exists_two_nsmul
-      "Alias of the forwards direction of\n`even_iff_exists_two_nsmul`."]
+      "Alias of the forwards direction of `even_iff_exists_two_nsmul`."]
   IsSquare.exists_sq
 
 @[to_additive Even.nsmul]

Mathlib/Algebra/Ring/CompTypeclasses.lean

@@ -127,7 +127,7 @@ theorem of_ringEquiv (e : R₁ ≃+* R₂) : RingHomInvPair (↑e : R₁ →+* R
 #align ring_hom_inv_pair.of_ring_equiv RingHomInvPair.of_ringEquiv
 
 /--
-Swap the direction of a `ring_hom_inv_pair`. This is not an instance as it would loop, and better
+Swap the direction of a `RingHomInvPair`. This is not an instance as it would loop, and better
 instances are often available and may often be preferrable to using this one. Indeed, this
 declaration is not currently used in mathlib.
 

Mathlib/Data/Fin/Tuple/Basic.lean

@@ -611,7 +611,7 @@ variable {α : Fin (n + 1) → Type u} {β : Type v}
 /- Porting note: Lean told me `(fun x x_1 ↦ α x)` was an invalid motive, but disabling
 automatic insertion and specifying that motive seems to work. -/
 /-- Define a function on `Fin (n + 1)` from a value on `i : Fin (n + 1)` and values on each
-`Fin.succAbove i j`, `j : fin n`. This version is elaborated as eliminator and works for
+`Fin.succAbove i j`, `j : Fin n`. This version is elaborated as eliminator and works for
 propositions, see also `Fin.insertNth` for a version without an `@[elab_as_elim]`
 attribute. -/
 @[elab_as_elim]