diff --git a/FltRegular/CaseI/Statement.lean b/FltRegular/CaseI/Statement.lean index 320a3fce..3fb65546 100644 --- 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 index f002344e..ab67ed26 100644 --- 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 index 4de92c71..737c0b18 100644 --- 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 index c3c74b12..c7c41c20 100644 --- 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 index 70240703..b859ec30 100644 --- 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 index 71e0e4b2..d17d017e 100644 --- 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 index 0474015a..4f083ffa 100644 --- 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 index c5dccace..e7dc87df 100644 --- 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 index 78f39e21..0ba3faf8 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.8.0-rc2 +leanprover/lean4:v4.9.0-rc1