bump

Author: riccardobrasca

FltRegular/NumberTheory/Finrank.lean

@@ -181,9 +181,8 @@ lemma FiniteDimensional.exists_of_finrank_lt [IsDomain R] [IsPrincipalIdealRing
     ∃ m : M, ∀ r : R, r ≠ 0 → r • m ∉ N := by
   obtain ⟨s, hs, hs'⟩ :=
     FiniteDimensional.exists_finset_card_eq_finrank_and_linearIndependent R (M ⧸ N)
-  obtain ⟨v, hv⟩ : s.Nonempty
-  · rwa [Finset.nonempty_iff_ne_empty, ne_eq, ← Finset.card_eq_zero, hs,
-      FiniteDimensional.finrank_quotient, tsub_eq_zero_iff_le, not_le]
+  obtain ⟨v, hv⟩ : s.Nonempty := by rwa [Finset.nonempty_iff_ne_empty, ne_eq, ← Finset.card_eq_zero,
+    hs, FiniteDimensional.finrank_quotient, tsub_eq_zero_iff_le, not_le]
   obtain ⟨v, rfl⟩ := N.mkQ_surjective v
   use v
   intro r hr

FltRegular/NumberTheory/Hilbert92.lean

@@ -747,7 +747,6 @@ lemma Hilbert92ish_aux2 (E : (𝓞 K)ˣ) (ζ : k) (hE : algebraMap k K ζ = E /
   · exact even_iff_two_dvd.1 (hp.even_sub_one hpodd)
   · simp
 
-
 attribute [-instance] Fintype.decidableForallFintype
 lemma unit_to_U_pow (x) (n : ℕ) : mkG (x ^ n) = n • (mkG x) := by
   induction n with
@@ -838,8 +837,8 @@ lemma Hilbert92ish (hpodd : (p : ℕ) ≠ 2) :
       · refine ha'' ?_ this
         ext
         simpa using hζ
-      obtain ⟨ε', hε'⟩ : ∃ ε' : (𝓞 k)ˣ, ε' ^ (p : ℕ) = NE
-      · rw [← (Nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd] at ha'
+      obtain ⟨ε', hε'⟩ : ∃ ε' : (𝓞 k)ˣ, ε' ^ (p : ℕ) = NE := by
+        rw [← (Nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd] at ha'
         obtain ⟨α, β, hαβ⟩ := ha'
         choose ι' hι' using hε'
         rw [Fin.sum_univ_castSucc] at ha
@@ -852,8 +851,9 @@ lemma Hilbert92ish (hpodd : (p : ℕ) ≠ 2) :
         exact ⟨_, ha.symm⟩
       have hζ'' := (hζ.pow (p ^ h.succ).pos (pow_succ _ _)).map_of_injective
         (algebraMap k K).injective
-      obtain ⟨ε'', hε''⟩ : ∃ ε'' : (𝓞 k)ˣ, E = Units.map (algebraMap (𝓞 k) (𝓞 K)).toMonoidHom ε''
-      · rw [← hε', map_pow, eq_comm, ← mul_inv_eq_one, ← inv_pow, ← mul_pow] at NE_p_pow
+      obtain ⟨ε'', hε''⟩ :
+          ∃ ε'' : (𝓞 k)ˣ, E = Units.map (algebraMap (𝓞 k) (𝓞 K)).toMonoidHom ε'' := by
+        rw [← hε', map_pow, eq_comm, ← mul_inv_eq_one, ← inv_pow, ← mul_pow] at NE_p_pow
         apply_fun ((↑) : (𝓞 K)ˣ → K) at NE_p_pow
         simp only [RingHom.toMonoidHom_eq_coe, Units.val_pow_eq_pow_val, Units.val_mul,
           Units.coe_map_inv, MonoidHom.coe_coe, SubmonoidClass.coe_pow, Submonoid.coe_mul,

FltRegular/NumberTheory/KummersLemma/Field.lean

@@ -239,8 +239,9 @@ lemma separable_poly_aux {L : Type*} [Field L] [Algebra K L] (α : L)
   refine separable_prod' ?_ (fun _ _ => separable_X_sub_C)
   intros i hi j hj hij
   apply isCoprime_X_sub_C_of_isUnit_sub
-  obtain ⟨v, hv⟩ : Associated (hζ.unit' - 1 : 𝓞 K) ((hζ.unit' : 𝓞 K) ^ j - (hζ.unit' : 𝓞 K) ^ i)
-  · refine hζ.unit'_coe.associated_sub_one hpri.out ?_ ?_ ?_
+  obtain ⟨v, hv⟩ :
+      Associated (hζ.unit' - 1 : 𝓞 K) ((hζ.unit' : 𝓞 K) ^ j - (hζ.unit' : 𝓞 K) ^ i) := by
+    refine hζ.unit'_coe.associated_sub_one hpri.out ?_ ?_ ?_
     · rw [mem_nthRootsFinset p.pos, ← pow_mul, mul_comm, pow_mul, hζ.unit'_coe.pow_eq_one, one_pow]
     · rw [mem_nthRootsFinset p.pos, ← pow_mul, mul_comm, pow_mul, hζ.unit'_coe.pow_eq_one, one_pow]
     · exact mt (hζ.unit'_coe.injOn_pow hj hi) hij.symm

FltRegular/NumberTheory/KummersLemma/KummersLemma.lean

@@ -50,8 +50,8 @@ theorem eq_pow_prime_of_unit_of_congruent (u : (𝓞 K)ˣ)
     ∃ v, u = v ^ (p : ℕ) := by
   haveI : Fact (Nat.Prime p) := hpri
   obtain ⟨ζ, hζ⟩ := IsCyclotomicExtension.exists_prim_root (S := {p}) ℚ (B := K) (n := p) rfl
-  obtain ⟨x, hx⟩ : (p : 𝓞 K) ∣ (↑(u ^ (p - 1 : ℕ)) : 𝓞 K) - 1
-  · obtain ⟨n, hn⟩ := hcong
+  obtain ⟨x, hx⟩ : (p : 𝓞 K) ∣ (↑(u ^ (p - 1 : ℕ)) : 𝓞 K) - 1 := by
+    obtain ⟨n, hn⟩ := hcong
     have hn' : (p : ℤ) ∣ n ^ (p - 1 : ℕ) - 1
     · refine Int.modEq_iff_dvd.mp (Int.ModEq.pow_card_sub_one_eq_one hpri.out (n := n) ?_).symm
       rw [isCoprime_comm, (Nat.prime_iff_prime_int.mp hpri.out).coprime_iff_not_dvd]

FltRegular/NumberTheory/QuotientTrace.lean

@@ -169,8 +169,8 @@ lemma comap_map_eq_map_of_isLocalization_algebraMapSubmonoid :
   rw [IsScalarTower.algebraMap_eq R S Sₚ, ← Ideal.map_map, eq_comm]
   apply Ideal.le_comap_map.antisymm
   intro x hx
-  obtain ⟨α, hα, hαx⟩ : ∃ α ∉ p, α • x ∈ pS
-  · have ⟨⟨y, s⟩, hy⟩ := (IsLocalization.mem_map_algebraMap_iff
+  obtain ⟨α, hα, hαx⟩ : ∃ α ∉ p, α • x ∈ pS := by
+    have ⟨⟨y, s⟩, hy⟩ := (IsLocalization.mem_map_algebraMap_iff
       (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ).mp hx
     rw [← map_mul,
       IsLocalization.eq_iff_exists (Algebra.algebraMapSubmonoid S p.primeCompl)] at hy
@@ -179,8 +179,8 @@ lemma comap_map_eq_map_of_isLocalization_algebraMapSubmonoid :
     refine ⟨α, hα, ?_⟩
     rw [Algebra.smul_def, e, Submonoid.coe_mul, mul_assoc, mul_comm _ x, hc]
     exact Ideal.mul_mem_left _ _ y.prop
-  obtain ⟨β, γ, hγ, hβ⟩ : ∃ β γ, γ ∈ p ∧ β * α = 1 + γ
-  · obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹
+  obtain ⟨β, γ, hγ, hβ⟩ : ∃ β γ, γ ∈ p ∧ β * α = 1 + γ := by
+    obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹
     refine ⟨β, β * α - 1, ?_, ?_⟩
     · rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one,
         map_mul, hβ, inv_mul_cancel, sub_self]
@@ -210,8 +210,8 @@ def quotMapEquivQuotMapMaximalIdealOfIsLocalization : S ⧸ pS ≃+* Sₚ ⧸ pS
     obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective
       (Algebra.algebraMapSubmonoid S p.primeCompl) x
     obtain ⟨α, hα : α ∉ p, e⟩ := s.prop
-    obtain ⟨β, γ, hγ, hβ⟩ : ∃ β γ, γ ∈ p ∧ α * β = 1 + γ
-    · obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹
+    obtain ⟨β, γ, hγ, hβ⟩ : ∃ β γ, γ ∈ p ∧ α * β = 1 + γ := by
+      obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹
       refine ⟨β, α * β - 1, ?_, ?_⟩
       · rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one,
           map_mul, hβ, mul_inv_cancel, sub_self]

lake-manifest.json

@@ -31,10 +31,10 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
+   "rev": "fc8f85bab627d5196b2342bd2f08c0ace749ec89",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.36",
+   "inputRev": "v0.0.37",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "0eb87504b21018e2a4200d4417d57fc06c99c960",
+   "rev": "397d87803ee60c11623fdd680199366acaaedaef",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.9.0-rc2
+leanprover/lean4:v4.9.0-rc3