diff --git a/FltRegular/CaseI/Statement.lean b/FltRegular/CaseI/Statement.lean index 7d058cdd..d9b5f38a 100644 --- a/FltRegular/CaseI/Statement.lean +++ b/FltRegular/CaseI/Statement.lean @@ -45,7 +45,7 @@ theorem may_assume : SlightlyEasier → Statement := by intro h simp [h] at hI have hp5 : 5 ≤ p := by - by_contra' habs + by_contra! habs have : p ∈ Finset.Ioo 2 5 := (Finset.mem_Ioo).2 ⟨Nat.lt_of_le_of_ne hpri.out.two_le hodd.symm, by linarith⟩ fin_cases this @@ -73,7 +73,7 @@ end CaseI theorem ab_coprime {a b c : ℤ} (H : a ^ p + b ^ p = c ^ p) (hpzero : p ≠ 0) (hgcd : ({a, b, c} : Finset ℤ).gcd id = 1) : IsCoprime a b := by rw [← gcd_eq_one_iff_coprime] - by_contra' h + by_contra! h obtain ⟨q, hqpri, hq⟩ := exists_prime_and_dvd h replace hqpri : Prime (q : ℤ) := prime_iff_natAbs_prime.2 (by simp [hqpri]) obtain ⟨n, hn⟩ := hq diff --git a/FltRegular/CaseII/AuxLemmas.lean b/FltRegular/CaseII/AuxLemmas.lean index 64b81189..19fb152e 100644 --- a/FltRegular/CaseII/AuxLemmas.lean +++ b/FltRegular/CaseII/AuxLemmas.lean @@ -143,27 +143,6 @@ theorem isPrincipal_of_isPrincipal_pow_of_Coprime' rw [orderOf_dvd_iff_pow_eq_one, ← map_pow, ClassGroup.mk_eq_one_iff] simp only [Units.val_pow_eq_pow_val, IsUnit.val_unit', hI] -lemma mul_mem_nthRootsFinset {R : Type*} {n : ℕ} [CommRing R] [IsDomain R] - {η₁ : R} (hη₁ : η₁ ∈ nthRootsFinset n R) {η₂ : R} (hη₂ : η₂ ∈ nthRootsFinset n R) : - η₁ * η₂ ∈ nthRootsFinset n R := by - cases n with - | zero => - simp only [Nat.zero_eq, nthRootsFinset_zero, Finset.not_mem_empty] at hη₁ - | succ n => - rw [mem_nthRootsFinset n.succ_pos] at hη₁ hη₂ ⊢ - rw [mul_pow, hη₁, hη₂, one_mul] - -lemma ne_zero_of_mem_nthRootsFinset {R : Type*} {n : ℕ} [CommRing R] [IsDomain R] - {η : R} (hη : η ∈ nthRootsFinset n R) : η ≠ 0 := by - nontriviality R - rintro rfl - cases n with - | zero => - simp only [Nat.zero_eq, nthRootsFinset_zero, Finset.not_mem_empty] at hη - | succ n => - rw [mem_nthRootsFinset n.succ_pos, zero_pow n.succ_pos] at hη - exact zero_ne_one hη - variable (hp : p ≠ 2) open FractionalIdeal in diff --git a/FltRegular/FltThree/FltThree.lean b/FltRegular/FltThree/FltThree.lean index 6d52e4ec..45b2c899 100644 --- a/FltRegular/FltThree/FltThree.lean +++ b/FltRegular/FltThree/FltThree.lean @@ -268,7 +268,7 @@ theorem gcd1or3 (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity : apply basic _ hdprime <;> apply dvd_trans hddvdg <;> rw [hg'] exacts[Int.gcd_dvd_left _ _, Int.gcd_dvd_right _ _] refine' ⟨k, hg, _⟩ - by_contra' H + by_contra! H rw [← pow_mul_pow_sub _ H] at hg have : ¬IsUnit (3 : ℤ) := by rw [Int.isUnit_iff_natAbs_eq] diff --git a/FltRegular/NumberTheory/AuxLemmas.lean b/FltRegular/NumberTheory/AuxLemmas.lean index c0f7c6aa..53028e36 100644 --- a/FltRegular/NumberTheory/AuxLemmas.lean +++ b/FltRegular/NumberTheory/AuxLemmas.lean @@ -973,10 +973,6 @@ lemma RingHom.toIntAlgHom_injective {R₁ R₂} [Ring R₁] [Ring R₂] [Algebra Function.Injective (RingHom.toIntAlgHom : (R₁ →+* R₂) → _) := fun _ _ e ↦ FunLike.ext _ _ (fun x ↦ FunLike.congr_fun e x) --- Mathlib/Data/Polynomial/RingDivision.lean -lemma one_mem_nthRootsFinset {R : Type*} {n : ℕ} [CommRing R] [IsDomain R] (hn : 0 < n) : - 1 ∈ nthRootsFinset n R := by rw [mem_nthRootsFinset hn, one_pow] - -- Mathlib/LinearAlgebra/FiniteDimensional.lean lemma FiniteDimensional.finrank_eq_one_of_linearEquiv {R V} [Field R] [AddCommGroup V] [Module R V] (e : R ≃ₗ[R] V) : finrank R V = 1 := diff --git a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean index 5a2033cc..7965074a 100644 --- a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean +++ b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean @@ -388,7 +388,7 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact (p : ℕ).Prime] {ζ : 𝓞 L} by_cases H : i = ⟨(p : ℕ).pred, pred_lt hp.out.ne_zero⟩ · simp [H.symm, Hi] have hi : ↑i < (p : ℕ).pred := by - by_contra' habs + by_contra! habs simp [le_antisymm habs (le_pred_of_lt (Fin.is_lt i))] at H obtain ⟨y, hy⟩ := hdiv rw [← Equiv.sum_comp (Fin.castIso (succ_pred_prime hp.out)).toEquiv, Fin.sum_univ_castSucc] at hy @@ -440,7 +440,7 @@ theorem dvd_coeff_cycl_integer (hp : (p : ℕ).Prime) {ζ : 𝓞 L} (hζ : IsPri by_cases H : j = ⟨(p : ℕ).pred, pred_lt hp.ne_zero⟩ · simpa [H] using last_dvd have hj : ↑j < (p : ℕ).pred := by - by_contra' habs + by_contra! habs simp [le_antisymm habs (le_pred_of_lt (Fin.is_lt j))] at H obtain ⟨y, hy⟩ := hdiv rw [← Equiv.sum_comp (Fin.castIso (succ_pred_prime hp)).toEquiv, Fin.sum_univ_castSucc] at hy diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index 4f0f042a..9e729c98 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/FltRegular/NumberTheory/Hilbert92.lean @@ -363,7 +363,8 @@ instance : Module.Finite ℤ (Additive <| (𝓞 K)ˣ) := by exact (Submodule.fg_top _).mp this.1 show Module.Finite ℤ (Additive <| NumberField.Units.torsion K) rw [Module.Finite.iff_addGroup_fg, ← GroupFG.iff_add_fg] - infer_instance + -- Note: `infer_instance` timed out as of `v4.4.0-rc1` + exact Group.fg_of_finite local instance : Module.Finite ℤ (Additive <| RelativeUnits k K) := by delta RelativeUnits @@ -598,6 +599,7 @@ lemma h_exists' : ∃ (h : ℕ) (ζ : (𝓞 k)ˣ), refine ⟨j, ζ, IsPrimitiveRoot.coe_coe_iff.mpr (hj' ▸ IsPrimitiveRoot.orderOf ζ.1), fun ε n hn ↦ ?_⟩ have : Fintype H := Set.fintypeSubset (NumberField.Units.torsion k) (by exact this) + have := Finite.of_fintype H -- Note: added to avoid timeout as of `v4.4.0-rc1` obtain ⟨i, hi⟩ := mem_powers_iff_mem_zpowers.mpr (hζ ⟨ε, ⟨_, n, rfl⟩, hn⟩) exact ⟨i, congr_arg Subtype.val hi⟩ diff --git a/FltRegular/NumberTheory/SystemOfUnits.lean b/FltRegular/NumberTheory/SystemOfUnits.lean index 222c71cb..100b9862 100644 --- a/FltRegular/NumberTheory/SystemOfUnits.lean +++ b/FltRegular/NumberTheory/SystemOfUnits.lean @@ -36,7 +36,7 @@ structure systemOfUnits (r : ℕ) namespace systemOfUnits lemma nontrivial (hr : r ≠ 0) : Nontrivial G := by - by_contra' h + by_contra! h rw [not_nontrivial_iff_subsingleton] at h rw [FiniteDimensional.finrank_zero_of_subsingleton] at hf simp only [ge_iff_le, zero_eq_mul, tsub_eq_zero_iff_le] at hf @@ -92,7 +92,7 @@ lemma existence' [Module A G] {R : ℕ} (S : systemOfUnits p G R) (hR : R < r) : obtain ⟨g, hg⟩ := ex_not_mem p hp G r hf S hR refine ⟨⟨Fin.cases g S.units, ?_⟩⟩ refine LinearIndependent.fin_cons' g S.units S.linearIndependent (fun a y hy ↦ ?_) - by_contra' ha + by_contra! ha letI := Fact.mk hp obtain ⟨n, h0, f, Hf⟩ := CyclotomicIntegers.exists_dvd_int p _ ha replace hy := congr_arg (f • ·) hy diff --git a/lake-manifest.json b/lake-manifest.json index 6a5916d4..6adf8d85 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "415a6731db08f4d98935e5d80586d5a5499e02af", + "rev": "9e37a01f8590f81ace095b56710db694b5bf8ca0", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -13,7 +13,7 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755", + "rev": "ccba5d35d07a448fab14c0e391c8105df6e2564c", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "c7cff4551258d31c0d2d453b3f9cbca757d445f1", + "rev": "3141402ba5a5f0372d2378fd75a481bc79a74ecf", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "153b6b05d3c8191a7ea093279d19ee4d601b0962", + "rev": "db61ac24294a5e37c17d73df71770a59856a38b5", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/lean-toolchain b/lean-toolchain index 5cadc9da..91ccf6ac 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.3.0 +leanprover/lean4:v4.4.0-rc1