Proj as a scheme: `mem_tac` works accidentally?

Stream: mathlib4

[Anne Baanen]

I'm going through all the undocumented tactics in Mathlib and writing documentation for them, and encountered mem_tac (docs#AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.tacticMem_tac) and mem_tac_aux. But it doesn't really make sense to me, it seems broken?

/-- `mem_tac_aux` tries to prove goals of the form `x ∈ 𝒜 i` when `x` has the form of:
* `y ^ n` where `i = n • j` and `y ∈ 𝒜 j`.
* a natural number `n`.
-/
macro "mem_tac_aux" : tactic =>
  `(tactic| first | exact pow_mem_graded _ (SetLike.coe_mem _) | exact natCast_mem_graded _ _ |
    exact pow_mem_graded _ f_deg)

macro "mem_tac" : tactic =>
  `(tactic| first | mem_tac_aux |
    repeat (all_goals (apply SetLike.GradedMonoid.toGradedMul.mul_mem)); mem_tac_aux)

SetLike.GradedMonoid.toGradedMul.mul_mem does not seem to typecheck, but I suppose it's intended to be docs#GradedMul.mul_mem pre-applied to docs#SetLike.GradedMonoid. But, if I want to check this by removing all the extra features, the code builds just the same with:

macro "mem_tac" : tactic => `(tactic| mem_tac_aux)

So should we just promote mem_tac_aux into mem_tac? Or is there a reason to have the distinction for the future?

[Anne Baanen]

cc @Jujian Zhang who wrote mem_tac back in the age of Mathlib 3.