chore: adaptations for nightly-2024-05-11

Archive/Examples/MersennePrimes.lean

@@ -19,6 +19,7 @@ for ideas about extending this to larger Mersenne primes.
 -- The Lucas-Lehmer test does not apply to `mersenne 2`
 example : ¬ LucasLehmerTest 2 := by norm_num
 
+unseal Nat.minFacAux in
 example : (mersenne 2).Prime := by decide
 
 example : (mersenne 3).Prime :=

Archive/Imo/Imo2005Q4.lean

@@ -24,6 +24,7 @@ def a (n : ℕ) : ℤ :=
   2 ^ n + 3 ^ n + 6 ^ n - 1
 #align imo2005_q4.a IMO2005Q4.a
 
+unseal Nat.minFacAux in
 /-- Key lemma (a modular arithmetic calculation):  Given a prime `p` other than `2` or `3`, the
 `(p - 2)`th term of the sequence has `p` as a factor. -/
 theorem find_specified_factor {p : ℕ} (hp : Nat.Prime p) (hp2 : p ≠ 2) (hp3 : p ≠ 3) :

Archive/Wiedijk100Theorems/AbelRuffini.lean

@@ -162,6 +162,7 @@ theorem complex_roots_Phi (h : (Φ ℚ a b).Separable) : Fintype.card ((Φ ℚ a
   (card_rootSet_eq_natDegree h (IsAlgClosed.splits_codomain _)).trans (natDegree_Phi a b)
 #align abel_ruffini.complex_roots_Phi AbelRuffini.complex_roots_Phi
 
+unseal Nat.minFacAux in
 theorem gal_Phi (hab : b < a) (h_irred : Irreducible (Φ ℚ a b)) :
     Bijective (galActionHom (Φ ℚ a b) ℂ) := by
   apply galActionHom_bijective_of_prime_degree' h_irred

Mathlib/CategoryTheory/Filtered/Small.lean

@@ -75,8 +75,12 @@ private noncomputable def inductiveStepRealization (n : ℕ)
   | (InductiveStep.coeq _ _ _ _ f g) => coeq f g
 
 /-- All steps of building the abstract filtered closure together with the realization function,
-    as a function of `ℕ`. -/
-private noncomputable def bundledAbstractFilteredClosure : ℕ → Σ t : Type (max v w), t → C
+    as a function of `ℕ`.
+
+   The function is defined by well-founded recursion, but we really want to use its
+   definitional equalities in the proofs below, so lets make it semireducible.  -/
+@[semireducible] private noncomputable def bundledAbstractFilteredClosure :
+    ℕ → Σ t : Type (max v w), t → C
   | 0 => ⟨ULift.{v} α, f ∘ ULift.down⟩
   | (n + 1) => ⟨_, inductiveStepRealization (n + 1) (fun m _ => bundledAbstractFilteredClosure m)⟩
 
@@ -204,8 +208,12 @@ private noncomputable def inductiveStepRealization (n : ℕ)
   | (InductiveStep.eq _ _ _ _ f g) => eq f g
 
 /-- Implementation detail for the instance
-    `EssentiallySmall.{max v w} (FullSubcategory (CofilteredClosure f))`. -/
-private noncomputable def bundledAbstractCofilteredClosure : ℕ → Σ t : Type (max v w), t → C
+   `EssentiallySmall.{max v w} (FullSubcategory (CofilteredClosure f))`.
+
+   The function is defined by well-founded recursion, but we really want to use its
+   definitional equalities in the proofs below, so lets make it semireducible.  -/
+@[semireducible] private noncomputable def bundledAbstractCofilteredClosure :
+    ℕ → Σ t : Type (max v w), t → C
   | 0 => ⟨ULift.{v} α, f ∘ ULift.down⟩
   | (n + 1) => ⟨_, inductiveStepRealization (n + 1) (fun m _ => bundledAbstractCofilteredClosure m)⟩
 

Mathlib/Computability/Partrec.lean

@@ -735,7 +735,9 @@ theorem nat_strong_rec (f : α → ℕ → σ) {g : α → List σ → Option σ
 theorem list_ofFn :
     ∀ {n} {f : Fin n → α → σ},
       (∀ i, Computable (f i)) → Computable fun a => List.ofFn fun i => f i a
-  | 0, _, _ => const []
+  | 0, _, _ => by
+    simp only [List.ofFn_zero]
+    exact const []
   | n + 1, f, hf => by
     simp only [List.ofFn_succ]
     exact list_cons.comp (hf 0) (list_ofFn fun i => hf i.succ)

Mathlib/Data/Fin/Basic.lean

@@ -781,6 +781,7 @@ theorem zero_ne_one' [NeZero n] : (0 : Fin (n + 1)) ≠ 1 := Fin.ne_of_lt one_po
 
 #align fin.succ_zero_eq_one' Fin.succ_zero_eq_one
 
+unseal Nat.modCore in
 /--
 The `Fin.succ_one_eq_two` in `Lean` only applies in `Fin (n+2)`.
 This one instead uses a `NeZero n` typeclass hypothesis.

Mathlib/Data/Fin/VecNotation.lean

@@ -211,15 +211,18 @@ theorem cons_val_one (x : α) (u : Fin m.succ → α) : vecCons x u 1 = vecHead
   rfl
 #align matrix.cons_val_one Matrix.cons_val_one
 
+unseal Nat.modCore in
 @[simp]
 theorem cons_val_two (x : α) (u : Fin m.succ.succ → α) : vecCons x u 2 = vecHead (vecTail u) :=
   rfl
 
+unseal Nat.modCore in
 @[simp]
 lemma cons_val_three (x : α) (u : Fin m.succ.succ.succ → α) :
     vecCons x u 3 = vecHead (vecTail (vecTail u)) :=
   rfl
 
+unseal Nat.modCore in
 @[simp]
 lemma cons_val_four (x : α) (u : Fin m.succ.succ.succ.succ → α) :
     vecCons x u 4 = vecHead (vecTail (vecTail (vecTail u))) :=
@@ -361,9 +364,7 @@ theorem vecAlt1_vecAppend (v : Fin (n + 1) → α) : vecAlt1 rfl (vecAppend rfl
     simp only [Nat.zero_eq, zero_add, Nat.lt_one_iff] at hi; subst i; rfl
   | succ n =>
     split_ifs with h <;> simp_rw [bit1, bit0] <;> congr
-    · rw [Fin.val_mk] at h
-      rw [Nat.mod_eq_of_lt (Nat.lt_of_succ_lt h)]
-      erw [Nat.mod_eq_of_lt h]
+    · simp [Nat.mod_eq_of_lt, h]
     · rw [Fin.val_mk, not_lt] at h
       simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk, Nat.mod_add_mod, Fin.val_one,
         Nat.mod_eq_sub_mod h, show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by omega)]

Mathlib/Data/List/Basic.lean

@@ -940,7 +940,7 @@ decreasing_by
 @[simp]
 theorem reverseRecOn_nil {motive : List α → Sort*} (nil : motive [])
     (append_singleton : ∀ (l : List α) (a : α), motive l → motive (l ++ [a])) :
-    reverseRecOn [] nil append_singleton = nil := by unfold reverseRecOn; rfl
+    reverseRecOn [] nil append_singleton = nil := reverseRecOn.eq_1 ..
 
 -- `unusedHavesSuffices` is getting confused by the unfolding of `reverseRecOn`
 @[simp, nolint unusedHavesSuffices]
@@ -986,8 +986,7 @@ termination_by l => l.length
 theorem bidirectionalRec_nil {motive : List α → Sort*}
     (nil : motive []) (singleton : ∀ a : α, motive [a])
     (cons_append : ∀ (a : α) (l : List α) (b : α), motive l → motive (a :: (l ++ [b]))) :
-    bidirectionalRec nil singleton cons_append [] = nil := by
-  unfold bidirectionalRec; rfl
+    bidirectionalRec nil singleton cons_append [] = nil := bidirectionalRec.eq_1 ..
 
 
 @[simp]

Mathlib/Data/Nat/Choose/Multinomial.lean

@@ -213,6 +213,7 @@ theorem multinomial_filter_ne [DecidableEq α] (a : α) (m : Multiset α) :
     · rw [not_ne_iff.1 h, Function.update_same]
 #align multiset.multinomial_filter_ne Multiset.multinomial_filter_ne
 
+unseal Nat.div in
 @[simp]
 theorem multinomial_zero [DecidableEq α] : multinomial (0 : Multiset α) = 1 := rfl
 
@@ -224,6 +225,7 @@ namespace Finset
 
 variable {α : Type*} [DecidableEq α] (s : Finset α) {R : Type*}
 
+unseal Nat.div in
 /-- The multinomial theorem
 
   Proof is by induction on the number of summands.
@@ -247,7 +249,6 @@ theorem sum_pow_of_commute [Semiring R] (x : α → R)
       · have : Zero (Sym α 0) := Sym.instZeroSym
         exact ⟨0, by simp [eq_iff_true_of_subsingleton]⟩
       convert (@one_mul R _ _).symm
-      dsimp only
       convert @Nat.cast_one R _
     · rw [_root_.pow_succ, mul_zero]
       -- Porting note: Lean cannot infer this instance by itself

Mathlib/Data/Nat/Factorization/Basic.lean

@@ -114,10 +114,12 @@ theorem factorization_inj : Set.InjOn factorization { x : ℕ | x ≠ 0 } := fun
   eq_of_factorization_eq ha hb fun p => by simp [h]
 #align nat.factorization_inj Nat.factorization_inj
 
+unseal Nat.factors in
 @[simp]
 theorem factorization_zero : factorization 0 = 0 := by decide
 #align nat.factorization_zero Nat.factorization_zero
 
+unseal Nat.factors in
 @[simp]
 theorem factorization_one : factorization 1 = 0 := by decide
 #align nat.factorization_one Nat.factorization_one

Mathlib/Data/Nat/Factors.lean

@@ -36,8 +36,8 @@ def factors : ℕ → List ℕ
   | 1 => []
   | k + 2 =>
     let m := minFac (k + 2)
-    have : (k + 2) / m < (k + 2) := factors_lemma
     m :: factors ((k + 2) / m)
+decreasing_by show (k + 2) / m < (k + 2); exact factors_lemma
 #align nat.factors Nat.factors
 
 @[simp]

Mathlib/Data/Nat/PrimeFin.lean

@@ -56,7 +56,9 @@ lemma pos_of_mem_primeFactors (hp : p ∈ n.primeFactors) : 0 < p :=
 lemma le_of_mem_primeFactors (h : p ∈ n.primeFactors) : p ≤ n :=
   le_of_dvd (mem_primeFactors.1 h).2.2.bot_lt <| dvd_of_mem_primeFactors h
 
+unseal Nat.factors in
 @[simp] lemma primeFactors_zero : primeFactors 0 = ∅ := rfl
+unseal Nat.factors in
 @[simp] lemma primeFactors_one : primeFactors 1 = ∅ := rfl
 
 @[simp] lemma primeFactors_eq_empty : n.primeFactors = ∅ ↔ n = 0 ∨ n = 1 := by

Mathlib/Data/Nat/Squarefree.lean

@@ -254,6 +254,7 @@ theorem squarefree_iff_minSqFac {n : ℕ} : Squarefree n ↔ n.minSqFac = none :
 instance : DecidablePred (Squarefree : ℕ → Prop) := fun _ =>
   decidable_of_iff' _ squarefree_iff_minSqFac
 
+unseal Nat.factors in
 theorem squarefree_two : Squarefree 2 := by
   rw [squarefree_iff_nodup_factors] <;> decide
 #align nat.squarefree_two Nat.squarefree_two

Mathlib/Data/Rat/Defs.lean

@@ -87,6 +87,7 @@ lemma mkRat_eq_divInt (n d) : mkRat n d = n /. d := rfl
 #align rat.zero_mk_nat Rat.zero_mkRat
 #align rat.zero_mk Rat.zero_divInt
 
+unseal Nat.gcd in
 @[simp] lemma mk'_zero (d) (h : d ≠ 0) (w) : mk' 0 d h w = 0 := by congr
 
 @[simp]

Mathlib/Data/ZMod/Basic.lean

@@ -616,7 +616,7 @@ theorem cast_zmod_eq_zero_iff_of_le {m n : ℕ} [NeZero m] (h : m ≤ n) (a : ZM
   exact Injective.eq_iff' (cast_injective_of_le h) rfl
 
 -- Porting note: commented
--- attribute [local semireducible] Int.NonNeg
+-- unseal Int.NonNeg
 
 @[simp]
 theorem natCast_toNat (p : ℕ) : ∀ {z : ℤ} (_h : 0 ≤ z), (z.toNat : ZMod p) = z

Mathlib/GroupTheory/CommutingProbability.lean

@@ -166,9 +166,11 @@ def reciprocalFactors (n : ℕ) : List ℕ :=
   else
     n % 4 * n :: reciprocalFactors (n / 4 + 1)
 
-@[simp] lemma reciprocalFactors_zero : reciprocalFactors 0 = [0] := rfl
+@[simp] lemma reciprocalFactors_zero : reciprocalFactors 0 = [0] :=  by
+  unfold reciprocalFactors; rfl
 
-@[simp] lemma reciprocalFactors_one : reciprocalFactors 1 = [] := rfl
+@[simp] lemma reciprocalFactors_one : reciprocalFactors 1 = [] := by
+  unfold reciprocalFactors; rfl
 
 lemma reciprocalFactors_even {n : ℕ} (h0 : n ≠ 0) (h2 : Even n) :
     reciprocalFactors n = 3 :: reciprocalFactors (n / 2) := by

Mathlib/GroupTheory/Coxeter/Length.lean

@@ -145,7 +145,7 @@ theorem length_simple (i : B) : ℓ (s i) = 1 := by
   · by_contra! length_lt_one
     have : cs.lengthParity (s i) = Multiplicative.ofAdd 0 := by
       rw [lengthParity_eq_ofAdd_length, Nat.lt_one_iff.mp length_lt_one, Nat.cast_zero]
-    have : Multiplicative.ofAdd 0 = Multiplicative.ofAdd 1 :=
+    have : Multiplicative.ofAdd (0 : ZMod 2) = Multiplicative.ofAdd 1 :=
       this.symm.trans (cs.lengthParity_simple i)
     contradiction
 

Mathlib/NumberTheory/ArithmeticFunction.lean

@@ -780,6 +780,7 @@ theorem eq_iff_eq_on_prime_powers [CommMonoidWithZero R] (f : ArithmeticFunction
   exact Finset.prod_congr rfl fun p hp ↦ h p _ (Nat.prime_of_mem_primeFactors hp)
 #align nat.arithmetic_function.is_multiplicative.eq_iff_eq_on_prime_powers ArithmeticFunction.IsMultiplicative.eq_iff_eq_on_prime_powers
 
+unseal Nat.factors in
 @[arith_mult]
 theorem prodPrimeFactors [CommMonoidWithZero R] (f : ℕ → R) :
     IsMultiplicative (prodPrimeFactors f) := by
@@ -957,9 +958,11 @@ theorem cardFactors_apply {n : ℕ} : Ω n = n.factors.length :=
   rfl
 #align nat.arithmetic_function.card_factors_apply ArithmeticFunction.cardFactors_apply
 
+unseal Nat.factors in
 @[simp, nolint simpNF] -- this is a `dsimp` lemma
 lemma cardFactors_zero : Ω 0 = 0 := rfl
 
+unseal Nat.factors in
 @[simp] theorem cardFactors_one : Ω 1 = 0 := rfl
 #align nat.arithmetic_function.card_factors_one ArithmeticFunction.cardFactors_one
 

Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean

@@ -366,6 +366,7 @@ theorem div_four_left {a : ℤ} {b : ℕ} (ha4 : a % 4 = 0) (hb2 : b % 2 = 1) :
   rw [Int.mul_ediv_cancel_left _ (by decide), jacobiSym.mul_left,
     (by decide : (4 : ℤ) = (2 : ℕ) ^ 2), jacobiSym.sq_one' this, one_mul]
 
+unseal Nat.modCore in
 theorem even_odd {a : ℤ} {b : ℕ} (ha2 : a % 2 = 0) (hb2 : b % 2 = 1) :
     (if b % 8 = 3 ∨ b % 8 = 5 then -J(a / 2 | b) else J(a / 2 | b)) = J(a | b) := by
   obtain ⟨a, rfl⟩ := Int.dvd_of_emod_eq_zero ha2

Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean

@@ -212,13 +212,15 @@ def frobeniusRotation {a₁ a₂ : 𝕎 k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ :
   WittVector.mk p (frobeniusRotationCoeff p ha₁ ha₂)
 #align witt_vector.frobenius_rotation WittVector.frobeniusRotation
 
+unseal frobeniusRotationCoeff in
 theorem frobeniusRotation_nonzero {a₁ a₂ : 𝕎 k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) :
     frobeniusRotation p ha₁ ha₂ ≠ 0 := by
   intro h
   apply solution_nonzero p ha₁ ha₂
   simpa [← h, frobeniusRotation, frobeniusRotationCoeff] using WittVector.zero_coeff p k 0
 #align witt_vector.frobenius_rotation_nonzero WittVector.frobeniusRotation_nonzero
 
+unseal frobeniusRotationCoeff in
 theorem frobenius_frobeniusRotation {a₁ a₂ : 𝕎 k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) :
     frobenius (frobeniusRotation p ha₁ ha₂) * a₁ = frobeniusRotation p ha₁ ha₂ * a₂ := by
   ext n
@@ -242,6 +244,7 @@ theorem frobenius_frobeniusRotation {a₁ a₂ : 𝕎 k} (ha₁ : a₁.coeff 0 
 
 local notation "φ" => IsFractionRing.fieldEquivOfRingEquiv (frobeniusEquiv p k)
 
+unseal frobeniusRotationCoeff in
 theorem exists_frobenius_solution_fractionRing_aux (m n : ℕ) (r' q' : 𝕎 k) (hr' : r'.coeff 0 ≠ 0)
     (hq' : q'.coeff 0 ≠ 0) (hq : (p : 𝕎 k) ^ n * q' ∈ nonZeroDivisors (𝕎 k)) :
     let b : 𝕎 k := frobeniusRotation p hr' hq'

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

@@ -217,6 +217,10 @@ def gfpApprox (a : Ordinal.{u}) : α :=
 termination_by a
 decreasing_by exact h
 
+-- By unsealing these recursive definitions we can relate them
+-- by definitional equality
+unseal gfpApprox lfpApprox
+
 theorem gfpApprox_antitone : Antitone (gfpApprox f x) :=
   lfpApprox_monotone (OrderHom.dual f) x
 

Mathlib/Tactic/NormNum/Prime.lean

@@ -47,6 +47,7 @@ def deriveNotPrime (n d : ℕ) (en : Q(ℕ)) : Q(¬ Nat.Prime $en) := Id.run <|
 def MinFacHelper (n k : ℕ) : Prop :=
   2 < k ∧ k % 2 = 1 ∧ k ≤ minFac n
 
+unseal minFacAux in
 theorem MinFacHelper.one_lt {n k : ℕ} (h : MinFacHelper n k) : 1 < n := by
   have : 2 < minFac n := h.1.trans_le h.2.2
   obtain rfl | h := n.eq_zero_or_pos

Mathlib/Tactic/ToAdditive.lean

@@ -491,7 +491,7 @@ open Lean.Expr.FindImpl in
   and we're not remembering the cache between these calls. -/
 unsafe def additiveTestUnsafe (findTranslation? : Name → Option Name)
   (ignore : Name → Option (List ℕ)) (e : Expr) : Option Name :=
-  let rec visit (e : Expr) (inApp := false) : OptionT (FindM Id) Name := do
+  let rec visit (e : Expr) (inApp := false) : OptionT FindM Name := do
     if e.isConst then
       if inApp || (findTranslation? e.constName).isSome then
         failure

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "022321f7e18dc982db80f941f6784e92cb4766ff",
+   "rev": "e40e17375cece89474d63e1ed1455229f3b3b092",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "e9fb4ecc5d718eb36faae5308880cd3f243788df",
+   "rev": "59e6786376e5a0427524702fb2c1dcb864f2c9f7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-05-09
+leanprover/lean4:nightly-2024-05-11

test/hint.lean

@@ -37,6 +37,7 @@ info: Try these:
 #guard_msgs in
 example : 37^2 - 35^2 = 72 * 2 := by hint
 
+unseal Nat.minFacAux in
 /--
 info: Try these:
 • decide