Merge remote-tracking branch 'origin/master' into structured-arrow-abbrev

Author: joelriou

Cache/Requests.lean

@@ -13,6 +13,9 @@ namespace Cache.Requests
 
 open System (FilePath)
 
+/-- The full name of the main Mathlib GitHub repository. -/
+def MATHLIBREPO := "leanprover-community/mathlib4"
+
 /--
 Structure to hold repository information with priority ordering
 -/
@@ -37,7 +40,7 @@ def isRemoteURL (url : String) : Bool :=
 /--
 Helper function to get repository from a remote name
 -/
-def getRepoFromRemote (mathlibDepPath : FilePath) (remoteName : String) (errorContext : String) : IO String := do
+def getRepoFromRemote (mathlibDepPath : FilePath) (remoteName : String) (errorContext : String) : IO (Option String) := do
   -- If the remote is already a valid URL, attempt to extract the repo from it. This happens with `gh pr checkout`
   if isRemoteURL remoteName then
     repoFromURL remoteName
@@ -46,23 +49,25 @@ def getRepoFromRemote (mathlibDepPath : FilePath) (remoteName : String) (errorCo
   -- standard name like `origin` or `upstream` or it errors out.
   let out ← IO.Process.output
     {cmd := "git", args := #["remote", "get-url", remoteName], cwd := mathlibDepPath}
-  -- If `git remote get-url` fails then bail out with an error to help debug
+  -- If `git remote get-url` fails then return none.
   let output := out.stdout.trimAscii
   unless out.exitCode == 0 do
-    throw <| IO.userError s!"\
-      Failed to run Git to determine Mathlib's repository from {remoteName} remote (exit code: {out.exitCode}).\n\
+    IO.println s!"\
+      Warning: failed to run Git to determine Mathlib's repository from {remoteName} remote\n\
       {errorContext}\n\
-      Stdout:\n{output}\nStderr:\n{out.stderr.trimAscii}\n"
+      Continuing to fetch the cache from {MATHLIBREPO}."
+    return none
   -- Finally attempt to extract the repository from the remote URL returned by `git remote get-url`
   repoFromURL output.copy
-where repoFromURL (url : String) : IO String := do
+where repoFromURL (url : String) : IO (Option String) := do
     if let some repo := extractRepoFromUrl url then
-      return repo
+      return some repo
     else
-      throw <| IO.userError s!"\
-        Failed to extract repository from remote URL: {url}.\n\
+      IO.println s!"\
+        Warning: Failed to extract repository from remote URL: {url}.\n\
         {errorContext}\n\
-        Please ensure the remote URL is valid and points to a GitHub repository."
+        Continuing to fetch the cache from {MATHLIBREPO}."
+      return none
 
 /--
 Finds the remote name that points to `leanprover-community/mathlib4` repository.
@@ -146,7 +151,7 @@ Attempts to determine the GitHub repository of a version of Mathlib from its Git
 If the current commit coincides with a PR ref, it will determine the source fork
 of that PR rather than just using the origin remote.
 -/
-def getRemoteRepo (mathlibDepPath : FilePath) : IO RepoInfo := do
+def getRemoteRepo (mathlibDepPath : FilePath) : IO (Option RepoInfo) := do
 
   -- Since currently we need to push a PR to `leanprover-community/mathlib` build a user cache,
   -- we check if we are a special branch or a branch with PR. This leaves out non-PRed fork
@@ -176,7 +181,7 @@ def getRemoteRepo (mathlibDepPath : FilePath) : IO RepoInfo := do
       let repo := "leanprover-community/mathlib4-nightly-testing"
       let cacheService := if useCloudflareCache then "Cloudflare" else "Azure"
       IO.println s!"Using cache ({cacheService}) from nightly-testing remote: {repo}"
-      return {repo := repo, useFirst := true}
+      return some {repo := repo, useFirst := true}
 
     -- Only search for PR refs if we're not on a regular branch like master, bump/*, or nightly-testing*
     -- let isSpecialBranch := branchName == "master" || branchName.startsWith "bump/" ||
@@ -234,11 +239,16 @@ def getRemoteRepo (mathlibDepPath : FilePath) : IO RepoInfo := do
     -- If no tracking remote is configured, fall back to origin
     "origin"
 
-  let repo ← getRepoFromRemote mathlibDepPath remoteName
+  let repo? ← getRepoFromRemote mathlibDepPath remoteName
     s!"Ensure Git is installed and the '{remoteName}' remote points to its GitHub repository."
   let cacheService := if useCloudflareCache then "Cloudflare" else "Azure"
-  IO.println s!"Using cache ({cacheService}) from {remoteName}: {repo}"
-  return {repo := repo, useFirst := false}
+  match repo? with
+  | some repo =>
+    IO.println s!"Using cache ({cacheService}) from {remoteName}: {repo?}"
+    return some {repo := repo, useFirst := false}
+  | none =>
+    IO.println s!"Using cache ({cacheService}) from {MATHLIBREPO}."
+    return none
 
 /-- Public URL for mathlib cache -/
 initialize URL : String ← do
@@ -275,9 +285,6 @@ def getUploadAuth : IO UploadAuth := do
     throw <| IO.userError
       "environment variable MATHLIB_CACHE_AZURE_BEARER_TOKEN or MATHLIB_CACHE_SAS must be set to upload caches"
 
-/-- The full name of the main Mathlib GitHub repository. -/
-def MATHLIBREPO := "leanprover-community/mathlib4"
-
 /--
 Given a file name like `"1234.tar.gz"`, makes the URL to that file on the server.
 
@@ -663,16 +670,19 @@ def getFiles
       isMathlibRoot mathlibDepPath
     if failed > 0 then IO.Process.exit 1
   else
-    let repoInfo ← getRemoteRepo (← read).mathlibDepPath
+    let repoInfo? ← getRemoteRepo (← read).mathlibDepPath
 
     -- Build list of repositories to download from in order
     let repos : List String :=
-      if repoInfo.repo == MATHLIBREPO then
-        [repoInfo.repo]
-      else if repoInfo.useFirst then
-        [repoInfo.repo, MATHLIBREPO]
+      if let some repoInfo := repoInfo? then
+        if repoInfo.repo == MATHLIBREPO then
+          [MATHLIBREPO]
+        else if repoInfo.useFirst then
+          [repoInfo.repo, MATHLIBREPO]
+        else
+          [MATHLIBREPO, repoInfo.repo]
       else
-        [MATHLIBREPO, repoInfo.repo]
+        [MATHLIBREPO]
 
     let mut failed : Nat := 0
     for h : i in [0:repos.length] do

Mathlib.lean

@@ -899,6 +899,7 @@ public import Mathlib.Algebra.Order.Antidiag.Pi
 public import Mathlib.Algebra.Order.Antidiag.Prod
 public import Mathlib.Algebra.Order.Archimedean.Basic
 public import Mathlib.Algebra.Order.Archimedean.Class
+public import Mathlib.Algebra.Order.Archimedean.Defs
 public import Mathlib.Algebra.Order.Archimedean.Hom
 public import Mathlib.Algebra.Order.Archimedean.IndicatorCard
 public import Mathlib.Algebra.Order.Archimedean.Submonoid
@@ -1493,6 +1494,7 @@ public import Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiM
 public import Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
 public import Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty
 public import Mathlib.AlgebraicTopology.SimplexCategory.Rev
+public import Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
 public import Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
 public import Mathlib.AlgebraicTopology.SimplexCategory.Truncated
 public import Mathlib.AlgebraicTopology.SimplicialCategory.Basic
@@ -1536,8 +1538,10 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
 public import Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
 public import Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
 public import Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
+public import Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
 public import Mathlib.AlgebraicTopology.SimplicialSet.Op
 public import Mathlib.AlgebraicTopology.SimplicialSet.Path
+public import Mathlib.AlgebraicTopology.SimplicialSet.PiZero
 public import Mathlib.AlgebraicTopology.SimplicialSet.Presentable
 public import Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
 public import Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
@@ -6229,6 +6233,7 @@ public import Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
 public import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
 public import Mathlib.RingTheory.AlgebraicIndependent.Transcendental
 public import Mathlib.RingTheory.Artinian.Algebra
+public import Mathlib.RingTheory.Artinian.Defs
 public import Mathlib.RingTheory.Artinian.Instances
 public import Mathlib.RingTheory.Artinian.Module
 public import Mathlib.RingTheory.Artinian.Ring
@@ -6243,6 +6248,7 @@ public import Mathlib.RingTheory.Binomial
 public import Mathlib.RingTheory.ChainOfDivisors
 public import Mathlib.RingTheory.ClassGroup
 public import Mathlib.RingTheory.Coalgebra.Basic
+public import Mathlib.RingTheory.Coalgebra.CoassocSimps
 public import Mathlib.RingTheory.Coalgebra.Convolution
 public import Mathlib.RingTheory.Coalgebra.Equiv
 public import Mathlib.RingTheory.Coalgebra.GroupLike

Mathlib/Algebra/Algebra/Equiv.lean

@@ -69,9 +69,6 @@ def toAlgEquiv {F R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B] [Alg
     [Algebra R B] [EquivLike F A B] [AlgEquivClass F R A B] (f : F) : A ≃ₐ[R] B :=
   { (f : A ≃ B), (f : A ≃+* B) with commutes' := commutes f }
 
-instance (F R A B : Type*) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
-    [EquivLike F A B] [AlgEquivClass F R A B] : CoeTC F (A ≃ₐ[R] B) :=
-  ⟨toAlgEquiv⟩
 end AlgEquivClass
 
 namespace AlgEquiv
@@ -137,7 +134,7 @@ theorem toEquiv_eq_coe : e.toEquiv = e :=
 
 @[simp]
 protected theorem coe_coe {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂] (f : F) :
-    ⇑(f : A₁ ≃ₐ[R] A₂) = f :=
+    ⇑(AlgEquivClass.toAlgEquiv f) = f :=
   rfl
 
 theorem coe_fun_injective : @Function.Injective (A₁ ≃ₐ[R] A₂) (A₁ → A₂) fun e => (e : A₁ → A₂) :=
@@ -255,13 +252,13 @@ theorem invFun_eq_symm {e : A₁ ≃ₐ[R] A₂} : e.invFun = e.symm :=
 @[simp]
 theorem coe_apply_coe_coe_symm_apply {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂]
     (f : F) (x : A₂) :
-    f ((f : A₁ ≃ₐ[R] A₂).symm x) = x :=
+    f ((AlgEquivClass.toAlgEquiv f).symm x) = x :=
   EquivLike.right_inv f x
 
 @[simp]
 theorem coe_coe_symm_apply_coe_apply {F : Type*} [EquivLike F A₁ A₂] [AlgEquivClass F R A₁ A₂]
     (f : F) (x : A₁) :
-    (f : A₁ ≃ₐ[R] A₂).symm (f x) = x :=
+    (AlgEquivClass.toAlgEquiv f).symm (f x) = x :=
   EquivLike.left_inv f x
 
 /-- `simp` normal form of `invFun_eq_symm` -/

Mathlib/Algebra/Algebra/Spectrum/Basic.lean

@@ -424,7 +424,7 @@ theorem AlgEquiv.spectrum_eq {F R A B : Type*} [CommSemiring R] [Ring A] [Ring B
     spectrum R (f a) = spectrum R a :=
   Set.Subset.antisymm (AlgHom.spectrum_apply_subset _ _) <| by
     simpa only [AlgEquiv.coe_algHom, AlgEquiv.coe_coe_symm_apply_coe_apply] using
-      AlgHom.spectrum_apply_subset (f : A ≃ₐ[R] B).symm (f a)
+      AlgHom.spectrum_apply_subset (AlgEquivClass.toAlgEquiv f : A ≃ₐ[R] B).symm (f a)
 
 section ConjugateUnits
 

Mathlib/Algebra/BigOperators/Intervals.lean

@@ -78,12 +78,12 @@ theorem prod_Icc_succ_top {a b : ℕ} (hab : a ≤ b + 1) (f : ℕ → M) :
 @[to_additive]
 theorem prod_range_mul_prod_Ico (f : ℕ → M) {m n : ℕ} (h : m ≤ n) :
     ((∏ k ∈ range m, f k) * ∏ k ∈ Ico m n, f k) = ∏ k ∈ range n, f k :=
-  Nat.Ico_zero_eq_range ▸ Nat.Ico_zero_eq_range ▸ prod_Ico_consecutive f m.zero_le h
+  Nat.Ico_zero_eq_range m ▸ Nat.Ico_zero_eq_range n ▸ prod_Ico_consecutive f m.zero_le h
 
 @[to_additive]
 theorem prod_range_eq_mul_Ico (f : ℕ → M) {n : ℕ} (hn : 0 < n) :
     ∏ x ∈ Finset.range n, f x = f 0 * ∏ x ∈ Ico 1 n, f x :=
-  Finset.range_eq_Ico ▸ Finset.prod_eq_prod_Ico_succ_bot hn f
+  Finset.range_eq_Ico n ▸ Finset.prod_eq_prod_Ico_succ_bot hn f
 
 @[to_additive]
 theorem prod_Ico_eq_mul_inv {δ : Type*} [CommGroup δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) :

Mathlib/Algebra/BigOperators/Module.lean

@@ -59,7 +59,8 @@ theorem sum_range_by_parts :
       f (n - 1) • G n - ∑ i ∈ range (n - 1), (f (i + 1) - f i) • G (i + 1) := by
   by_cases hn : n = 0
   · simp [hn]
-  · rw [range_eq_Ico, sum_Ico_by_parts f g (Nat.pos_of_ne_zero hn), sum_range_zero, smul_zero,
-      sub_zero, range_eq_Ico]
+  · simp only [range_eq_Ico]
+    rw [sum_Ico_by_parts f g (Nat.pos_of_ne_zero hn), sum_range_zero, smul_zero, sub_zero]
+    simp only [← range_eq_Ico]
 
 end Finset

Mathlib/Algebra/Exact.lean

@@ -92,7 +92,7 @@ lemma iff_rangeFactorization [One P] (hg : 1 ∈ Set.range g) :
     MulExact f g ↔ MulExact ((↑) : Set.range f → N) (Set.rangeFactorization g) := by
   letI : One (Set.range g) := ⟨⟨1, hg⟩⟩
   have : ((1 : Set.range g) : P) = 1 := rfl
-  simp [MulExact, Set.rangeFactorization, Subtype.ext_iff, this]
+  simp [MulExact, Subtype.ext_iff, this]
 
 /-- If two maps `f : M → N` and `g : N → P` are exact, then the induced maps
 `Set.range f → N → Set.range g` are exact.
@@ -430,8 +430,7 @@ def Exact.splitInjectiveEquiv
     · intro x y e
       simp only [prod_apply, Pi.prod, Prod.mk.injEq] at e
       obtain ⟨z, hz⟩ := (h (x - y)).mp (by simpa [sub_eq_zero] using e.2)
-      suffices z = 0 by rw [← sub_eq_zero, ← hz, this, map_zero]
-      rw [← h₁ z, hz, map_sub, e.1, sub_self]
+      rw [← sub_eq_zero, ← hz, ← h₁ z, hz, map_sub, e.1, sub_self, map_zero]
     · rintro ⟨x, y⟩
       obtain ⟨y, rfl⟩ := hg y
       refine ⟨f x + y - f (l.1 y), by ext <;> simp [h₁, h₂]⟩

Mathlib/Algebra/Module/Torsion/Basic.lean

@@ -534,9 +534,8 @@ namespace Module
 variable [Ring R] [AddCommGroup M] [Module R M]
 variable {I : Ideal R} {r : R}
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- can't be an instance because `hM` can't be inferred -/
+@[implicit_reducible]
 def IsTorsionBySet.hasSMul (hM : IsTorsionBySet R M I) : SMul (R ⧸ I) M where
   smul b := QuotientAddGroup.lift I.toAddSubgroup (smulAddHom R M)
     (by rwa [isTorsionBySet_iff_subset_annihilator] at hM) b
@@ -557,17 +556,16 @@ theorem IsTorsionBy.mk_smul [(Ideal.span {r}).IsTwoSided] (hM : IsTorsionBy R M
     Ideal.Quotient.mk (Ideal.span {r}) b • x = b • x :=
   rfl
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- An `(R ⧸ I)`-module is an `R`-module which `IsTorsionBySet R M I`. -/
+@[implicit_reducible]
 def IsTorsionBySet.module [I.IsTwoSided] (hM : IsTorsionBySet R M I) : Module (R ⧸ I) M :=
-  letI := hM.hasSMul; I.mkQ_surjective.moduleLeft _ (IsTorsionBySet.mk_smul hM)
+  letI := hM.hasSMul; fast_instance% I.mkQ_surjective.moduleLeft _ (IsTorsionBySet.mk_smul hM)
 
 instance IsTorsionBySet.isScalarTower [I.IsTwoSided] (hM : IsTorsionBySet R M I)
     {S : Type*} [SMul S R] [SMul S M] [IsScalarTower S R M] [IsScalarTower S R R] :
-    @IsScalarTower S (R ⧸ I) M _ (IsTorsionBySet.module hM).toSMul _ :=
+    @IsScalarTower S (R ⧸ I) M _ hM.hasSMul _ :=
   -- Porting note: still needed to be fed the Module R / I M instance
-  @IsScalarTower.mk S (R ⧸ I) M _ (IsTorsionBySet.module hM).toSMul _
+  @IsScalarTower.mk S (R ⧸ I) M _ hM.hasSMul _
     (fun b d x => Quotient.inductionOn' d fun c => (smul_assoc b c x :))
 
 /-- If an `R`-module `M` is annihilated by a two-sided ideal `I`, then the identity is a semilinear
@@ -580,20 +578,19 @@ def IsTorsionBySet.semilinearMap [I.IsTwoSided] (hM : IsTorsionBySet R M I) :
     map_smul' := fun _ _ ↦ rfl }
 
 theorem IsTorsionBySet.isSemisimpleModule_iff [I.IsTwoSided]
-    (hM : Module.IsTorsionBySet R M I) : let _ := hM.module
+    (hM : Module.IsTorsionBySet R M I) : letI := hM.module
     IsSemisimpleModule (R ⧸ I) M ↔ IsSemisimpleModule R M :=
-  let _ := hM.module
+  letI := hM.module
   (hM.semilinearMap.isSemisimpleModule_iff_of_bijective Function.bijective_id).symm
 
 /-- An `(R ⧸ Ideal.span {r})`-module is an `R`-module for which `IsTorsionBy R M r`. -/
 abbrev IsTorsionBy.module [h : (Ideal.span {r}).IsTwoSided] (hM : IsTorsionBy R M r) :
     Module (R ⧸ Ideal.span {r}) M := by
   rw [Ideal.span] at h; exact ((isTorsionBySet_span_singleton_iff r).mpr hM).module
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- Any module is also a module over the quotient of the ring by the annihilator.
 Not an instance because it causes synthesis failures / timeouts. -/
+@[implicit_reducible]
 def quotientAnnihilator : Module (R ⧸ Module.annihilator R M) M :=
   (isTorsionBySet_annihilator R M).module
 
@@ -989,9 +986,8 @@ lemma torsionBy.mod_self_nsmul' (s : ℕ) {x : A} (h : x ∈ A[n]) :
     s • x = (s % n) • x :=
   nsmul_eq_mod_nsmul s (torsionBy.nsmul_iff.mp h)
 
--- adding `@[implicit_reducible]` causes downstream breakage
-set_option warn.classDefReducibility false in
 /-- For a natural number `n`, the `n`-torsion subgroup of `A` is a `ZMod n` module. -/
+@[implicit_reducible]
 def torsionBy.zmodModule : Module (ZMod n) A[n] :=
   AddCommGroup.zmodModule torsionBy.nsmul