chore: fix backtick in docs (#5077)

I wrote a script to find lines that contain an odd number of backticks

Mathlib/Algebra/Group/Prod.lean

@@ -22,7 +22,7 @@ trivial `simp` lemmas, and define the following operations on `MonoidHom`s:
   as `MonoidHom`s;
 * `inl M N : M →* M × N`, `inr M N : N →* M × N`: inclusions of first/second monoid
   into the product;
-* `f.prod g : `M →* N × P`: sends `x` to `(f x, g x)`;
+* `f.prod g` : `M →* N × P`: sends `x` to `(f x, g x)`;
 * `f.coprod g : M × N →* P`: sends `(x, y)` to `f x * g y`;
 * `f.prodMap g : M × N → M' × N'`: `prod.map f g` as a `MonoidHom`,
   sends `(x, y)` to `(f x, g y)`.

Mathlib/Algebra/Module/Bimodule.lean

@@ -32,8 +32,8 @@ Note that the corresponding result holds for the canonically isomorphic ring `R
 preferable to use the `R ⊗[ℕ] Sᵐᵒᵖ` instance since it works without additive inverses.
 
 Bimodules are thus just a special case of `Module`s and most of their properties follow from the
-theory of `Module`s`. In particular a two-sided Submodule of a bimodule is simply a term of type
-`submodule (R ⊗[ℕ] Sᵐᵒᵖ) M`.
+theory of `Module`s. In particular a two-sided Submodule of a bimodule is simply a term of type
+`Submodule (R ⊗[ℕ] Sᵐᵒᵖ) M`.
 
 This file is a place to collect results which are specific to bimodules.
 

Mathlib/Algebra/Order/Group/Defs.lean

@@ -1090,7 +1090,7 @@ class LinearOrderedAddCommGroup (α : Type u) extends OrderedAddCommGroup α, Li
 #align linear_ordered_add_comm_group LinearOrderedAddCommGroup
 
 /-- A linearly ordered commutative monoid with an additively absorbing `⊤` element.
-  Instances should include number systems with an infinite element adjoined.` -/
+  Instances should include number systems with an infinite element adjoined. -/
 class LinearOrderedAddCommGroupWithTop (α : Type _) extends LinearOrderedAddCommMonoidWithTop α,
   SubNegMonoid α, Nontrivial α where
   protected neg_top : -(⊤ : α) = ⊤

Mathlib/Algebra/Order/Monoid/Defs.lean

@@ -103,7 +103,7 @@ class LinearOrderedCommMonoid (α : Type _) extends LinearOrder α, OrderedCommM
 attribute [to_additive existing] LinearOrderedCommMonoid.toOrderedCommMonoid
 
 /-- A linearly ordered commutative monoid with an additively absorbing `⊤` element.
-  Instances should include number systems with an infinite element adjoined.` -/
+  Instances should include number systems with an infinite element adjoined. -/
 class LinearOrderedAddCommMonoidWithTop (α : Type _) extends LinearOrderedAddCommMonoid α,
     Top α where
   /-- In a `LinearOrderedAddCommMonoidWithTop`, the `⊤` element is larger than any other element.-/

Mathlib/Algebra/Quaternion.lean

@@ -315,7 +315,7 @@ theorem sub_self_re : a - a.re = a.im :=
 * `j * j = c₂`;
 * `i * j = k`, `j * i = -k`;
 * `k * k = -c₁ * c₂`;
-* `i * k = c₁ * j`, `k * i = `-c₁ * j`;
+* `i * k = c₁ * j`, `k * i = -c₁ * j`;
 * `j * k = -c₂ * i`, `k * j = c₂ * i`.  -/
 instance : Mul ℍ[R,c₁,c₂] :=
   ⟨fun a b =>

Mathlib/Analysis/BoxIntegral/Basic.lean

@@ -15,7 +15,7 @@ import Mathlib.Topology.UniformSpace.Compact
 /-!
 # Integrals of Riemann, Henstock-Kurzweil, and McShane
 
-In this file we define the integral of a function over a box in `ℝⁿ. The same definition works for
+In this file we define the integral of a function over a box in `ℝⁿ`. The same definition works for
 Riemann, Henstock-Kurzweil, and McShane integrals.
 
 As usual, we represent `ℝⁿ` as the type of functions `ι → ℝ` for some finite type `ι`. A rectangular
@@ -812,7 +812,7 @@ box `J ≤ I` such that
 the distance between the term `vol J (f x)` of an integral sum corresponding to `J` and `g J` is
 less than or equal to `ε` if `x ∈ s` and is less than or equal to `ε * B J` otherwise.
 
-Then `f` is integrable on `I along `l` with integral `g I`. -/
+Then `f` is integrable on `I` along `l` with integral `g I`. -/
 theorem HasIntegral.of_le_Henstock_of_forall_isLittleO (hl : l ≤ Henstock) (B : ι →ᵇᵃ[I] ℝ)
     (hB0 : ∀ J, 0 ≤ B J) (g : ι →ᵇᵃ[I] F) (s : Set ℝⁿ) (hs : s.Countable)
     (H₁ : ∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ ε > (0 : ℝ),

Mathlib/Analysis/Calculus/ContDiff.lean

@@ -932,12 +932,12 @@ theorem contDiff_prodAssoc_symm : ContDiff 𝕜 ⊤ <| (Equiv.prodAssoc E F G).s
 /-! ### Bundled derivatives are smooth -/
 
 /-- One direction of `contDiffWithinAt_succ_iff_hasFDerivWithinAt`, but where all derivatives
-taken within the same set. Version for partial derivatives / functions with parameters.  f x` is a
+taken within the same set. Version for partial derivatives / functions with parameters.  `f x` is a
 `C^n+1` family of functions and `g x` is a `C^n` family of points, then the derivative of `f x` at
 `g x` depends in a `C^n` way on `x`. We give a general version of this fact relative to sets which
-may not have unique derivatives, in the following form.  If `f : E × F → G` is `C^n+1` at `(x₀,
-g(x₀))` in `(s ∪ {x₀}) × t ⊆ E × F` and `g : E → F` is `C^n` at `x₀` within some set `s ⊆ E`, then
-there is a function `f' : E → F →L[𝕜] G` that is `C^n` at `x₀` within `s` such that for all `x`
+may not have unique derivatives, in the following form.  If `f : E × F → G` is `C^n+1` at
+`(x₀, g(x₀))` in `(s ∪ {x₀}) × t ⊆ E × F` and `g : E → F` is `C^n` at `x₀` within some set `s ⊆ E`,
+then there is a function `f' : E → F →L[𝕜] G` that is `C^n` at `x₀` within `s` such that for all `x`
 sufficiently close to `x₀` within `s ∪ {x₀}` the function `y ↦ f x y` has derivative `f' x` at `g x`
 within `t ⊆ F`.  For convenience, we return an explicit set of `x`'s where this holds that is a
 subset of `s ∪ {x₀}`.  We need one additional condition, namely that `t` is a neighborhood of

Mathlib/Analysis/Calculus/FDerivMeasurable.lean

@@ -18,14 +18,14 @@ import Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
 In this file we prove that the derivative of any function with complete codomain is a measurable
 function. Namely, we prove:
 
-* `measurable_set_of_differentiable_at`: the set `{x | differentiable_at 𝕜 f x}` is measurable;
+* `measurableSet_of_differentiableAt`: the set `{x | DifferentiableAt 𝕜 f x}` is measurable;
 * `measurable_fderiv`: the function `fderiv 𝕜 f` is measurable;
 * `measurable_fderiv_apply_const`: for a fixed vector `y`, the function `fun x ↦ fderiv 𝕜 f x y`
   is measurable;
 * `measurable_deriv`: the function `deriv f` is measurable (for `f : 𝕜 → F`).
 
 We also show the same results for the right derivative on the real line
-(see `measurable_deriv_within_Ici` and ``measurable_deriv_within_Ioi`), following the same
+(see `measurable_derivWithin_Ici` and `measurable_derivWithin_Ioi`), following the same
 proof strategy.
 
 ## Implementation

Mathlib/Analysis/Calculus/LocalExtr.lean

@@ -26,7 +26,7 @@ This set is used in the proof of Fermat's Theorem (see below), and can be used t
 ## Main statements
 
 For each theorem name listed below,
-we also prove similar theorems for `min`, `extr` (if applicable)`,
+we also prove similar theorems for `min`, `extr` (if applicable),
 and `(f)deriv` instead of `has_fderiv`.
 
 * `IsLocalMaxOn.hasFDerivWithinAt_nonpos` : `f' y ≤ 0` whenever `a` is a local maximum

Mathlib/Analysis/Complex/CauchyIntegral.lean

@@ -352,7 +352,7 @@ theorem circleIntegral_eq_of_differentiable_on_annulus_off_countable {c : ℂ} {
 /-- **Cauchy integral formula** for the value at the center of a disc. If `f` is continuous on a
 punctured closed disc of radius `R`, is differentiable at all but countably many points of the
 interior of this disc, and has a limit `y` at the center of the disc, then the integral
-$\oint_{‖z-c‖=R} \frac{f(z)}{z-c}\,dz$ is equal to $2πiy`. -/
+$\oint_{‖z-c‖=R} \frac{f(z)}{z-c}\,dz$ is equal to `2πiy`. -/
 theorem circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable_of_tendsto {c : ℂ}
     {R : ℝ} (h0 : 0 < R) {f : ℂ → E} {y : E} {s : Set ℂ} (hs : s.Countable)
     (hc : ContinuousOn f (closedBall c R \ {c}))
@@ -400,7 +400,7 @@ theorem circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable_of
 
 /-- **Cauchy integral formula** for the value at the center of a disc. If `f : ℂ → E` is continuous
 on a closed disc of radius `R` and is complex differentiable at all but countably many points of its
-interior, then the integral $\oint_{|z-c|=R} \frac{f(z)}{z-c}\,dz$ is equal to $2πiy`. -/
+interior, then the integral $\oint_{|z-c|=R} \frac{f(z)}{z-c}\,dz$ is equal to `2πiy`. -/
 theorem circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable {R : ℝ} (h0 : 0 < R)
     {f : ℂ → E} {c : ℂ} {s : Set ℂ} (hs : s.Countable) (hc : ContinuousOn f (closedBall c R))
     (hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z) :
@@ -620,4 +620,3 @@ protected theorem _root_.Differentiable.hasFPowerSeriesOnBall {f : ℂ → E} (h
 #align differentiable.has_fpower_series_on_ball Differentiable.hasFPowerSeriesOnBall
 
 end Complex
-

Mathlib/Analysis/Convex/Normed.lean

@@ -100,7 +100,7 @@ theorem convexHull_exists_dist_ge2 {s t : Set E} {x y : E} (hx : x ∈ convexHul
   exact le_trans Hx' (dist_comm y x' ▸ dist_comm y' x' ▸ Hy')
 #align convex_hull_exists_dist_ge2 convexHull_exists_dist_ge2
 
-/-- Emetric diameter of the convex hull of a set `s` equals the emetric diameter of `s. -/
+/-- Emetric diameter of the convex hull of a set `s` equals the emetric diameter of `s`. -/
 @[simp]
 theorem convexHull_ediam (s : Set E) : EMetric.diam (convexHull ℝ s) = EMetric.diam s := by
   refine' (EMetric.diam_le fun x hx y hy => _).antisymm (EMetric.diam_mono <| subset_convexHull ℝ s)
@@ -111,7 +111,7 @@ theorem convexHull_ediam (s : Set E) : EMetric.diam (convexHull ℝ s) = EMetric
   exact EMetric.edist_le_diam_of_mem hx' hy'
 #align convex_hull_ediam convexHull_ediam
 
-/-- Diameter of the convex hull of a set `s` equals the emetric diameter of `s. -/
+/-- Diameter of the convex hull of a set `s` equals the emetric diameter of `s`. -/
 @[simp]
 theorem convexHull_diam (s : Set E) : Metric.diam (convexHull ℝ s) = Metric.diam s := by
   simp only [Metric.diam, convexHull_ediam]

Mathlib/Analysis/Convex/StrictConvexSpace.lean

@@ -178,8 +178,8 @@ theorem norm_combo_lt_of_ne (hx : ‖x‖ ≤ r) (hy : ‖y‖ ≤ r) (hne : x 
   exact combo_mem_ball_of_ne hx hy hne ha hb hab
 #align norm_combo_lt_of_ne norm_combo_lt_of_ne
 
-/-- In a strictly convex space, if `x` and `y` are not in the same ray, then `‖x + y‖ < ‖x‖ +
-‖y‖`. -/
+/-- In a strictly convex space, if `x` and `y` are not in the same ray, then `‖x + y‖ < ‖x‖ + ‖y‖`.
+-/
 theorem norm_add_lt_of_not_sameRay (h : ¬SameRay ℝ x y) : ‖x + y‖ < ‖x‖ + ‖y‖ := by
   simp only [sameRay_iff_inv_norm_smul_eq, not_or, ← Ne.def] at h
   rcases h with ⟨hx, hy, hne⟩

Mathlib/Analysis/InnerProductSpace/ConformalLinearMap.lean

@@ -29,8 +29,8 @@ open LinearIsometry ContinuousLinearMap
 open RealInnerProductSpace
 
 /-- A map between two inner product spaces is a conformal map if and only if it preserves inner
-products up to a scalar factor, i.e., there exists a positive `c : ℝ` such that `⟪f u, f v⟫ = c *
-⟪u, v⟫` for all `u`, `v`. -/
+products up to a scalar factor, i.e., there exists a positive `c : ℝ` such that
+`⟪f u, f v⟫ = c * ⟪u, v⟫` for all `u`, `v`. -/
 theorem isConformalMap_iff (f : E →L[ℝ] F) :
     IsConformalMap f ↔ ∃ c : ℝ, 0 < c ∧ ∀ u v : E, ⟪f u, f v⟫ = c * ⟪u, v⟫ := by
   constructor

Mathlib/Analysis/Normed/Group/AddTorsor.lean

@@ -207,8 +207,7 @@ theorem edist_vsub_vsub_le (p₁ p₂ p₃ p₄ : P) :
 #align edist_vsub_vsub_le edist_vsub_vsub_le
 
 /-- The pseudodistance defines a pseudometric space structure on the torsor. This
-is not an instance because it depends on `V` to define a `MetricSpace
-P`. -/
+is not an instance because it depends on `V` to define a `MetricSpace P`. -/
 def pseudoMetricSpaceOfNormedAddCommGroupOfAddTorsor (V P : Type _) [SeminormedAddCommGroup V]
     [AddTorsor V P] : PseudoMetricSpace P where
   dist x y := ‖(x -ᵥ y : V)‖
@@ -223,8 +222,7 @@ def pseudoMetricSpaceOfNormedAddCommGroupOfAddTorsor (V P : Type _) [SeminormedA
 #align pseudo_metric_space_of_normed_add_comm_group_of_add_torsor pseudoMetricSpaceOfNormedAddCommGroupOfAddTorsor
 
 /-- The distance defines a metric space structure on the torsor. This
-is not an instance because it depends on `V` to define a `MetricSpace
-P`. -/
+is not an instance because it depends on `V` to define a `MetricSpace P`. -/
 def metricSpaceOfNormedAddCommGroupOfAddTorsor (V P : Type _) [NormedAddCommGroup V]
     [AddTorsor V P] : MetricSpace P where
   dist x y := ‖(x -ᵥ y : V)‖

Mathlib/Analysis/NormedSpace/MazurUlam.lean

@@ -65,7 +65,7 @@ theorem midpoint_fixed {x y : PE} :
   -- midpoint `z` of `[x, y]`.
   set R : PE ≃ᵢ PE := (pointReflection ℝ z).toIsometryEquiv
   set f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e => ((e.trans R).trans e.symm).trans R
-  -- Note that `f` doubles the value of ``dist (e z) z`
+  -- Note that `f` doubles the value of `dist (e z) z`
   have hf_dist : ∀ e, dist (f e z) z = 2 * dist (e z) z := by
     intro e
     dsimp

Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean

@@ -119,7 +119,7 @@ theorem coe_int_mul_eq_zsmul (x : ℝ) (n : ℤ) : ↑((n : ℝ) * x : ℝ) = n
 theorem angle_eq_iff_two_pi_dvd_sub {ψ θ : ℝ} : (θ : Angle) = ψ ↔ ∃ k : ℤ, θ - ψ = 2 * π * k := by
   simp only [QuotientAddGroup.eq, AddSubgroup.zmultiples_eq_closure,
     AddSubgroup.mem_closure_singleton, zsmul_eq_mul', (sub_eq_neg_add _ _).symm, eq_comm]
-  -- Porting note: added `rw`, `simp [Angle.coe, QuotientAddGroup.eq] doesn't fire otherwise
+  -- Porting note: added `rw`, `simp [Angle.coe, QuotientAddGroup.eq]` doesn't fire otherwise
   rw [Angle.coe, Angle.coe, QuotientAddGroup.eq]
   simp only [AddSubgroup.zmultiples_eq_closure,
     AddSubgroup.mem_closure_singleton, zsmul_eq_mul', (sub_eq_neg_add _ _).symm, eq_comm]

Mathlib/CategoryTheory/Abelian/LeftDerived.lean

@@ -162,7 +162,7 @@ def leftDerivedZeroToSelfAppIso [EnoughProjectives C] [PreservesFiniteColimits F
 #align category_theory.abelian.functor.left_derived_zero_to_self_app_iso CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfAppIso
 
 /-- Given `P : ProjectiveResolution X` and `Q : ProjectiveResolution Y` and a morphism `f : X ⟶ Y`,
-naturality of the square given by `left_derived_zero_to_self_obj_hom. -/
+naturality of the square given by `leftDerived_zero_to_self_obj_hom`. -/
 theorem leftDerived_zero_to_self_natural [EnoughProjectives C] {X : C} {Y : C} (f : X ⟶ Y)
     (P : ProjectiveResolution X) (Q : ProjectiveResolution Y) :
     (F.leftDerived 0).map f ≫ leftDerivedZeroToSelfApp F Q =

Mathlib/CategoryTheory/Action.lean

@@ -22,7 +22,7 @@ types, mapping the single object of M to X and an element `m : M` to map `X →
 multiplication by `m`.
   This functor induces a category structure on X -- a special case of the category of elements.
 A morphism `x ⟶ y` in this category is simply a scalar `m : M` such that `m • x = y`. In the case
-where M is a group, this category is a groupoid -- the `action groupoid'.
+where M is a group, this category is a groupoid -- the *action groupoid*.
 -/
 
 

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

@@ -16,8 +16,8 @@ import Mathlib.CategoryTheory.Limits.Constructions.EpiMono
 # Concrete categories
 
 A concrete category is a category `C` with a fixed faithful functor
-`forget : C ⥤ Type _`.  We define concrete categories using `class
-concrete_category`.  In particular, we impose no restrictions on the
+`forget : C ⥤ Type _`.  We define concrete categories using `class ConcreteCategory`.
+In particular, we impose no restrictions on the
 carrier type `C`, so `Type` is a concrete category with the identity
 forgetful functor.
 

Mathlib/CategoryTheory/Limits/Fubini.lean

@@ -321,7 +321,7 @@ theorem limitCurrySwapCompLimIsoLimitCurryCompLim_hom_π_π {j} {k} :
   simp only [Iso.refl_hom, Prod.braiding_counitIso_hom_app, Limits.HasLimit.isoOfEquivalence_hom_π,
     Iso.refl_inv, limitIsoLimitCurryCompLim_hom_π_π, eqToIso_refl, Category.assoc]
   erw [NatTrans.id_app]
-  -- Why can't `simp` do this`?
+  -- Why can't `simp` do this?
   dsimp
   -- porting note: the original proof only had `simp`.
   -- However, now `CategoryTheory.Bifunctor.map_id` does not get used by `simp`

Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean

@@ -135,7 +135,7 @@ def compNatIso {D : Type u'} [Category.{v} D] [HasZeroMorphisms D] (F : C ⥤ D)
 
 end
 
-/-- If `s` is a limit kernel fork and `k : W ⟶ X` satisfies ``k ≫ f = 0`, then there is some
+/-- If `s` is a limit kernel fork and `k : W ⟶ X` satisfies `k ≫ f = 0`, then there is some
     `l : W ⟶ s.X` such that `l ≫ fork.ι s = k`. -/
 def KernelFork.IsLimit.lift' {s : KernelFork f} (hs : IsLimit s) {W : C} (k : W ⟶ X)
     (h : k ≫ f = 0) : { l : W ⟶ s.pt // l ≫ Fork.ι s = k } :=

Mathlib/CategoryTheory/Preadditive/Projective.lean

@@ -26,8 +26,8 @@ projective object.
 epimorphism.
 
 Given a morphism `f : X ⟶ Y`, `CategoryTheory.Projective.left f` is a projective object over
-`CategoryTheory.Limits.kernel f`, and `projective.d f : projective.left f ⟶ X` is the morphism `π
-(kernel f) ≫ kernel.ι f`.
+`CategoryTheory.Limits.kernel f`, and `projective.d f : projective.left f ⟶ X` is the morphism
+`π (kernel f) ≫ kernel.ι f`.
 
 -/
 

Mathlib/Combinatorics/Quiver/Symmetric.lean

@@ -54,7 +54,7 @@ def reverse {V} [Quiver.{v + 1} V] [HasReverse V] {a b : V} : (a ⟶ b) → (b 
   HasReverse.reverse'
 #align quiver.reverse Quiver.reverse
 
-/-- A quiver `HasInvolutiveReverse` if reversing twice is the identity.`-/
+/-- A quiver `HasInvolutiveReverse` if reversing twice is the identity. -/
 class HasInvolutiveReverse extends HasReverse V where
   /-- `reverse` is involutive -/
   inv' : ∀ {a b : V} (f : a ⟶ b), reverse (reverse f) = f

Mathlib/Control/Monad/Basic.lean

@@ -27,8 +27,8 @@ import Mathlib.Tactic.Common
 Set of rewrite rules and automation for monads in general and
 `ReaderT`, `StateT`, `ExceptT` and `OptionT` in particular.
 
-The rewrite rules for monads are carefully chosen so that `simp with
-functor_norm` will not introduce monadic vocabulary in a context where
+The rewrite rules for monads are carefully chosen so that `simp with functor_norm`
+will not introduce monadic vocabulary in a context where
 applicatives would do just fine but will handle monadic notation
 already present in an expression.
 

Mathlib/Data/Finset/NoncommProd.lean

@@ -228,7 +228,7 @@ namespace Finset
 variable [Monoid β] [Monoid γ]
 
 
-/-- Proof used in definition of `Finset.noncommProd -/
+/-- Proof used in definition of `Finset.noncommProd` -/
 @[to_additive]
 theorem noncommProd_lemma (s : Finset α) (f : α → β)
     (comm : (s : Set α).Pairwise fun a b => Commute (f a) (f b)) :

Mathlib/Data/Fintype/Sort.lean

@@ -35,7 +35,7 @@ def monoEquivOfFin (α : Type _) [Fintype α] [LinearOrder α] {k : ℕ} (h : Fi
 variable {α : Type _} [DecidableEq α] [Fintype α] [LinearOrder α] {m n : ℕ} {s : Finset α}
 
 /-- If `α` is a linearly ordered fintype, `s : Finset α` has cardinality `m` and its complement has
-cardinality `n`, then `Fin m ⊕ Fin n ≃ α`. The equivalence sends elements of Fin m` to
+cardinality `n`, then `Fin m ⊕ Fin n ≃ α`. The equivalence sends elements of `Fin m` to
 elements of `s` and elements of `Fin n` to elements of `sᶜ` while preserving order on each
 "half" of `Fin m ⊕ Fin n` (using `Set.orderIsoOfFin`). -/
 def finSumEquivOfFinset (hm : s.card = m) (hn : sᶜ.card = n) : Sum (Fin m) (Fin n) ≃ α :=

Mathlib/Data/List/MinMax.lean

@@ -19,7 +19,7 @@ The main definitions are `argmax`, `argmin`, `minimum` and `maximum` for lists.
 
 `argmax f l` returns `some a`, where `a` of `l` that maximises `f a`. If there are `a b` such that
   `f a = f b`, it returns whichever of `a` or `b` comes first in the list.
-  `argmax f []` = none`
+  `argmax f [] = none`
 
 `minimum l` returns a `WithTop α`, the smallest element of `l` for nonempty lists, and `⊤` for
 `[]`
@@ -95,14 +95,14 @@ variable [Preorder β] [@DecidableRel β (· < ·)] {f : α → β} {l : List α
 
 /-- `argmax f l` returns `some a`, where `f a` is maximal among the elements of `l`, in the sense
 that there is no `b ∈ l` with `f a < f b`. If `a`, `b` are such that `f a = f b`, it returns
-whichever of `a` or `b` comes first in the list. `argmax f []` = none`. -/
+whichever of `a` or `b` comes first in the list. `argmax f [] = none`. -/
 def argmax (f : α → β) (l : List α) : Option α :=
   l.foldl (argAux fun b c => f c < f b) none
 #align list.argmax List.argmax
 
 /-- `argmin f l` returns `some a`, where `f a` is minimal among the elements of `l`, in the sense
 that there is no `b ∈ l` with `f b < f a`. If `a`, `b` are such that `f a = f b`, it returns
-whichever of `a` or `b` comes first in the list. `argmin f []` = none`. -/
+whichever of `a` or `b` comes first in the list. `argmin f [] = none`. -/
 def argmin (f : α → β) (l : List α) :=
   l.foldl (argAux fun b c => f b < f c) none
 #align list.argmin List.argmin