bump

leanprover-community · Jun 11, 2024 · 36e783c · 36e783c
1 parent 359ab56
commit 36e783c
Show file tree

Hide file tree

Showing 9 changed files with 18 additions and 17 deletions.
diff --git a/FltRegular/CaseI/Statement.lean b/FltRegular/CaseI/Statement.lean
@@ -205,7 +205,7 @@ theorem auxf' (hp5 : 5 ≤ p) (a b : ℤ) (k₁ k₂ : Fin p) :
     rw [← Finset.card_pos, hcard, card_range]
     exact Nat.sub_pos_of_lt (lt_of_lt_of_le this hp5)
   obtain ⟨i, hi⟩ := hcard
-  refine' ⟨i, sdiff_subset _ _ hi, _⟩
+  refine' ⟨i, sdiff_subset hi, _⟩
   have hi0 : i ≠ 0 := fun h => by simp [h, s] at hi
   have hi1 : i ≠ 1 := fun h => by simp [h, s] at hi
   have hik₁ : i ≠ k₁ := fun h => by simp [h, s] at hi

diff --git a/FltRegular/FltThree/Primes.lean b/FltRegular/FltThree/Primes.lean
@@ -2,7 +2,6 @@
 Copyright (c) 2020 Ruben Van de Velde. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
-import Mathlib.Data.Int.Parity
 import Mathlib.RingTheory.Int.Basic
 
 section

diff --git a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean
@@ -31,7 +31,7 @@ lemma norm_Int_zeta_sub_one : Algebra.norm ℤ (↑(IsPrimitiveRoot.unit' hζ) -
   letI := IsCyclotomicExtension.numberField {p} ℚ K
   haveI : Fact (Nat.Prime p) := hpri
   apply RingHom.injective_int (algebraMap ℤ ℚ)
-  simp [Algebra.coe_norm_int, hζ.sub_one_norm_prime (cyclotomic.irreducible_rat p.2) hp]
+  simp [Algebra.coe_norm_int, hζ.norm_sub_one_of_prime_ne_two' (cyclotomic.irreducible_rat p.2) hp]
 
 @[simp]
 lemma PNat.coe_two : (2 : ℕ+) = (2 : ℕ) := rfl
@@ -179,6 +179,7 @@ lemma quotient_zero_sub_one_comp_aut (σ : 𝓞 K →+* 𝓞 K) :
   · rw [mem_nthRootsFinset p.pos, ← map_pow, hζ.unit'_coe.pow_eq_one, map_one]
   · rw [mem_nthRootsFinset p.pos, hζ.unit'_coe.pow_eq_one]
 
+set_option maxHeartbeats 400000 in
 set_option synthInstance.maxHeartbeats 80000 in
 lemma zeta_sub_one_dvd_trace_sub_smul (x : 𝓞 K) :
     (hζ.unit' - 1 : 𝓞 K) ∣ Algebra.trace ℤ _ x - (p - 1 : ℕ) • x := by

diff --git a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean
@@ -148,7 +148,7 @@ theorem IsPrimitiveRoot.eq_one_mod_sub_of_pow {A : Type _} [CommRing A] [IsDomai
   obtain ⟨k, -, rfl⟩ := hζ.eq_pow_of_pow_eq_one hμ p.pos
   rw [map_pow, eq_one_mod_one_sub, one_pow]
 
-set_option synthInstance.maxHeartbeats 40000 in
+set_option synthInstance.maxHeartbeats 80000 in
 set_option maxHeartbeats 400000 in
 theorem aux {t} {l : 𝓞 K} {f : Fin t → ℤ} {μ : K} (hμ : IsPrimitiveRoot μ p)
     (h : ∑ x : Fin t, f x • (⟨μ, hμ.isIntegral p.pos⟩ : 𝓞 K) ^ (x : ℕ) = l) :
@@ -359,6 +359,7 @@ lemma unit_inv_conj_not_neg_zeta_runity_aux (u : Rˣ) (hp : (p : ℕ).Prime) :
     rw [this a]
   exact (aux hζ hζ hu).trans (aux hζ hζ.inv hu').symm
 
+set_option maxHeartbeats 400000 in
 set_option synthInstance.maxHeartbeats 80000 in
 theorem unit_inv_conj_not_neg_zeta_runity (h : p ≠ 2) (u : Rˣ) (n : ℕ) (hp : (p : ℕ).Prime) :
     u * (unitGalConj K p u)⁻¹ ≠ -hζ.unit' ^ n := by

diff --git a/FltRegular/NumberTheory/Finrank.lean b/FltRegular/NumberTheory/Finrank.lean
@@ -54,9 +54,9 @@ lemma FiniteDimensional.finrank_add_finrank_quotient_le (N : Submodule R M) :
   apply LinearIndependent.finset_card_le_finrank
   · rw [← LinearIndependent.finset_toSet, Finset.coe_union, Finset.coe_image, Finset.coe_image]
     refine LinearIndependent.union ?_ ?_ H
-    · rw [← linearIndependent_image (Subtype.val_injective.injOn _)]
+    · rw [← linearIndependent_image Subtype.val_injective.injOn]
       exact hs'.map' N.subtype N.ker_subtype
-    · rw [← linearIndependent_image (hf.injective.injOn _)]
+    · rw [← linearIndependent_image hf.injective.injOn]
       apply LinearIndependent.of_comp N.mkQ
       convert ht'
       exact funext fun x => hf _

diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean
@@ -56,8 +56,8 @@ theorem Finsupp.prod_congr' {α M N} [Zero M] [CommMonoid N] {f₁ f₂ : α →
     (h : ∀ x, g1 x (f₁ x) = g2 x (f₂ x)) (hg1 : ∀ i, g1 i 0 = 1) (hg2 : ∀ i, g2 i 0 = 1) :
     f₁.prod g1 = f₂.prod g2 := by
   classical
-  rw [f₁.prod_of_support_subset (Finset.subset_union_left _ f₂.support) _ (fun i _ ↦ hg1 i),
-    f₂.prod_of_support_subset (Finset.subset_union_right f₁.support _) _ (fun i _ ↦ hg2 i)]
+  rw [f₁.prod_of_support_subset Finset.subset_union_left _ (fun i _ ↦ hg1 i),
+    f₂.prod_of_support_subset Finset.subset_union_right _ (fun i _ ↦ hg2 i)]
   exact Finset.prod_congr rfl (fun x _ ↦ h x)
 
 lemma LinearIndependent.update {ι} [DecidableEq ι] {R} [CommRing R] [Module R G]
@@ -160,7 +160,7 @@ lemma lemma2 [Module A G] (S : systemOfUnits p G r) (hs : S.IsFundamental) (i :
   let S' : systemOfUnits p G (r + 1) := ⟨Function.update S.units i g,
     LinearIndependent.update' _ _ _ _ _ _ (CyclotomicIntegers.one_sub_zeta_mem_nonZeroDivisors p)
     hg (ha ▸ one_mem A⁰) S.linearIndependent⟩
-  let a' := a.comapDomain (Fin.succAbove i) (Fin.succAbove_right_injective.injOn _)
+  let a' := a.comapDomain (Fin.succAbove i) Fin.succAbove_right_injective.injOn
   have hS' : S'.units ∘ Fin.succAbove i = S.units ∘ Fin.succAbove i
   · ext; simp only [Function.comp_apply, ne_eq, Fin.succAbove_ne, not_false_eq_true,
       Function.update_noteq]

diff --git a/FltRegular/ReadyForMathlib/Homogenization.lean b/FltRegular/ReadyForMathlib/Homogenization.lean
@@ -808,7 +808,7 @@ theorem support_sum_monomial_subset' [DecidableEq ι] {α : Type _} (S : Finset
     apply Finset.union_subset
     · apply Finset.Subset.trans support_monomial_subset _
       rw [Finset.image_insert]
-      convert Finset.subset_union_left _ (Finset.image g S)
+      exact union_subset_left fun ⦃a⦄ a => a
     · apply Finset.Subset.trans hsi _
       rw [Finset.image_insert]
       exact Finset.subset_insert (g s) (Finset.image g S)

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -1,10 +1,10 @@
-{"version": 7,
+{"version": "1.0.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "60d622c124cebcecc000853cdae93f4251f4beb5",
+   "rev": "6a63eb6a326181df29d95a84ce1f16c1145e66d8",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
+   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "70ec1d99be1e1b835d831f39c01b0d14921d2118",
+   "rev": "7e3bd939c6badfcb1e607c0fddb509548baafd05",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "b167323652ab59a5d1b91e906ca4172d1c0474b7",
+   "rev": "7983e959f8f4a79313215720de3ef1eca2d6d474",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "9220d10df329407f9ddb9911812afacd2a7e1af2",
+   "rev": "303e71911e1c040ac1278de13fc2032102888a6e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc2
+leanprover/lean4:v4.9.0-rc1
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.8.0-rc2
		leanprover/lean4:v4.9.0-rc1