Can't reproduce `continuity` tactic

Stream: lean4

[Tomas Skrivan]

I want to create tactic that is almost identical to continuity tactic but for a different predicate on functions. However, I'm having hard time reproducing it.

The theorem similar to Continuous.comp' is screwing up continuous_fst.

File: Init.lean

import Aesop

declare_aesop_rule_sets [Foo]

File: Main.lean

import Init

macro "foo" : attr =>
  `(attr|aesop safe apply (rule_sets [$(Lean.mkIdent `Foo):ident]))

macro "foo" : tactic =>
  `(tactic| aesop (options := { terminal := true }) (rule_sets [$(Lean.mkIdent `Foo):ident]))

variable {α β γ : Type _}

structure Foo (f : α → β) : Prop

@[foo]
theorem id_foo : Foo (fun x : α => x) := ⟨⟩

@[foo]
theorem comp_foo (f : β → γ) (g : α → β) (_ : Foo f) (_ : Foo g) : Foo (fun x => f (g x)) := ⟨⟩

@[foo]
theorem fst_foo : Foo (@Prod.fst α β) := ⟨⟩

example : Foo (fun x : α => x) := by foo
example (f : β → γ) (g : α → β) (_ : Foo f) (_ : Foo g) : Foo (fun x => f (g x)) := by foo
example : Foo (@Prod.fst α β) := by foo -- tactic 'aesop' failed

The last example proving Foo (@Prod.fst α β) fails for some reason. There is some infinite recursion going on as the trace shows case x.x.x.x.x.x.x.x.x.x.x.x.x.x.x but I have very little experience with aesop and I do not know how to read the trace.

[Tomas Skrivan]

It works if I mark comp_foo with @[aesop unsafe apply (rule_sets [Foo])] , but mathlib is not doing it.