Merge lean-pr-testing-13305 into nightly-testing: adapt to new do elaborator (lean4#13305)

Brings in the do-elaborator adaptations for 14 Mathlib files (Ring, NormNum,
FieldSimp, Whitespace linter, etc.) and repoints batteries/Qq/aesop/plausible
to their nightly-testing branches (which carry the corresponding fixes).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: kim-em

Mathlib/Data/Fin/Tuple/Reflection.lean

@@ -175,10 +175,10 @@ open Lean Meta Qq
 that shows it is equal to `∏ i, f i`. -/
 meta def mkProdEqQ {u : Level} {α : Q(Type u)}
     (inst : Q(CommMonoid $α)) (n : ℕ) (f : Q(Fin $n → $α)) :
-    MetaM <| (val : Q($α)) × Q(∏ i, $f i = $val) := do
+    MetaM <| (val : Q($α)) × Q(∏ i, $f i = $val) :=
   match n with
-  | 0 => return ⟨q((1 : $α)), q(Fin.prod_univ_zero $f)⟩
-  | m + 1 =>
+  | 0 => do return ⟨q((1 : $α)), q(Fin.prod_univ_zero $f)⟩
+  | m + 1 => do
     let nezero : Q(NeZero ($m + 1)) := q(⟨Nat.succ_ne_zero _⟩)
     let val ← makeRHS (m + 1) f nezero (m + 1)
     let _ : $val =Q FinVec.prod $f := ⟨⟩
@@ -198,10 +198,10 @@ where
 that shows it is equal to `∑ i, f i`. -/
 meta def mkSumEqQ {u : Level} {α : Q(Type u)}
     (inst : Q(AddCommMonoid $α)) (n : ℕ) (f : Q(Fin $n → $α)) :
-    MetaM <| (val : Q($α)) × Q(∑ i, $f i = $val) := do
+    MetaM <| (val : Q($α)) × Q(∑ i, $f i = $val) :=
   match n with
   | 0 => return ⟨q((0 : $α)), q(Fin.sum_univ_zero $f)⟩
-  | m + 1 =>
+  | m + 1 => do
     let nezero : Q(NeZero ($m + 1)) := q(⟨Nat.succ_ne_zero _⟩)
     let val ← makeRHS (m + 1) f nezero (m + 1)
     let _ : $val =Q FinVec.sum $f := ⟨⟩
@@ -228,7 +228,7 @@ open Qq Lean FinVec
 simproc_decl prod_univ_ofNat (∏ _ : Fin _, _) := .ofQ fun u _ e => do
   match u, e with
   | .succ _, ~q(@Finset.prod (Fin $n) _ $inst (@Finset.univ _ $instF) $f) => do
-    match (generalizing := false) n.nat? with
+    match n.nat? with
     | none =>
       return .continue
     | some nVal =>

Mathlib/Tactic/Algebra/Basic.lean

@@ -165,24 +165,24 @@ namespace RingCompute
 
 /-- Evaluate the sum of two normalized expressions in `R` using `ring`. -/
 def add (cR : Common.Cache sR) {a b : Q($A)} (za : BaseType sAlg a) (zb : BaseType sAlg b) :
-    MetaM (Common.Result (BaseType sAlg) q($a + $b) × Option Q(IsNat ($a + $b) 0)) := do
-  let ⟨r, vr⟩ := za
-  let ⟨s, vs⟩ := zb
-  let ⟨t, vt, pt⟩ ← Common.evalAdd (Ring.ringCompute cR) rcℕ vr vs
-  match vt with
-  | .zero =>
-    have : $t =Q 0 := ⟨⟩
-    return  ⟨⟨_, .mk _ vt, q(add_algebraMap $pt)⟩, some q(add_algebraMap_isNat_zero $pt)⟩
-  | vt =>
-    return ⟨⟨_, .mk _ vt, q(add_algebraMap $pt)⟩, none⟩
+    MetaM (Common.Result (BaseType sAlg) q($a + $b) × Option Q(IsNat ($a + $b) 0)) :=
+  match za, zb with
+  | .mk r vr, .mk s vs => do
+    let ⟨t, vt, pt⟩ ← Common.evalAdd (Ring.ringCompute cR) rcℕ vr vs
+    match (dependent := true) vt with
+    | .zero =>
+      have : $t =Q 0 := ⟨⟩
+      return  ⟨⟨_, .mk _ vt, q(add_algebraMap $pt)⟩, some q(add_algebraMap_isNat_zero $pt)⟩
+    | vt =>
+      return ⟨⟨_, .mk _ vt, q(add_algebraMap $pt)⟩, none⟩
 
 /-- Evaluate the product of two normalized expressions in `R` using `ring`. -/
 def mul (cR : Common.Cache sR) {a b : Q($A)} (za : BaseType sAlg a) (zb : BaseType sAlg b) :
-    MetaM (Common.Result (BaseType sAlg) q($a * $b)) := do
-  let ⟨r, vr⟩ := za
-  let ⟨s, vs⟩ := zb
-  let ⟨t, vt, pt⟩ ← Common.evalMul (Ring.ringCompute cR) rcℕ vr vs
-  return ⟨_, .mk _ vt, q(by simp [← $pt, map_mul])⟩
+    MetaM (Common.Result (BaseType sAlg) q($a * $b)) :=
+  match za, zb with
+  | .mk r vr, .mk s vs => do
+    let ⟨t, vt, pt⟩ ← Common.evalMul (Ring.ringCompute cR) rcℕ vr vs
+    return ⟨_, .mk _ vt, q(by simp [← $pt, map_mul])⟩
 
 /-- Take an expression `r'` in a ring `R'` such that `R` is an `R'`-algebra and cast `r'` to `R`
 using `algebraMap R' R`, so that the scalar multiplication action on `A` is preserved. -/
@@ -195,7 +195,7 @@ def cast (cR : Algebra.Cache sR) (u' : Level) (R' : Q(Type u'))
   let ⟨r, pf_smul⟩ ← evalSMulCast q($sAlg) q($_smul) r'
   let ⟨_r'', vr, pr⟩ ←
     Common.eval rcℕ (Ring.ringCompute cR.toCache) cR.toCache q($r)
-  match vr with
+  match (dependent := true) vr with
   | .zero .. =>
     assumeInstancesCommute
     return ⟨_, .zero, q(cast_zero_smul_eq_zero_mul $pr $pf_smul)⟩
@@ -206,37 +206,40 @@ def cast (cR : Algebra.Cache sR) (u' : Level) (R' : Q(Type u'))
 
 /-- Evaluate the product of two normalized expressions in `R` using `ring`. -/
 def neg (cR : Algebra.Cache sR) {a : Q($A)} (_rA : Q(CommRing $A)) (za : BaseType sAlg a) :
-    MetaM (Common.Result (BaseType sAlg) q(-$a)) := do
-  let ⟨r, vr⟩ := za
-  match cR.rα with
-  | some rR =>
-    let ⟨_, vt, pt⟩ ← Common.evalNeg (Ring.ringCompute cR.toCache) q($rR) vr
-    assumeInstancesCommute
-    return ⟨_, .mk _ vt, q(neg_algebraMap $pt)⟩
-  | none => failure
+    MetaM (Common.Result (BaseType sAlg) q(-$a)) :=
+  match za with
+  | .mk r vr => do
+    match cR.rα with
+    | some rR =>
+      let ⟨_, vt, pt⟩ ← Common.evalNeg (Ring.ringCompute cR.toCache) q($rR) vr
+      assumeInstancesCommute
+      return ⟨_, .mk _ vt, q(neg_algebraMap $pt)⟩
+    | none => failure
 
 /-- Raise a normalized expression in `R` to the power of a normalized natural number expression
 using `ring`. -/
 def pow (cR : Common.Cache sR) {a : Q($A)} {b : Q(ℕ)} (za : BaseType sAlg a)
     (vb : Common.ExProdNat q($b)) :
-    OptionT MetaM (Common.Result (BaseType sAlg) q($a ^ $b)) := do
-  let ⟨r, vr⟩ := za
-  let ⟨_, vs, ps⟩ ← Common.evalPow₁ (Ring.ringCompute cR) rcℕ vr vb
-  return ⟨_, ⟨_, vs⟩, q(pow_algebraMap $ps)⟩
+    OptionT MetaM (Common.Result (BaseType sAlg) q($a ^ $b)) :=
+  match za with
+  | .mk r vr => do
+    let ⟨_, vs, ps⟩ ← Common.evalPow₁ (Ring.ringCompute cR) rcℕ vr vb
+    return ⟨_, ⟨_, vs⟩, q(pow_algebraMap $ps)⟩
 
 /-- Evaluate the inverse of two normalized expressions in `R` using `ring`. -/
 /- We include the CharZero argument to match the type signature of the ringCompute entry. -/
 @[nolint unusedArguments]
 def inv (cR : Algebra.Cache sR) {a : Q($A)} (_ : Option Q(CharZero $A)) (fA : Q(Semifield $A))
-    (za : BaseType sAlg a) : AtomM (Option (Common.Result (BaseType sAlg) q($a⁻¹))) := do
-  match cR.dsα with
-  | some fR =>
-    let ⟨r, vr⟩ := za
-    let ⟨_, vs, ps⟩ ← Common.ExSum.evalInv (Ring.ringCompute cR.toCache) rcℕ q($fR) cR.czα vr
-    assumeInstancesCommute
-    return some ⟨_, ⟨_, vs⟩, q(inv_algebraMap $ps)⟩
-  | none =>
-    return none
+    (za : BaseType sAlg a) : AtomM (Option (Common.Result (BaseType sAlg) q($a⁻¹))) :=
+  match za with
+  | .mk r vr => do
+    match cR.dsα with
+    | some fR =>
+      let ⟨_, vs, ps⟩ ← Common.ExSum.evalInv (Ring.ringCompute cR.toCache) rcℕ q($fR) cR.czα vr
+      assumeInstancesCommute
+      return some ⟨_, ⟨_, vs⟩, q(inv_algebraMap $ps)⟩
+    | none =>
+      return none
 
 /-- Evaluate constants in `A` using `norm_num`. -/
 def derive (cR : Algebra.Cache sR) (cA : Algebra.Cache sA) (x : Q($A)) :

Mathlib/Tactic/FieldSimp.lean

@@ -62,7 +62,7 @@ def onExponent (l : qNF M) (f : ℤ → ℤ) : qNF M :=
 
 /-- Build a transparent expression for the product of powers represented by `l : qNF M`. -/
 def evalPrettyMonomial (iM : Q(GroupWithZero $M)) (r : ℤ) (x : Q($M)) :
-    MetaM (Σ e : Q($M), Q(zpow' $x $r = $e)) := do
+    MetaM (Σ e : Q($M), Q(zpow' $x $r = $e)) :=
   match r with
   | 0 => /- If an exponent is zero then we must not have been able to prove that x is nonzero.  -/
     return ⟨q($x / $x), q(zpow'_zero_eq_div ..)⟩
@@ -111,10 +111,10 @@ def removeZeros
 of) the negative powers. -/
 def split (iM : Q(CommGroupWithZero $M)) (l : qNF M) :
     MetaM (Σ l_n l_d : qNF M, Q(NF.eval $(l.toNF)
-      = NF.eval $(l_n.toNF) / NF.eval $(l_d.toNF))) := do
+      = NF.eval $(l_n.toNF) / NF.eval $(l_d.toNF))) :=
   match l with
   | [] => return ⟨[], [], q(Eq.symm (div_one (1:$M)))⟩
-  | ((r, x), i) :: t =>
+  | ((r, x), i) :: t => do
     let ⟨t_n, t_d, pf⟩ ← split iM t
     if r > 0 then
       return ⟨((r, x), i) :: t_n, t_d, (q(NF.cons_eq_div_of_eq_div $r $x $pf):)⟩
@@ -125,13 +125,13 @@ def split (iM : Q(CommGroupWithZero $M)) (l : qNF M) :
       return ⟨t_n, ((r', x), i) :: t_d, (q(NF.cons_eq_div_of_eq_div' $r' $x $pf):)⟩
 
 private def evalPrettyAux (iM : Q(CommGroupWithZero $M)) (l : qNF M) :
-    MetaM (Σ e : Q($M), Q(NF.eval $(l.toNF) = $e)) := do
+    MetaM (Σ e : Q($M), Q(NF.eval $(l.toNF) = $e)) :=
   match l with
   | [] => return ⟨q(1), q(rfl)⟩
-  | [((r, x), _)] =>
+  | [((r, x), _)] => do
     let ⟨e, pf⟩ ← evalPrettyMonomial q(inferInstance) r x
     return ⟨e, q(by rw [NF.eval_cons]; exact Eq.trans (one_mul _) $pf)⟩
-  | ((r, x), k) :: t =>
+  | ((r, x), k) :: t => do
     let ⟨e, pf_e⟩ ← evalPrettyMonomial q(inferInstance) r x
     let ⟨t', pf⟩ ← evalPrettyAux iM t
     have pf'' : Q(NF.eval $(qNF.toNF (((r, x), k) :: t)) = (NF.eval $(qNF.toNF t)) * zpow' $x $r) :=
@@ -144,7 +144,7 @@ def evalPretty (iM : Q(CommGroupWithZero $M)) (l : qNF M) :
   let ⟨l_n, l_d, pf⟩ ← split iM l
   let ⟨num, pf_n⟩ ← evalPrettyAux q(inferInstance) l_n
   let ⟨den, pf_d⟩ ← evalPrettyAux q(inferInstance) l_d
-  match l_d with
+  match (dependent := true) l_d with
   | [] => return ⟨num, q(eq_div_of_eq_one_of_subst $pf $pf_n)⟩
   | _ =>
     let pf_n : Q(NF.eval $(l_n.toNF) = $num) := pf_n
@@ -281,14 +281,14 @@ def mkDenomConditionProofSucc {iM : Q(CommGroupWithZero $M)}
     (disch : ∀ {u : Level} (type : Q(Sort u)), MetaM Q($type))
     {cond : DenomCondition (M := M) q(inferInstance)}
     {L : qNF M} (hL : cond.proof L) (e : Q($M)) (r : ℤ) (i : ℕ) :
-    MetaM (Q($e ≠ 0) × cond.proof (((r, e), i) :: L)) := do
+    MetaM (Q($e ≠ 0) × cond.proof (((r, e), i) :: L)) :=
   match cond with
   | .none => return (← disch q($e ≠ 0), Unit.unit)
-  | .nonzero =>
+  | .nonzero => do
     let pf ← disch q($e ≠ 0)
     let pf₀ : Q(NF.eval $(qNF.toNF L) ≠ 0) := hL
     return (pf, q(NF.cons_ne_zero $r $pf $pf₀))
-  | .positive _ _ _ _ =>
+  | .positive _ _ _ _ => do
     let pf ← disch q(0 < $e)
     let pf₀ : Q(0 < NF.eval $(qNF.toNF L)) := hL
     let pf' := q(NF.cons_pos $r (x := $e) $pf $pf₀)
@@ -301,14 +301,14 @@ def mkDenomConditionProofSucc' {iM : Q(CommGroupWithZero $M)}
     (disch : ∀ {u : Level} (type : Q(Sort u)), MetaM Q($type))
     {cond : DenomCondition (M := M) q(inferInstance)}
     {L : qNF M} (hL : cond.proof L) (e : Q($M)) (r : ℤ) (i : ℕ) :
-    MetaM (cond.proof (((r, e), i) :: L)) := do
+    MetaM (cond.proof (((r, e), i) :: L)) :=
   match cond with
   | .none => return Unit.unit
-  | .nonzero =>
+  | .nonzero => do
     let pf ← disch q($e ≠ 0)
     let pf₀ : Q(NF.eval $(qNF.toNF L) ≠ 0) := hL
     return q(NF.cons_ne_zero $r $pf $pf₀)
-  | .positive _ _ _ _ =>
+  | .positive _ _ _ _ => do
     let pf ← disch q(0 < $e)
     let pf₀ : Q(0 < NF.eval $(qNF.toNF L)) := hL
     return q(NF.cons_pos $r (x := $e) $pf $pf₀)

Mathlib/Tactic/FieldSimp/Lemmas.lean

@@ -398,7 +398,7 @@ def Sign.expr : Sign M → Q($M) → Q($M)
 the product with `c` of (± `y`) (here taking the specified sign) is ± `c * y`. -/
 def Sign.mulRight (iM : Q(CommGroupWithZero $M)) (c y : Q($M)) (g : Sign M) :
     MetaM Q($(g.expr q($c * $y)) = $c * $(g.expr y)) := do
-  match g with
+  match (dependent := true) g with
   | .plus => pure q(rfl)
   | .minus _ =>
     assumeInstancesCommute
@@ -409,7 +409,7 @@ the product of (± `y₁`) and (± `y₂`) (here taking the specified signs) is
 proof and the computed sign. -/
 def Sign.mul (iM : Q(CommGroupWithZero $M)) (y₁ y₂ : Q($M)) (g₁ g₂ : Sign M) :
     MetaM (Σ (G : Sign M), Q($(g₁.expr y₁) * $(g₂.expr y₂) = $(G.expr q($y₁ * $y₂)))) := do
-  match g₁, g₂ with
+  match (dependent := true) g₁, g₂ with
   | .plus, .plus => pure ⟨.plus, q(rfl)⟩
   | .plus, .minus i =>
     assumeInstancesCommute
@@ -425,7 +425,7 @@ def Sign.mul (iM : Q(CommGroupWithZero $M)) (y₁ y₂ : Q($M)) (g₁ g₂ : Sig
 the inverse of (± `y`) (here taking the specified sign) is ± `y⁻¹`. -/
 def Sign.inv (iM : Q(CommGroupWithZero $M)) (y : Q($M)) (g : Sign M) :
     MetaM (Q($(g.expr y)⁻¹ = $(g.expr q($y⁻¹)))) := do
-  match g with
+  match (dependent := true) g with
   | .plus => pure q(rfl)
   | .minus _ =>
     assumeInstancesCommute
@@ -436,7 +436,7 @@ the quotient of (± `y₁`) and (± `y₂`) (here taking the specified signs) is
 proof and the computed sign. -/
 def Sign.div (iM : Q(CommGroupWithZero $M)) (y₁ y₂ : Q($M)) (g₁ g₂ : Sign M) :
     MetaM (Σ (G : Sign M), Q($(g₁.expr y₁) / $(g₂.expr y₂) = $(G.expr q($y₁ / $y₂)))) := do
-  match g₁, g₂ with
+  match (dependent := true) g₁, g₂ with
   | .plus, .plus => pure ⟨.plus, q(rfl)⟩
   | .plus, .minus i =>
     assumeInstancesCommute
@@ -452,7 +452,7 @@ def Sign.div (iM : Q(CommGroupWithZero $M)) (y₁ y₂ : Q($M)) (g₁ g₂ : Sig
 the negation of (± `y`) (here taking the specified sign) is ∓ `y`. -/
 def Sign.neg (iM : Q(Field $M)) (y : Q($M)) (g : Sign M) :
     MetaM (Σ (G : Sign M), Q(-$(g.expr y) = $(G.expr y))) := do
-  match g with
+  match (dependent := true) g with
   | .plus => pure ⟨.minus iM, q(rfl)⟩
   | .minus _ =>
     assumeInstancesCommute
@@ -463,7 +463,7 @@ the exponentiation to power `s : ℕ` of (± `y`) (here taking the specified sig
 return this proof and the computed sign. -/
 def Sign.pow (iM : Q(CommGroupWithZero $M)) (y : Q($M)) (g : Sign M) (s : ℕ) :
     MetaM (Σ (G : Sign M), Q($(g.expr y) ^ $s = $(G.expr q($y ^ $s)))) := do
-  match g with
+  match (dependent := true) g with
   | .plus => pure ⟨.plus, q(rfl)⟩
   | .minus i =>
     assumeInstancesCommute
@@ -479,7 +479,7 @@ the exponentiation to power `s : ℤ` of (± `y`) (here taking the specified sig
 return this proof and the computed sign. -/
 def Sign.zpow (iM : Q(CommGroupWithZero $M)) (y : Q($M)) (g : Sign M) (s : ℤ) :
     MetaM (Σ (G : Sign M), Q($(g.expr y) ^ $s = $(G.expr q($y ^ $s)))) := do
-  match g with
+  match (dependent := true) g with
   | .plus => pure ⟨.plus, q(rfl)⟩
   | .minus i =>
     assumeInstancesCommute

Mathlib/Tactic/Linter/Whitespace.lean

@@ -335,7 +335,7 @@ def whitespaceLinter : Linter where run := withSetOptionIn fun stx ↦ do
 
   let fmt : Option Format := ←
       try
-        liftCoreM <| PrettyPrinter.ppCategory `command stx
+        liftCoreM <| some <$> PrettyPrinter.ppCategory `command stx
       catch _ =>
         Linter.logLintIf linter.style.whitespace.verbose (stx.getHead?.getD stx)
           m!"The `whitespace` linter had some parsing issues: \

Mathlib/Tactic/NormNum/Core.lean

@@ -150,7 +150,7 @@ and returning the truth or falsity of `p' : Prop` from an equivalence `p ↔ p'`
 def deriveBoolOfIff (p p' : Q(Prop)) (hp : Q($p ↔ $p')) :
     MetaM ((b : Bool) × BoolResult p' b) := do
   let ⟨b, pb⟩ ← deriveBool p
-  match b with
+  match (dependent := true) b with
   | true  => return ⟨true, q(Iff.mp $hp $pb)⟩
   | false => return ⟨false, q((Iff.not $hp).mp $pb)⟩