Merge branch 'master' into mans0954/quadratic-maps

Mathlib.lean

@@ -3926,7 +3926,7 @@ import Mathlib.Tactic.Clear_
 import Mathlib.Tactic.Coe
 import Mathlib.Tactic.Common
 import Mathlib.Tactic.ComputeDegree
-import Mathlib.Tactic.Congr!
+import Mathlib.Tactic.CongrExclamation
 import Mathlib.Tactic.CongrM
 import Mathlib.Tactic.Constructor
 import Mathlib.Tactic.Continuity

Mathlib/Algebra/Algebra/NonUnitalHom.lean

@@ -167,7 +167,7 @@ variable [NonUnitalNonAssocSemiring C] [DistribMulAction T C]
 -- instance : CoeFun (A →ₙₐ[R] B) fun _ => A → B :=
 --   ⟨toFun⟩
 
-instance  : DFunLike (A →ₛₙₐ[φ] B) A fun _ => B where
+instance : DFunLike (A →ₛₙₐ[φ] B) A fun _ => B where
   coe f := f.toFun
   coe_injective' := by rintro ⟨⟨⟨f, _⟩, _⟩, _⟩ ⟨⟨⟨g, _⟩, _⟩, _⟩ h; congr
 

Mathlib/Algebra/Algebra/Operations.lean

@@ -27,7 +27,7 @@ An interface for multiplication and division of sub-R-modules of an R-algebra A
 
 Let `R` be a commutative ring (or semiring) and let `A` be an `R`-algebra.
 
-* `1 : Submodule R A`       : the R-submodule R of the R-algebra A
+* `1 : Submodule R A`   : the R-submodule R of the R-algebra A
 * `Mul (Submodule R A)` : multiplication of two sub-R-modules M and N of A is defined to be
                               the smallest submodule containing all the products `m * n`.
 * `Div (Submodule R A)` : `I / J` is defined to be the submodule consisting of all `a : A` such

Mathlib/Algebra/BigOperators/Ring.lean

@@ -67,6 +67,10 @@ lemma sum_mul_sum {κ : Type*} (s : Finset ι) (t : Finset κ) (f : ι → α) (
   simp_rw [sum_mul, ← mul_sum]
 #align finset.sum_mul_sum Finset.sum_mul_sum
 
+lemma _root_.Fintype.sum_mul_sum {κ : Type*} [Fintype ι] [Fintype κ] (f : ι → α) (g : κ → α) :
+    (∑ i, f i) * ∑ j, g j = ∑ i, ∑ j, f i * g j :=
+  Finset.sum_mul_sum _ _ _ _
+
 lemma _root_.Commute.sum_right [NonUnitalNonAssocSemiring α] (s : Finset ι) (f : ι → α) (b : α)
     (h : ∀ i ∈ s, Commute b (f i)) : Commute b (∑ i ∈ s, f i) :=
   (Commute.multiset_sum_right _ _) fun b hb => by
@@ -307,9 +311,6 @@ variable {ι κ α : Type*} [DecidableEq ι] [Fintype ι] [Fintype κ] [CommSemi
 lemma sum_pow (f : ι → α) (n : ℕ) : (∑ a, f a) ^ n = ∑ p : Fin n → ι, ∏ i, f (p i) := by
   simp [sum_pow']
 
-lemma sum_mul_sum (f : ι → α) (g : κ → α) : (∑ i, f i) * ∑ j, g j = ∑ i, ∑ j, f i * g j :=
-  Finset.sum_mul_sum _ _ _ _
-
 /-- A product of sums can be written as a sum of products. -/
 lemma prod_sum {κ : ι → Type*} [Fintype ι] [∀ i, Fintype (κ i)] (f : ∀ i, κ i → α) :
     ∏ i, ∑ j, f i j = ∑ x : ∀ i, κ i, ∏ i, f i (x i) := Finset.prod_univ_sum _ _

Mathlib/Algebra/CharZero/Lemmas.lean

@@ -135,40 +135,12 @@ theorem nat_mul_inj' {n : ℕ} {a b : R} (h : (n : R) * a = (n : R) * b) (w : n
   simpa [w] using nat_mul_inj h
 #align nat_mul_inj' nat_mul_inj'
 
-set_option linter.deprecated false
-
-theorem bit0_injective : Function.Injective (bit0 : R → R) := fun a b h => by
-  dsimp [bit0] at h
-  simp only [(two_mul a).symm, (two_mul b).symm] at h
-  refine nat_mul_inj' ?_ two_ne_zero
-  exact mod_cast h
-#align bit0_injective bit0_injective
-
-theorem bit1_injective : Function.Injective (bit1 : R → R) := fun a b h => by
-  simp only [bit1, add_left_inj] at h
-  exact bit0_injective h
-#align bit1_injective bit1_injective
-
-@[simp]
-theorem bit0_eq_bit0 {a b : R} : bit0 a = bit0 b ↔ a = b :=
-  bit0_injective.eq_iff
-#align bit0_eq_bit0 bit0_eq_bit0
-
-@[simp]
-theorem bit1_eq_bit1 {a b : R} : bit1 a = bit1 b ↔ a = b :=
-  bit1_injective.eq_iff
-#align bit1_eq_bit1 bit1_eq_bit1
-
-@[simp]
-theorem bit1_eq_one {a : R} : bit1 a = 1 ↔ a = 0 := by
-  rw [show (1 : R) = bit1 0 by simp, bit1_eq_bit1]
-#align bit1_eq_one bit1_eq_one
-
-@[simp]
-theorem one_eq_bit1 {a : R} : 1 = bit1 a ↔ a = 0 := by
-  rw [eq_comm]
-  exact bit1_eq_one
-#align one_eq_bit1 one_eq_bit1
+#noalign bit0_injective
+#noalign bit1_injective
+#noalign bit0_eq_bit0
+#noalign bit1_eq_bit1
+#noalign bit1_eq_one
+#noalign one_eq_bit1
 
 end
 

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -18,10 +18,10 @@ This file defines extra structures on `CancelCommMonoidWithZero`s, including `Is
 * `NormalizationMonoid`
 * `GCDMonoid`
 * `NormalizedGCDMonoid`
-* `gcdMonoid_of_gcd`, `gcdMonoid_of_exists_gcd`, `normalizedGCDMonoid_of_gcd`,
-  `normalizedGCDMonoid_of_exists_gcd`
-* `gcdMonoid_of_lcm`, `gcdMonoid_of_exists_lcm`, `normalizedGCDMonoid_of_lcm`,
-  `normalizedGCDMonoid_of_exists_lcm`
+* `gcdMonoidOfGCD`, `gcdMonoidOfExistsGCD`, `normalizedGCDMonoidOfGCD`,
+  `normalizedGCDMonoidOfExistsGCD`
+* `gcdMonoidOfLCM`, `gcdMonoidOfExistsLCM`, `normalizedGCDMonoidOfLCM`,
+  `normalizedGCDMonoidOfExistsLCM`
 
 For the `NormalizedGCDMonoid` instances on `ℕ` and `ℤ`, see `Mathlib.Algebra.GCDMonoid.Nat`.
 
@@ -38,17 +38,17 @@ definition as currently implemented does casework on `0`.
   normalized. This makes `gcd`s of polynomials easier to work with, but excludes Euclidean domains,
   and monoids without zero.
 
-* `gcdMonoid_of_gcd` and `normalizedGCDMonoid_of_gcd` noncomputably construct a `GCDMonoid`
+* `gcdMonoidOfGCD` and `normalizedGCDMonoidOfGCD` noncomputably construct a `GCDMonoid`
   (resp. `NormalizedGCDMonoid`) structure just from the `gcd` and its properties.
 
-* `gcdMonoid_of_exists_gcd` and `normalizedGCDMonoid_of_exists_gcd` noncomputably construct a
+* `gcdMonoidOfExistsGCD` and `normalizedGCDMonoidOfExistsGCD` noncomputably construct a
   `GCDMonoid` (resp. `NormalizedGCDMonoid`) structure just from a proof that any two elements
   have a (not necessarily normalized) `gcd`.
 
-* `gcdMonoid_of_lcm` and `normalizedGCDMonoid_of_lcm` noncomputably construct a `GCDMonoid`
+* `gcdMonoidOfLCM` and `normalizedGCDMonoidOfLCM` noncomputably construct a `GCDMonoid`
   (resp. `NormalizedGCDMonoid`) structure just from the `lcm` and its properties.
 
-* `gcdMonoid_of_exists_lcm` and `normalizedGCDMonoid_of_exists_lcm` noncomputably construct a
+* `gcdMonoidOfExistsLCM` and `normalizedGCDMonoidOfExistsLCM` noncomputably construct a
   `GCDMonoid` (resp. `NormalizedGCDMonoid`) structure just from a proof that any two elements
   have a (not necessarily normalized) `lcm`.
 

Mathlib/Algebra/Homology/HomologicalComplex.lean

@@ -1061,7 +1061,7 @@ then a function which takes a differential,
 and returns the next object, its differential, and the fact it composes appropriately to zero.
 -/
 def mk' (X₀ X₁ : V) (d : X₀ ⟶ X₁)
-    -- (succ' : ∀  : ΣX₀ X₁ : V, X₀ ⟶ X₁, Σ' (X₂ : V) (d : t.2.1 ⟶ X₂), t.2.2 ≫ d = 0) :
+    -- (succ' : ∀ : ΣX₀ X₁ : V, X₀ ⟶ X₁, Σ' (X₂ : V) (d : t.2.1 ⟶ X₂), t.2.2 ≫ d = 0) :
     (succ' : ∀ {X₀ X₁ : V} (f : X₀ ⟶ X₁), Σ' (X₂ : V) (d : X₁ ⟶ X₂), f ≫ d = 0) :
     CochainComplex V ℕ :=
   mk _ _ _ _ _ (succ' d).2.2 (fun S => succ' S.g)

Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean

@@ -78,7 +78,7 @@ structure SnakeInput where
   h₀ : IsLimit (KernelFork.ofι _ w₀₂)
   /-- `L₃` is the cokernel of `v₁₂ : L₁ ⟶ L₂`. -/
   h₃ : IsColimit (CokernelCofork.ofπ _ w₁₃)
-  L₁_exact  : L₁.Exact
+  L₁_exact : L₁.Exact
   epi_L₁_g : Epi L₁.g
   L₂_exact : L₂.Exact
   mono_L₂_f : Mono L₂.f

Mathlib/Algebra/Module/LocalizedModule.lean

@@ -17,15 +17,15 @@ localize `M` by `S`. This gives us a `Localization S`-module.
 
 ## Main definitions
 
-* `LocalizedModule.r` : the equivalence relation defining this localization, namely
+* `LocalizedModule.r`: the equivalence relation defining this localization, namely
   `(m, s) ≈ (m', s')` if and only if there is some `u : S` such that `u • s' • m = u • s • m'`.
-* `LocalizedModule M S` : the localized module by `S`.
-* `LocalizedModule.mk`  : the canonical map sending `(m, s) : M × S ↦ m/s : LocalizedModule M S`
-* `LocalizedModule.liftOn` : any well defined function `f : M × S → α` respecting `r` descents to
+* `LocalizedModule M S`: the localized module by `S`.
+* `LocalizedModule.mk`: the canonical map sending `(m, s) : M × S ↦ m/s : LocalizedModule M S`
+* `LocalizedModule.liftOn`: any well defined function `f : M × S → α` respecting `r` descents to
   a function `LocalizedModule M S → α`
-* `LocalizedModule.liftOn₂` : any well defined function `f : M × S → M × S → α` respecting `r`
+* `LocalizedModule.liftOn₂`: any well defined function `f : M × S → M × S → α` respecting `r`
   descents to a function `LocalizedModule M S → LocalizedModule M S`
-* `LocalizedModule.mk_add_mk` : in the localized module
+* `LocalizedModule.mk_add_mk`: in the localized module
   `mk m s + mk m' s' = mk (s' • m + s • m') (s * s')`
 * `LocalizedModule.mk_smul_mk` : in the localized module, for any `r : R`, `s t : S`, `m : M`,
   we have `mk r s • mk m t = mk (r • m) (s * t)` where `mk r s : Localization S` is localized ring

Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean

@@ -128,7 +128,6 @@ def metricSpaceAux : MetricSpace ℍ where
   dist_triangle := UpperHalfPlane.dist_triangle
   eq_of_dist_eq_zero {z w} h := by
     simpa [dist_eq, Real.sqrt_eq_zero', (mul_pos z.im_pos w.im_pos).not_le, ext_iff] using h
-  edist_dist _ _ := by exact ENNReal.coe_nnreal_eq _
 #align upper_half_plane.metric_space_aux UpperHalfPlane.metricSpaceAux
 
 open Complex

Mathlib/Analysis/Convex/Body.lean

@@ -196,7 +196,6 @@ noncomputable instance : PseudoMetricSpace (ConvexBody V) where
   dist_self _ := Metric.hausdorffDist_self_zero
   dist_comm _ _ := Metric.hausdorffDist_comm
   dist_triangle K L M := Metric.hausdorffDist_triangle hausdorffEdist_ne_top
-  edist_dist _ _ := by exact ENNReal.coe_nnreal_eq _
 
 @[simp, norm_cast]
 theorem hausdorffDist_coe : Metric.hausdorffDist (K : Set V) L = dist K L :=

Mathlib/Analysis/Normed/Group/AddTorsor.lean

@@ -206,8 +206,6 @@ 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)‖
-  -- Porting note: `edist_dist` is no longer an `autoParam`
-  edist_dist _ _ := by simp only [← ENNReal.ofReal_eq_coe_nnreal]
   dist_self x := by simp
   dist_comm x y := by simp only [← neg_vsub_eq_vsub_rev y x, norm_neg]
   dist_triangle x y z := by
@@ -221,7 +219,6 @@ 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)‖
-  edist_dist _ _ := by simp only; rw [ENNReal.ofReal_eq_coe_nnreal]
   dist_self x := by simp
   eq_of_dist_eq_zero h := by simpa using h
   dist_comm x y := by simp only [← neg_vsub_eq_vsub_rev y x, norm_neg]

Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean

@@ -264,7 +264,7 @@ linear equivalence between `ContinuousMultilinearMap 𝕜 E F` and `(⨂[𝕜] i
 (induced by `PiTensorProduct.lift`). Here we give the upgrade of this equivalence to
 an isometric linear equivalence; in particular, it is a continuous linear equivalence.
 -/
-noncomputable def liftIsometry  : ContinuousMultilinearMap 𝕜 E F ≃ₗᵢ[𝕜] (⨂[𝕜] i, E i) →L[𝕜] F :=
+noncomputable def liftIsometry : ContinuousMultilinearMap 𝕜 E F ≃ₗᵢ[𝕜] (⨂[𝕜] i, E i) →L[𝕜] F :=
   { liftEquiv 𝕜 E F with
     norm_map' := by
       intro f

Mathlib/CategoryTheory/Limits/Shapes/Countable.lean

@@ -86,7 +86,7 @@ noncomputable def sequentialFunctor_obj : ℕ → J := fun
   | .succ n => (IsCofilteredOrEmpty.cone_objs ((exists_surjective_nat _).choose n)
       (sequentialFunctor_obj n)).choose
 
-theorem sequentialFunctor_map  : Antitone (sequentialFunctor_obj J) :=
+theorem sequentialFunctor_map : Antitone (sequentialFunctor_obj J) :=
   antitone_nat_of_succ_le fun n ↦
     leOfHom (IsCofilteredOrEmpty.cone_objs ((exists_surjective_nat _).choose n)
       (sequentialFunctor_obj J n)).choose_spec.choose_spec.choose

Mathlib/Combinatorics/SetFamily/FourFunctions.lean

@@ -109,7 +109,7 @@ lemma collapse_eq (ha : a ∉ s) (𝒜 : Finset (Finset α)) (f : Finset α →
   rw [collapse, filter_collapse_eq ha]
   split_ifs <;> simp [(ne_of_mem_of_not_mem' (mem_insert_self a s) ha).symm, *]
 
-lemma collapse_of_mem (ha : a ∉ s) (ht : t ∈ 𝒜) (hu  : u ∈ 𝒜) (hts : t = s)
+lemma collapse_of_mem (ha : a ∉ s) (ht : t ∈ 𝒜) (hu : u ∈ 𝒜) (hts : t = s)
     (hus : u = insert a s) : collapse 𝒜 a f s = f t + f u := by
   subst hts; subst hus; simp_rw [collapse_eq ha, if_pos ht, if_pos hu]
 

Mathlib/Computability/Encoding.lean

@@ -19,10 +19,10 @@ It also contains several examples:
 
 ## Examples
 
-- `finEncodingNatBool`   : a binary encoding of ℕ in a simple alphabet.
+- `finEncodingNatBool`  : a binary encoding of ℕ in a simple alphabet.
 - `finEncodingNatΓ'`    : a binary encoding of ℕ in the alphabet used for TM's.
 - `unaryFinEncodingNat` : a unary encoding of ℕ
-- `finEncodingBoolBool`  : an encoding of bool.
+- `finEncodingBoolBool` : an encoding of bool.
 -/
 
 

Mathlib/Data/Fin/Basic.lean

@@ -497,55 +497,14 @@ theorem val_add_eq_ite {n : ℕ} (a b : Fin n) :
     Nat.mod_eq_of_lt (show ↑b < n from b.2)]
 #align fin.coe_add_eq_ite Fin.val_add_eq_ite
 
-section deprecated
-set_option linter.deprecated false
-
-@[deprecated (since := "2023-01-12")]
-theorem val_bit0 {n : ℕ} (k : Fin n) : ((bit0 k : Fin n) : ℕ) = bit0 (k : ℕ) % n := by
-  cases k
-  rfl
-#align fin.coe_bit0 Fin.val_bit0
-
-@[deprecated (since := "2023-01-12")]
-theorem val_bit1 {n : ℕ} [NeZero n] (k : Fin n) :
-    ((bit1 k : Fin n) : ℕ) = bit1 (k : ℕ) % n := by
-  cases n
-  · cases' k with k h
-    cases k
-    · show _ % _ = _
-      simp at h
-    cases' h with _ h
-  simp [bit1, Fin.val_bit0, Fin.val_add, Fin.val_one]
-#align fin.coe_bit1 Fin.val_bit1
-
-end deprecated
-
+#noalign fin.coe_bit0
+#noalign fin.coe_bit1
 #align fin.coe_add_one_of_lt Fin.val_add_one_of_lt
 #align fin.last_add_one Fin.last_add_one
 #align fin.coe_add_one Fin.val_add_one
-
-section Bit
-set_option linter.deprecated false
-
-@[simp, deprecated (since := "2023-01-12")]
-theorem mk_bit0 {m n : ℕ} (h : bit0 m < n) :
-    (⟨bit0 m, h⟩ : Fin n) = (bit0 ⟨m, (Nat.le_add_right m m).trans_lt h⟩ : Fin _) :=
-  eq_of_val_eq (Nat.mod_eq_of_lt h).symm
-#align fin.mk_bit0 Fin.mk_bit0
-
-@[simp, deprecated (since := "2023-01-12")]
-theorem mk_bit1 {m n : ℕ} [NeZero n] (h : bit1 m < n) :
-    (⟨bit1 m, h⟩ : Fin n) =
-      (bit1 ⟨m, (Nat.le_add_right m m).trans_lt ((m + m).lt_succ_self.trans h)⟩ : Fin _) := by
-  ext
-  simp only [bit1, bit0] at h
-  simp only [bit1, bit0, val_add, val_one', ← Nat.add_mod, Nat.mod_eq_of_lt h]
-#align fin.mk_bit1 Fin.mk_bit1
-
-end Bit
-
+#noalign fin.mk_bit0
+#noalign fin.mk_bit1
 #align fin.val_two Fin.val_two
-
 --- Porting note: syntactically the same as the above
 #align fin.coe_two Fin.val_two
 

Mathlib/Data/Finset/Basic.lean

@@ -31,16 +31,16 @@ Finsets give a basic foundation for defining finite sums and products over types
   2. `∏ i ∈ (s : Finset α), f i`.
 
 Lean refers to these operations as big operators.
-More information can be found in `Mathlib.Algebra.BigOperators.Group.Finset`.
+More information can be found in `Mathlib/Algebra/BigOperators/Group/Finset.lean`.
 
 Finsets are directly used to define fintypes in Lean.
 A `Fintype α` instance for a type `α` consists of a universal `Finset α` containing every term of
-`α`, called `univ`. See `Mathlib.Data.Fintype.Basic`.
+`α`, called `univ`. See `Mathlib/Data/Fintype/Basic.lean`.
 There is also `univ'`, the noncomputable partner to `univ`,
 which is defined to be `α` as a finset if `α` is finite,
-and the empty finset otherwise. See `Mathlib.Data.Fintype.Basic`.
+and the empty finset otherwise. See `Mathlib/Data/Fintype/Basic.lean`.
 
-`Finset.card`, the size of a finset is defined in `Mathlib.Data.Finset.Card`.
+`Finset.card`, the size of a finset is defined in `Mathlib/Data/Finset/Card.lean`.
 This is then used to define `Fintype.card`, the size of a type.
 
 ## Main declarations
@@ -78,8 +78,8 @@ This is then used to define `Fintype.card`, the size of a type.
 
 There is a natural lattice structure on the subsets of a set.
 In Lean, we use lattice notation to talk about things involving unions and intersections. See
-`Mathlib.Order.Lattice`. For the lattice structure on finsets, `⊥` is called `bot` with `⊥ = ∅` and
-`⊤` is called `top` with `⊤ = univ`.
+`Mathlib/Order/Lattice.lean`. For the lattice structure on finsets, `⊥` is called `bot` with
+`⊥ = ∅` and `⊤` is called `top` with `⊤ = univ`.
 
 * `Finset.instHasSubsetFinset`: Lots of API about lattices, otherwise behaves as one would expect.
 * `Finset.instUnionFinset`: Defines `s ∪ t` (or `s ⊔ t`) as the union of `s` and `t`.
@@ -97,7 +97,7 @@ In Lean, we use lattice notation to talk about things involving unions and inter
 * `Finset.erase`: For any `a : α`, `erase s a` returns `s` with the element `a` removed.
 * `Finset.instSDiffFinset`: Defines the set difference `s \ t` for finsets `s` and `t`.
 * `Finset.product`: Given finsets of `α` and `β`, defines finsets of `α × β`.
-  For arbitrary dependent products, see `Mathlib.Data.Finset.Pi`.
+  For arbitrary dependent products, see `Mathlib/Data/Finset/Pi.lean`.
 
 ### Predicates on finsets
 
@@ -107,8 +107,8 @@ In Lean, we use lattice notation to talk about things involving unions and inter
 
 ### Equivalences between finsets
 
-* The `Mathlib.Data.Equiv` files describe a general type of equivalence, so look in there for any
-  lemmas. There is some API for rewriting sums and products from `s` to `t` given that `s ≃ t`.
+* The `Mathlib/Data/Equiv.lean` files describe a general type of equivalence, so look in there for
+  any lemmas. There is some API for rewriting sums and products from `s` to `t` given that `s ≃ t`.
   TODO: examples
 
 ## Tags

Mathlib/Data/Nat/Choose/Basic.lean

@@ -304,12 +304,10 @@ theorem choose_le_succ_of_lt_half_left {r n : ℕ} (h : r < n / 2) :
 
 /-- Show that for small values of the right argument, the middle value is largest. -/
 private theorem choose_le_middle_of_le_half_left {n r : ℕ} (hr : r ≤ n / 2) :
-    choose n r ≤ choose n (n / 2) :=
-  decreasingInduction
-    (fun _ k a =>
-      (eq_or_lt_of_le a).elim (fun t => t.symm ▸ le_rfl) fun h =>
-        (choose_le_succ_of_lt_half_left h).trans (k h))
-    hr (fun _ => le_rfl) hr
+    choose n r ≤ choose n (n / 2) := by
+  induction hr using decreasingInduction with
+  | self => rfl
+  | of_succ k hk ih => exact (choose_le_succ_of_lt_half_left hk).trans ih
 
 /-- `choose n r` is maximised when `r` is `n/2`. -/
 theorem choose_le_middle (r n : ℕ) : choose n r ≤ choose n (n / 2) := by