chore: adaptations for nightly-2025-10-08

.github/workflows/nightly-docgen.yml

@@ -57,7 +57,7 @@ jobs:
           [[require]]
           scope = "leanprover"
           name = "doc-gen4"
-          rev = "main"
+          rev = "nightly-testing"
           EOF
 
           # Initialise docbuild as a Lean project

Cache/IO.lean

@@ -317,6 +317,11 @@ def mkBuildPaths (mod : Name) : CacheM <| List (FilePath × Bool) := do
     (packageDir / LIBDIR / path.withExtension "ilean.hash", true),
     (packageDir / IRDIR  / path.withExtension "c", true),
     (packageDir / IRDIR  / path.withExtension "c.hash", true),
+     -- this is needed for packages using the module system:
+    (packageDir / LIBDIR / path.withExtension "olean.private", false),
+    (packageDir / LIBDIR / path.withExtension "olean.private.hash", false),
+    (packageDir / LIBDIR / path.withExtension "olean.server", false),
+    (packageDir / LIBDIR / path.withExtension "olean.server.hash", false),
     (packageDir / LIBDIR / path.withExtension "extra", false)]
 
 /-- Check that all required build files exist. -/

Mathlib/Algebra/Algebra/StrictPositivity.lean

@@ -60,7 +60,7 @@ lemma _root_.IsUnit.isStrictlyPositive [LE A] [Monoid A] [Zero A]
 lemma isSelfAdjoint [Semiring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] {a : A}
     (ha : IsStrictlyPositive a) : IsSelfAdjoint a := ha.nonneg.isSelfAdjoint
 
-@[simp, grind]
+@[simp, grind .]
 lemma _root_.isStrictlyPositive_one [LE A] [Monoid A] [Zero A] [ZeroLEOneClass A] :
     IsStrictlyPositive (1 : A) := iff_of_unital.mpr ⟨zero_le_one, isUnit_one⟩
 

Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean

@@ -263,7 +263,7 @@ lemma standardσ_simplicialInsert (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj :
       simp only [standardσ_cons, Category.assoc, this,
         h_rec hL.tail (j + 1) (by grind) (by grind)]
 
-attribute [local grind] simplicialInsert_length simplicialInsert_isAdmissible in
+attribute [local grind! .] simplicialInsert_length simplicialInsert_isAdmissible in
 /-- Using `standardσ_simplicialInsert`, we can prove that every morphism satisfying `P_σ` is equal
 to some `standardσ` for some admissible list of indices. -/
 theorem exists_normal_form_P_σ {x y : SimplexCategoryGenRel} (f : x ⟶ y) (hf : P_σ f) :

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean

@@ -115,12 +115,12 @@ variable {A : Type*} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A]
 matrices, operators on a Hilbert space, elements of a C⋆-algebra, etc. -/
 noncomputable def log (a : A) : A := cfc Real.log a
 
-@[simp, grind]
+@[simp, grind =>]
 protected lemma _root_.IsSelfAdjoint.log {a : A} : IsSelfAdjoint (log a) := cfc_predicate _ a
 
-@[simp, grind] lemma log_zero : log (0 : A) = 0 := by simp [log]
+@[simp, grind =] lemma log_zero : log (0 : A) = 0 := by simp [log]
 
-@[simp, grind] lemma log_one : log (1 : A) = 0 := by simp [log]
+@[simp, grind =] lemma log_one : log (1 : A) = 0 := by simp [log]
 
 @[simp, grind =]
 lemma log_algebraMap {r : ℝ} : log (algebraMap ℝ A r) = algebraMap ℝ A (Real.log r) := by

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

@@ -93,7 +93,7 @@ noncomputable instance (priority := 100) : Pow A ℝ≥0 where
 @[simp]
 lemma nnrpow_eq_pow {a : A} {y : ℝ≥0} : nnrpow a y = a ^ y := rfl
 
-@[simp, grind]
+@[simp, grind =>]
 lemma nnrpow_nonneg {a : A} {x : ℝ≥0} : 0 ≤ a ^ x := cfcₙ_predicate _ a
 
 lemma nnrpow_def {a : A} {y : ℝ≥0} : a ^ y = cfcₙ (NNReal.nnrpow · y) a := rfl
@@ -226,7 +226,7 @@ section sqrt
 /-- Square roots of operators, based on the non-unital continuous functional calculus. -/
 noncomputable def sqrt (a : A) : A := cfcₙ NNReal.sqrt a
 
-@[simp, grind]
+@[simp, grind =>]
 lemma sqrt_nonneg (a : A) : 0 ≤ sqrt a := cfcₙ_predicate _ a
 
 lemma sqrt_eq_nnrpow (a : A) : sqrt a = a ^ (1 / 2 : ℝ≥0) := by
@@ -385,7 +385,7 @@ noncomputable instance (priority := 100) : Pow A ℝ where
 @[simp]
 lemma rpow_eq_pow {a : A} {y : ℝ} : rpow a y = a ^ y := rfl
 
-@[simp, grind]
+@[simp, grind =>]
 lemma rpow_nonneg {a : A} {y : ℝ} : 0 ≤ a ^ y := cfc_predicate _ a
 
 lemma rpow_def {a : A} {y : ℝ} : a ^ y = cfc (fun x : ℝ≥0 => x ^ y) a := rfl

Mathlib/Control/Monad/Cont.lean

@@ -8,7 +8,6 @@ import Mathlib.Control.Monad.Writer
 import Mathlib.Control.Lawful
 import Batteries.Tactic.Congr
 import Batteries.Lean.Except
-import Batteries.Control.OptionT
 
 /-!
 # Continuation Monad
@@ -179,8 +178,7 @@ instance [MonadCont m] [LawfulMonadCont m] : LawfulMonadCont (OptionT m) where
   callCC_bind_left := by
     intros
     simp only [callCC, OptionT.callCC, OptionT.goto_mkLabel, bind_pure_comp, OptionT.run_bind,
-      OptionT.run_mk, Option.elimM_map, Option.elim_some, Function.comp_apply,
-      @callCC_bind_left m _]
+      OptionT.run_mk, Option.elimM_map, Option.elim_some, @callCC_bind_left m _]
     ext; rfl
   callCC_dummy := by intros; simp only [callCC, OptionT.callCC, @callCC_dummy m _]; ext; rfl
 

Mathlib/Data/Int/LeastGreatest.lean

@@ -75,7 +75,11 @@ theorem exists_least_of_bdd
 theorem coe_leastOfBdd_eq {P : ℤ → Prop} [DecidablePred P] {b b' : ℤ} (Hb : ∀ z : ℤ, P z → b ≤ z)
     (Hb' : ∀ z : ℤ, P z → b' ≤ z) (Hinh : ∃ z : ℤ, P z) :
     (leastOfBdd b Hb Hinh : ℤ) = leastOfBdd b' Hb' Hinh := by
-  grind
+  #adaptation_note /-- 2025-09-30 (https://github.com/leanprover/lean4/issues/10622)
+    Used to be `grind` -/
+  rcases leastOfBdd b Hb Hinh with ⟨n, hn, h2n⟩
+  rcases leastOfBdd b' Hb' Hinh with ⟨n', hn', h2n'⟩
+  exact le_antisymm (h2n _ hn') (h2n' _ hn)
 
 /-- A computable version of `exists_greatest_of_bdd`: given a decidable predicate on the
 integers, with an explicit upper bound and a proof that it is somewhere true, return
@@ -112,6 +116,10 @@ theorem exists_greatest_of_bdd
 theorem coe_greatestOfBdd_eq {P : ℤ → Prop} [DecidablePred P] {b b' : ℤ}
     (Hb : ∀ z : ℤ, P z → z ≤ b) (Hb' : ∀ z : ℤ, P z → z ≤ b') (Hinh : ∃ z : ℤ, P z) :
     (greatestOfBdd b Hb Hinh : ℤ) = greatestOfBdd b' Hb' Hinh := by
-  grind
+  #adaptation_note /-- 2025-09-30 (https://github.com/leanprover/lean4/issues/10622)
+    Used to be `grind` -/
+  rcases greatestOfBdd b Hb Hinh with ⟨n, hn, h2n⟩
+  rcases greatestOfBdd b' Hb' Hinh with ⟨n', hn', h2n'⟩
+  exact le_antisymm (h2n' _ hn) (h2n _ hn')
 
 end Int

Mathlib/Data/String/Basic.lean

@@ -16,8 +16,6 @@ Supplementary theorems about the `String` type.
 
 namespace String
 
-@[simp] theorem endPos_empty : "".endPos = 0 := rfl
-
 /-- `<` on string iterators. This coincides with `<` on strings as lists. -/
 def ltb (s₁ s₂ : Iterator) : Bool :=
   if s₂.hasNext then
@@ -63,7 +61,7 @@ theorem ltb_cons_addChar' (c : Char) (s₁ s₂ : Iterator) :
     rw [ltb, Iterator.hasNext_cons_addChar, Iterator.hasNext_cons_addChar,
       if_pos (by simpa using h₁), if_pos (by simpa using h₂), if_pos, ← ih]
     · simp [Iterator.next, String.next, get_cons_addChar]
-      congr 2 <;> apply Pos.addChar_right_comm
+      congr 2 <;> apply Pos.Raw.addChar_right_comm
     · simpa [Iterator.curr, get_cons_addChar] using h
   | case2 s₁ s₂ h₁ h₂ h =>
     rw [ltb, Iterator.hasNext_cons_addChar, Iterator.hasNext_cons_addChar,
@@ -76,7 +74,7 @@ theorem ltb_cons_addChar' (c : Char) (s₁ s₂ : Iterator) :
   | case4 s₁ s₂ h₁ =>
     rw [ltb, Iterator.hasNext_cons_addChar, if_neg (by simpa using h₁)]
 
-theorem ltb_cons_addChar (c : Char) (cs₁ cs₂ : List Char) (i₁ i₂ : Pos) :
+theorem ltb_cons_addChar (c : Char) (cs₁ cs₂ : List Char) (i₁ i₂ : Pos.Raw) :
     ltb ⟨mk (c :: cs₁), i₁ + c⟩ ⟨mk (c :: cs₂), i₂ + c⟩ = ltb ⟨mk cs₁, i₁⟩ ⟨mk cs₂, i₂⟩ := by
   rw [eq_comm, ← ltb_cons_addChar' c]
   simp
@@ -98,13 +96,13 @@ theorem lt_iff_toList_lt : ∀ {s₁ s₂ : String}, s₁ < s₂ ↔ s₁.toList
         simp [Iterator.hasNext]
       · apply not_lt_of_gt; apply List.nil_lt_cons
     · rename_i c₁ cs₁ ih c₂ cs₂; unfold ltb
-      simp only [Iterator.hasNext, Pos.byteIdx_zero, endPos_asString, utf8Len_cons, add_pos_iff,
+      simp only [Iterator.hasNext, Pos.Raw.byteIdx_zero, endPos_asString, utf8Len_cons, add_pos_iff,
         Char.utf8Size_pos, or_true, decide_true, ↓reduceIte, Iterator.curr, get, List.data_asString,
         utf8GetAux, Iterator.next, next, Bool.ite_eq_true_distrib, decide_eq_true_eq]
       simp only [← String.mk_eq_asString]
       split_ifs with h
       · subst c₂
-        suffices ltb ⟨mk (c₁ :: cs₁), (0 : Pos) + c₁⟩ ⟨mk (c₁ :: cs₂), (0 : Pos) + c₁⟩ =
+        suffices ltb ⟨mk (c₁ :: cs₁), (0 : Pos.Raw) + c₁⟩ ⟨mk (c₁ :: cs₂), (0 : Pos.Raw) + c₁⟩ =
           ltb ⟨mk cs₁, 0⟩ ⟨mk cs₂, 0⟩ by rw [this]; exact (ih cs₂).trans List.lex_cons_iff.symm
         apply ltb_cons_addChar
       · refine ⟨List.Lex.rel, fun e ↦ ?_⟩

Mathlib/MeasureTheory/Integral/IntervalIntegral/LebesgueDifferentiationThm.lean

@@ -70,7 +70,10 @@ theorem IntervalIntegrable.ae_hasDerivAt_integral {f : ℝ → ℝ} {a b : ℝ}
       |>.integrable_of_forall_notMem_eq_zero (by grind) |>.locallyIntegrable
   filter_upwards [LocallyIntegrable.ae_hasDerivAt_integral hg, h₁, h₂] with x hx _ _ _
   intro c hc
-  refine HasDerivWithinAt.hasDerivAt (s := Ioo a b) ?_ <| Ioo_mem_nhds (by grind) (by grind)
-  rw [show f x = g x by grind]
+  #adaptation_note /-- 2025-09-30 https://github.com/leanprover/lean4/issues/10622
+    `grind -order` calls used be `grind` -/
+  refine HasDerivWithinAt.hasDerivAt (s := Ioo a b) ?_ <|
+    Ioo_mem_nhds (by grind -order) (by grind -order)
+  rw [show f x = g x by grind -order]
   refine (hx c).hasDerivWithinAt.congr (fun y hy ↦ ?_) ?_
   all_goals apply intervalIntegral.integral_congr_ae' <;> filter_upwards <;> grind

Mathlib/SetTheory/PGame/Basic.lean

@@ -3,7 +3,6 @@ Copyright (c) 2019 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Reid Barton, Mario Carneiro, Isabel Longbottom, Kim Morrison, Yuyang Zhao
 -/
-import Mathlib.Data.Nat.Basic
 import Mathlib.Logic.Equiv.Defs
 import Mathlib.Tactic.Convert
 import Mathlib.Tactic.Linter.DeprecatedModule

Mathlib/Tactic/DeclarationNames.lean

@@ -21,7 +21,7 @@ namespace Mathlib.Linter
 If `pos` is a `String.Pos`, then `getNamesFrom pos` returns the array of identifiers
 for the names of the declarations whose syntax begins in position at least `pos`.
 -/
-def getNamesFrom {m} [Monad m] [MonadEnv m] [MonadFileMap m] (pos : String.Pos) :
+def getNamesFrom {m} [Monad m] [MonadEnv m] [MonadFileMap m] (pos : String.Pos.Raw) :
     m (Array Syntax) := do
   -- declarations from parallelism branches should not be interesting here, so use `local`
   let drs := declRangeExt.toPersistentEnvExtension.getState (asyncMode := .local) (← getEnv)

Mathlib/Tactic/Linter/CommandStart.lean

@@ -50,7 +50,7 @@ formatting.
 This is every declaration until the type-specification, if there is one, or the value,
 as well as all `variable` commands.
 -/
-def CommandStart.endPos (stx : Syntax) : Option String.Pos :=
+def CommandStart.endPos (stx : Syntax) : Option String.Pos.Raw :=
   if let some cmd := stx.find? (#[``Parser.Command.declaration, `lemma].contains ·.getKind) then
     if let some ind := cmd.find? (·.isOfKind ``Parser.Command.inductive) then
       match ind.find? (·.isOfKind ``Parser.Command.optDeclSig) with
@@ -78,7 +78,7 @@ structure FormatError where
   /-- The distance to the end of the source string, as number of characters -/
   srcNat : Nat
   /-- The distance to the end of the source string, as number of string positions -/
-  srcEndPos : String.Pos
+  srcEndPos : String.Pos.Raw
   /-- The distance to the end of the formatted string, as number of characters -/
   fmtPos : Nat
   /-- The kind of formatting error. For example: `extra space`, `remove line break` or
@@ -90,7 +90,7 @@ structure FormatError where
   /-- The length of the mismatch, as number of characters. -/
   length : Nat
   /-- The starting position of the mismatch, as a `String.pos`. -/
-  srcStartPos : String.Pos
+  srcStartPos : String.Pos.Raw
   deriving Inhabited
 
 instance : ToString FormatError where

Mathlib/Tactic/Linter/Header.lean

@@ -96,15 +96,15 @@ parsing the file linearly, it will only need to parse
 In conclusion, either the parsing is successful, and the linter can continue with its analysis,
 or the parsing is not successful and the linter will flag a missing module doc-string!
 -/
-def parseUpToHere (pos : String.Pos) (post : String := "") : CommandElabM Syntax := do
+def parseUpToHere (pos : String.Pos.Raw) (post : String := "") : CommandElabM Syntax := do
   let upToHere : Substring := { str := (← getFileMap).source, startPos := ⟨0⟩, stopPos := pos }
   -- Append a further string after the content of `upToHere`.
   Parser.testParseModule (← getEnv) "linter.style.header" (upToHere.toString ++ post)
 
 /-- `toSyntax s pattern` converts the two input strings into a `Syntax`, assuming that `pattern`
 is a substring of `s`:
 the syntax is an atom with value `pattern` whose the range is the range of `pattern` in `s`. -/
-def toSyntax (s pattern : String) (offset : String.Pos := 0) : Syntax :=
+def toSyntax (s pattern : String) (offset : String.Pos.Raw := 0) : Syntax :=
   let beg := ((s.splitOn pattern).getD 0 "").endPos + offset
   let fin := (((s.splitOn pattern).getD 0 "") ++ pattern).endPos + offset
   mkAtomFrom (.ofRange ⟨beg, fin⟩) pattern
@@ -116,7 +116,7 @@ produces.
 `authorsLineChecks` computes a position for its warning *relative to `line`*.
 The `offset` input passes on the starting position of `line` in the whole file.
 -/
-def authorsLineChecks (line : String) (offset : String.Pos) : Array (Syntax × String) :=
+def authorsLineChecks (line : String) (offset : String.Pos.Raw) : Array (Syntax × String) :=
   Id.run do
   -- We cannot reasonably validate the author names, so we look only for a few common mistakes:
   -- the line starting wrongly, double spaces, using ' and ' between names,

Mathlib/Tactic/ToAdditive/GuessName.lean

@@ -35,7 +35,7 @@ open String in
 
 E.g. `#eval "InvHMulLEConjugate₂SMul_ne_top".splitCase` yields
 `["Inv", "HMul", "LE", "Conjugate₂", "SMul", "_", "ne", "_", "top"]`. -/
-partial def _root_.String.splitCase (s : String) (i₀ : Pos := 0) (r : List String := []) :
+partial def _root_.String.splitCase (s : String) (i₀ : Pos.Raw := 0) (r : List String := []) :
     List String := Id.run do
   -- We test if we need to split between `i₀` and `i₁`.
   let i₁ := s.next i₀
@@ -60,7 +60,7 @@ partial def _root_.String.splitCase (s : String) (i₀ : Pos := 0) (r : List Str
   return splitCase s i₁ r
 
 /-- Helper for `capitalizeLike`. -/
-partial def capitalizeLikeAux (s : String) (i : String.Pos := 0) (p : String) : String :=
+partial def capitalizeLikeAux (s : String) (i : String.Pos.Raw := 0) (p : String) : String :=
   if p.atEnd i || s.atEnd i then
     p
   else

Mathlib/Tactic/ToExpr.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
 import Mathlib.Util.WhatsNew
+import Mathlib.Tactic.AdaptationNote
 
 /-!
 # `ToExpr` instances for Mathlib
@@ -12,6 +13,8 @@ import Mathlib.Util.WhatsNew
 namespace Mathlib
 open Lean
 
+#adaptation_note /-- 2025-10-06 https://github.com/leanprover/lean4/issues/10678
+  Added `docBlame` nolint for `Mathlib.instToExprULift_mathlib.toExpr` -/
 set_option autoImplicit true in
 deriving instance ToExpr for ULift
 
@@ -21,7 +24,7 @@ instance [ToLevel.{u}] : ToExpr PUnit.{u+1} where
   toExpr _ := mkConst ``PUnit.unit [toLevel.{u+1}]
   toTypeExpr := mkConst ``PUnit [toLevel.{u+1}]
 
-deriving instance ToExpr for String.Pos
+deriving instance ToExpr for String.Pos.Raw
 deriving instance ToExpr for Substring
 deriving instance ToExpr for SourceInfo
 deriving instance ToExpr for Syntax

Mathlib/Tactic/Widget/Calc.lean

@@ -59,7 +59,7 @@ structure CalcParams extends SelectInsertParams where
 
 /-- Return the link text and inserted text above and below of the calc widget. -/
 def suggestSteps (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Expr) (params : CalcParams) :
-    MetaM (String × String × Option (String.Pos × String.Pos)) := do
+    MetaM (String × String × Option (String.Pos.Raw × String.Pos.Raw)) := do
   let subexprPos := getGoalLocations pos
   let some (rel, lhs, rhs) ← Lean.Elab.Term.getCalcRelation? goalType |
       throwError "invalid 'calc' step, relation expected{indentExpr goalType}"
@@ -108,7 +108,7 @@ def suggestSteps (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Expr) (par
   | true, true => "Create two new steps"
   | true, false | false, true => "Create a new step"
   | false, false => "This should not happen"
-  let pos : String.Pos := insertedCode.find (fun c => c == '?')
+  let pos : String.Pos.Raw := insertedCode.find (fun c => c == '?')
   return (stepInfo, insertedCode, some (pos, ⟨pos.byteIdx + 2⟩) )
 
 /-- Rpc function for the calc widget. -/

Mathlib/Tactic/Widget/CongrM.lean

@@ -21,7 +21,8 @@ open Lean Meta Server ProofWidgets
 /-- Return the link text and inserted text above and below of the congrm widget. -/
 @[nolint unusedArguments]
 def makeCongrMString (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Expr)
-    (_ : SelectInsertParams) : MetaM (String × String × Option (String.Pos × String.Pos)) := do
+    (_ : SelectInsertParams) :
+    MetaM (String × String × Option (String.Pos.Raw × String.Pos.Raw)) := do
   let subexprPos := getGoalLocations pos
   unless goalType.isAppOf ``Eq || goalType.isAppOf ``Iff do
     throwError "The goal must be an equality or iff."

Mathlib/Tactic/Widget/Conv.lean

@@ -86,7 +86,8 @@ open Lean Syntax in
 /-- Return the link text and inserted text above and below of the conv widget. -/
 @[nolint unusedArguments]
 def insertEnter (locations : Array Lean.SubExpr.GoalsLocation) (goalType : Expr)
-    (params : SelectInsertParams) : MetaM (String × String × Option (String.Pos × String.Pos)) := do
+    (params : SelectInsertParams) :
+    MetaM (String × String × Option (String.Pos.Raw × String.Pos.Raw)) := do
   let some pos := locations[0]? | throwError "You must select something."
   let (fvar, subexprPos) ← match pos with
   | ⟨_, .target subexprPos⟩ => pure (none, subexprPos)

Mathlib/Tactic/Widget/GCongr.lean

@@ -17,7 +17,8 @@ open Lean Meta Server ProofWidgets
 /-- Return the link text and inserted text above and below of the gcongr widget. -/
 @[nolint unusedArguments]
 def makeGCongrString (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Expr)
-    (_ : SelectInsertParams) : MetaM (String × String × Option (String.Pos × String.Pos)) := do
+    (_ : SelectInsertParams) :
+    MetaM (String × String × Option (String.Pos.Raw × String.Pos.Raw)) := do
 let subexprPos := getGoalLocations pos
 unless goalType.isAppOf ``LE.le || goalType.isAppOf ``LT.lt || goalType.isAppOf `Int.ModEq do
   panic! "The goal must be a ≤ or < or ≡."

Mathlib/Tactic/Widget/SelectPanelUtils.lean

@@ -74,7 +74,7 @@ We also make sure `mkCmdStr` is executed in the right context.
 -/
 def mkSelectionPanelRPC {Params : Type} [SelectInsertParamsClass Params]
     (mkCmdStr : (pos : Array GoalsLocation) → (goalType : Expr) → Params →
-    MetaM (String × String × Option (String.Pos × String.Pos)))
+    MetaM (String × String × Option (String.Pos.Raw × String.Pos.Raw)))
     (helpMsg : String) (title : String) (onlyGoal := true) (onlyOne := false) :
     (params : Params) → RequestM (RequestTask Html) :=
   fun params ↦ RequestM.asTask do

Mathlib/Util/CompileInductive.lean

@@ -176,7 +176,7 @@ def compileInductiveOnly (iv : InductiveVal) (rv : RecursorVal) (warn := true) :
     }]
     Compiler.CSimp.add name .global
   for name in iv.all do
-    for aux in [mkRecOnName name, mkBRecOnName name] do
+    for aux in [mkRecOnName name, (mkBRecOnName name).str "go", mkBRecOnName name] do
       if let some (.defnInfo dv) := (← getEnv).find? aux then
         compileDefn dv
 
@@ -234,6 +234,7 @@ end Mathlib.Util
 
 -- `Nat.rec` already has a `@[csimp]` lemma in Lean.
 compile_def% Nat.recOn
+compile_def% Nat.brecOn.go
 compile_def% Nat.brecOn
 compile_inductive% Prod
 compile_inductive% List