chore: adaptations for nightly-2024-05-09

Mathlib/Algebra/Group/MinimalAxioms.lean

@@ -40,7 +40,7 @@ def Group.ofLeftAxioms {G : Type u} [Mul G] [Inv G] [One G]
     one_mul := one_mul,
     mul_left_inv := mul_left_inv,
     mul_one := fun a => by
-      have mul_right_inv : ∀ a, a * a⁻¹ = 1 := fun a =>
+      have mul_right_inv : ∀ a : G, a * a⁻¹ = 1 := fun a =>
         calc a * a⁻¹ = 1 * (a * a⁻¹) := (one_mul _).symm
           _ = ((a * a⁻¹)⁻¹ * (a * a⁻¹)) * (a * a⁻¹) := by
             rw [mul_left_inv]
@@ -63,7 +63,7 @@ def Group.ofRightAxioms {G : Type u} [Mul G] [Inv G] [One G]
     (assoc : ∀ a b c : G, (a * b) * c = a * (b * c))
     (mul_one : ∀ a : G, a * 1 = a)
     (mul_right_inv : ∀ a : G, a * a⁻¹ = 1) : Group G :=
-  have mul_left_inv : ∀ a, a⁻¹ * a = 1 := fun a =>
+  have mul_left_inv : ∀ a : G, a⁻¹ * a = 1 := fun a =>
     calc a⁻¹ * a = (a⁻¹ * a) * 1 := (mul_one _).symm
       _ = (a⁻¹ * a) * ((a⁻¹ * a) * (a⁻¹ * a)⁻¹) := by
         rw [mul_right_inv]

Mathlib/CategoryTheory/Comma/Basic.lean

@@ -239,7 +239,7 @@ instance full_map [F.Faithful] [F₁.Full] [F₂.Full] [IsIso α] [IsIso β] : (
           assoc, assoc]
         erw [← α.naturality_assoc, β.naturality]
         dsimp
-        rw [F₁.image_preimage, F₂.image_preimage]
+        rw [F₁.map_preimage, F₂.map_preimage]
         simpa using φ.w) }, by aesop_cat⟩
 
 instance essSurj_map [F₁.EssSurj] [F₂.EssSurj] [F.Full] [IsIso α] [IsIso β] :

Mathlib/Lean/Elab/Term.lean

@@ -19,5 +19,5 @@ def elabPattern (patt : Term) (expectedType? : Option Expr) : TermElabM Expr :=
   withTheReader Term.Context ({ · with ignoreTCFailures := true, errToSorry := false }) <|
     withSynthesizeLight do
       let t ← elabTerm patt expectedType?
-      synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
+      synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
       instantiateMVars t

Mathlib/NumberTheory/Cyclotomic/Discriminant.lean

@@ -102,8 +102,8 @@ theorem discr_prime_pow_ne_two [IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : F
     replace H := congr_arg (Algebra.norm K) H
     have hnorm : (norm K) (ζ ^ (p : ℕ) ^ k - 1) = (p : K) ^ (p : ℕ) ^ k := by
       by_cases hp : p = 2
-      · exact mod_cast hζ.pow_sub_one_norm_prime_pow_of_ne_zero hirr le_rfl (hp2 hp)
-      · exact mod_cast hζ.pow_sub_one_norm_prime_ne_two hirr le_rfl hp
+      · exact mod_cast hζ.norm_pow_sub_one_eq_prime_pow_of_ne_zero hirr le_rfl (hp2 hp)
+      · exact mod_cast hζ.norm_pow_sub_one_of_prime_ne_two hirr le_rfl hp
     rw [MonoidHom.map_mul, hnorm, MonoidHom.map_mul, ← map_natCast (algebraMap K L),
       Algebra.norm_algebraMap, finrank L hirr] at H
     conv_rhs at H => -- Porting note: need to drill down to successfully rewrite the totient

Mathlib/Tactic/Convert.lean

@@ -111,7 +111,7 @@ elab_rules : tactic
         withTheReader Term.Context (fun ctx => { ctx with ignoreTCFailures := true }) do
           let t ← elabTermEnsuringType (mayPostpone := true) term expectedType
           -- Process everything so that tactics get run, but again allow TC failures
-          Term.synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
+          Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
           -- Use a type hint to ensure we collect goals from the type too
           mkExpectedTypeHint t (← inferType t)
     liftMetaTactic fun g ↦

Mathlib/Tactic/FBinop.lean

@@ -48,7 +48,7 @@ private inductive Tree where
 
 private partial def toTree (s : Syntax) : TermElabM Tree := do
   let result ← go s
-  synthesizeSyntheticMVars (mayPostpone := true)
+  synthesizeSyntheticMVars (postpone := .yes)
   return result
 where
   go (s : Syntax) : TermElabM Tree := do

Mathlib/Tactic/Find.lean

@@ -99,7 +99,7 @@ lemmas which are `apply`able against the current goal.
 elab "#find " t:term : command =>
   liftTermElabM do
     let t ← Term.elabTerm t none
-    Term.synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
+    Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
     findType t
 
 /- (Note that you'll get an error trying to run these here:
@@ -132,5 +132,5 @@ See also the `find` tactic to search for theorems matching the current goal.
 -/
 elab "#find " t:term : tactic => do
   let t ← Term.elabTerm t none
-  Term.synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
+  Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
   findType t

Mathlib/Tactic/FunProp/Decl.lean

@@ -132,7 +132,7 @@ def tacticToDischarge (tacticCode : TSyntax `tactic) : Expr → MetaM (Option Ex
           instantiateMVarDeclMVars mvar.mvarId!
 
           let _ ←
-            withSynthesize (mayPostpone := false) do
+            withSynthesize (postpone := .no) do
               Tactic.run mvar.mvarId! (Tactic.evalTactic tacticCode *> Tactic.pruneSolvedGoals)
 
           let result ← instantiateMVars mvar

Mathlib/Tactic/Have.lean

@@ -72,7 +72,7 @@ def haveLetCore (goal : MVarId) (name : TSyntax ``optBinderIdent)
       | none => mkFreshTypeMVar
       | some stx => withRef stx do
         let e ← Term.elabType stx
-        Term.synthesizeSyntheticMVars false
+        Term.synthesizeSyntheticMVars (postpone := .no)
         instantiateMVars e
       let p ← mkFreshExprMVar t MetavarKind.syntheticOpaque n
       pure (p.mvarId!, ← mkForallFVars es t, ← mkLambdaFVars es p)

Mathlib/Tactic/NormNum/Pow.lean

@@ -226,40 +226,60 @@ theorem isRat_zpow_neg {α : Type*} [DivisionRing α] {a : α} {b : ℤ} {nb : 
     IsRat (a^b) num den := by
   rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]
 
+#adaptation_note
+/--
+Prior to https://github.com/leanprover/lean4/pull/4096,
+the repeated
+```
+have h : $e =Q (HPow.hPow (γ := $α) $a $b) := ⟨⟩
+h.check
+```
+blocks below were not necessary: we just did it once outside the `match rb with` block.
+-/
 /-- The `norm_num` extension which identifies expressions of the form `a ^ b`,
 such that `norm_num` successfully recognises both `a` and `b`, with `b : ℤ`. -/
 @[norm_num (_ : α) ^ (_ : ℤ)]
 def evalZPow : NormNumExt where eval {u α} e := do
   let .app (.app (f : Q($α → ℤ → $α)) (a : Q($α))) (b : Q(ℤ)) ← whnfR e | failure
   let _c ← synthInstanceQ q(DivisionSemiring $α)
   let rb ← derive (α := q(ℤ)) b
-  have h : $e =Q $a ^ $b := ⟨⟩
-  h.check
   match rb with
   | .isBool .. | .isRat _ .. => failure
   | .isNat sβ nb pb =>
     match ← derive q($a ^ $nb) with
     | .isBool .. => failure
     | .isNat sα' ne' pe' =>
+      have h : $e =Q (HPow.hPow (γ := $α) $a $b) := ⟨⟩
+      h.check
       assumeInstancesCommute
       return .isNat sα' ne' q(isNat_zpow_pos $pb $pe')
     | .isNegNat sα' ne' pe' =>
+      have h : $e =Q (HPow.hPow (γ := $α) $a $b) := ⟨⟩
+      h.check
       let _c ← synthInstanceQ q(DivisionRing $α)
       assumeInstancesCommute
       return .isNegNat sα' ne' q(isInt_zpow_pos $pb $pe')
     | .isRat sα' qe' nume' dene' pe' =>
+      have h : $e =Q (HPow.hPow (γ := $α) $a $b) := ⟨⟩
+      h.check
       assumeInstancesCommute
       return .isRat sα' qe' nume' dene' q(isRat_zpow_pos $pb $pe')
   | .isNegNat sβ nb pb =>
     match ← derive q(($a ^ $nb)⁻¹) with
     | .isBool .. => failure
     | .isNat sα' ne' pe' =>
+      have h : $e =Q (HPow.hPow (γ := $α) $a $b) := ⟨⟩
+      h.check
       assumeInstancesCommute
       return .isNat sα' ne' q(isNat_zpow_neg $pb $pe')
     | .isNegNat sα' ne' pe' =>
+      have h : $e =Q (HPow.hPow (γ := $α) $a $b) := ⟨⟩
+      h.check
       let _c ← synthInstanceQ q(DivisionRing $α)
       assumeInstancesCommute
       return .isNegNat sα' ne' q(isInt_zpow_neg $pb $pe')
     | .isRat sα' qe' nume' dene' pe' =>
+      have h : $e =Q (HPow.hPow (γ := $α) $a $b) := ⟨⟩
+      h.check
       assumeInstancesCommute
       return .isRat sα' qe' nume' dene' q(isRat_zpow_neg $pb $pe')

Mathlib/Tactic/TermCongr.lean

@@ -621,7 +621,7 @@ def elabTermCongr : Term.TermElab := fun stx expectedType? => do
         unless ← isDefEq expRhs rhs do
           throwError "Right-hand side of elaborated pattern{indentD rhs}\n\
             is not definitionally equal to right-hand side of expected type{indentD expectedType}"
-        Term.synthesizeSyntheticMVars (mayPostpone := true)
+        Term.synthesizeSyntheticMVars (postpone := .yes)
         let res ← mkCongrOf 0 mvarCounterSaved lhs rhs
         let expectedType' ← whnf expectedType
         let pf ← if expectedType'.iff?.isSome then res.iff
@@ -632,7 +632,7 @@ def elabTermCongr : Term.TermElab := fun stx expectedType? => do
     -- Case 2: No expected type or it's not obviously Iff/Eq/HEq. We generate an Eq.
     let lhs ← elaboratePattern t none true
     let rhs ← elaboratePattern t none false
-    Term.synthesizeSyntheticMVars (mayPostpone := true)
+    Term.synthesizeSyntheticMVars (postpone := .yes)
     let res ← mkCongrOf 0 mvarCounterSaved lhs rhs
     let pf ← res.eq
     let ty ← mkEq res.lhs res.rhs

Mathlib/Tactic/Variable.lean

@@ -127,7 +127,7 @@ partial def getSubproblem
     withTheReader Term.Context (fun ctx => {ctx with ignoreTCFailures := true}) do
     Term.withAutoBoundImplicit do
       _ ← Term.elabType ty
-      Term.synthesizeSyntheticMVars (mayPostpone := true) (ignoreStuckTC := true)
+      Term.synthesizeSyntheticMVars (postpone := .yes) (ignoreStuckTC := true)
       let fvarIds := (← getLCtx).getFVarIds
       if let some mvarId ← pendingActionableSynthMVar binder then
         trace[«variable?»] "Actionable mvar:{mvarId}"

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "91d3fcfdc2e9e815954a542442b9ccf59e43e968",
+   "rev": "022321f7e18dc982db80f941f6784e92cb4766ff",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -13,19 +13,19 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
+   "rev": "44f57616b0d9b8f9e5606f2c58d01df54840eba7",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "2225b0e4a3528da20499e2304b521e0c4c2a4563",
+   "rev": "f1bfa6ae737248969c360a3715a5c05df0eea55b",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "c46d22bbe4f8363c0829ce0eb48a95012cdc0d79",
+   "rev": "e9fb4ecc5d718eb36faae5308880cd3f243788df",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.lean

@@ -22,8 +22,8 @@ meta if get_config? doc = some "on" then -- do not download and build doc-gen4 b
 require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
 
 require batteries from git "https://github.com/leanprover-community/batteries" @ "nightly-testing"
-require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
-require aesop from git "https://github.com/leanprover-community/aesop" @ "master"
+require Qq from git "https://github.com/leanprover-community/quote4" @ "nightly-testing"
+require aesop from git "https://github.com/leanprover-community/aesop" @ "nightly-testing"
 require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.36"
 require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"
 require importGraph from git "https://github.com/leanprover-community/import-graph.git" @ "main"

lean-toolchain

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