This issue parallels the content of Mathlib/Mathport/Syntax.lean, tracking the remaining work to port mathlib3 tactics to mathlib4, but also contains "ephemeral" information that does not belong in that file.

Primarily, this issue contains a list of tactics (or groups of tactics), along with any relevant information about work-in-progress (e.g. people who've "claimed" a tactic, PRs, abandoned work, etc). Some "claims" are probably out-of-date. Feel free to remove yourself from anything here without explanation!

We hope that everyone will edit this freely to try to keep it up to date.

Currently this is in the same order as Syntax.lean (although with tactics we might skip or only "stub" deferred to the end), but it may be worthwhile to turn this into a prioritised list.

🔹 – unclaimed
◼️ – claimed
☑️ – PR'd, unneeded, or otherwise done

E: Easy. It's a simple macro in terms of existing things,
or an elab tactic for which we have many similar examples. Example: left
M: Medium. An elab tactic, not too hard, perhaps a 100-200 lines file. Example: have
N: Possibly requires new mechanisms in lean 4, some investigation required
B: Hard, because it is a big and complicated tactic
S: Possibly easy, because we can just stub it out or replace with something else
?: uncategorized

• 🔹 N parameter
  • there is a proposal in terms of nullary typeclasses
• ☑️ S abstract
  • ported in core as as_aux_lemma
• ☑️ B cc
  • @Komyyy PR'd as [Merged by Bors] - feat: port cc tactic (3/3) #5938
• 🔹 M unfold_projs
  • there are some porting notes that should be reviewed, to decide if we're just missing simp lemmas, or really want this tactic
• 🔹 N try_for
  • Started by @bollu, but connect maxHeartbeats in CoreM to kernel variable max_heartbeats leanprover/lean4#1364 stalled. @bollu is no longer working on it
• ☑️ S clean
  • @mkaratarakis PR'd as [Merged by Bors] - port the clean tactic from lean 3 to lean 4 #5909
• ☑️ S refine_struct
  • Use refine' with built-in .. syntax, e.g. refine' { x := 0, y := 1 .. }
• 🔹 M match_hyp
• 🔹 N field / S have_field / S apply_field
• 🔹 M h_generalize
• ☑️ M congrm
  • [Merged by Bors] - feat: congr(...) congruence quotations and port congrm tactic #2544
• ☑️ E ac_change
  • @Komyyy PR'd as [Merged by Bors] - feat: port ac_change tactic #5869
• 🔹 M decide!
• 🔹 M delta_instance
• 🔹 M generalizes
• ☑️ B itauto
  • @digama0 PR'd as [Merged by Bors] - feat: port itauto from lean 3  #9398
• 🔹 B obviously
• 🔹 M assoc_rw
• 🔹 S dsimp_result / N simp_result
• 🔹 M trunc_cases
• 🔹 E apply_normed
• ◼️ M mono
  • A quick version is PR'd as [Merged by Bors] - feat: quick version of mono tactic #1740
  • @thorimur is working on the full version
• 🔹 B ac_mono
• 🔹 M unfold_cases
• 🔹 B equiv_rw
• ☑️ N nth_rw
  • PR'd as [Merged by Bors] - feat: port nth_rewrite #823, although this doesn't actually reproduce the mathlib3 behaviour
• ☑️ M compute_degree_le
  • @adomani PR'd as feat: Add tactic compute_degree_le #5882 [Merged by Bors] - feat: tactic compute_degree #6221
• 🔹 M padic_index_simp
• ☑️ E uniqueDiffWithinAt_Ici_Iic_univ
• ☑️ M ghost_fun_tac
• ☑️ M ghost_calc
• ☑️ M init_ring
• ☑️ E ghost_simp
• ☑️ E witt_truncate_fun_tac
• ☑️ M pure_coherence / M coherence
• 🔹 (conv mode) E [norm_num][norm_num-conv] / E [norm_num1][norm_num1-conv]
  • @bollu claimed this is no longer working on it
• ☑️ (attribute) ? protect_proj
  • Not needed because protected can be used for constructors.
• ☑️ (attribute) M notation_class
• ◼️ (attribute) M mono
  • A quick version is PR'd as [Merged by Bors] - feat: quick version of mono tactic #1740
  • @thorimur is working on the full version
• ☑️ N add_tactic_doc
  • @lakesare PR'd as feat: port addTacticDoc #639
• 🔹 (command) N mk_simp_attribute
• ☑️ (command) M add_hint_tactic
  • @Komyyy PR'd as feat: port tactic hint #5363
  • @semorrison PR'd as [Merged by Bors] - feat: the 'hint' tactic #8363 and renamed to register_hint
• 🔹 (command) N def_replacer
• 🔹 (command) M reassoc_axiom

We then have a number of tactics and commands for which mere stubs will suffice for the port. Sometimes this is because the tactic is only used during development (but not in PRs to mathlib), other times because it is not used at all anymore in mathlib.

• 🔹 (attribute) S intro / S intro!
• 🔹 S propagate_tags
  • PR'd as feat: propagate_tags tactic #258 (abandoned?)
• 🔹 ? quote / ? pquote / ? ppquote
• 🔹 S mapply
• 🔹 S destruct
• 🔹 S rsimp
• ☑️ S comp_val
  • Use decide.
• 🔹 S async
• 🔹 S continue
• ☑️ S extract_goal
  • @robertylewis claimed this.
  • @adomani PR'd as [Merged by Bors] - feat(Tactic/ExtractGoal + test/ExtractGoal): port extract_goal tactic #4595
• 🔹 S revert_deps
• 🔹 S revert_after
• ☑️ S revert_target_deps
  • PR'd as feat: revert_target_deps tactic #333
• 🔹 S rcases?
• 🔹 S rintro?
• ☑️ S hint
  • @Komyyy PR'd as feat: port tactic hint #5363
  • @semorrison PR'd as [Merged by Bors] - feat: the 'hint' tactic #8363
• 🔹 S clarify / S safe / S finish
• 🔹 S cases'' / S induction''
• 🔹 S pretty_cases
• 🔹 S suggest
• ☑️ S omega
• 🔹 S transport
• ☑️ S rw_search
  • @semorrison PR'd as [Merged by Bors] - feat: the rw_search tactic #6120
• ☑️ S mk_decorations
• ☑️ S mv_bisim
• @Komyyy PR'd as [Merged by Bors] - feat: port Data.QPF.Multivariate.Constructions.Cofix #2444
• 🔹 S subtype_instance
• 🔹 S elide / S unelide
• ☑️ S guard_tags
  • PR'd as feat: propagate_tags tactic #258
• 🔹 S guard_proof_term
• ☑️ S fail_if_success
• ☑️ (command) S setup_tactic_parser
  • This command is not needed because ? and * notations for sytaxes are available without a command.
• 🔹 (command) S #list_unused_decls
• ☑️ (command) S #simp
• ☑️ (command) S #where
• ☑️ (command) S #sample