chore: bump mathlib to v4.22.0 (#696)

Co-authored-by: Kevin Buzzard <[email protected]>

Author: Ruben-VandeVelde

FLT.lean

@@ -54,8 +54,6 @@ import FLT.Mathlib.Algebra.IsQuaternionAlgebra
 import FLT.Mathlib.Algebra.Module.LinearMap.Defs
 import FLT.Mathlib.Algebra.Module.Submodule.Basic
 import FLT.Mathlib.Algebra.Order.AbsoluteValue.Basic
-import FLT.Mathlib.Algebra.Order.GroupWithZero
-import FLT.Mathlib.Algebra.Order.GroupWithZero.Canonical
 import FLT.Mathlib.Analysis.Normed.Ring.WithAbs
 import FLT.Mathlib.Analysis.SpecialFunctions.Stirling
 import FLT.Mathlib.Data.Fin.Basic

FLT/AutomorphicRepresentation/Example.lean

@@ -262,10 +262,10 @@ lemma multiples (N : ℕ+) (z : ZHat) : (∃ (y : ZHat), N * y = z) ↔ z N = 0
         rw [h, ZMod.castHom_apply, ZMod.cast_eq_val, ZMod.natCast_eq_zero_iff] at hk
         have hNjk := z.prop (N * j) (N * k) (mul_dvd_mul (dvd_refl _) hjk)
         rw [ZMod.castHom_apply, ZMod.cast_eq_val] at hNjk
-        simp only [PNat.mul_coe, map_natCast, ZMod.eq_iff_modEq_nat]
+        simp only [PNat.mul_coe, map_natCast, ZMod.natCast_eq_natCast_iff]
         apply Nat.ModEq.mul_right_cancel' (c := N) (by simp)
         rw [Nat.div_mul_cancel hj, Nat.div_mul_cancel hk,
-          mul_comm (j : ℕ) (N : ℕ), ← ZMod.eq_iff_modEq_nat, hNjk]
+          mul_comm (j : ℕ) (N : ℕ), ← ZMod.natCast_eq_natCast_iff, hNjk]
         simp
     }
     refine ⟨y, ?_⟩

FLT/DedekindDomain/AdicValuation.lean

@@ -6,7 +6,7 @@ Authors: Matthew Jasper
 import FLT.Mathlib.Topology.Algebra.Valued.ValuationTopology
 import FLT.Mathlib.RingTheory.Valuation.ValuationSubring
 import FLT.Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
-import FLT.Mathlib.Algebra.Order.GroupWithZero
+import Mathlib.Algebra.Order.GroupWithZero.Canonical
 import Mathlib.RingTheory.DedekindDomain.AdicValuation
 import Mathlib.Algebra.Group.Int.TypeTags
 import Mathlib.NumberTheory.RamificationInertia.Basic

FLT/Deformations/RepresentationTheory/AbsoluteGaloisGroup.lean

@@ -278,7 +278,7 @@ instance neZero_maximalIdeal_integralClosure :
     NeZero (𝔪 (IntegralClosure 𝒪ᵥ (Kᵥᵃˡᵍ))) := by
   have : 𝒪ᵥ ≠ ⊤ := by
     refine fun h ↦ IsDiscreteValuationRing.not_isField 𝒪ᵥ (h ▸ ?_)
-    exact (Subring.topEquiv (R := Kᵥ)).isField _ (Semifield.toIsField Kᵥ)
+    exact (Subring.topEquiv (R := Kᵥ)).isField (Semifield.toIsField Kᵥ)
   exact ⟨(Ideal.bot_lt_of_maximal (𝔪 _)
     (not_isField_integralClosure (L := Kᵥᵃˡᵍ) _ this)).ne'⟩
 

FLT/Deformations/RepresentationTheory/Basic.lean

@@ -271,11 +271,9 @@ lemma Matrix.map_det {F α β n : Type*} [CommRing β] [CommRing α] [Fintype n]
     (M.map f).det = f M.det :=
   (RingHom.map_det (f : α →+* β) M).symm
 
-@[simp]
 lemma LinearMap.trace_toLin' {R n : Type*} [CommSemiring R] [DecidableEq n]
     [Fintype n] (M : Matrix n n R) : LinearMap.trace _ _ M.toLin' = M.trace := by
-  rw [LinearMap.trace_eq_matrix_trace _ (Pi.basisFun ..), LinearMap.toMatrix_eq_toMatrix',
-      LinearMap.toMatrix'_toLin']
+  simp
 
 omit [NumberField K] in
 lemma FramedGaloisRep.det_baseChange [IsTopologicalRing B]

FLT/HaarMeasure/HaarChar/AddEquiv.lean

@@ -41,8 +41,9 @@ variable [BorelSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G]
 
 /-- If `φ : G ≃ₜ* G` then `mulEquivHaarChar φ` is the positive real factor by which
 `φ` scales Haar measure on `G`. -/
-@[to_additive "If `φ : A ≃ₜ+ A` then `addEquivAddHaarChar φ` is the positive
-real factor by which `φ` scales Haar measure on `A`."]
+@[to_additive
+/-- If `φ : A ≃ₜ+ A` then `addEquivAddHaarChar φ` is the positive real factor by which
+`φ` scales Haar measure on `A`. -/]
 noncomputable def mulEquivHaarChar (φ : G ≃ₜ* G) : ℝ≥0 :=
   haarScalarFactor haar (map φ haar)
 
@@ -240,8 +241,9 @@ lemma mulEquivHaarChar_eq_mulEquivHaarChar_of_isOpenEmbedding {X Y : Type*}
 
 /-- A version of `mulEquivHaarChar_eq_mulEquivHaarChar_of_isOpenEmbedding` with the stronger
 assumption that `f` is a `ContinuousMulEquiv`, for convenience. -/
-@[to_additive "A version of `addEquivAddHaarChar_eq_addEquivAddHaarChar_of_isOpenEmbedding`
-with the stronger assumption that `f` is a `ContinuousAddEquiv`, for convenience."]
+@[to_additive
+/-- A version of `addEquivAddHaarChar_eq_addEquivAddHaarChar_of_isOpenEmbedding` with the stronger
+assumption that `f` is a `ContinuousAddEquiv`, for convenience. -/]
 lemma mulEquivHaarChar_eq_mulEquivHaarChar_of_continuousMulEquiv {X Y : Type*}
     [TopologicalSpace X] [Group X] [IsTopologicalGroup X] [LocallyCompactSpace X]
     [MeasurableSpace X] [BorelSpace X]
@@ -260,8 +262,9 @@ variable {A B C D : Type*} [Group A] [Group B] [Group C] [Group D]
 
 /-- The product of two multiplication-preserving homeomorphisms is
 a multiplication-preserving homeomorphism. -/
-@[to_additive "The product of
-two addition-preserving homeomorphisms is an addition-preserving homeomorphism."]
+@[to_additive
+/-- The product of two addition-preserving homeomorphisms is
+an addition-preserving homeomorphism. -/]
 def _root_.ContinuousMulEquiv.prodCongr (φ : A ≃ₜ* B) (ψ : C ≃ₜ* D) : A × C ≃ₜ* B × D where
   __ := φ.toMulEquiv.prodCongr ψ
   continuous_toFun := Continuous.prodMap φ.continuous_toFun ψ.continuous_toFun
@@ -388,8 +391,9 @@ variable {ι : Type*} {G H : ι → Type*}
 /-- An arbitrary product of multiplication-preserving homeomorphisms
 is a multiplication-preserving homeomorphism.
 -/
-@[to_additive "An arbitrary product of
-addition-preserving homeomorphisms is an addition-preserving homeomorphism."]
+@[to_additive
+/-- An arbitrary product of addition-preserving homeomorphisms
+is an addition-preserving homeomorphism. -/]
 def _root_.ContinuousMulEquiv.piCongrRight (ψ : Π i, (G i) ≃ₜ* (H i)) :
     (∀ i, G i) ≃ₜ* (∀ i, H i) where
   __ := MulEquiv.piCongrRight (fun i ↦ ψ i)

FLT/Mathlib/Algebra/Order/GroupWithZero.lean

@@ -21,8 +21,8 @@ def ContinuousAddEquiv.quotientPi {ι : Type*} {G : ι → Type*} [(i : ι) →
 /-- A family indexed by a type with a unique element
 is `ContinuousMulEquiv` to the element at the single index. -/
 @[to_additive
-  "A family indexed by a type with a unique element
-  is `ContinuousAddEquiv` to the element at the single index."]
+/-- A family indexed by a type with a unique element
+is `ContinuousAddEquiv` to the element at the single index. -/]
 def ContinuousMulEquiv.piUnique {ι : Type*} (M : ι → Type*) [(j : ι) → Mul (M j)]
     [(j : ι) → TopologicalSpace (M j)] [Unique ι] :
     ((j : ι) → M j) ≃ₜ* M default where
@@ -33,8 +33,8 @@ def ContinuousMulEquiv.piUnique {ι : Type*} (M : ι → Type*) [(j : ι) → Mu
 /-- Splits the indices of `∀ (i : ι), Y i` along the predicate `p`.
 This is `Equiv.piEquivPiSubtypeProd` as a `ContinuousMulEquiv`. -/
 @[to_additive piEquivPiSubtypeProd
-  "Splits the indices of `∀ (i : ι), Y i` along the predicate `p`.
-  This is `Equiv.piEquivPiSubtypeProd` as a `ContinuousAddEquiv`."]
+/-- Splits the indices of `∀ (i : ι), Y i` along the predicate `p`.
+This is `Equiv.piEquivPiSubtypeProd` as a `ContinuousAddEquiv`. -/]
 def ContinuousMulEquiv.piEquivPiSubtypeProd {ι : Type*} (p : ι → Prop) (Y : ι → Type*)
     [(i : ι) → TopologicalSpace (Y i)] [(i : ι) → Mul (Y i)] [DecidablePred p] :
     ((i : ι) → Y i) ≃ₜ* ((i : { x : ι // p x }) → Y i) × ((i : { x : ι // ¬p x }) → Y i) :=

FLT/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

@@ -66,8 +66,9 @@ variable [Π i, Monoid (G i)] [Π i, SubmonoidClass (S i) (G i)]
     [Π i, Monoid (H i)] [Π i, SubmonoidClass (T i) (H i)] in
 /-- The monoid homomorphism between restricted products over a fixed index type,
 given monoid homomorphisms on the factors. -/
-@[to_additive "The additive monoid homomorphism between restricted products over a fixed index type,
-given additive monoid homomorphisms on the factors."]
+@[to_additive
+/-- The additive monoid homomorphism between restricted products over a fixed index type,
+given additive monoid homomorphisms on the factors. -/]
 def MonoidHom.restrictedProductCongrRight (φ : (i : ι) → G i →* H i)
     (hφ : ∀ᶠ i in ℱ, Set.MapsTo (φ i) (A i) (B i)) :
     Πʳ i, [G i, A i]_[ℱ] →* Πʳ i, [H i, B i]_[ℱ] where
@@ -109,8 +110,9 @@ variable [(i : ι) → One (G i)] in
 /-- The support of an element of a restricted product of monoids (or more generally,
 objects with a 1. The support is the components which aren't 1.)
 -/
-@[to_additive "The support of an element of a restricted product of additive monoids
-(or more generally, objects with a 0. The support is the components which aren't 0."]
+@[to_additive
+/-- The support of an element of a restricted product of additive monoids (or more generally,
+objects with a 0. The support is the components which aren't 0. -/]
 def mulSupport (u : Πʳ i, [G i, A i]) : Set ι :=
   {i : ι | u i ≠ 1}
 
@@ -328,7 +330,8 @@ variable (A : (i : ι) → (S i))
 variable [DecidableEq ι]
 
 /-- The function supported at `i`, with value `x` there, and `1` elsewhere. -/
-@[to_additive "The function supported at `i`, with value `x` there, and `0` elsewhere."]
+@[to_additive
+/-- The function supported at `i`, with value `x` there, and `0` elsewhere. -/]
 def mulSingle [∀ i, One (G i)] [∀ i, OneMemClass (S i) (G i)] (i : ι) (x : G i) :
     Πʳ i, [G i, A i] where
   val := Pi.mulSingle i x