bump

FltRegular/CaseI/AuxLemmas.lean

@@ -93,7 +93,7 @@ theorem auxf0k₂ (hp5 : 5 ≤ p) (a b : ℤ) : ∃ i : Fin P, f0k₂ a b (i : 
     simp only [Fin.ext_iff, Fin.val_mk] at h; contradiction
   have hzero : ((⟨2, two_lt hp5⟩ : Fin p) : ℕ) ≠ 0 := by
     intro h
-    simp only [Fin.ext_iff, Fin.val_mk] at h
+    simp [Fin.ext_iff, Fin.val_mk] at h
   simp only [f0k₂, h1, if_false, hzero, one_lt_two.ne']
 
 theorem aux0k₂ {a b : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ p) (hab : ¬a ≡ b [ZMOD p])

FltRegular/CaseI/Statement.lean

@@ -31,7 +31,7 @@ theorem may_assume : SlightlyEasier → Statement := by
     rw [h] at H hI
     refine hI <| Dvd.dvd.mul_left ?_ _
     simp only [Nat.cast_ofNat] at hI ⊢
-    rw [← even_iff_two_dvd, ← Int.odd_iff_not_even] at hI
+    rw [← even_iff_two_dvd, Int.not_even_iff_odd] at hI
     rw [← even_iff_two_dvd, ← Int.even_pow' (show 2 ≠ 0 by norm_num), ← H]
     exact (Int.Odd.of_mul_left (Odd.of_mul_left hI)).pow.add_odd
       (Int.Odd.of_mul_right (Odd.of_mul_left hI)).pow

FltRegular/CaseII/AuxLemmas.lean

@@ -20,7 +20,7 @@ lemma WfDvdMonoid.multiplicity_finite {M : Type*} [CancelCommMonoidWithZero M] [
   rw [multiplicity.Finite, not_exists_not] at h
   choose f hf using h
   obtain ⟨_, ⟨n, rfl⟩, hn⟩ :=
-    (WfDvdMonoid.wellFounded_dvdNotUnit (α := M)).has_min (Set.range f) (Set.range_nonempty f)
+    (wellFounded_dvdNotUnit (α := M)).has_min (Set.range f) (Set.range_nonempty f)
   apply hn _ ⟨n + 1, rfl⟩
   constructor
   · intro e

FltRegular/NumberTheory/Finrank.lean

@@ -26,7 +26,7 @@ lemma FiniteDimensional.exists_finset_card_eq_finrank_and_linearIndependent :
   cases nonempty_fintype s
   exact ⟨s.toFinset,
     Cardinal.natCast_injective (by rwa [Set.toFinset_card, ← Cardinal.mk_fintype]),
-    by convert hs <;> simp only [Set.mem_toFinset]⟩
+    by convert hs using 2 <;> simp only [Set.mem_toFinset]⟩
 
 variable {R M}
 
@@ -45,10 +45,11 @@ lemma FiniteDimensional.finrank_add_finrank_quotient_le (N : Submodule R M) :
       Disjoint (Submodule.span R (Subtype.val '' (s : Set N))) (Submodule.span R (f '' t)) := by
     apply Disjoint.mono_left (Submodule.span_le.mpr Set.image_val_subset)
     rw [disjoint_iff, eq_bot_iff, ← @Subtype.range_val (M ⧸ N) t, ← Set.range_comp,
-      ← Finsupp.range_total]
+      ← Finsupp.range_linearCombination]
     rintro _ ⟨h, l, rfl⟩
     rw [SetLike.mem_coe, ← Submodule.Quotient.mk_eq_zero, ← Submodule.mkQ_apply,
-      Finsupp.apply_total, ← Function.comp.assoc, show N.mkQ ∘ f = id from funext hf] at h
+      Finsupp.apply_linearCombination, ← Function.comp.assoc,
+      show N.mkQ ∘ f = id from funext hf] at h
     rw [linearIndependent_iff.mp ht' l h, map_zero]
     exact zero_mem _
   rw [← hs, ← ht, ← t.card_image_of_injective hf.injective,
@@ -122,8 +123,8 @@ lemma FiniteDimensional.finrank_add_finrank_quotient_of_free [IsDomain R] [IsPri
     rw [linearIndependent_iff]
     intros l hl
     ext i
-    rw [← Finsupp.apply_total, N.mkQ_apply, Submodule.Quotient.mk_eq_zero, Finsupp.total_apply,
-      Finsupp.sum_fintype _ _ (by simp)] at hl
+    rw [← Finsupp.apply_linearCombination, N.mkQ_apply, Submodule.Quotient.mk_eq_zero,
+      Finsupp.linearCombination_apply, Finsupp.sum_fintype _ _ (by simp)] at hl
     simpa only [Function.comp_apply, map_sum, map_smul, Basis.repr_self, Finsupp.smul_single,
       smul_eq_mul, mul_one, Finsupp.single_apply, Finsupp.finset_sum_apply,
       ← Subtype.ext_iff, Finset.sum_ite_eq', Finset.mem_univ, ite_true] using
@@ -191,6 +192,6 @@ lemma FiniteDimensional.exists_of_finrank_lt [IsDomain R] [IsPrincipalIdealRing
   use v
   intro r hr
   have := linearIndependent_iff.mp hs' (Finsupp.single ⟨_, hv⟩ r)
-  rw [Finsupp.total_single, Finsupp.single_eq_zero, ← LinearMap.map_smul,
+  rw [Finsupp.linearCombination_single, Finsupp.single_eq_zero, ← LinearMap.map_smul,
     Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at this
   exact mt this hr

FltRegular/NumberTheory/Hilbert92.lean

@@ -67,8 +67,9 @@ lemma LinearIndependent.update {ι} [DecidableEq ι] {R} [CommRing R] [Module R
   classical
   rw [linearIndependent_iff] at hf ⊢
   intros l hl
-  have : (Finsupp.total ι G R f) (Finsupp.update (σ • l) i (l i)) = 0 := by
-    rw [← smul_zero σ, ← hl, Finsupp.total_apply, Finsupp.total_apply, Finsupp.smul_sum]
+  have : (Finsupp.linearCombination R f) (Finsupp.update (σ • l) i (l i)) = 0 := by
+    rw [← smul_zero σ, ← hl, Finsupp.linearCombination_apply, Finsupp.linearCombination_apply,
+      Finsupp.smul_sum]
     apply Finsupp.sum_congr'
     · intro x
       simp only [Finsupp.coe_update, Finsupp.coe_smul, Function.update_apply, ite_smul, smul_ite]
@@ -88,21 +89,21 @@ lemma LinearIndependent.update {ι} [DecidableEq ι] {R} [CommRing R] [Module R
 noncomputable
 def Finsupp.ltotal (α M R) [CommSemiring R] [AddCommMonoid M] [Module R M] :
     (α → M) →ₗ[R] (α →₀ R) →ₗ[R] M where
-  toFun := Finsupp.total α M R
+  toFun := Finsupp.linearCombination R
   map_add' := fun u v ↦ by ext f; simp
   map_smul' := fun r v ↦ by ext f; simp
 
 lemma Finsupp.total_pi_single {α M R} [CommSemiring R] [AddCommMonoid M] [Module R M]
     [DecidableEq α] (i : α) (m : M) (f : α →₀ R) :
-    Finsupp.total α M R (Pi.single i m) f = f i • m := by
-  simp only [Finsupp.total, ne_eq, Pi.single_apply, coe_lsum, LinearMap.coe_smulRight,
+    Finsupp.linearCombination R (Pi.single i m) f = f i • m := by
+  simp only [Finsupp.linearCombination, ne_eq, Pi.single_apply, coe_lsum, LinearMap.coe_smulRight,
     LinearMap.id_coe, id_eq, smul_ite, smul_zero, sum_ite_eq', mem_support_iff, ite_eq_left_iff,
     not_not]
   exact fun e ↦ e ▸ (zero_smul R m).symm
 
 lemma LinearIndependent.update' {ι} [DecidableEq ι] {R} [CommRing R] [Module R G]
     (f : ι → G) (l : ι →₀ R) (i : ι) (g : G) (σ : R)
-    (hσ : σ ∈ nonZeroDivisors R) (hg : σ • g = Finsupp.total _ _ R f l)
+    (hσ : σ ∈ nonZeroDivisors R) (hg : σ • g = Finsupp.linearCombination R f l)
     (hl : l i ∈ nonZeroDivisors R) (hf : LinearIndependent R f) :
     LinearIndependent R (Function.update f i g) := by
   classical
@@ -113,7 +114,7 @@ lemma LinearIndependent.update' {ι} [DecidableEq ι] {R} [CommRing R] [Module R
   simp only [Finsupp.ltotal_apply, LinearMap.add_apply, LinearMap.sub_apply,
     Finsupp.total_pi_single, smul_add, smul_sub, smul_zero] at hl'
   rw [smul_comm σ (l' i) g, hg, ← LinearMap.map_smul, ← LinearMap.map_smul, smul_smul,
-    ← Finsupp.total_single, ← (Finsupp.total ι G R f).map_sub, ← map_add] at hl'
+    ← Finsupp.linearCombination_single, ← (Finsupp.linearCombination R f).map_sub, ← map_add] at hl'
   replace hl' : ∀ j, (σ * l' j - (Finsupp.single i (σ * l' i)) j) + l' i * l j = 0 := by
     intro j
     exact DFunLike.congr_fun (hf _ hl') j
@@ -163,7 +164,7 @@ lemma existence [Module.Free ℤ G] [Module A G] :
 
 lemma lemma2 [Module A G] (S : systemOfUnits p G r) (hs : S.IsFundamental)
     (i : Fin r) (a : Fin r →₀ A) (ha : a i = 1) :
-    ∀ g : G, (1 - zeta p) • g ≠ Finsupp.total _ G A S.units a := by
+    ∀ g : G, (1 - zeta p) • g ≠ Finsupp.linearCombination A S.units a := by
   cases' r with r
   · exact isEmptyElim i
   intro g hg
@@ -176,9 +177,9 @@ lemma lemma2 [Module A G] (S : systemOfUnits p G r) (hs : S.IsFundamental)
     ext; simp only [Function.comp_apply, ne_eq, Fin.succAbove_ne, not_false_eq_true,
       Function.update_noteq]
   have ha' :
-      Finsupp.total _ G A (S'.units ∘ Fin.succAbove i) a' + S.units i = (1 - zeta p) • g := by
-    rw [hS', Finsupp.total_comp, LinearMap.comp_apply, Finsupp.lmapDomain_apply,
-      ← one_smul A (S.units i), hg, ← ha, ← Finsupp.total_single, ← map_add]
+      Finsupp.linearCombination A (S'.units ∘ Fin.succAbove i) a' + S.units i = (1 - zeta p) • g := by
+    rw [hS', Finsupp.linearCombination_comp, LinearMap.comp_apply, Finsupp.lmapDomain_apply,
+      ← one_smul A (S.units i), hg, ← ha, ← Finsupp.linearCombination_single, ← map_add]
     congr 1
     ext j
     rw [Finsupp.coe_add, Pi.add_apply, Finsupp.single_apply]
@@ -201,17 +202,17 @@ lemma lemma2 [Module A G] (S : systemOfUnits p G r) (hs : S.IsFundamental)
       rw [← hij, ha']
       apply sub_mem
       · exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨i, Function.update_same _ _ _⟩)
-      · rw [← Finsupp.range_total, Finsupp.total_comp, LinearMap.comp_apply]
+      · rw [← Finsupp.range_linearCombination, Finsupp.linearCombination_comp, LinearMap.comp_apply]
         exact ⟨_, rfl⟩
     · exact Submodule.subset_span ⟨j, Function.update_noteq (Ne.symm hij) _ _⟩
   · refine ⟨g, Submodule.subset_span ⟨i, Function.update_same _ _ _⟩, ?_⟩
-    rw [← Finsupp.range_total]
+    rw [← Finsupp.range_linearCombination]
     rintro ⟨l, rfl⟩
     letI := (Algebra.id A).toModule
     letI : SMulZeroClass A A := SMulWithZero.toSMulZeroClass
     letI : Module A (Fin r →₀ A) := Finsupp.module (Fin r) A
     rw [← LinearMap.map_smul, ← sub_eq_zero,
-      ← (Finsupp.total (Fin _) G A S.units).map_sub] at hg
+      ← (Finsupp.linearCombination A S.units).map_sub] at hg
     have := DFunLike.congr_fun (linearIndependent_iff.mp S.linearIndependent _ hg) i
     simp only [algebraMap_int_eq, Int.coe_castRingHom, Finsupp.coe_sub, Finsupp.coe_smul, ha,
       Pi.sub_apply, Finsupp.mapRange_apply, Finsupp.coe_zero, Pi.zero_apply, sub_eq_zero] at this
@@ -230,7 +231,7 @@ lemma corollary [Module A G] (S : systemOfUnits p G r) (hs : S.IsFundamental) (a
   have hb : b i = 1 := by rw [← e]; rfl
   apply lemma2 p hp G r hf S hs i b hb (x • ∑ i, S.units i + y • g)
   rw [smul_add, smul_smul _ y, mul_comm, ← smul_smul, hg, smul_sum, smul_sum, smul_sum,
-    ← sum_add_distrib, Finsupp.total_apply, Finsupp.sum_fintype]
+    ← sum_add_distrib, Finsupp.linearCombination_apply, Finsupp.sum_fintype]
   congr
   · ext j
     simp only [smul_smul, Finsupp.ofSupportFinite_coe, add_smul, b', b]
@@ -267,6 +268,7 @@ lemma norm_eq_prod_pow_gen
     [IsGalois k K] [FiniteDimensional k K]
     (σ : K ≃ₐ[k] K) (hσ : ∀ x, x ∈ Subgroup.zpowers σ) (η : K) :
     algebraMap k K (Algebra.norm k η) = (∏ i in Finset.range (orderOf σ), (σ ^ i) η)   := by
+  let _ : Fintype (Subgroup.zpowers σ) := inferInstance
   rw [Algebra.norm_eq_prod_automorphisms, ← Fin.prod_univ_eq_prod_range,
     ← (finEquivZPowers σ <| isOfFinOrder_of_finite _).symm.prod_comp]
   simp only [pow_finEquivZPowers_symm_apply]
@@ -757,6 +759,7 @@ lemma h_exists' : ∃ (h : ℕ) (ζ : (𝓞 k)ˣ),
   obtain ⟨j, _, hj'⟩ := (Nat.dvd_prime_pow hp).mp (orderOf_dvd_of_pow_eq_one hiζ)
   refine ⟨j, ζ, IsPrimitiveRoot.coe_coe_iff.mpr (hj' ▸ IsPrimitiveRoot.orderOf ζ.1),
     fun ε n hn ↦ ?_⟩
+  let _ :   Fintype (Units.torsion k) := inferInstance
   have : Fintype H := Set.fintypeSubset (NumberField.Units.torsion k) (by exact this)
   obtain ⟨i, hi⟩ := mem_powers_iff_mem_zpowers.mpr (hζ ⟨ε, ⟨_, n, rfl⟩, hn⟩)
   exact ⟨i, congr_arg Subtype.val hi⟩

FltRegular/NumberTheory/KummersLemma/Field.lean

@@ -42,9 +42,10 @@ lemma monic_poly_aux :
     rw [natDegree_poly_aux hζ, coeff_C, if_neg p.pos.ne.symm]
   · rw [leadingCoeff_pow, ← C.map_one, leadingCoeff, natDegree_sub_C, natDegree_mul_X]
     simp only [map_one, natDegree_C, zero_add, coeff_sub, coeff_mul_X, coeff_C, ite_true,
-      coeff_one, ite_false, sub_zero]
+      coeff_one, ite_false, sub_zero, one_ne_zero, ↓reduceIte]
     exact C_ne_zero.mpr (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt)
 
+
 variable [IsCyclotomicExtension {p} ℚ K]
 
 noncomputable def poly : (𝓞 K)[X] := (zeta_sub_one_pow_dvd_poly hp hζ u hcong).choose
@@ -287,7 +288,7 @@ lemma polyRoot_spec {L : Type*} [Field L] [Algebra K L] (α : L)
 lemma mem_adjoin_polyRoot {L : Type*} [Field L] [Algebra K L] (α : L)
     (e : α ^ (p : ℕ) = algebraMap K L u) (i) :
     α ∈ Algebra.adjoin K {(polyRoot hp hζ u hcong α e i : L)} := by
-  conv_lhs => rw [polyRoot_spec hp hζ u hcong α e i]
+  conv => enter [2]; rw [polyRoot_spec hp hζ u hcong α e i]
   exact Subalgebra.smul_mem _ (sub_mem (one_mem _)
     (Subalgebra.smul_mem _ (Algebra.self_mem_adjoin_singleton K _) _)) _
 

FltRegular/NumberTheory/QuotientTrace.lean

@@ -94,7 +94,8 @@ lemma basisQuotientOfLocalRing_repr {ι} [Fintype ι] (b : Basis ι R S) (x) (i)
   apply (basisQuotientOfLocalRing b).repr.symm.injective
   simp only [Finsupp.linearEquivFunOnFinite_symm_coe, LinearEquiv.symm_apply_apply,
     Basis.repr_symm_apply]
-  rw [Finsupp.total_eq_fintype_total_apply _ (R ⧸ p), Fintype.total_apply]
+  rw [Finsupp.linearCombination_eq_fintype_linearCombination_apply _ (R ⧸ p),
+    Fintype.linearCombination_apply]
   simp only [Function.comp_apply, basisQuotientOfLocalRing_apply,
     Ideal.Quotient.mk_smul_mk_quotient_map_quotient, ← Algebra.smul_def]
   rw [← map_sum, Basis.sum_repr b x]

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ad26fe1ebccc9d5b7ca9111d5daf9b4488374415",
+   "rev": "8feac540abb781cb1349688c816dc02fae66b49c",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
+   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "776a5a8f9c789395796e442d78a9d4cb9c4c9d03",
+   "rev": "e291aa4de57079b3d2199b9eb7b4b00922b85a7c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
+   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.41",
+   "inputRev": "v0.0.42",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
+   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "577bed1b4cd26b7a3138f67bfdef4ab08cd11f56",
+   "rev": "5695a9fb1a23bf5bee2f94296c2a99f1459a715d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5c11428272fe190b7e726ebe448f93437d057b74",
+   "rev": "7afce91e4fcee25c1ed06dca8d71b82bed396776",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "bd8747df9ee72fca365efa5bd3bd0d8dcd083b9f",
+   "rev": "0a294fe9bf23b396c5cc955054c50b9b652ec5ad",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6d8e3118ab526f8dfcabcbdf9f05dc34e5c423a8",
+   "rev": "1b0072fea2aa6a0ef8ef8b506ec5223b184cb4d0",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

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