chore: remove upstreamed tactics 11-21 (#684)

Author: digama0

Mathlib.lean

@@ -148,13 +148,11 @@ import Mathlib.Tactic.Clear!
 import Mathlib.Tactic.ClearExcept
 import Mathlib.Tactic.Clear_
 import Mathlib.Tactic.Coe
-import Mathlib.Tactic.Congr
 import Mathlib.Tactic.Constructor
 import Mathlib.Tactic.Contrapose
 import Mathlib.Tactic.Conv
 import Mathlib.Tactic.Convert
 import Mathlib.Tactic.Core
-import Mathlib.Tactic.DocCommands
 import Mathlib.Tactic.Existsi
 import Mathlib.Tactic.Expect
 import Mathlib.Tactic.FinCases
@@ -199,11 +197,9 @@ import Mathlib.Tactic.Ring.RingNF
 import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Sat.FromLRAT
 import Mathlib.Tactic.ScopedNS
-import Mathlib.Tactic.SeqFocus
 import Mathlib.Tactic.Set
 import Mathlib.Tactic.SimpIntro
 import Mathlib.Tactic.SimpRw
-import Mathlib.Tactic.SimpTrace
 import Mathlib.Tactic.Simps.Basic
 import Mathlib.Tactic.Simps.NotationClass
 import Mathlib.Tactic.SolveByElim

Mathlib/Data/FunLike/Basic.lean

@@ -148,9 +148,8 @@ instance (priority := 100) : CoeFun F fun _ ↦ ∀ a : α, β a where coe := Fu
   Tactic.NormCast.registerCoercion ``FunLike.coe
     (some { numArgs := 5, coercee := 4, type := .coeFun })
 
-@[simp]
-theorem coe_eq_coe_fn : (FunLike.coe : F → ∀ a : α, β a) = (fun f ↦ ↑f) :=
-  rfl
+-- @[simp] -- porting note: this loops in lean 4
+theorem coe_eq_coe_fn : (FunLike.coe (F := F)) = (fun f => ↑f) := rfl
 
 theorem coe_injective : Function.Injective (fun f : F ↦ (f : ∀ a : α, β a)) :=
   FunLike.coe_injective'

Mathlib/Init/Logic.lean

@@ -8,7 +8,6 @@ import Std.Tactic.Lint.Basic
 import Std.Logic
 import Mathlib.Tactic.Alias
 import Mathlib.Tactic.Basic
-import Mathlib.Tactic.SimpTrace
 import Mathlib.Tactic.Relation.Symm
 import Mathlib.Mathport.Attributes
 import Mathlib.Mathport.Rename

Mathlib/Logic/Basic.lean

@@ -8,7 +8,6 @@ import Mathlib.Init.Function
 import Mathlib.Init.Algebra.Classes
 import Mathlib.Tactic.Basic
 import Mathlib.Tactic.LeftRight
-import Mathlib.Tactic.SimpTrace
 import Std.Util.LibraryNote
 import Std.Tactic.Lint.Basic
 

Mathlib/Mathport/Syntax.lean

@@ -21,13 +21,11 @@ import Mathlib.Tactic.Classical
 import Mathlib.Tactic.Clear_
 import Mathlib.Tactic.Clear!
 import Mathlib.Tactic.ClearExcept
-import Mathlib.Tactic.Congr
 import Mathlib.Tactic.Constructor
 import Mathlib.Tactic.Contrapose
 import Mathlib.Tactic.Conv
 import Mathlib.Tactic.Convert
 import Mathlib.Tactic.Core
-import Mathlib.Tactic.DocCommands
 import Mathlib.Tactic.Existsi
 import Mathlib.Tactic.FinCases
 import Mathlib.Tactic.Find
@@ -58,12 +56,10 @@ import Mathlib.Tactic.RestateAxiom
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.ScopedNS
-import Mathlib.Tactic.SeqFocus
 import Mathlib.Tactic.Set
 import Mathlib.Tactic.SimpIntro
 import Mathlib.Tactic.SimpRw
 import Mathlib.Tactic.Simps.Basic
-import Mathlib.Tactic.SimpTrace
 import Mathlib.Tactic.SolveByElim
 import Mathlib.Tactic.SplitIfs
 import Mathlib.Tactic.Substs
@@ -209,7 +205,6 @@ namespace Tactic
 
 /- S -/ syntax (name := propagateTags) "propagate_tags " tacticSeq : tactic
 /- S -/ syntax (name := mapply) "mapply " term : tactic
-/- S -/ syntax (name := withCases) "with_cases " tacticSeq : tactic
 /- S -/ syntax "destruct " term : tactic
 /- N -/ syntax (name := abstract) "abstract" (ppSpace ident)? ppSpace tacticSeq : tactic
 
@@ -221,15 +216,6 @@ namespace Tactic
 /- S -/ syntax (name := compVal) "comp_val" : tactic
 /- S -/ syntax (name := async) "async " tacticSeq : tactic
 
-/- E -/ syntax (name := apply') "apply' " term : tactic
-/- E -/ syntax (name := fapply') "fapply' " term : tactic
-/- E -/ syntax (name := eapply') "eapply' " term : tactic
-/- E -/ syntax (name := applyWith') "apply_with' " (config)? term : tactic
-/- E -/ syntax (name := mapply') "mapply' " term : tactic
-/- E -/ syntax (name := rfl') "rfl'" : tactic
-/- E -/ syntax (name := symm') "symm'" (ppSpace location)? : tactic
-/- E -/ syntax (name := trans') "trans'" (ppSpace term)? : tactic
-
 /- M -/ syntax (name := injectionsAndClear) "injections_and_clear" : tactic
 
 /- E -/ syntax (name := tryFor) "try_for " term:max tacticSeq : tactic