chore: bump to stable v4.16.0 (#337)

FLT/AutomorphicRepresentation/Example.lean

@@ -76,7 +76,7 @@ instance charZero : CharZero ZHat := ⟨ fun a b h ↦ by
 open BigOperators Nat Finset in
 /-- A nonarchimedean analogue `0! + 1! + 2! + ⋯` of `e = 1/0! + 1/1! + 1/2! + ⋯`.
 It is defined as the function whose value at `ZMod n` is the sum of `i!` for `0 ≤ i < n`.-/
-def e : ZHat := ⟨fun (n : ℕ+) ↦ ∑ i in range (n : ℕ), i !, by
+def e : ZHat := ⟨fun (n : ℕ+) ↦ ∑ i ∈ range (n : ℕ), i !, by
   intros D N hDN
   dsimp only
   obtain ⟨k, hk⟩ := exists_add_of_le <| le_of_dvd N.pos hDN
@@ -88,7 +88,7 @@ def e : ZHat := ⟨fun (n : ℕ+) ↦ ∑ i in range (n : ℕ), i !, by
 
 open BigOperators Nat Finset
 
-lemma e_def (n : ℕ+) : e n = ∑ i in range (n : ℕ), (i ! : ZMod n) := rfl
+lemma e_def (n : ℕ+) : e n = ∑ i ∈ range (n : ℕ), (i ! : ZMod n) := rfl
 
 lemma _root_.Nat.sum_factorial_lt_factorial_succ {j : ℕ} (hj : 1 < j) :
     ∑ i ∈ range (j + 1), i ! < (j + 1) ! := by

FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean

@@ -342,9 +342,7 @@ theorem range_adicCompletionComapAlgIso_tensorAdicCompletionIntegersTo_le_pi
     RingHom.coe_coe, AlgHom.coe_comp, AlgHom.coe_restrictScalars', AlgHom.coe_coe,
     Function.comp_apply, SetLike.mem_coe]
   induction' x with x y x y hx hy
-  · rw [(tensorAdicCompletionIntegersTo A K L B v).map_zero,
-      (tensorAdicCompletionComapAlgHom A K L B v).map_zero]
-    exact zero_mem _
+  · simp [map_zero, Pi.zero_apply, zero_mem]
   · simp only [tensorAdicCompletionIntegersTo, Algebra.TensorProduct.lift_tmul, AlgHom.coe_comp,
       Function.comp_apply, Algebra.ofId_apply, AlgHom.commutes,
       Algebra.TensorProduct.algebraMap_apply, AlgHom.coe_restrictScalars',
@@ -362,9 +360,7 @@ theorem range_adicCompletionComapAlgIso_tensorAdicCompletionIntegersTo_le_pi
     · exact Ideal.IsDedekindDomain.ramificationIdx_ne_zero  ((Ideal.map_eq_bot_iff_of_injective
         (algebraMap_injective_of_field_isFractionRing A B K L)).not.mpr
         (comap A i.1).3) i.1.2 Ideal.map_comap_le
-  · rw [(tensorAdicCompletionIntegersTo A K L B v).map_add,
-      (tensorAdicCompletionComapAlgHom A K L B v).map_add]
-    exact add_mem hx hy
+  · simp [map_add, Pi.add_apply, add_mem hx hy]
 
 theorem adicCompletionComapAlgEquiv_integral : ∃ S : Finset (HeightOneSpectrum A), ∀ v ∉ S,
     AlgHom.range (((tensorAdicCompletionComapAlgHom A K L B v).restrictScalars B).comp

FLT/GlobalLanglandsConjectures/GLnDefs.lean

@@ -284,7 +284,7 @@ open CategoryTheory
 noncomputable def preweight.fdRep (n : ℕ) (w : preweight n) :
     FDRep ℂ (orthogonalGroup (Fin n) ℝ) where
   V := FGModuleCat.of ℂ (Fin w.d → ℂ)
-  ρ := {
+  ρ := MonCat.ofHom {
     toFun := fun A ↦ ModuleCat.ofHom {
       toFun := fun x ↦ (w.rho A).1 *ᵥ x
       map_add' := fun _ _ ↦ Matrix.mulVec_add ..

FLT/HaarMeasure/DistribHaarChar/RealComplex.lean

@@ -31,7 +31,7 @@ open Real Complex MeasureTheory Measure Set
 open scoped Pointwise
 
 lemma Real.volume_real_smul (x : ℝ) (s : Set ℝ) : volume (x • s) = ‖x‖₊ * volume s := by
-  simp [← ennnorm_eq_ofReal_abs]
+  simp [← enorm_eq_ofReal_abs, enorm_eq_nnnorm]
 
 /-- The distributive Haar character of the action of `ℝˣ` on `ℝ` is the usual norm.
 
@@ -62,7 +62,7 @@ lemma distribHaarChar_complex (z : ℂˣ) : distribHaarChar ℂ z = ‖(z : ℂ)
     (f := (LinearMap.mul ℂ ℂ z⁻¹).restrictScalars ℝ) _ _ using 2
   · simpa [LinearMap.mul, LinearMap.mk₂, LinearMap.mk₂', LinearMap.mk₂'ₛₗ, Units.smul_def, eq_comm]
       using preimage_smul_inv z (Icc 0 1 ×ℂ Icc 0 1)
-  · simp [key, ofReal_norm_eq_coe_nnnorm, ← Complex.norm_eq_abs, ENNReal.ofReal_pow, zpow_ofNat]
+  · simp [key, ofReal_norm_eq_enorm, ← Complex.norm_eq_abs, ENNReal.ofReal_pow, zpow_ofNat]; rfl
   · simp [key, zpow_ofNat]
 
 lemma Complex.volume_complex_smul (z : ℂ) (s : Set ℂ) : volume (z • s) = ‖z‖₊ ^ 2 * volume s := by

FLT/MathlibExperiments/Coalgebra/Monoid.lean

@@ -68,13 +68,13 @@ lemma mul_def (φ ψ : LinearPoint R A L) :
     φ * ψ = LinearMap.mul' _ _ ∘ₗ TensorProduct.map φ ψ ∘ₗ Coalgebra.comul := rfl
 
 lemma mul_repr' {ι : Type* } (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A)
-    (repr : Coalgebra.comul (R := R) a = ∑ i in ℐ, Δ₁ i ⊗ₜ Δ₂ i) :
-    φ.mul ψ a = ∑ i in ℐ, φ (Δ₁ i) * ψ (Δ₂ i) := by
+    (repr : Coalgebra.comul (R := R) a = ∑ i ∈ ℐ, Δ₁ i ⊗ₜ Δ₂ i) :
+    φ.mul ψ a = ∑ i ∈ ℐ, φ (Δ₁ i) * ψ (Δ₂ i) := by
   simp only [mul, comp_apply, repr, map_sum, map_tmul, mul'_apply]
 
 lemma mul_repr {ι : Type* } (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A)
-    (repr : Coalgebra.comul (R := R) a = ∑ i in ℐ, Δ₁ i ⊗ₜ Δ₂ i) :
-    (φ * ψ) a = ∑ i in ℐ, φ (Δ₁ i) * ψ (Δ₂ i) :=
+    (repr : Coalgebra.comul (R := R) a = ∑ i ∈ ℐ, Δ₁ i ⊗ₜ Δ₂ i) :
+    (φ * ψ) a = ∑ i ∈ ℐ, φ (Δ₁ i) * ψ (Δ₂ i) :=
   mul_repr' _ _ a ℐ Δ₁ Δ₂ repr
 
 lemma mul_assoc' : φ * ψ * χ = φ * (ψ * χ) := LinearMap.ext fun x ↦ by
@@ -172,8 +172,8 @@ lemma mul_def (φ ψ : AlgHomPoint R A L) :
       Algebra.TensorProduct.map φ ψ |>.comp <| Bialgebra.comulAlgHom R A) := rfl
 
 lemma mul_repr {ι : Type* } (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A)
-    (repr : Coalgebra.comul (R := R) a = ∑ i in ℐ, Δ₁ i ⊗ₜ Δ₂ i) :
-    (φ * ψ) a = ∑ i in ℐ, φ (Δ₁ i) * ψ (Δ₂ i) :=
+    (repr : Coalgebra.comul (R := R) a = ∑ i ∈ ℐ, Δ₁ i ⊗ₜ Δ₂ i) :
+    (φ * ψ) a = ∑ i ∈ ℐ, φ (Δ₁ i) * ψ (Δ₂ i) :=
   LinearPoint.mul_repr _ _ a ℐ Δ₁ Δ₂ repr
 
 lemma mul_assoc' : φ * ψ * χ = φ * (ψ * χ) := by

FLT/MathlibExperiments/Coalgebra/Sweedler.lean

@@ -31,18 +31,18 @@ variable [AddCommMonoid A] [Module R A] [Coalgebra R A]
 
 lemma exists_repr (x : A) :
     ∃ (I : Finset (A ⊗[R] A)) (x1 : A ⊗[R] A → A) (x2 : A ⊗[R] A → A),
-    Coalgebra.comul x = ∑ i in I, x1 i ⊗ₜ[R] x2 i := by
+    Coalgebra.comul x = ∑ i ∈ I, x1 i ⊗ₜ[R] x2 i := by
   classical
   have mem1 : comul x ∈ (⊤ : Submodule R (A ⊗[R] A)) := ⟨⟩
   rw [← TensorProduct.span_tmul_eq_top, mem_span_set] at mem1
-  obtain ⟨r, hr, (eq1 : ∑ i in r.support, (_ • _) = _)⟩ := mem1
+  obtain ⟨r, hr, (eq1 : ∑ i ∈ r.support, (_ • _) = _)⟩ := mem1
   choose a a' haa' using hr
   replace eq1 := calc _
-    comul x = ∑ i in r.support, r i • i := eq1.symm
-    _ = ∑ i in r.support.attach, (r i : R) • i.1 := Finset.sum_attach _ _ |>.symm
-    _ = ∑ i in r.support.attach, (r i • a i.2 ⊗ₜ[R] a' i.2) :=
+    comul x = ∑ i ∈ r.support, r i • i := eq1.symm
+    _ = ∑ i ∈ r.support.attach, (r i : R) • i.1 := Finset.sum_attach _ _ |>.symm
+    _ = ∑ i ∈ r.support.attach, (r i • a i.2 ⊗ₜ[R] a' i.2) :=
         Finset.sum_congr rfl fun i _ ↦ congr(r i.1 • $(haa' i.2)).symm
-    _ = ∑ i in r.support.attach, ((r i • a i.2) ⊗ₜ[R] a' i.2) :=
+    _ = ∑ i ∈ r.support.attach, ((r i • a i.2) ⊗ₜ[R] a' i.2) :=
         Finset.sum_congr rfl fun i _ ↦ TensorProduct.smul_tmul' _ _ _
   refine ⟨r.support, fun i ↦ if h : i ∈ r.support then r i • a h else 0,
     fun i ↦ if h : i ∈ r.support then a' h else 0, eq1 ▸ ?_⟩
@@ -60,17 +60,17 @@ noncomputable def Δ₂ (a : A) : A ⊗[R] A → A :=
   exists_repr a |>.choose_spec.choose_spec.choose
 
 lemma comul_repr (a : A) :
-    Coalgebra.comul a = ∑ i in ℐ a, Δ₁ a i ⊗ₜ[R] Δ₂ (R := R) a i :=
+    Coalgebra.comul a = ∑ i ∈ ℐ a, Δ₁ a i ⊗ₜ[R] Δ₂ (R := R) a i :=
   exists_repr a |>.choose_spec.choose_spec.choose_spec
 
 lemma sum_counit_tmul (a : A) {ι : Type*} (s : Finset ι) (x y : ι → A)
-    (repr : comul a = ∑ i in s, x i ⊗ₜ[R] y i) :
-    ∑ i in s, counit (R := R) (x i) ⊗ₜ y i = 1 ⊗ₜ[R] a := by
+    (repr : comul a = ∑ i ∈ s, x i ⊗ₜ[R] y i) :
+    ∑ i ∈ s, counit (R := R) (x i) ⊗ₜ y i = 1 ⊗ₜ[R] a := by
   simpa [repr, map_sum] using congr($(rTensor_counit_comp_comul (R := R) (A := A)) a)
 
 lemma sum_tmul_counit (a : A) {ι : Type*} (s : Finset ι) (x y : ι → A)
-    (repr : comul a = ∑ i in s, x i ⊗ₜ[R] y i) :
-    ∑ i in s, (x i) ⊗ₜ counit (R := R) (y i) = a ⊗ₜ[R] 1 := by
+    (repr : comul a = ∑ i ∈ s, x i ⊗ₜ[R] y i) :
+    ∑ i ∈ s, (x i) ⊗ₜ counit (R := R) (y i) = a ⊗ₜ[R] 1 := by
   simpa [repr, map_sum] using congr($(lTensor_counit_comp_comul (R := R) (A := A)) a)
 
 end Coalgebra

FLT/MathlibExperiments/Coalgebra/TensorProduct.lean

@@ -94,23 +94,23 @@ variable {R A B}
 
 lemma comul_apply_repr (a : A) (b : B) {ιA ιB : Type*}
     (sA : Finset ιA) (sB : Finset ιB)
-    (xA yA : ιA → A) (repr_a : comul a = ∑ i in sA, xA i ⊗ₜ[R] yA i)
-    (xB yB : ιB → B) (repr_b : comul b = ∑ i in sB, xB i ⊗ₜ[R] yB i) :
-    comul (a ⊗ₜ[R] b) = ∑ i in sA, ∑ j in sB, (xA i ⊗ₜ xB j) ⊗ₜ[R] (yA i ⊗ₜ yB j) := by
+    (xA yA : ιA → A) (repr_a : comul a = ∑ i ∈ sA, xA i ⊗ₜ[R] yA i)
+    (xB yB : ιB → B) (repr_b : comul b = ∑ i ∈ sB, xB i ⊗ₜ[R] yB i) :
+    comul (a ⊗ₜ[R] b) = ∑ i ∈ sA, ∑ j ∈ sB, (xA i ⊗ₜ xB j) ⊗ₜ[R] (yA i ⊗ₜ yB j) := by
   simpa [TensorProduct.comul_def, repr_a, repr_b, map_sum, sum_tmul, tmul_sum] using Finset.sum_comm
 
 lemma comul_apply_repr' (a : A) (b : B) {ιA ιB : Type*}
     (sA : Finset ιA) (sB : Finset ιB)
-    (xA yA : ιA → A) (repr_a : comul a = ∑ i in sA, xA i ⊗ₜ[R] yA i)
-    (xB yB : ιB → B) (repr_b : comul b = ∑ i in sB, xB i ⊗ₜ[R] yB i) :
-    comul (a ⊗ₜ[R] b) = ∑ j in sB, ∑ i in sA, (xA i ⊗ₜ xB j) ⊗ₜ[R] (yA i ⊗ₜ yB j) := by
+    (xA yA : ιA → A) (repr_a : comul a = ∑ i ∈ sA, xA i ⊗ₜ[R] yA i)
+    (xB yB : ιB → B) (repr_b : comul b = ∑ i ∈ sB, xB i ⊗ₜ[R] yB i) :
+    comul (a ⊗ₜ[R] b) = ∑ j ∈ sB, ∑ i ∈ sA, (xA i ⊗ₜ xB j) ⊗ₜ[R] (yA i ⊗ₜ yB j) := by
   simp [TensorProduct.comul_def, repr_a, repr_b, map_sum, sum_tmul, tmul_sum]
 
 lemma comul_apply_repr'' (a : A) (b : B) {ιA ιB : Type*}
     (sA : Finset ιA) (sB : Finset ιB)
-    (xA yA : ιA → A) (repr_a : comul a = ∑ i in sA, xA i ⊗ₜ[R] yA i)
-    (xB yB : ιB → B) (repr_b : comul b = ∑ i in sB, xB i ⊗ₜ[R] yB i) :
-    comul (a ⊗ₜ[R] b) = ∑ i in sA ×ˢ sB, (xA i.1 ⊗ₜ xB i.2) ⊗ₜ[R] (yA i.1 ⊗ₜ yB i.2) := by
+    (xA yA : ιA → A) (repr_a : comul a = ∑ i ∈ sA, xA i ⊗ₜ[R] yA i)
+    (xB yB : ιB → B) (repr_b : comul b = ∑ i ∈ sB, xB i ⊗ₜ[R] yB i) :
+    comul (a ⊗ₜ[R] b) = ∑ i ∈ sA ×ˢ sB, (xA i.1 ⊗ₜ xB i.2) ⊗ₜ[R] (yA i.1 ⊗ₜ yB i.2) := by
   rw [TensorProduct.comul_apply_repr (repr_a := repr_a) (repr_b := repr_b), Finset.sum_product]
 
 end Coalgebra

FLT/MathlibExperiments/HopfAlgebra/Basic.lean

@@ -36,27 +36,27 @@ variable (A : Type*) [Semiring A] [HopfAlgebra R A]
 variable {R A}
 
 lemma antipode_repr {ι : Type*} (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A)
-    (repr : Coalgebra.comul a = ∑ i in ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) :
-    ∑ i in ℐ, antipode (R := R) (Δ₁ i) * Δ₂ i = algebraMap R A (Coalgebra.counit a) := by
+    (repr : Coalgebra.comul a = ∑ i ∈ ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) :
+    ∑ i ∈ ℐ, antipode (R := R) (Δ₁ i) * Δ₂ i = algebraMap R A (Coalgebra.counit a) := by
   have := mul_antipode_rTensor_comul_apply (R := R) a
   rw [repr, map_sum, map_sum] at this
   exact this
 
 lemma antipode_repr_eq_smul {ι : Type*} (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A)
-    (repr : Coalgebra.comul a = ∑ i in ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) :
-    ∑ i in ℐ, antipode (R := R) (Δ₁ i) * Δ₂ i = (Coalgebra.counit a : R) • (1 : A) := by
+    (repr : Coalgebra.comul a = ∑ i ∈ ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) :
+    ∑ i ∈ ℐ, antipode (R := R) (Δ₁ i) * Δ₂ i = (Coalgebra.counit a : R) • (1 : A) := by
   rw [antipode_repr (repr := repr), Algebra.smul_def, mul_one]
 
 lemma antipode_repr' {ι : Type*} (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A)
-    (repr : Coalgebra.comul a = ∑ i in ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) :
-    ∑ i in ℐ, Δ₁ i * antipode (R := R) (Δ₂ i) = algebraMap R A (Coalgebra.counit a) := by
+    (repr : Coalgebra.comul a = ∑ i ∈ ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) :
+    ∑ i ∈ ℐ, Δ₁ i * antipode (R := R) (Δ₂ i) = algebraMap R A (Coalgebra.counit a) := by
   have := mul_antipode_lTensor_comul_apply (R := R) a
   rw [repr, map_sum, map_sum] at this
   exact this
 
 lemma antipode_repr_eq_smul' {ι : Type*} (a : A) (ℐ : Finset ι) (Δ₁ Δ₂ : ι → A)
-    (repr : Coalgebra.comul a = ∑ i in ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) :
-    ∑ i in ℐ, Δ₁ i * antipode (R := R) (Δ₂ i) = (Coalgebra.counit a : R) • 1 := by
+    (repr : Coalgebra.comul a = ∑ i ∈ ℐ, Δ₁ i ⊗ₜ[R] Δ₂ i) :
+    ∑ i ∈ ℐ, Δ₁ i * antipode (R := R) (Δ₂ i) = (Coalgebra.counit a : R) • 1 := by
   rw [antipode_repr' (repr := repr), Algebra.smul_def, mul_one]
 
 lemma antipode_mul_id : antipode (R := R) (A := A) * LinearMap.id = 1 := by

FLT/MathlibExperiments/IsCentralSimple.lean

@@ -35,7 +35,7 @@ structure IsCentralSimple
 variable (K : Type u) [Field K]
 
 theorem RingCon.sum {R : Type u} [AddCommMonoid R] [Mul R] {ι : Type v} {s : Finset ι} {a b : ι → R}
-    {r : RingCon R} (h : ∀ i ∈ s, r (a i) (b i)) : r (∑ i in s, a i) (∑ i in s, b i) := by
+    {r : RingCon R} (h : ∀ i ∈ s, r (a i) (b i)) : r (∑ i ∈ s, a i) (∑ i ∈ s, b i) := by
   induction s using Finset.induction_on with
   | empty =>
     simp only [Finset.sum_empty]

docbuild/lakefile.toml

@@ -10,4 +10,4 @@ path = "../"
 [[require]]
 scope = "leanprover"
 name = "doc-gen4"
-rev = "main"
+rev = "v4.16.0"

lake-manifest.json

@@ -15,10 +15,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2a71f56e8867536abeae5d73fdb6666dc21ff7d4",
+   "rev": "a6276f4c6097675b1cf5ebd49b1146b735f38c02",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "stable",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f72319c9686788305a8ab059f3c4d8c724785c83",
+   "rev": "1a6613663c3eb08c401ce0fd1a408412f2c2321e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5b23a1297aba9683f231c4b1a7ab4076af4ad53d",
+   "rev": "01006c9e86bf9e397c026fef4190478dd1fd897e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.lean

@@ -8,7 +8,7 @@ package FLT where
     ⟨`relaxedAutoImplicit, false⟩ -- switch off relaxed auto-implicit
   ]
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "master"
+require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "stable"
 
 require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.16.0-rc2
+leanprover/lean4:v4.16.0