refactor: do not import old-style have/suffices/replace within …

…mathlib (#10534)

This syntax remains available downstream with `import Mathlib.Tactic`, but is no longer available in mathlib itself.

This follows on from #10640, which remove all current uses of this syntax.

By removing these imports, we prevent further regressions in mathlib,
and save reviewers from having to look out for this in review.

In future we could delete this syntax entirely, but this would harm downstream code, especially mathport output.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Mathlib/Data/Rat/Lemmas.lean

@@ -7,7 +7,6 @@ import Mathlib.Data.Rat.Defs
 import Mathlib.Data.Int.Cast.Lemmas
 import Mathlib.Data.Int.Div
 import Mathlib.Algebra.GroupWithZero.Units.Lemmas
-import Mathlib.Tactic.Replace
 import Mathlib.Data.PNat.Defs
 
 #align_import data.rat.lemmas from "leanprover-community/mathlib"@"550b58538991c8977703fdeb7c9d51a5aa27df11"

Mathlib/Tactic/Common.lean

@@ -48,7 +48,6 @@ import Mathlib.Tactic.Find
 import Mathlib.Tactic.GeneralizeProofs
 import Mathlib.Tactic.GuardGoalNums
 import Mathlib.Tactic.GuardHypNums
-import Mathlib.Tactic.Have
 import Mathlib.Tactic.HelpCmd
 import Mathlib.Tactic.HigherOrder
 import Mathlib.Tactic.Hint
@@ -68,7 +67,6 @@ import Mathlib.Tactic.Observe
 import Mathlib.Tactic.ProjectionNotation
 import Mathlib.Tactic.Propose
 import Mathlib.Tactic.PushNeg
-import Mathlib.Tactic.Replace
 import Mathlib.Tactic.RSuffices
 import Mathlib.Tactic.Recover
 import Mathlib.Tactic.Relation.Symm

Mathlib/Tactic/Have.lean

@@ -12,6 +12,9 @@ import Lean.Meta.Tactic.Assert
 
 This file extends the `have`, `let` and `suffices` tactics to allow the addition of hypotheses to
 the context without requiring their proofs to be provided immediately.
+
+As a style choice, this should not be used in mathlib; but is provided for downstream users who
+preferred the old style.
 -/
 
 namespace Mathlib.Tactic

Mathlib/Tactic/Replace.lean

@@ -6,6 +6,16 @@ Authors: Arthur Paulino, Mario Carneiro
 import Std.Tactic.Replace
 import Mathlib.Tactic.Have
 
+/-!
+# Extending `replace`
+
+This file extends the `replace` tactic from `Std` to allow the addition of hypotheses to
+the context without requiring their proofs to be provided immediately.
+
+As a style choice, this should not be used in mathlib; but is provided for downstream users who
+preferred the old style.
+-/
+
 namespace Mathlib.Tactic
 
 open Lean Elab.Tactic

test/slim_check.lean

@@ -2,6 +2,7 @@ import Mathlib.Tactic.SlimCheck
 import Mathlib.Tactic.SuccessIfFailWithMsg
 import Mathlib.Data.Finsupp.Notation
 import Mathlib.Testing.SlimCheck.Functions
+import Mathlib.Tactic.Have
 
 private axiom test_sorry : ∀ {α}, α