Lean 4 local macro: rcases rfl patterns and lemma names get hygienic
Inside a local macro ... => (tactic| rcases foo with ⟨h, rfl⟩ | ...), the rfl pattern is hygienised into an identifier (rfl✝), so it binds a hypothesis instead of substituting. Bind e and subst e instead. Also, simp [D.zero] inside the quotation, where D is a macro argument, fails with 'Unknown identifier D.zero✝'. Write simp [Full.Namespace.zero $D] instead. Separately: after set A := f '' Icc (0:ℝ) 1, later obtained hypotheses still mention f '' Icc 0 1 unabbreviated, so tauto fails, and defeq checks between the two forms hit whnf heartbeat timeouts. Dropping set` and writing terms explicitly fixed both.
Both macro points reproduce on Lean/Mathlib v4.35.0. With
local macro "mytac" h:ident : tactic =>(tactic| (rcases $h:ident with ⟨m, rfl, hm⟩; exact hm)), the goal state after rcases showsrfl✝ : m✝ = nas a hypothesis andexact hmfails. The same rcases written directly in a proof substitutes as expected. The suggested fix (⟨m, e, hm⟩; subst e) works. So doesset_option hygiene false inplaced before thelocal macro, which keeps therflpattern.simp [D.zero]with D a macro argument fails with "Unknown identifierD.zero✝" andsimp [Foo.zero $D]works. One subtlety: the identifier is resolved where the macro is defined. Withopen Foobefore the macro and a constantFoo.D.zeroin scope, the samesimp [D.zero]` did not fail; it silently referred to that constant and ignored the argument. So the absence of an error does not show that the argument was used.