chore(*): rename some defs to camelCase (#19795)

Author: urkud

Mathlib/CategoryTheory/Monoidal/Bimon_.lean

@@ -157,14 +157,20 @@ def trivial : Bimon_ C := Comon_.trivial (Mon_ C)
 
 /-- The bimonoid morphism from the trivial bimonoid to any bimonoid. -/
 @[simps]
-def trivial_to (A : Bimon_ C) : trivial C ⟶ A :=
+def trivialTo (A : Bimon_ C) : trivial C ⟶ A :=
   { hom := (default : Mon_.trivial C ⟶ A.X), }
 
+@[deprecated (since := "2024-12-07")] alias trivial_to := trivialTo
+@[deprecated (since := "2024-12-07")] alias trivial_to_hom := trivialTo_hom
+
 /-- The bimonoid morphism from any bimonoid to the trivial bimonoid. -/
 @[simps!]
-def to_trivial (A : Bimon_ C) : A ⟶ trivial C :=
+def toTrivial (A : Bimon_ C) : A ⟶ trivial C :=
   (default : @Quiver.Hom (Comon_ (Mon_ C)) _ A (Comon_.trivial (Mon_ C)))
 
+@[deprecated (since := "2024-12-07")] alias to_trivial := toTrivial
+@[deprecated (since := "2024-12-07")] alias to_trivial_hom := toTrivial_hom
+
 /-! # Additional lemmas -/
 
 variable {C}

Mathlib/Data/Set/Lattice.lean

@@ -924,10 +924,12 @@ theorem sUnion_powerset_gc :
   gc_sSup_Iic
 
 /-- `⋃₀` and `𝒫` form a Galois insertion. -/
-def sUnion_powerset_gi :
+def sUnionPowersetGI :
     GaloisInsertion (⋃₀ · : Set (Set α) → Set α) (𝒫 · : Set α → Set (Set α)) :=
   gi_sSup_Iic
 
+@[deprecated (since := "2024-12-07")] alias sUnion_powerset_gi := sUnionPowersetGI
+
 /-- If all sets in a collection are either `∅` or `Set.univ`, then so is their union. -/
 theorem sUnion_mem_empty_univ {S : Set (Set α)} (h : S ⊆ {∅, univ}) :
     ⋃₀ S ∈ ({∅, univ} : Set (Set α)) := by

Mathlib/LinearAlgebra/FreeProduct/Basic.lean

@@ -68,7 +68,7 @@ universe uS uA uB
 then their quotients are also `R`-equivalent.
 
 (Special case of the third isomorphism theorem.)-/
-def algEquiv_quot_algEquiv
+def algEquivQuotAlgEquiv
     {R : Type u} [CommSemiring R] {A B : Type v} [Semiring A] [Semiring B]
     [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) (rel : A → A → Prop) :
     RingQuot rel ≃ₐ[R] RingQuot (rel on f.symm) :=
@@ -83,16 +83,20 @@ def algEquiv_quot_algEquiv
       fun x y h ↦ by apply RingQuot.mkAlgHom_rel; simpa⟩))
     (by ext b; simp) (by ext a; simp)
 
+@[deprecated (since := "2024-12-07")] alias algEquiv_quot_algEquiv := algEquivQuotAlgEquiv
+
 /--If two (semi)rings are equivalent and their quotients by a relation `rel` are defined,
 then their quotients are also equivalent.
 
 (Special case of `algEquiv_quot_algEquiv` when `R = ℕ`, which in turn is a special
 case of the third isomorphism theorem.)-/
-def equiv_quot_equiv {A B : Type v} [Semiring A] [Semiring B] (f : A ≃+* B) (rel : A → A → Prop)  :
+def equivQuotEquiv {A B : Type v} [Semiring A] [Semiring B] (f : A ≃+* B) (rel : A → A → Prop) :
     RingQuot rel ≃+* RingQuot (rel on f.symm) :=
   let f_alg : A ≃ₐ[ℕ] B :=
     AlgEquiv.ofRingEquiv (f := f) (fun n ↦ by simp)
-  algEquiv_quot_algEquiv f_alg rel |>.toRingEquiv
+  algEquivQuotAlgEquiv f_alg rel |>.toRingEquiv
+
+@[deprecated (since := "2024-12-07")] alias equiv_quot_equiv := equivQuotEquiv
 
 end RingQuot
 
@@ -143,11 +147,14 @@ theorem rel_id (i : I) : rel R A (ι R <| lof R I A i 1) 1 := rel.id
 @[reducible] def _root_.LinearAlgebra.FreeProduct := RingQuot <| FreeProduct.rel R A
 
 /--The free product of the collection of `R`-algebras `A i`, as a quotient of `PowerAlgebra R A`-/
-@[reducible] def _root_.LinearAlgebra.FreeProduct_ofPowers := RingQuot <| FreeProduct.rel' R A
+@[reducible] def _root_.LinearAlgebra.FreeProductOfPowers := RingQuot <| FreeProduct.rel' R A
+
+@[deprecated (since := "2024-12-07")]
+alias _root_.LinearAlgebra.FreeProduct_ofPowers := LinearAlgebra.FreeProductOfPowers
 
 /--The `R`-algebra equivalence relating `FreeProduct` and `FreeProduct_ofPowers`-/
-noncomputable def equivPowerAlgebra : FreeProduct_ofPowers R A ≃ₐ[R] FreeProduct R A :=
-  RingQuot.algEquiv_quot_algEquiv
+noncomputable def equivPowerAlgebra : FreeProductOfPowers R A ≃ₐ[R] FreeProduct R A :=
+  RingQuot.algEquivQuotAlgEquiv
     (FreeProduct.powerAlgebra_equiv_freeAlgebra R A |>.symm) (FreeProduct.rel R A)
   |>.symm
 

Mathlib/Tactic/Linter/OldObtain.lean

@@ -54,12 +54,15 @@ open Lean Elab
 namespace Mathlib.Linter.Style
 
 /-- Whether a syntax element is an `obtain` tactic call without a provided proof. -/
-def is_obtain_without_proof : Syntax → Bool
+def isObtainWithoutProof : Syntax → Bool
   -- Using the `obtain` tactic without a proof requires proving a type;
   -- a pattern is optional.
   | `(tactic|obtain : $_type) | `(tactic|obtain $_pat : $_type) => true
   | _ => false
 
+/-- Deprecated alias for `Mathlib.Linter.Style.isObtainWithoutProof`. -/
+@[deprecated isObtainWithoutProof (since := "2024-12-07")]
+def is_obtain_without_proof := @isObtainWithoutProof
 
 /-- The `oldObtain` linter emits a warning upon uses of the "stream-of-conciousness" variants
 of the `obtain` tactic, i.e. with the proof postponed. -/
@@ -74,7 +77,7 @@ def oldObtainLinter : Linter where run := withSetOptionIn fun stx => do
       return
     if (← MonadState.get).messages.hasErrors then
       return
-    if let some head := stx.find? is_obtain_without_proof then
+    if let some head := stx.find? isObtainWithoutProof then
       Linter.logLint linter.oldObtain head m!"Please remove stream-of-conciousness `obtain` syntax"
 
 initialize addLinter oldObtainLinter

Mathlib/Tactic/Linter/Style.lean

@@ -52,16 +52,24 @@ namespace Style.setOption
 
 /-- Whether a syntax element is a `set_option` command, tactic or term:
 Return the name of the option being set, if any. -/
-def parse_set_option : Syntax → Option Name
+def parseSetOption : Syntax → Option Name
   -- This handles all four possibilities of `_val`: a string, number, `true` and `false`.
   | `(command|set_option $name:ident $_val) => some name.getId
   | `(set_option $name:ident $_val in $_x) => some name.getId
   | `(tactic|set_option $name:ident $_val in $_x) => some name.getId
   | _ => none
 
+/-- Deprecated alias for `Mathlib.Linter.Style.setOption.parseSetOption`. -/
+@[deprecated parseSetOption (since := "2024-12-07")]
+def parse_set_option := @parseSetOption
+
 /-- Whether a given piece of syntax is a `set_option` command, tactic or term. -/
-def is_set_option : Syntax → Bool :=
-  fun stx ↦ parse_set_option stx matches some _name
+def isSetOption : Syntax → Bool :=
+  fun stx ↦ parseSetOption stx matches some _name
+
+/-- Deprecated alias for `Mathlib.Linter.Style.setOption.isSetOption`. -/
+@[deprecated isSetOption (since := "2024-12-07")]
+def is_set_option := @isSetOption
 
 /-- The `setOption` linter: this lints any `set_option` command, term or tactic
 which sets a `pp`, `profiler` or `trace` option.
@@ -76,8 +84,8 @@ def setOptionLinter : Linter where run := withSetOptionIn fun stx => do
       return
     if (← MonadState.get).messages.hasErrors then
       return
-    if let some head := stx.find? is_set_option then
-      if let some name := parse_set_option head then
+    if let some head := stx.find? isSetOption then
+      if let some name := parseSetOption head then
         let forbidden := [`debug, `pp, `profiler, `trace]
         if forbidden.contains name.getRoot then
           Linter.logLint linter.style.setOption head

Mathlib/Tactic/MoveAdd.lean

@@ -336,7 +336,7 @@ def pairUp : List (Expr × Bool × Syntax) → List Expr →
 To support a new binary operation, extend the list in this definition, so that it contains
 enough lemmas to allow `simp` to close a generic permutation goal for the new binary operation.
 -/
-def move_oper_simpCtx : MetaM Simp.Context := do
+def moveOperSimpCtx : MetaM Simp.Context := do
   let simpNames := Elab.Tactic.simpOnlyBuiltins ++ [
     ``add_comm, ``add_assoc, ``add_left_comm,  -- for `HAdd.hAdd`
     ``mul_comm, ``mul_assoc, ``mul_left_comm,  -- for `HMul.hMul`
@@ -348,6 +348,9 @@ def move_oper_simpCtx : MetaM Simp.Context := do
   let simpThms ← simpNames.foldlM (·.addConst ·) ({} : SimpTheorems)
   Simp.mkContext {} (simpTheorems := #[simpThms])
 
+@[deprecated (since := "2024-12-07")]
+alias move_oper_simpCtx := moveOperSimpCtx
+
 /-- `reorderAndSimp mv op instr` takes as input an `MVarId`  `mv`, the name `op` of a binary
 operation and a list of "instructions" `instr` that it passes to `permuteExpr`.
 
@@ -368,7 +371,7 @@ def reorderAndSimp (mv : MVarId) (instr : List (Expr × Bool)) :
     throwError m!"There should only be 2 goals, instead of {twoGoals.length}"
   -- `permGoal` is the single goal `mv_permuted`, possibly more operations will be permuted later on
   let permGoal ← twoGoals.filterM fun v => return !(← v.isAssigned)
-  match ← (simpGoal (permGoal[1]!) (← move_oper_simpCtx)) with
+  match ← (simpGoal (permGoal[1]!) (← moveOperSimpCtx)) with
     | (some x, _) => throwError m!"'move_oper' could not solve {indentD x.2}"
     | (none, _) => return permGoal