chore: bump mathlib (#759)

Also, change `lakefile.toml` to point to the master branch of mathlib.

Author: kbuzzard

FLT/Data/QHat.lean

@@ -690,7 +690,7 @@ lemma unitsrat_join_unitszHat : unitsratsub ⊔ unitszHatsub = ⊤ := by
     have h : (M : QHat) = (M : ℚ) ⊗ₜ[ℤ] 1 := by norm_cast
     rw [Algebra.TensorProduct.includeRight_apply, hxinv, h, Algebra.TensorProduct.tmul_mul_tmul,
       mul_one, one_div, inv_mul_cancel₀]
-    simp only [ne_eq, Rat.natCast_eq_zero, PNat.ne_zero, not_false_eq_true]
+    simp only [ne_eq, Rat.natCast_eq_zero_iff, PNat.ne_zero, not_false_eq_true]
   rcases hx with ⟨X, hX⟩
   let I := Ideal.span {X}
   let J := I.comap (Int.castRingHom ZHat)
@@ -729,7 +729,7 @@ lemma unitsrat_join_unitszHat : unitsratsub ⊔ unitszHatsub = ⊤ := by
     set G : ℚ := 1 / g with G_def
     have gG : g * G = 1 := by
       rw [G_def, one_div, mul_inv_cancel₀]
-      simp only [ne_eq, Rat.intCast_eq_zero, Int.ne_of_gt gpos, not_false_eq_true]
+      simp only [ne_eq, Rat.intCast_eq_zero_iff, Int.ne_of_gt gpos, not_false_eq_true]
     use ⟨g, G, gG, mul_comm _ G ▸ gG⟩
     use ⟨z, y, by rw[mul_comm]; exact this, this⟩
     simp only [← Units.val_inj, ← hX, Units.map_mk, MonoidHom.coe_coe, map_intCast,

FLT/DedekindDomain/AdicValuation.lean

@@ -89,8 +89,8 @@ lemma emultiplicity_eq_of_valuation_eq_ofAdd {a : A} {k : ℕ}
   have hnz : a ≠ 0 := ne_zero_of_some_le_intValuation _ (le_of_eq hv.symm)
   have hnb : Ideal.span {a} ≠ ⊥ := by
     rwa [ne_eq, Ideal.span_singleton_eq_bot]
-  simp only [intValuation_if_neg _ hnz, ofAdd_neg, WithZero.coe_inv, inv_inj, WithZero.coe_inj,
-    EmbeddingLike.apply_eq_iff_eq, Nat.cast_inj] at hv
+  simp only [intValuation_if_neg _ hnz, WithZero.exp, ofAdd_neg, WithZero.coe_inv, inv_inj,
+    WithZero.coe_inj, EmbeddingLike.apply_eq_iff_eq, Nat.cast_inj] at hv
   rw [← hv, UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors v.irreducible hnb,
     count_associates_factors_eq hnb v.isPrime v.ne_bot, normalize_eq]
 
@@ -117,7 +117,7 @@ lemma exists_adicValued_mul_sub_le {a b : A} {γ : WithZero (Multiplicative ℤ)
       (emultiplicity_eq_of_valuation_eq_ofAdd v <| intValuation_eq_coe_neg_multiplicity v hnz)
       (ENat.coe_le_coe.mpr hle)
   have hb : b ∈ v.asIdeal ^ multiplicity v.asIdeal (Ideal.span {a}) := by
-    rwa [← intValuation_le_pow_iff_mem, ← intValuation_eq_coe_neg_multiplicity _ hnz]
+    rwa [← intValuation_le_pow_iff_mem, WithZero.exp, ← intValuation_eq_coe_neg_multiplicity _ hnz]
   -- Now make use of
   -- `v.asIdeal ^ multiplicity v.asIdeal (Ideal.span {a}) = v.asIdeal ^ n ⊔ Ideal.span {a}`
   -- (this is where we need `IsDedekindDomain A`)
@@ -127,7 +127,7 @@ lemma exists_adicValued_mul_sub_le {a b : A} {γ : WithZero (Multiplicative ℤ)
   obtain ⟨y, hy⟩ := Ideal.mem_span_singleton'.mp hz
   use y
   -- And again prove the result about valuations by turning into one about ideals.
-  rwa [hy, ← hxz, sub_add_cancel_right, intValuation_le_pow_iff_mem, neg_mem_iff]
+  rwa [hy, ← hxz, sub_add_cancel_right, ← WithZero.exp, intValuation_le_pow_iff_mem, neg_mem_iff]
 
 lemma exists_adicValued_sub_lt_of_adicValued_le_one {x : (WithVal (v.valuation K))}
     (γ : (WithZero (Multiplicative ℤ))ˣ) (hx : Valued.v x ≤ 1) :
@@ -432,7 +432,7 @@ theorem exists_uniformizer (v : HeightOneSpectrum A) :
     ∃ π : v.adicCompletionIntegers K, Valued.v π.1 = Multiplicative.ofAdd (- 1 : ℤ) := by
   obtain ⟨π, hπ⟩ := v.intValuation_exists_uniformizer
   use π
-  rw [← hπ, ← ValuationSubring.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
+  rw [← WithZero.exp, ← hπ, ← ValuationSubring.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
     v.valuedAdicCompletion_eq_valuation, v.valuation_of_algebraMap]
 
 variable {K} in

FLT/DedekindDomain/IntegralClosure.lean

@@ -109,7 +109,7 @@ lemma intValuation_comap (hAB : Function.Injective (algebraMap A B))
   simp only [intValuation, Valuation.coe_mk, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]
   change (ite _ _ _) ^ _ = ite _ _ _
   rw [map_eq_zero_iff _ hAB, if_neg hx, if_neg hx, ← Set.image_singleton, ← Ideal.map_span,
-    mk_count_factors_map _ _ hAB, mul_comm]
+    mk_count_factors_map _ _ hAB, mul_comm, WithZero.exp, WithZero.exp]
   simp
 
 omit [IsIntegralClosure B A L] in

FLT/Deformations/Lemmas.lean

@@ -81,7 +81,7 @@ instance IsTopologicalGroup.discreteUniformity
     {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DiscreteTopology G] :
     letI := IsTopologicalGroup.toUniformSpace G
     DiscreteUniformity G := by
-  simp only [discreteUniformity_iff_idRel_mem_uniformity]
+  simp only [discreteUniformity_iff_relId_mem_uniformity]
   exact ⟨{1}, by simp [Set.subset_def, div_eq_one]⟩
 
 lemma IsLocalRing.map_maximalIdeal {R S} [CommRing R] [CommRing S]

FLT/Mathlib/Algebra/Algebra/Hom.lean

@@ -81,8 +81,3 @@ theorem SemialgHom.algebraMap_apply {A B : Type*} [CommSemiring A] [CommSemiring
     algebraMap A B a = f a := rfl
 
 end semialghom
-
-@[simp]
-theorem AlgHom.coe_toLinearMap {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B]
-    [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
-    ⇑(f : A →ₗ[R] B) = ⇑f := rfl

FLT/Mathlib/Topology/Algebra/Valued/WithZeroMulInt.lean

@@ -114,11 +114,11 @@ theorem finite_cover_of_uniformity_basis [IsDiscreteValuationRing 𝒪[K]] {γ :
   let ⟨m, hm⟩ := exists_pow_lt_of_le_neg_one (irreducible_valuation_le_ofAdd_neg_one hϖ) γ
   letI := finite_quotient_maximalIdeal_pow_of_finite_residueField h m
   have h := Fintype.ofFinite (𝒪[K] ⧸ 𝓂[K] ^ m)
-  let T := Subtype.val '' (h.elems.image Quotient.out).toSet
+  let T := Subtype.val '' (h.elems.image Quotient.out : Set 𝒪[K])
   refine ⟨T, (Set.Finite.image _ (Finset.finite_toSet _)), fun x hx => ?_⟩
   simp only [Set.mem_iUnion]
   let y := (Ideal.Quotient.mk (𝓂[K] ^ m) ⟨x, hx⟩).out
-  refine ⟨y, Set.mem_image_of_mem _ <| Finset.mem_image_of_mem _ (h.complete _),
+  refine ⟨y, Set.mem_image_of_mem _ <| Finset.mem_image_of_mem Quotient.out (h.complete _),
     lt_of_le_of_lt (mem_maximalIdeal_pow_valuation (Ideal.Quotient.out_sub _ _) hϖ) hm⟩
 
 variable (K)

FLT/NumberField/AdeleRing.lean

@@ -480,7 +480,7 @@ theorem Rat.AdeleRing.cocompact :
         simpa using HeightOneSpectrum.coe_algebraMap_mem (𝓞 ℚ) ℚ v xi
     refine ⟨b, hb, ?_⟩
     unfold b; unfold a
-    simp [c]
+    simp [-algebraMap.coe_inj, c]
   { isCompact_univ := h_W_image ▸ IsCompact.image h_W_compact continuous_quot_mk }
 
 variable (K L : Type*) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L]

lake-manifest.json

@@ -15,17 +15,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "da2fd30c91aa177fc00c364d00e2c55334a5b32b",
+   "rev": "9003b8fbd74a577536c5e79a21854807a31a793d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.25.0-rc1",
+   "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7607162f5a1c1eb23c23027629a418b3a160670e",
+   "rev": "8864a73bf79aad549e34eff972c606343935106d",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e5c37730d22634ee0169c164f25dac49918ed951",
+   "rev": "451499ea6e97cee4c8979b507a9af5581a849161",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cbe864cd5177966c9e005418cfdc1fb36db62e13",
+   "rev": "1fa48c6a63b4c4cda28be61e1037192776e77ac0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "593aa51c4aa07ee81e9233b53e1f61a5b4d9f761",
+   "rev": "95c2f8afe09d9e49d3cacca667261da04f7f93f7",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5bd478197f2e5d2a4fde527cf3581d83f49baa9b",
+   "rev": "c029ceb9956ef9d567fc034e5403ec829f8d0d87",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,10 +95,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "f75f4926aff7ba19949e16c19094d7298806b1a6",
+   "rev": "72ae7004d9f0ddb422aec5378204fdd7828c5672",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.25.0-rc1",
+   "inputRev": "v4.25.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "FLT",

lakefile.toml

@@ -15,7 +15,7 @@ warn.sorry = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.25.0-rc1"
+rev = "master"
 
 [[require]]
 name = "checkdecls"

lean-toolchain

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