chore: compatibility with Lean incrementality branch (#12796)

Backward-compatible fixes for leanprover/lean4#3940. In particular, gets rid of two `open private` (out of six in all of Mathlib) which in my opinion really were not necessary and just invited breakage.

Somehow the unused variables and unnecessary `have` linters became *more* complete, which might be due to earlier mvar instantiation in `Elab.MutualDef` but I haven't investigated deeply.

Mathlib/Algebra/CharZero/Lemmas.lean

@@ -206,7 +206,7 @@ section RingHom
 
 variable {R S : Type*} [NonAssocSemiring R] [NonAssocSemiring S]
 
-theorem RingHom.charZero (ϕ : R →+* S) [hS : CharZero S] : CharZero R :=
+theorem RingHom.charZero (ϕ : R →+* S) [CharZero S] : CharZero R :=
   ⟨fun a b h => CharZero.cast_injective (by rw [← map_natCast ϕ, ← map_natCast ϕ, h])⟩
 #align ring_hom.char_zero RingHom.charZero
 

Mathlib/LinearAlgebra/Semisimple.lean

@@ -129,7 +129,6 @@ theorem IsSemisimple.minpoly_squarefree : Squarefree (minpoly K f) :=
 protected theorem IsSemisimple.aeval (p : K[X]) : (aeval f p).IsSemisimple :=
   let R := K[X] ⧸ Ideal.span {minpoly K f}
   have : Finite K R := (AdjoinRoot.powerBasis' <| minpoly.monic <| isIntegral f).finite
-  have : IsArtinianRing R := .of_finite K R
   have : IsReduced R := (Ideal.isRadical_iff_quotient_reduced _).mp <|
     span_minpoly_eq_annihilator K f ▸ hf.annihilator_isRadical
   isSemisimple_of_squarefree_aeval_eq_zero ((minpoly.isRadical K _).squarefree <|

Mathlib/Tactic/Cases.lean

@@ -38,7 +38,12 @@ Prefer `cases` or `rcases` when possible, because these tactics promote structur
 namespace Mathlib.Tactic
 open Lean Meta Elab Elab.Tactic
 
-open private getAltNumFields in evalCases ElimApp.evalAlts.go in
+private def getAltNumFields (elimInfo : ElimInfo) (altName : Name) : TermElabM Nat := do
+  for altInfo in elimInfo.altsInfo do
+    if altInfo.name == altName then
+      return altInfo.numFields
+  throwError "unknown alternative name '{altName}'"
+
 def ElimApp.evalNames (elimInfo : ElimInfo) (alts : Array ElimApp.Alt) (withArg : Syntax)
     (numEqs := 0) (generalized : Array FVarId := #[]) (toClear : Array FVarId := #[])
     (toTag : Array (Ident × FVarId) := #[]) :

Mathlib/Tactic/Recall.lean

@@ -3,8 +3,8 @@ Copyright (c) 2023 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone, Kyle Miller
 -/
-import Lean.Elab.MutualDef
-import Batteries.Tactic.OpenPrivate
+import Lean.Elab.Command
+import Lean.Elab.DeclUtil
 
 /-!
 # `recall` command
@@ -35,7 +35,6 @@ recall Nat.add_comm {n m : Nat} : n + m = m + n
 syntax (name := recall) "recall " ident ppIndent(optDeclSig) (declVal)? : command
 
 open Lean Meta Elab Command Term
-open private elabHeaders from Lean.Elab.MutualDef
 
 elab_rules : command
   | `(recall $id $sig:optDeclSig $[$val?]?) => withoutModifyingEnv do
@@ -63,10 +62,17 @@ elab_rules : command
           throwErrorAt val err
     else
       let (binders, type?) := expandOptDeclSig sig
-      let views := #[{
-        declId := newId, binders, type?, value := .missing,
-        ref := ← getRef, kind := default, modifiers := {} : DefView}]
-      liftTermElabM do
-        let elabView := (← elabHeaders views)[0]!
-        unless (← isDefEq info.type elabView.type) do
-          throwTypeMismatchError none info.type elabView.type declConst
+      if let some type := type? then
+        runTermElabM fun vars => do
+          withAutoBoundImplicit do
+            elabBinders binders.getArgs fun xs => do
+              let xs ← addAutoBoundImplicits xs
+              let type ← elabType type
+              Term.synthesizeSyntheticMVarsNoPostponing
+              let type ← mkForallFVars xs type
+              let type ← mkForallFVars vars type (usedOnly := true)
+              unless (← isDefEq info.type type) do
+                throwTypeMismatchError none info.type type declConst
+      else
+        unless binders.getNumArgs == 0 do
+          throwError "expected type after ':'"

Mathlib/Tactic/Says.lean

@@ -67,7 +67,7 @@ def evalTacticCapturingMessages (tac : TSyntax `tactic) (only : Message → Bool
   try
     evalTactic tac
     let (capture, leave) := (← getThe Core.State).messages.msgs.toList.partition only
-    msgs := ⟨leave.foldl (fun m => m.push) msgs.msgs⟩
+    msgs := leave.foldl (·.add) msgs
     return capture
   catch e =>
     msgs := msgs ++ (← getThe Core.State).messages