From 38b54e1ec0e2f45a2579e558f7467d419094ef52 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 10 May 2024 12:00:05 +0000
Subject: [PATCH] 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  |  2 +-
 Mathlib/LinearAlgebra/Semisimple.lean |  1 -
 Mathlib/Tactic/Cases.lean             |  7 ++++++-
 Mathlib/Tactic/Recall.lean            | 26 ++++++++++++++++----------
 Mathlib/Tactic/Says.lean              |  2 +-
 5 files changed, 24 insertions(+), 14 deletions(-)

diff --git a/Mathlib/Algebra/CharZero/Lemmas.lean b/Mathlib/Algebra/CharZero/Lemmas.lean
index be3d3af831e2e9..449c2c022f3ff7 100644
--- a/Mathlib/Algebra/CharZero/Lemmas.lean
+++ b/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
 
diff --git a/Mathlib/LinearAlgebra/Semisimple.lean b/Mathlib/LinearAlgebra/Semisimple.lean
index d13b7b1cf83e82..04a49b655dabae 100644
--- a/Mathlib/LinearAlgebra/Semisimple.lean
+++ b/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 <|
diff --git a/Mathlib/Tactic/Cases.lean b/Mathlib/Tactic/Cases.lean
index 6ab93ef383a3e8..506b29caf60cd9 100644
--- a/Mathlib/Tactic/Cases.lean
+++ b/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) := #[]) :
diff --git a/Mathlib/Tactic/Recall.lean b/Mathlib/Tactic/Recall.lean
index cdd3c8d630e001..373b55ea8adddd 100644
--- a/Mathlib/Tactic/Recall.lean
+++ b/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 ':'"
diff --git a/Mathlib/Tactic/Says.lean b/Mathlib/Tactic/Says.lean
index b653ac9dbc5434..e2c341cb51cd2b 100644
--- a/Mathlib/Tactic/Says.lean
+++ b/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