bump

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

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

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]

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 :=

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

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⟩
 

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

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,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.3.0
+leanprover/lean4:v4.4.0-rc1