Merge branch 'master' into mrb/test_driver

.github/workflows/nightly_detect_failure.yml

@@ -50,9 +50,10 @@ jobs:
               git tag "nightly-testing-${version}"
               git push origin "nightly-testing-${version}"
               hash="$(git rev-parse "nightly-testing-${version}")"
-              printf 'SHA=%s\n' "${hash}" >> "${GITHUB_ENV}"
               curl -X POST "http://speed.lean-fro.org/mathlib4/api/queue/commit/e7b27246-a3e6-496a-b552-ff4b45c7236e/$hash" -u "admin:${{ secrets.SPEED }}"
           fi
+          hash="$(git rev-parse "nightly-testing-${version}")"
+          printf 'SHA=%s\n' "${hash}" >> "${GITHUB_ENV}"
         else
           echo "Error: The file lean-toolchain does not contain the expected pattern."
           exit 1

Archive/Imo/Imo1986Q5.lean

@@ -26,7 +26,7 @@ Formalization is based on
 with minor modifications.
 -/
 
-open Set NNReal Classical
+open NNReal
 
 namespace Imo1986Q5
 

Archive/Sensitivity.lean

@@ -33,14 +33,11 @@ The project was developed at https://github.com/leanprover-community/lean-sensit
 archived at https://github.com/leanprover-community/mathlib/blob/master/archive/sensitivity.lean
 -/
 
-
-
 namespace Sensitivity
 
 /-! The next two lines assert we do not want to give a constructive proof,
 but rather use classical logic. -/
 noncomputable section
-open scoped Classical
 
 local notation "√" => Real.sqrt
 
@@ -194,6 +191,7 @@ noncomputable def ε : ∀ {n : ℕ}, Q n → V n →ₗ[ℝ] ℝ
 
 variable {n : ℕ}
 
+open Classical in
 theorem duality (p q : Q n) : ε p (e q) = if p = q then 1 else 0 := by
   induction' n with n IH
   · rw [show p = q from Subsingleton.elim (α := Q 0) p q]
@@ -225,6 +223,7 @@ theorem epsilon_total {v : V n} (h : ∀ p : Q n, (ε p) v = 0) : v = 0 := by
 
 open Module
 
+open Classical in
 /-- `e` and `ε` are dual families of vectors. It implies that `e` is indeed a basis
 and `ε` computes coefficients of decompositions of vectors on that basis. -/
 theorem dualBases_e_ε (n : ℕ) : DualBases (@e n) (@ε n) where
@@ -237,9 +236,11 @@ since this cardinal is finite, as a natural number in `finrank_V` -/
 
 theorem dim_V : Module.rank ℝ (V n) = 2 ^ n := by
   have : Module.rank ℝ (V n) = (2 ^ n : ℕ) := by
+    classical
     rw [rank_eq_card_basis (dualBases_e_ε _).basis, Q.card]
   assumption_mod_cast
 
+open Classical in
 instance : FiniteDimensional ℝ (V n) :=
   FiniteDimensional.of_fintype_basis (dualBases_e_ε _).basis
 
@@ -285,7 +286,7 @@ theorem f_squared : ∀ v : V n, (f n) (f n v) = (n : ℝ) • v := by
 /-! We now compute the matrix of `f` in the `e` basis (`p` is the line index,
 `q` the column index). -/
 
-
+open Classical in
 theorem f_matrix : ∀ p q : Q n, |ε q (f n (e p))| = if p ∈ q.adjacent then 1 else 0 := by
   induction' n with n IH
   · intro p q
@@ -360,7 +361,7 @@ local notation "Card " X:70 => Finset.card (Set.toFinset X)
 equipped with their subspace structures. The notations come from the general
 theory of lattices, with inf and sup (also known as meet and join). -/
 
-
+open Classical in
 /-- If a subset `H` of `Q (m+1)` has cardinal at least `2^m + 1` then the
 subspace of `V (m+1)` spanned by the corresponding basis vectors non-trivially
 intersects the range of `g m`. -/
@@ -395,6 +396,7 @@ theorem exists_eigenvalue (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :
   rw [Set.toFinset_card] at hH
   linarith
 
+open Classical in
 /-- **Huang sensitivity theorem** also known as the **Huang degree theorem** -/
 theorem huang_degree_theorem (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :
     ∃ q, q ∈ H ∧ √ (m + 1) ≤ Card H ∩ q.adjacent := by

Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

@@ -21,13 +21,10 @@ https://en.wikipedia.org/wiki/Erdos-Szekeres_theorem#Pigeonhole_principle.
 sequences, increasing, decreasing, Ramsey, Erdos-Szekeres, Erdős–Szekeres, Erdős-Szekeres
 -/
 
-
 variable {α : Type*} [LinearOrder α] {β : Type*}
 
 open Function Finset
 
-open scoped Classical
-
 namespace Theorems100
 
 /-- **Erdős–Szekeres Theorem**: Given a sequence of more than `r * s` distinct values, there is an

Archive/Wiedijk100Theorems/FriendshipGraphs.lean

@@ -38,7 +38,6 @@ be phrased in terms of counting walks.
 
 -/
 
-
 open scoped Classical
 
 namespace Theorems100

Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean

@@ -38,10 +38,6 @@ The formalization follows Erdős's proof by upper and lower estimates.
 https://en.wikipedia.org/wiki/Divergence_of_the_sum_of_the_reciprocals_of_the_primes
 -/
 
-
-
-open scoped Classical
-
 open Filter Finset
 
 namespace Theorems100
@@ -57,6 +53,7 @@ of `p`, i.e., those `e < x` for which there is a prime `p ∈ (k, x]` that divid
 def U (x k : ℕ) :=
   Finset.biUnion (P x k) (fun p => Finset.filter (fun e => p ∣ e + 1) (range x))
 
+open Classical in
 /-- Those `e < x` for which `e + 1` is a product of powers of primes smaller than or equal to `k`.
 -/
 noncomputable def M (x k : ℕ) :=
@@ -217,6 +214,7 @@ theorem Real.tendsto_sum_one_div_prime_atTop :
   -- This is indeed a partition, so `|U| + |M| = |range x| = x`.
   have h2 : x = card U' + card M' := by
     rw [← card_range x, hU', hM', ← range_sdiff_eq_biUnion]
+    classical
     exact (card_sdiff_add_card_eq_card (Finset.filter_subset _ _)).symm
   -- But for the `x` we have chosen above, both `|U|` and `|M|` are less than or equal to `x / 2`,
   -- and for U, the inequality is strict.

LongestPole/Main.lean

@@ -22,7 +22,7 @@ open Lean Meta
 /-- Runs a terminal command and retrieves its output -/
 def runCmd (cmd : String) (args : Array String) (throwFailure := true) : IO String := do
   let out ← IO.Process.output { cmd := cmd, args := args }
-  if out.exitCode != 0 && throwFailure then throw $ IO.userError out.stderr
+  if out.exitCode != 0 && throwFailure then throw <| IO.userError out.stderr
   else return out.stdout
 
 def runCurl (args : Array String) (throwFailure := true) : IO String := do

Mathlib.lean

@@ -643,11 +643,13 @@ import Mathlib.Algebra.Order.Ring.Star
 import Mathlib.Algebra.Order.Ring.Synonym
 import Mathlib.Algebra.Order.Ring.Unbundled.Basic
 import Mathlib.Algebra.Order.Ring.Unbundled.Nonneg
+import Mathlib.Algebra.Order.Ring.Unbundled.Rat
 import Mathlib.Algebra.Order.Ring.WithTop
 import Mathlib.Algebra.Order.Sub.Basic
-import Mathlib.Algebra.Order.Sub.Canonical
 import Mathlib.Algebra.Order.Sub.Defs
 import Mathlib.Algebra.Order.Sub.Prod
+import Mathlib.Algebra.Order.Sub.Unbundled.Basic
+import Mathlib.Algebra.Order.Sub.Unbundled.Hom
 import Mathlib.Algebra.Order.Sub.WithTop
 import Mathlib.Algebra.Order.Sum
 import Mathlib.Algebra.Order.ToIntervalMod
@@ -1254,6 +1256,7 @@ import Mathlib.Analysis.RCLike.Lemmas
 import Mathlib.Analysis.Seminorm
 import Mathlib.Analysis.SpecialFunctions.Arsinh
 import Mathlib.Analysis.SpecialFunctions.Bernstein
+import Mathlib.Analysis.SpecialFunctions.BinaryEntropy
 import Mathlib.Analysis.SpecialFunctions.CompareExp
 import Mathlib.Analysis.SpecialFunctions.Complex.Analytic
 import Mathlib.Analysis.SpecialFunctions.Complex.Arctan
@@ -1546,6 +1549,7 @@ import Mathlib.CategoryTheory.Limits.FintypeCat
 import Mathlib.CategoryTheory.Limits.Fubini
 import Mathlib.CategoryTheory.Limits.FullSubcategory
 import Mathlib.CategoryTheory.Limits.FunctorCategory
+import Mathlib.CategoryTheory.Limits.FunctorCategoryEpiMono
 import Mathlib.CategoryTheory.Limits.FunctorToTypes
 import Mathlib.CategoryTheory.Limits.HasLimits
 import Mathlib.CategoryTheory.Limits.IndYoneda
@@ -1864,6 +1868,7 @@ import Mathlib.Combinatorics.Additive.AP.Three.Defs
 import Mathlib.Combinatorics.Additive.Corner.Defs
 import Mathlib.Combinatorics.Additive.Corner.Roth
 import Mathlib.Combinatorics.Additive.Dissociation
+import Mathlib.Combinatorics.Additive.DoublingConst
 import Mathlib.Combinatorics.Additive.ETransform
 import Mathlib.Combinatorics.Additive.Energy
 import Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
@@ -2289,6 +2294,7 @@ import Mathlib.Data.Multiset.Interval
 import Mathlib.Data.Multiset.Lattice
 import Mathlib.Data.Multiset.NatAntidiagonal
 import Mathlib.Data.Multiset.Nodup
+import Mathlib.Data.Multiset.OrderedMonoid
 import Mathlib.Data.Multiset.Pi
 import Mathlib.Data.Multiset.Powerset
 import Mathlib.Data.Multiset.Range
@@ -2458,7 +2464,6 @@ import Mathlib.Data.Set.BoolIndicator
 import Mathlib.Data.Set.Card
 import Mathlib.Data.Set.Constructions
 import Mathlib.Data.Set.Countable
-import Mathlib.Data.Set.Defs
 import Mathlib.Data.Set.Enumerate
 import Mathlib.Data.Set.Equitable
 import Mathlib.Data.Set.Finite
@@ -2471,6 +2476,7 @@ import Mathlib.Data.Set.MemPartition
 import Mathlib.Data.Set.MulAntidiagonal
 import Mathlib.Data.Set.NAry
 import Mathlib.Data.Set.Notation
+import Mathlib.Data.Set.Operations
 import Mathlib.Data.Set.Opposite
 import Mathlib.Data.Set.Pairwise.Basic
 import Mathlib.Data.Set.Pairwise.Lattice
@@ -2697,15 +2703,17 @@ import Mathlib.GroupTheory.Abelianization
 import Mathlib.GroupTheory.Archimedean
 import Mathlib.GroupTheory.ClassEquation
 import Mathlib.GroupTheory.Commensurable
-import Mathlib.GroupTheory.Commutator
+import Mathlib.GroupTheory.Commutator.Basic
+import Mathlib.GroupTheory.Commutator.Finite
 import Mathlib.GroupTheory.CommutingProbability
 import Mathlib.GroupTheory.Complement
 import Mathlib.GroupTheory.Congruence.Basic
 import Mathlib.GroupTheory.Congruence.BigOperators
 import Mathlib.GroupTheory.Congruence.Opposite
 import Mathlib.GroupTheory.Coprod.Basic
 import Mathlib.GroupTheory.CoprodI
-import Mathlib.GroupTheory.Coset
+import Mathlib.GroupTheory.Coset.Basic
+import Mathlib.GroupTheory.Coset.Card
 import Mathlib.GroupTheory.CosetCover
 import Mathlib.GroupTheory.Coxeter.Basic
 import Mathlib.GroupTheory.Coxeter.Inversion
@@ -2727,6 +2735,7 @@ import Mathlib.GroupTheory.FreeGroup.NielsenSchreier
 import Mathlib.GroupTheory.GroupAction.Basic
 import Mathlib.GroupTheory.GroupAction.BigOperators
 import Mathlib.GroupTheory.GroupAction.Blocks
+import Mathlib.GroupTheory.GroupAction.CardCommute
 import Mathlib.GroupTheory.GroupAction.ConjAct
 import Mathlib.GroupTheory.GroupAction.DomAct.ActionHom
 import Mathlib.GroupTheory.GroupAction.DomAct.Basic
@@ -2774,7 +2783,8 @@ import Mathlib.GroupTheory.Perm.Support
 import Mathlib.GroupTheory.Perm.ViaEmbedding
 import Mathlib.GroupTheory.PresentedGroup
 import Mathlib.GroupTheory.PushoutI
-import Mathlib.GroupTheory.QuotientGroup
+import Mathlib.GroupTheory.QuotientGroup.Basic
+import Mathlib.GroupTheory.QuotientGroup.Finite
 import Mathlib.GroupTheory.Schreier
 import Mathlib.GroupTheory.SchurZassenhaus
 import Mathlib.GroupTheory.SemidirectProduct

Mathlib/Algebra/Algebra/Equiv.lean

@@ -304,9 +304,7 @@ theorem invFun_eq_symm {e : A₁ ≃ₐ[R] A₂} : e.invFun = e.symm :=
   rfl
 
 @[simp]
-theorem symm_symm (e : A₁ ≃ₐ[R] A₂) : e.symm.symm = e := by
-  ext
-  rfl
+theorem symm_symm (e : A₁ ≃ₐ[R] A₂) : e.symm.symm = e := rfl
 
 theorem symm_bijective : Function.Bijective (symm : (A₁ ≃ₐ[R] A₂) → A₂ ≃ₐ[R] A₁) :=
   Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Mathlib/Algebra/Associated/Basic.lean

@@ -851,8 +851,8 @@ instance uniqueUnits : Unique (Associates α)ˣ where
   uniq := by
     rintro ⟨a, b, hab, hba⟩
     revert hab hba
-    exact Quotient.inductionOn₂ a b $ fun a b hab hba ↦ Units.ext $ Quotient.sound $
-      associated_one_of_associated_mul_one $ Quotient.exact hab
+    exact Quotient.inductionOn₂ a b <| fun a b hab hba ↦ Units.ext <| Quotient.sound <|
+      associated_one_of_associated_mul_one <| Quotient.exact hab
 
 @[deprecated (since := "2024-07-22")] alias mul_eq_one_iff := mul_eq_one
 @[deprecated (since := "2024-07-22")] protected alias units_eq_one := Subsingleton.elim

Mathlib/Algebra/BigOperators/Group/Finset.lean

@@ -39,6 +39,7 @@ See the documentation of `to_additive.attr` for more information.
 -- assert_not_exists AddCommMonoidWithOne
 assert_not_exists MonoidWithZero
 assert_not_exists MulAction
+assert_not_exists OrderedCommMonoid
 
 variable {ι κ α β γ : Type*}
 
@@ -456,7 +457,7 @@ of `s`, and over all subsets of `s` to which one adds `x`. -/
 of `s`, and over all subsets of `s` to which one adds `x`."]
 lemma prod_powerset_cons (ha : a ∉ s) (f : Finset α → β) :
     ∏ t ∈ (s.cons a ha).powerset, f t = (∏ t ∈ s.powerset, f t) *
-      ∏ t ∈ s.powerset.attach, f (cons a t $ not_mem_mono (mem_powerset.1 t.2) ha) := by
+      ∏ t ∈ s.powerset.attach, f (cons a t <| not_mem_mono (mem_powerset.1 t.2) ha) := by
   classical
   simp_rw [cons_eq_insert]
   rw [prod_powerset_insert ha, prod_attach _ fun t ↦ f (insert a t)]
@@ -721,7 +722,7 @@ but differ in the type of their element, `univ.pi t` is a `Finset (Π a ∈ univ
 lemma prod_univ_pi [DecidableEq ι] [Fintype ι] {κ : ι → Type*} (t : ∀ i, Finset (κ i))
     (f : (∀ i ∈ (univ : Finset ι), κ i) → β) :
     ∏ x ∈ univ.pi t, f x = ∏ x ∈ Fintype.piFinset t, f fun a _ ↦ x a := by
-  apply prod_nbij' (fun x i ↦ x i $ mem_univ _) (fun x i _ ↦ x i) <;> simp
+  apply prod_nbij' (fun x i ↦ x i <| mem_univ _) (fun x i _ ↦ x i) <;> simp
 
 @[to_additive (attr := simp)]
 lemma prod_diag [DecidableEq α] (s : Finset α) (f : α × α → β) :
@@ -1455,11 +1456,12 @@ theorem eq_prod_range_div' {M : Type*} [CommGroup M] (f : ℕ → M) (n : ℕ) :
 reduces to the difference of the last and first terms
 when the function we are summing is monotone.
 -/
-theorem sum_range_tsub [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α]
-    [ContravariantClass α α (· + ·) (· ≤ ·)] {f : ℕ → α} (h : Monotone f) (n : ℕ) :
+theorem sum_range_tsub [AddCommMonoid α] [PartialOrder α] [Sub α] [OrderedSub α]
+    [CovariantClass α α (· + ·) (· ≤ ·)] [ContravariantClass α α (· + ·) (· ≤ ·)] [ExistsAddOfLE α]
+    {f : ℕ → α} (h : Monotone f) (n : ℕ) :
     ∑ i ∈ range n, (f (i + 1) - f i) = f n - f 0 := by
   apply sum_range_induction
-  case base => apply tsub_self
+  case base => apply tsub_eq_of_eq_add; rw [zero_add]
   case step =>
     intro n
     have h₁ : f n ≤ f (n + 1) := h (Nat.le_succ _)
@@ -1684,7 +1686,7 @@ theorem prod_ite_one (s : Finset α) (p : α → Prop) [DecidablePred p]
     exact fun i hi => if_neg (h i hi)
 
 @[to_additive]
-theorem prod_erase_lt_of_one_lt {γ : Type*} [DecidableEq α] [OrderedCommMonoid γ]
+theorem prod_erase_lt_of_one_lt {γ : Type*} [DecidableEq α] [CommMonoid γ] [Preorder γ]
     [CovariantClass γ γ (· * ·) (· < ·)] {s : Finset α} {d : α} (hd : d ∈ s) {f : α → γ}
     (hdf : 1 < f d) : ∏ m ∈ s.erase d, f m < ∏ m ∈ s, f m := by
   conv in ∏ m ∈ s, f m => rw [← Finset.insert_erase hd]
@@ -1751,7 +1753,7 @@ variable [DecidableEq ι] [CancelCommMonoid α] {s t : Finset ι} {f : ι → α
 @[to_additive]
 lemma prod_sdiff_eq_prod_sdiff_iff :
     ∏ i ∈ s \ t, f i = ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i = ∏ i ∈ t, f i :=
-  eq_comm.trans $ eq_iff_eq_of_mul_eq_mul $ by
+  eq_comm.trans <| eq_iff_eq_of_mul_eq_mul <| by
     rw [← prod_union disjoint_sdiff_self_left, ← prod_union disjoint_sdiff_self_left,
       sdiff_union_self_eq_union, sdiff_union_self_eq_union, union_comm]
 
@@ -1985,7 +1987,7 @@ theorem prod_subtype_mul_prod_subtype {α β : Type*} [Fintype α] [CommMonoid 
 
 @[to_additive] lemma prod_subset {s : Finset ι} {f : ι → α} (h : ∀ i, f i ≠ 1 → i ∈ s) :
     ∏ i ∈ s, f i = ∏ i, f i :=
-  Finset.prod_subset s.subset_univ $ by simpa [not_imp_comm (a := _ ∈ s)]
+  Finset.prod_subset s.subset_univ <| by simpa [not_imp_comm (a := _ ∈ s)]
 
 @[to_additive]
 lemma prod_ite_eq_ite_exists (p : ι → Prop) [DecidablePred p] (h : ∀ i j, p i → p j → i = j)
@@ -2032,7 +2034,7 @@ variable [CommMonoid α]
 @[to_additive (attr := simp)]
 lemma prod_attach_univ [Fintype ι] (f : {i // i ∈ @univ ι _} → α) :
     ∏ i ∈ univ.attach, f i = ∏ i, f ⟨i, mem_univ _⟩ :=
-  Fintype.prod_equiv (Equiv.subtypeUnivEquiv mem_univ) _ _ $ by simp
+  Fintype.prod_equiv (Equiv.subtypeUnivEquiv mem_univ) _ _ <| by simp
 
 @[to_additive]
 theorem prod_erase_attach [DecidableEq ι] {s : Finset ι} (f : ι → α) (i : ↑s) :

Mathlib/Algebra/BigOperators/Ring.lean

@@ -168,7 +168,7 @@ theorem prod_add (f g : ι → α) (s : Finset ι) :
         (by simp)
         (by simp [Classical.em])
         (by simp_rw [mem_filter, Function.funext_iff, eq_iff_iff, mem_pi, mem_insert]; tauto)
-        (by simp_rw [ext_iff, @mem_filter _ _ (id _), mem_powerset]; tauto)
+        (by simp_rw [Finset.ext_iff, @mem_filter _ _ (id _), mem_powerset]; tauto)
         (fun a _ ↦ by
           simp only [prod_ite, filter_attach', prod_map, Function.Embedding.coeFn_mk,
             Subtype.map_coe, id_eq, prod_attach, filter_congr_decidable]

Mathlib/Algebra/Category/Grp/Colimits.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Mathlib.Algebra.Category.Grp.Preadditive
-import Mathlib.GroupTheory.QuotientGroup
 import Mathlib.CategoryTheory.Limits.Shapes.Kernels
 import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
 import Mathlib.CategoryTheory.ConcreteCategory.Elementwise
+import Mathlib.GroupTheory.QuotientGroup.Basic
 
 /-!
 # The category of additive commutative groups has all colimits.

Mathlib/Algebra/Category/Grp/EpiMono.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang
 -/
 import Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
-import Mathlib.GroupTheory.QuotientGroup
 import Mathlib.CategoryTheory.ConcreteCategory.EpiMono
 import Mathlib.CategoryTheory.Limits.Constructions.EpiMono
+import Mathlib.GroupTheory.QuotientGroup.Basic
 
 /-!
 # Monomorphisms and epimorphisms in `Group`

Mathlib/Algebra/CharZero/Quotient.lean

@@ -3,7 +3,9 @@ Copyright (c) 2022 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import Mathlib.GroupTheory.QuotientGroup
+import Mathlib.Algebra.Field.Basic
+import Mathlib.GroupTheory.QuotientGroup.Basic
+import Mathlib.Algebra.Order.Group.Unbundled.Int
 
 /-!
 # Lemmas about quotients in characteristic zero