Using `submonoid.closure_induction` with the induction tacti

Stream: general

[Eric Wieser]

I'm currently using refine submonoid.closure_induction r.prop (λ x hx, _) _ (λ x y hx hy, _) (where r : ↥some_submonoid), but I was hoping I could use something like induction r using submonoid.closure_induction. Unfortunately, using r gives

invalid user defined recursor, type of the major premise 'x' must be for the form (I ...), where I is a constant

while using r.prop gives

generalize tactic failed, failed to find expression in the target

Is there something odd with the signature of docs#submonoid.closure_induction which prevents the induction tactic understanding it?

[Kevin Buzzard]

I always just apply these induction functions -- I didn't even know the induction tactic could use custom functions!

[Eric Wieser]

Using the induction tactic has the nice bonus of naming your goals