Merge pull request #118 from Ruben-VandeVelde/bump

Bump mathlib

Author: kbuzzard

FLT/AutomorphicForm/QuaternionAlgebra.lean

@@ -40,11 +40,11 @@ instance : Algebra A (D ⊗[R] A) :=
     simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, Algebra.TensorProduct.includeRight_apply]
     intro a b
     apply TensorProduct.induction_on (motive := fun b ↦ 1 ⊗ₜ[R] a * b = b * 1 ⊗ₜ[R] a)
-    . simp only [mul_zero, zero_mul]
-    . intro d a'
+    · simp only [mul_zero, zero_mul]
+    · intro d a'
       simp only [Algebra.TensorProduct.tmul_mul_tmul, one_mul, mul_one]
       rw [NonUnitalCommSemiring.mul_comm]
-    . intro x y hx hy
+    · intro x y hx hy
       rw [left_distrib, hx, hy, right_distrib]
     )
 
@@ -205,6 +205,6 @@ lemma sMul_eval (g : Dfx F D) (f : AutomorphicForm F D M) (x : (D ⊗[F] FiniteA
   (g • f) x = f (x * g) := rfl
 
 instance : MulAction (Dfx F D) (AutomorphicForm F D M) where
-  smul := (. • .)
+  smul := (· • ·)
   one_smul := by intros; ext; simp only [sMul_eval, mul_one]
   mul_smul := by intros; ext; simp only [sMul_eval, mul_assoc]

FLT/AutomorphicRepresentation/Example.lean

@@ -54,9 +54,6 @@ lemma ext (x y : ZHat) (h : ∀ n : ℕ+, x n = y n) : x = y := by
   ext n
   apply h
 
-lemma ext_iff (x y : ZHat) : (∀ n : ℕ+, x n = y n) ↔ x = y :=
-  ⟨ext x y, fun h n => by exact congrFun (congrArg DFunLike.coe h) n⟩
-
 @[simp] lemma zero_val (n : ℕ+) : (0 : ZHat) n = 0 := rfl
 @[simp] lemma one_val (n : ℕ+) : (1 : ZHat) n = 1 := rfl
 @[simp] lemma ofNat_val (m : ℕ) [m.AtLeastTwo] (n : ℕ+) :
@@ -75,7 +72,7 @@ lemma zeroNeOne : (0 : ZHat) ≠ 1 := by
 instance nontrivial : Nontrivial ZHat := ⟨0, 1, zeroNeOne⟩
 
 instance charZero : CharZero ZHat := ⟨ fun a b h ↦ by
-  rw [← ext_iff] at h
+  rw [ZHat.ext_iff] at h
   specialize h ⟨_, (max a b).succ_pos⟩
   apply_fun ZMod.val at h
   rwa [natCast_val, ZMod.val_cast_of_lt, natCast_val, ZMod.val_cast_of_lt] at h
@@ -200,8 +197,7 @@ lemma torsionfree (N : ℕ+) : Function.Injective (fun z : ZHat ↦ N * z) := by
   rw [← AddMonoidHom.coe_mulLeft, injective_iff_map_eq_zero]
   intro a ha
   rw [AddMonoidHom.coe_mulLeft] at ha
-  rw [← ext_iff]
-  intro j
+  ext j
   rw [zero_val, ← a.prop j (N * j) (by simp)]
   apply torsionfree_aux
   apply Nat.dvd_of_mul_dvd_mul_left N.pos
@@ -824,7 +820,8 @@ lemma exists_near (a : ℍ) : ∃ q : 𝓞, dist a (toQuaternion q) < 1 := by
     rw [add_eq_zero_iff' (by positivity) (by positivity)]
     rw [add_eq_zero_iff' (by positivity) (by positivity)]
     rw [add_eq_zero_iff' (by positivity) (by positivity)]
-    simp_rw [and_assoc, sq_eq_zero_iff, sub_re, sub_imI, sub_imJ, sub_imK, sub_eq_zero, ← ext_iff]
+    simp_rw [and_assoc, sq_eq_zero_iff, sub_re, sub_imI, sub_imJ, sub_imK, sub_eq_zero,
+      ← Quaternion.ext_iff]
     symm
     apply leftInvOn_toQuaternion_fromQuaternion
     · simp only [Set.mem_setOf]

FLT/GlobalLanglandsConjectures/GLnDefs.lean

@@ -77,9 +77,10 @@ open scoped nonZeroDivisors
 noncomputable instance : Algebra R (FiniteAdeleRing R K) :=
   RingHom.toAlgebra ((algebraMap K (FiniteAdeleRing R K)).comp (algebraMap R K))
 
+@[deprecated mul_nonZeroDivisor_mem_finiteIntegralAdeles]
 lemma FiniteAdeleRing.clear_denominator (a : FiniteAdeleRing R K) :
     ∃ (b : R⁰) (c : R_hat R K), a * (b : R) = c := by
-  sorry -- there's a nearly-done mathlib PR which proves this
+  exact mul_nonZeroDivisor_mem_finiteIntegralAdeles a
 
 #check Classical.choose (v.valuation_exists_uniformizer K)
 
@@ -313,6 +314,7 @@ def annihilator {R} [CommSemiring R]
     (a : M) : Submodule R (M →ₗ[R] N) :=
   Submodule.compatibleMaps (Submodule.span R {a}) ⊥
 
+set_option synthInstance.maxHeartbeats 40000 in
 /-- Automorphic forms for GL_n/Q with weight ρ. -/
 structure AutomorphicFormForGLnOverQ (n : ℕ) (ρ : Weight n) where
   toFun : GL (Fin n) (FiniteAdeleRing ℤ ℚ) × GL (Fin n) ℝ → ℂ

FLT/GlobalLanglandsConjectures/GLzero.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard, Jonas Bayer
 -/
 import Mathlib.RingTheory.DedekindDomain.Ideal
-import Mathlib.RingTheory.IntegralRestrict
+import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 import Mathlib.RingTheory.Ideal.QuotientOperations
 import Mathlib.FieldTheory.Cardinality
 import FLT.GlobalLanglandsConjectures.GLnDefs

FLT/HIMExperiments/module_topology.lean

@@ -179,13 +179,13 @@ lemma LinearMap.continuous_on_prod (f : (M × N) →ₗ[A] A) :
   suffices Continuous fun (⟨m, n⟩ : M × N) ↦ f (⟨m, 0⟩) + f (⟨0, n⟩) by
     simpa [← LinearMap.map_add, Prod.mk_add_mk, add_zero, zero_add]
   apply Continuous.add
-  . refine Continuous.fst' (?_ : Continuous fun m ↦ f (m, 0))
+  · refine Continuous.fst' (?_ : Continuous fun m ↦ f (m, 0))
     exact Module.continuous_linear_to_ring A
       ({toFun := fun m ↦ f (m, 0),
         map_add' := by {intro x y; rw [← LinearMap.map_add, Prod.mk_add_mk, zero_add]},
         map_smul' := by intro m x; rw [←LinearMap.map_smul,
           RingHom.id_apply, Prod.smul_mk, smul_zero]})
-  . apply @Continuous.snd' _ _ _ _ _ _ (fun n ↦ f (0, n))
+  · apply @Continuous.snd' _ _ _ _ _ _ (fun n ↦ f (0, n))
     exact Module.continuous_linear_to_ring A
       ({toFun := fun n ↦ f (0, n),
         map_add' := by {intro x y; rw [← LinearMap.map_add, Prod.mk_add_mk, add_zero]},

FLT/mathlibExperiments/Coalgebra/Monoid.lean

@@ -210,7 +210,7 @@ lemma comp_one {A' : Type*} [CommSemiring A'] [Bialgebra R A']
     (f : AlgHomPoint R A' L) :
     f.comp (1 : AlgHomPoint R A' A') = 1 := by
   ext
-  simp [one_def, Algebra.ofId_apply, Algebra.algebraMap_eq_smul_one, f.map_smul, f.map_one]
+  simp [one_def, Algebra.ofId_apply, Algebra.algebraMap_eq_smul_one, map_smul, _root_.map_one]
 
 end commutative_bialgebra
 

FLT/mathlibExperiments/Frobenius.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jou Glasheen
 -/
 import Mathlib.RingTheory.DedekindDomain.Ideal
-import Mathlib.RingTheory.IntegralRestrict
+import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 import Mathlib.RingTheory.Ideal.QuotientOperations
 import Mathlib.FieldTheory.Cardinality
 
@@ -49,7 +49,7 @@ In this file, I :
 ## Notation
 
 Note that, to define the `MulAction` of `L ≃ₐ[K] L` on the prime ideals of `𝓞 L : = B`,
-we used the restriction map `galRestrict`, defined in the file Mathlib.RingTheory.IntegralRestrict.
+we used the restriction map `galRestrict`, defined in the file Mathlib.RingTheory.IntegralClosure.IntegralRestrict.
 The definition of `galRestrict` is in terms of an 'AKLB setup'; i.e., where
 "`A` is an integrally closed domain; `K` is the fraction ring of `A`; `L` is
 a finite (separable) extension of `K`; `B` is the integral closure of
@@ -258,7 +258,7 @@ lemma crt_representative (b : B) : ∃ (y : B),
       apply Ideal.prime_of_isPrime (h := MapPrimestoPrimes A K L B i Q)
       contrapose! Q_ne_bot
       -- goal: (Q_ne_bot : i • Q = ⊥) → Q = ⊥
-      apply_fun (i⁻¹ • .) at Q_ne_bot -- that's the hint it needs
+      apply_fun (i⁻¹ • ·) at Q_ne_bot -- that's the hint it needs
       simpa using Q_ne_bot
     )
     (fun i _ j _ hij ↦ by

FLT/mathlibExperiments/Frobenius2.lean

@@ -7,7 +7,7 @@ import Mathlib.FieldTheory.Cardinality
 import Mathlib.RingTheory.DedekindDomain.Ideal
 import Mathlib.RingTheory.Ideal.Pointwise
 import Mathlib.RingTheory.Ideal.QuotientOperations
-import Mathlib.RingTheory.IntegralRestrict
+import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 
 /-
 

FLT/mathlibExperiments/HopfAlgebra/Basic.lean

@@ -141,7 +141,7 @@ noncomputable instance instGroup : Group (AlgHomPoint R A L) where
   inv f := f.comp antipodeAlgHom
   mul_left_inv f := AlgHom.ext fun x ↦ by
     simp only [AlgHomPoint.mul_repr (repr := Coalgebra.comul_repr x), AlgHom.comp_apply,
-      antipodeAlgHom_apply, ← f.map_mul, ← map_sum, f.commutes, Algebra.ofId_apply,
+      antipodeAlgHom_apply, ← _root_.map_mul, ← map_sum, f.commutes, Algebra.ofId_apply,
       antipode_repr (repr := Coalgebra.comul_repr x), AlgHomPoint.one_def,
       Bialgebra.counitAlgHom_apply]
 

FLT/mathlibExperiments/IsFrobenius.lean

@@ -6,7 +6,7 @@ Authors: Ivan Farabella, Amelia Livingston, Jujian Zhang, Kevin Buzzard
 import Mathlib.Tactic
 import Mathlib.NumberTheory.NumberField.Basic
 import Mathlib.NumberTheory.NumberField.Discriminant
-import Mathlib.RingTheory.IntegralRestrict
+import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 import Mathlib.RingTheory.Ideal.QuotientOperations
 import Mathlib.NumberTheory.RamificationInertia
 

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "937cd3219c0beffa7b623d2905707d1304da259e",
+   "rev": "dc167d260ff7ee9849b436037add06bed15104be",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
+   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
+   "rev": "0444234b4216e944d5be2ce42a25d7410c67876f",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,27 +35,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
+   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.39",
+   "inputRev": "v0.0.41",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
+   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "90ef20a210ecd605e8036b280b6b85b9043b5447",
+   "rev": "3dd071bc2260b3cf9a71863d0dee1242fec41522",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9148a0a7506099963925cf239c491fcda5ed0044",
+   "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f93115d0209de6db335725dee900d379f40c0317",
+   "rev": "5c11428272fe190b7e726ebe448f93437d057b74",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -115,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04",
+   "rev": "6d8e3118ab526f8dfcabcbdf9f05dc34e5c423a8",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.10.0-rc2
+leanprover/lean4:v4.11.0-rc1