bump

leanprover-community · Jan 14, 2024 · ad70c5a · ad70c5a
1 parent fdbd993
commit ad70c5a
Show file tree

Hide file tree

Showing 5 changed files with 8 additions and 12 deletions.
diff --git a/FltRegular/FltThree/FltThree.lean b/FltRegular/FltThree/FltThree.lean
@@ -662,7 +662,7 @@ theorem descent_gcd3 (a b c p q : ℤ) (hp : p ≠ 0) (hq : q ≠ 0) (hcoprime :
         rw [hx, hs]
         congr 1
         ring
-      _ ≤ 2 * 3 * s.natAbs := (Nat.le_mul_of_pos_left (by norm_num))
+      _ ≤ 2 * 3 * s.natAbs := (Nat.le_mul_of_pos_left _ (by norm_num))
       _ = (2 * 3 * s).natAbs := by
         rw [Int.natAbs_mul (2 * 3)]
         rfl

diff --git a/FltRegular/FltThree/Spts.lean b/FltRegular/FltThree/Spts.lean
@@ -304,7 +304,7 @@ theorem factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime a.re a.im) (hod
         Nat.le_of_dvd (Int.natAbs_pos.mpr h8) (Int.natAbs_dvd_natAbs.mpr hwdvd)
       _ ≤ y.natAbs := by
         rw [hz, Int.natAbs_mul]
-        exact Nat.le_mul_of_pos_left (pow_pos hgpos 2)
+        exact Nat.le_mul_of_pos_left _ (pow_pos hgpos 2)
       _ < x.natAbs := h3
 
   · rw [← h6]

diff --git a/FltRegular/NumberTheory/AuxLemmas.lean b/FltRegular/NumberTheory/AuxLemmas.lean
@@ -31,10 +31,6 @@ lemma isIntegralClosure_self {R S : Type*} [CommRing R] [CommRing S] [Algebra R
   algebraMap_injective' := Function.injective_id
   isIntegral_iff := fun {x} ↦ ⟨fun _ ↦ ⟨x, rfl⟩, fun _ ↦ hRS _⟩
 
--- Mathlib/Algebra/Group/Units.lean
-lemma isUnit_iff_eq_one {M : Type*} [Monoid M] [Unique Mˣ] {x : M} : IsUnit x ↔ x = 1 :=
-  ⟨fun h ↦ congr_arg Units.val (Subsingleton.elim (h.unit) 1), fun h ↦ h ▸ isUnit_one⟩
-
 -- Mathlib/NumberTheory/RamificationInertia.lean
 section RamificationInertia
 

diff --git a/FltRegular/NumberTheory/SystemOfUnits.lean b/FltRegular/NumberTheory/SystemOfUnits.lean
@@ -94,7 +94,7 @@ lemma ex_not_mem {R : ℕ} (S : systemOfUnits p G R) (hR : R < r) :
     ((Submodule.span A (Set.range S.units)).restrictScalars ℤ) ?_
   show finrank ℤ (Submodule.span A _) < _
   rw [finrank_spanA p hp G S.units S.linearIndependent, hf, mul_comm]
-  exact Nat.mul_lt_mul hR rfl.le hp.pred_pos
+  exact Nat.mul_lt_mul_of_lt_of_le hR rfl.le hp.pred_pos
 
 lemma existence' [Module A G] {R : ℕ} (S : systemOfUnits p G R) (hR : R < r) :
         Nonempty (systemOfUnits p G (R + 1)) := by

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "c1a3cdf748424810985b479d2712998921c7c797",
+   "rev": "ca91956e8d5c311e00d6a69eb93d5eb5eef9b37d",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "69404390bdc1de946bf0a2e51b1a69f308e56d7a",
+   "rev": "2ae78a474ddf0a39bc2afb9f9f284d2e64f48a70",
    "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": "6f42d2822aba47eb690ed98c508a23e6f0becce2",
+   "rev": "7d051a52c49ac25ee5a04c7a2a70148cc95ddab3",
    "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": "702f3fe16c773ae1e34fbf179342d0877f8cb4f1",
+   "rev": "241edd498be916e377e839d840ebee6ef3c706b0",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -94,7 +94,7 @@
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
-   "rev": "21dd306f65153d58b1e7989e2c3c6e6b48f29811",
+   "rev": "b7fad51b87a5f8fb3a238dc820ec40ebfa2a636e",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",