Update lean-toolchain for leanprover/lean4#10967

Author: leanprover-community-mathlib4-bot

Cache/IO.lean

@@ -41,7 +41,9 @@ def isPartOfMathlibCache (mod : Name) : Bool := #[
   -- Allow PRs to upload oleans for Reap for testing.
   `Requests,
   `OpenAIClient,
-  `Reap,].contains mod.getRoot
+  `Reap,
+  -- Allow PRs to upload oleans for Canonical for testing.
+  `Canonical,].contains mod.getRoot
 
 /-- Target directory for caching -/
 initialize CACHEDIR : FilePath ← do

Mathlib.lean

@@ -2833,6 +2833,7 @@ import Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
 import Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
 import Mathlib.CategoryTheory.Sites.Hypercover.One
 import Mathlib.CategoryTheory.Sites.Hypercover.Zero
+import Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
 import Mathlib.CategoryTheory.Sites.IsSheafFor
 import Mathlib.CategoryTheory.Sites.JointlySurjective
 import Mathlib.CategoryTheory.Sites.LeftExact
@@ -3650,6 +3651,7 @@ import Mathlib.Data.Rat.Cardinal
 import Mathlib.Data.Rat.Cast.CharZero
 import Mathlib.Data.Rat.Cast.Defs
 import Mathlib.Data.Rat.Cast.Lemmas
+import Mathlib.Data.Rat.Cast.OfScientific
 import Mathlib.Data.Rat.Cast.Order
 import Mathlib.Data.Rat.Defs
 import Mathlib.Data.Rat.Denumerable
@@ -5384,6 +5386,7 @@ import Mathlib.Probability.Independence.InfinitePi
 import Mathlib.Probability.Independence.Integrable
 import Mathlib.Probability.Independence.Integration
 import Mathlib.Probability.Independence.Kernel
+import Mathlib.Probability.Independence.Process
 import Mathlib.Probability.Independence.ZeroOne
 import Mathlib.Probability.Integration
 import Mathlib.Probability.Kernel.Basic

Mathlib/Algebra/Group/Action/Defs.lean

@@ -584,7 +584,7 @@ class IsLeftCancelSMul [SMul G P] : Prop where
 
 @[to_additive]
 lemma IsLeftCancelSMul.left_cancel {G P} [SMul G P] [IsLeftCancelSMul G P] (a : G) (b c : P) :
-  a • b = a • c → b = c := IsLeftCancelSMul.left_cancel' a b c
+    a • b = a • c → b = c := IsLeftCancelSMul.left_cancel' a b c
 
 @[to_additive]
 instance [LeftCancelMonoid G] : IsLeftCancelSMul G G where
@@ -601,11 +601,11 @@ class IsCancelSMul [SMul G P] : Prop extends IsLeftCancelSMul G P where
 
 @[to_additive]
 lemma IsCancelSMul.left_cancel {G P} [SMul G P] [IsCancelSMul G P] (a : G) (b c : P) :
-  a • b = a • c → b = c := IsLeftCancelSMul.left_cancel' a b c
+    a • b = a • c → b = c := IsLeftCancelSMul.left_cancel' a b c
 
 @[to_additive]
 lemma IsCancelSMul.right_cancel {G P} [SMul G P] [IsCancelSMul G P] (a b : G) (c : P) :
-  a • c = b • c → a = b := IsCancelSMul.right_cancel' a b c
+    a • c = b • c → a = b := IsCancelSMul.right_cancel' a b c
 
 @[to_additive]
 instance [CancelMonoid G] : IsCancelSMul G G where

Mathlib/Algebra/Group/Basic.lean

@@ -15,7 +15,7 @@ import Mathlib.Tactic.SplitIfs
 
 This file lists various basic lemmas about semigroups, monoids, and groups. Most proofs are
 one-liners from the corresponding axioms. For the definitions of semigroups, monoids and groups, see
-`Algebra/Group/Defs.lean`.
+`Mathlib/Algebra/Group/Defs.lean`.
 -/
 
 assert_not_exists MonoidWithZero DenselyOrdered

Mathlib/Algebra/Group/Torsion.lean

@@ -35,19 +35,27 @@ lemma pow_left_injective (hn : n ≠ 0) : Injective fun a : M ↦ a ^ n :=
 @[to_additive nsmul_right_inj]
 lemma pow_left_inj (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b := (pow_left_injective hn).eq_iff
 
-@[to_additive]
-lemma IsMulTorsionFree.pow_eq_one_iff (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 :=
-  ⟨fun h ↦ by rwa [← pow_left_inj hn, one_pow], fun h ↦ by rw [h, one_pow]⟩
+@[to_additive IsAddTorsionFree.nsmul_eq_zero_iff_right]
+lemma IsMulTorsionFree.pow_eq_one_iff_left (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 := by
+  rw [← pow_left_inj (a := a) hn, one_pow]
 
-@[to_additive]
-lemma IsMulTorsionFree.pow_eq_one_iff' (ha : a ≠ 1) : a ^ n = 1 ↔ n = 0 := by
-  refine ⟨fun h ↦ ?_, fun h ↦ by rw [h, pow_zero]⟩
-  by_contra h'
-  simpa [h] using (pow_left_injective h').ne ha
+-- We want to use `IsAddTorsion.nsmul_eq_zero_iff` earlier than `smul_eq_zero`.
+@[to_additive (attr := simp high)]
+lemma IsMulTorsionFree.pow_eq_one_iff : a ^ n = 1 ↔ a = 1 ∨ n = 0 := by
+  obtain rfl | hn := eq_or_ne n 0 <;> simp [pow_eq_one_iff_left, *]
+
+@[to_additive IsAddTorsionFree.nsmul_eq_zero_iff_left]
+lemma IsMulTorsionFree.pow_eq_one_iff_right (ha : a ≠ 1) : a ^ n = 1 ↔ n = 0 := by simp [*]
+
+@[deprecated (since := "2025-10-19")]
+alias IsAddTorsionFree.nsmul_eq_zero_iff' := IsAddTorsionFree.nsmul_eq_zero_iff_left
+
+@[deprecated (since := "2025-10-19")]
+alias IsMulTorsionFree.pow_eq_one_iff' := IsMulTorsionFree.pow_eq_one_iff_right
 
 /-- See `sq_eq_one_iff` for a version that holds in rings. -/
 @[to_additive two_nsmul_eq_zero]
-lemma sq_eq_one : a ^ 2 = 1 ↔ a = 1 := IsMulTorsionFree.pow_eq_one_iff (by cutsat)
+lemma sq_eq_one : a ^ 2 = 1 ↔ a = 1 := IsMulTorsionFree.pow_eq_one_iff_left (by cutsat)
 
 end Monoid
 
@@ -69,6 +77,18 @@ lemma zpow_left_inj (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b := (zpow_left_injec
 and `zsmul_lt_zsmul_iff'`. -/]
 lemma zpow_eq_zpow_iff' (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b := zpow_left_inj hn
 
+@[to_additive IsAddTorsionFree.zsmul_eq_zero_iff_right]
+lemma IsMulTorsionFree.zpow_eq_one_iff_left (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 := by
+  rw [← zpow_left_inj (a := a) hn, one_zpow]
+
+-- We want to use `IsAddTorsion.zsmul_eq_zero_iff` earlier than `smul_eq_zero`.
+@[to_additive (attr := simp high)]
+lemma IsMulTorsionFree.zpow_eq_one_iff : a ^ n = 1 ↔ a = 1 ∨ n = 0 := by
+  obtain rfl | hn := eq_or_ne n 0 <;> simp [zpow_eq_one_iff_left, *]
+
+@[to_additive IsAddTorsionFree.zsmul_eq_zero_iff_left]
+lemma IsMulTorsionFree.zpow_eq_one_iff_right (ha : a ≠ 1) : a ^ n = 1 ↔ n = 0 := by simp [*]
+
 @[to_additive] lemma self_eq_inv : a = a⁻¹ ↔ a = 1 := by rw [← sq_eq_one, sq, mul_eq_one_iff_eq_inv]
 @[to_additive] lemma inv_eq_self : a⁻¹ = a ↔ a = 1 := by rw [eq_comm, self_eq_inv]
 @[to_additive] lemma self_ne_inv : a ≠ a⁻¹ ↔ a ≠ 1 := self_eq_inv.ne

Mathlib/Algebra/GroupWithZero/Torsion.lean

@@ -37,7 +37,7 @@ instance : IsMulTorsionFree M := by
       ← associated_iff_normalizedFactors_eq_normalizedFactors hx hy] at this
   replace hx : IsLeftRegular (x ^ n) := (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero hx).pow n
   rw [← hu, mul_pow, eq_comm, IsLeftRegular.mul_left_eq_self_iff hx, ← Units.val_pow_eq_pow_val,
-    Units.val_eq_one, IsMulTorsionFree.pow_eq_one_iff hn] at hxy
+    Units.val_eq_one, IsMulTorsionFree.pow_eq_one_iff_left hn] at hxy
   rwa [hxy, Units.val_one, mul_one] at hu
 
 end UniqueFactorizationMonoid

Mathlib/Algebra/Lie/Abelian.lean

@@ -64,7 +64,7 @@ theorem Function.Injective.isLieAbelian {R : Type u} {L₁ : Type v} {L₂ : Typ
       calc
         f ⁅x, y⁆ = ⁅f x, f y⁆ := LieHom.map_lie f x y
         _ = 0 := trivial_lie_zero _ _ _ _
-        _ = f 0 := f.toLinearMap.map_zero.symm}
+        _ = f 0 := (map_zero _).symm}
 
 theorem Function.Surjective.isLieAbelian {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R]
     [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] {f : L₁ →ₗ⁅R⁆ L₂}

Mathlib/Algebra/Lie/Basic.lean

@@ -568,9 +568,9 @@ theorem coe_injective : @Injective (L₁ ≃ₗ⁅R⁆ L₂) (L₁ → L₂) (
 
 instance : LinearEquivClass (L₁ ≃ₗ⁅R⁆ L₂) R L₁ L₂ where
   map_add _ _ _ := by
-    rw [← @coe_toLinearEquiv, map_add]
+    rw [← coe_toLinearEquiv, map_add]
   map_smulₛₗ _ _ _ := by
-    rw [← @coe_toLinearEquiv, map_smul, RingHom.id_apply]
+    rw [← coe_toLinearEquiv, map_smul, RingHom.id_apply]
 
 @[ext]
 theorem ext {f g : L₁ ≃ₗ⁅R⁆ L₂} (h : ∀ x, f x = g x) : f = g :=

Mathlib/Algebra/Lie/Character.lean

@@ -48,11 +48,14 @@ theorem lieCharacter_apply_of_mem_derived (χ : LieCharacter R L) {x : L}
     (h : x ∈ derivedSeries R L 1) : χ x = 0 := by
   rw [derivedSeries_def, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_zero, ←
     LieSubmodule.mem_toSubmodule, LieSubmodule.lieIdeal_oper_eq_linear_span] at h
-  refine Submodule.span_induction ?_ ?_ ?_ ?_ h
-  · rintro y ⟨⟨z, hz⟩, ⟨⟨w, hw⟩, rfl⟩⟩; apply lieCharacter_apply_lie
-  · exact χ.toLinearMap.map_zero
-  · intro y z _ _ hy hz; rw [map_add, hy, hz, add_zero]
-  · intro t y _ hy; rw [map_smul, hy, smul_zero]
+  induction h using Submodule.span_induction with
+  | mem y h =>
+    simp only [Subtype.exists, LieSubmodule.mem_top, exists_const, Set.mem_setOf_eq] at h
+    obtain ⟨z, w, rfl⟩ := h
+    exact lieCharacter_apply_lie ..
+  | zero => exact map_zero _
+  | add y z _ _ hy hz => rw [map_add, hy, hz, add_zero]
+  | smul t y _ hy => rw [map_smul, hy, smul_zero]
 
 /-- For an Abelian Lie algebra, characters are just linear forms. -/
 @[simps! apply symm_apply]

Mathlib/Algebra/Lie/Weights/IsSimple.lean

@@ -211,7 +211,7 @@ private theorem invtSubmoduleToLieIdeal_aux (hm_α : m_α ∈ sl2SubmoduleOfRoot
   · have hx_χ_in_H : x_χ ∈ H.toLieSubmodule := by
       rw [← rootSpace_zero_eq K L H]
       convert hx_χ; ext h; simp only [Pi.zero_apply]
-      have h_apply : (χ.toLinear : H → K) h = 0 := by rw [w_chi]; rfl
+      have h_apply : (χ.toLinear : H → K) h = 0 := by rw [w_chi, LinearMap.zero_apply]
       exact h_apply.symm
     apply LieSubmodule.mem_iSup_of_mem ⟨α, hαq, hα₀⟩
     rw [← (by rfl : ⁅(⟨x_χ, hx_χ_in_H⟩ : H), m_α⁆ = ⁅x_χ, m_α⁆)]