bump

FltRegular/CaseII/AuxLemmas.lean

@@ -117,9 +117,8 @@ lemma pow_dvd_pow_iff_dvd {M : Type*} [CancelCommMonoidWithZero M] [UniqueFactor
     {a b : M} {x : ℕ} (h' : x ≠ 0) : a ^ x ∣ b ^ x ↔ a ∣ b := by
   classical
   by_cases ha : a = 0
-  · rw [ha, zero_pow (Nat.pos_iff_ne_zero.mpr h'), zero_dvd_iff, zero_dvd_iff,
-      pow_eq_zero_iff (Nat.pos_iff_ne_zero.mpr h')]
-  have ha' : a ^ x ≠ 0 := (pow_eq_zero_iff (Nat.pos_iff_ne_zero.mpr h')).not.mpr ha
+  · rw [ha, zero_pow h', zero_dvd_iff, zero_dvd_iff, pow_eq_zero_iff h']
+  have ha' : a ^ x ≠ 0 := (pow_ne_zero_iff h').mpr ha
   rw [dvd_iff_multiplicity_le ha, dvd_iff_multiplicity_le ha']
   refine forall₂_congr (fun p hp ↦ ?_)
   simp_rw [multiplicity.pow hp, ← PartENat.withTopEquiv_le]

FltRegular/CaseII/InductionStep.lean

@@ -224,8 +224,8 @@ lemma prod_c : ∏ η in Finset.attach (nthRootsFinset p (𝓞 K)), 𝔠 η = (
     Finset.prod_mul_distrib, Finset.prod_const, Finset.card_attach,
     hζ.unit'_coe.card_nthRootsFinset] at e'
   rw [← mul_right_inj'
-    ((pow_ne_zero_iff hpri.out.pos).mpr (m_ne_zero hζ e hy) : _),
-    ← mul_left_inj' ((pow_ne_zero_iff hpri.out.pos).mpr (p_ne_zero hζ) : _), e',
+    ((pow_ne_zero_iff hpri.out.ne_zero).mpr (m_ne_zero hζ e hy) : _),
+    ← mul_left_inj' ((pow_ne_zero_iff hpri.out.ne_zero).mpr (p_ne_zero hζ) : _), e',
     exists_ideal_pow_eq_c_aux]
 
 lemma exists_ideal_pow_eq_c : ∃ I : Ideal (𝓞 K), (𝔠 η) = I ^ (p : ℕ) := by
@@ -437,8 +437,8 @@ lemma x_plus_y_mul_ne_zero : x + y * η ≠ 0 := by
     simp_rw [mul_comm _ y]
     exact Finset.dvd_prod_of_mem _ η.prop
   rw [hη, zero_dvd_iff, e] at this
-  simp only [mul_eq_zero, Units.ne_zero, PNat.pos,
-    pow_eq_zero_iff, add_pos_iff, or_true, false_or] at this
+  simp only [mul_eq_zero, Units.ne_zero, pow_eq_zero_iff p.ne_zero, add_pos_iff, or_true, false_or]
+    at this
   rw [this.resolve_left (pow_ne_zero (m + 1) (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt))] at hz
   exact hz (dvd_zero _)
 

FltRegular/NumberTheory/AuxLemmas.lean

@@ -10,17 +10,6 @@ This file contains lemmas that should go somewhere in a file in mathlib.
 -/
 open BigOperators UniqueFactorizationMonoid
 
--- Mathlib/RingTheory/DedekindDomain/Ideal.lean
-lemma Ideal.mem_normalizedFactors_iff {R} [CommRing R] [IsDedekindDomain R] [DecidableEq (Ideal R)]
-      {p I : Ideal R} (hI : I ≠ ⊥) :
-    p ∈ normalizedFactors I ↔ p.IsPrime ∧ I ≤ p := by
-  rw [← Ideal.dvd_iff_le]
-  by_cases hp : p = 0
-  · simp only [hp, zero_not_mem_normalizedFactors, isUnit_zero_iff, one_eq_top, zero_dvd_iff,
-      false_iff, not_and]
-    exact fun _ ↦ hI
-  · rwa [UniqueFactorizationMonoid.mem_normalizedFactors_iff hI, prime_iff_isPrime]
-
 -- Mathlib/RingTheory/Ideal/Operations.lean
 lemma Ideal.comap_coe {R S F : Type*} [Semiring R] [Semiring S] [RingHomClass F R S]
   (f : F) (I : Ideal S) : I.comap (f : R →+* S) = I.comap f := rfl

FltRegular/NumberTheory/Different.lean

@@ -36,7 +36,7 @@ variable [IsDedekindDomain A] [IsDedekindDomain B] [IsFractionRing B L]
 
 lemma pow_sub_one_dvd_differentIdeal_aux
     [NoZeroSMulDivisors A B] [Module.Finite A B]
-    {p : Ideal A} [p.IsMaximal] (P : Ideal B) (e : ℕ) (he : 0 < e) (hp : p ≠ ⊥)
+    {p : Ideal A} [p.IsMaximal] (P : Ideal B) (e : ℕ) (he : e ≠ 0) (hp : p ≠ ⊥)
     (hP : P ^ e ∣ p.map (algebraMap A B)) : P ^ (e - 1) ∣ differentIdeal A B := by
   obtain ⟨a, ha⟩ := (pow_dvd_pow _ (Nat.sub_le e 1)).trans hP
   have hp' := (Ideal.map_eq_bot_iff_of_injective
@@ -50,7 +50,7 @@ lemma pow_sub_one_dvd_differentIdeal_aux
     apply_fun (· ^ e : Ideal B → _) at ha
     apply_fun (· ^ (e - 1) : Ideal B → _) at hb
     simp only [mul_pow, ← pow_mul, mul_comm e] at ha hb
-    conv_lhs at ha => rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr he.ne.symm)]
+    conv_lhs at ha => rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr he)]
     rw [pow_add, hb, mul_assoc, mul_right_inj' (pow_ne_zero _ hPbot), pow_one, mul_comm] at ha
     exact ⟨_, ha.symm⟩
   suffices : ∀ x ∈ a, Algebra.intTrace A B x ∈ p
@@ -100,5 +100,4 @@ lemma pow_sub_one_dvd_differentIdeal
     Module.Finite_of_isLocalization A B _ _ A⁰
   by_cases he : e = 0
   · rw [he, pow_zero]; exact one_dvd _
-  rw [← Ne.def, ← Nat.pos_iff_ne_zero] at he
   exact pow_sub_one_dvd_differentIdeal_aux A (FractionRing A) (FractionRing B) B P e he hp hP

FltRegular/NumberTheory/GaloisPrime.lean

@@ -364,11 +364,11 @@ lemma prod_smul_primesOver [IsGalois K L] (p : Ideal R) (P : primesOver S p) [p.
       Ideal.comap_bot_of_injective _ (galRestrict R K L S _).injective, Finset.prod_const,
       Ideal.map_bot, Ideal.inertiaDegIn_bot R S (IsIntegralClosure.isIntegral_algebra R L)]
     refine (zero_pow ?_).trans (zero_pow ?_).symm
-    · rw [pos_iff_ne_zero, Finset.card_univ, Ne.def, Fintype.card_eq_zero_iff]
+    · rw [Finset.card_univ, Ne.def, Fintype.card_eq_zero_iff]
       simp only [not_isEmpty_of_nonempty, not_false_eq_true]
     · have hR := not_imp_not.mp (Ring.ne_bot_of_isMaximal_of_not_isField ‹_›) rfl
       letI : Field R := hR.toField
-      exact finrank_pos
+      exact finrank_pos.ne'
   rw [← prod_primesOverFinset_pow_ramificationIdxIn K L p hp]
   delta Finset.prod
   rw [← pow_mul, ← Multiset.prod_nsmul, Multiset.map_id']

FltRegular/NumberTheory/Hilbert92.lean

@@ -784,11 +784,10 @@ lemma Hilbert92ish_aux2 (E : (𝓞 K)ˣ) (ζ : k) (hE : algebraMap k K ζ = E /
   conv =>
     enter [1, 2, i]
     rw [h1 i, mul_comm]
-  rw [prod_mul_distrib, prod_const, card_range, prod_pow_eq_pow_sum]
-  simp only [inv_pow, ne_eq, PNat.pos, pow_eq_zero_iff, ZeroMemClass.coe_eq_zero, Units.ne_zero,
-    not_false_eq_true, mul_eq_left₀, inv_eq_one]
-  rw [sum_range_id, Nat.mul_div_assoc, pow_mul, ← map_pow, hζ, map_one, one_pow]
-  exact even_iff_two_dvd.1 (hp.even_sub_one hpodd)
+  rw [prod_mul_distrib, prod_const, card_range, prod_pow_eq_pow_sum, inv_pow, mul_eq_left₀,
+    inv_eq_one, sum_range_id, Nat.mul_div_assoc, pow_mul, ← map_pow, hζ, map_one, one_pow]
+  · exact even_iff_two_dvd.1 (hp.even_sub_one hpodd)
+  · simp
 
 
 attribute [-instance] instDecidableEq Fintype.decidableForallFintype

FltRegular/NumberTheory/KummersLemma/Field.lean

@@ -108,15 +108,16 @@ theorem aeval_poly {L : Type*} [Field L] [Algebra K L] (α : L)
     aeval (((1 : L) - ζ ^ m • α) / (algebraMap K L (ζ - 1))) (poly hp hζ u hcong) = 0 := by
   have hζ' : algebraMap K L ζ - 1 ≠ 0
   · simpa using (algebraMap K L).injective.ne (hζ.sub_one_ne_zero hpri.out.one_lt)
+  rw [map_sub, map_one]
   have := congr_arg (aeval ((1 - ζ ^ m • α) / (algebraMap K L (ζ - 1))))
     (poly_spec hp hζ u hcong)
   simp only [map_sub, map_one, map_pow, map_mul, aeval_C, Subalgebra.algebraMap_eq, smul_pow,
     RingHom.coe_comp, RingHom.coe_coe, Subalgebra.coe_val, Function.comp_apply, e,
     IsPrimitiveRoot.val_unit'_coe, map_add, aeval_X, ← mul_div_assoc, mul_div_cancel_left _ hζ',
     sub_sub_cancel_left, (hpri.out.odd_of_ne_two (PNat.coe_injective.ne hp)).neg_pow] at this
-  rw [← pow_mul, mul_comm m, pow_mul, hζ.pow_eq_one, one_pow, one_smul] at this
-  simp only [add_left_neg, mul_eq_zero, PNat.pos, pow_eq_zero_iff, hζ', false_or] at this
-  simpa only [map_sub, map_one] using this
+  rw [← pow_mul, mul_comm m, pow_mul, hζ.pow_eq_one, one_pow, one_smul, add_left_neg,
+    mul_eq_zero] at this
+  exact this.resolve_left (pow_ne_zero _ hζ')
 
 def polyRoot {L : Type*} [Field L] [Algebra K L] (α : L)
     (e : α ^ (p : ℕ) = algebraMap K L u) (m : ℕ) : 𝓞 L :=
@@ -130,7 +131,7 @@ theorem roots_poly {L : Type*} [Field L] [Algebra K L] (α : L)
       (Finset.range (p : ℕ)).val.map
         (fun i ↦ ((1 : L) - ζ ^ i • α) / (algebraMap K L (ζ - 1))) := by
   by_cases hα : α = 0
-  · rw [hα, zero_pow p.pos] at e
+  · rw [hα, zero_pow p.ne_zero] at e
     exact (((algebraMap (𝓞 K) L).isUnit_map u.isUnit).ne_zero e.symm).elim
   have hζ' : algebraMap K L ζ - 1 ≠ 0
   · simpa using (algebraMap K L).injective.ne (hζ.sub_one_ne_zero hpri.out.one_lt)

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "0d0ac1c43e1ec1965e0806af9e7a32999ea31096",
+   "rev": "a11bdfc39e95fa5b09e06638a43bd8bd2eddce12",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "cea4f7aabfdbf6d0967d580d38017fb0469b84b9",
+   "rev": "fdcd4ee3a122bf44fc58dc912fb5243ea4fe8916",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,