Commit 2023-09-05 07:06 4047be94

View on Github →

chore: remove unnecessary imports in tactics (#6940) This is motivated by preparations for upstreaming tactics to Std.

Estimated changes

Modified Mathlib/Data/Part.lean

Modified Mathlib/Tactic/InferParam.lean

Modified Mathlib/Tactic/NormCast/Tactic.lean

Modified Mathlib/Tactic/Recover.lean

Modified Mathlib/Tactic/Rewrites.lean

Modified Mathlib/Tactic/SolveByElim.lean

Modified Mathlib/Tactic/SplitIfs.lean

Modified Mathlib/Tactic/Tauto.lean

Modified test/SplitIfs.lean

modified theorem foo