tactic porting tracking issue

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 #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 leanprover/lean4#1364 stalled. @bollu is no longer working on it
• ☑️ S clean
  • @mkaratarakis PR'd as #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
  • #2544
• ☑️ E ac_change
  • @Komyyy PR'd as #5869
• 🔹 M decide!
• 🔹 M delta_instance
• 🔹 M generalizes
• ☑️ B itauto
  • @digama0 PR'd as #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 #1740
  • @thorimur is working on the full version
• 🔹 B ac_mono
• 🔹 M unfold_cases
• 🔹 B equiv_rw
• ☑️ N nth_rw
  • PR'd as #823, although this doesn't actually reproduce the mathlib3 behaviour
• ☑️ M compute_degree_le
  • @adomani PR'd as #5882 #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 #1740
  • @thorimur is working on the full version
• ☑️ N add_tactic_doc
  • @lakesare PR'd as #639
• 🔹 (command) N mk_simp_attribute
• ☑️ (command) M add_hint_tactic
  • @Komyyy PR'd as #5363
  • @semorrison PR'd as #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 #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 #4595
• 🔹 S revert_deps
• 🔹 S revert_after
• ☑️ S revert_target_deps
  • PR'd as #333
• 🔹 S rcases?
• 🔹 S rintro?
• ☑️ S hint
  • @Komyyy PR'd as #5363
  • @semorrison PR'd as #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 #6120
• ☑️ S mk_decorations
• ☑️ S mv_bisim
• @Komyyy PR'd as #2444
• 🔹 S subtype_instance
• 🔹 S elide / S unelide
• ☑️ S guard_tags
  • PR'd as #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

Start by comparing the unclaimed entries in Mathlib/Mathport/Syntax.lean with this tracker, then review the linked tactic references and any recorded porting notes for one specific item. Done means completing or stubbing that tactic as appropriate and updating its status and notes here.