Is this form of induction' tactic documented anywhere?

Stream: new members

[Dan Abramov]

Found this in @Rado Kirov's solutions:

induction' hi: (x1: ℕ) with n1 ih

Specifically, I've never seen the form with adding hi: in front of what you're inducting on before. It seems pretty important (without it, the exercise I'm working on seems impossible to prove). Is this syntax documented anywhere?

I've looked at the induction' docstring and there's no mention of this. I've also looked at the induction docstring, which mentions "induction e, where e is an expression instead of a variable", but I'm not sure if this is the case it's referring to.

[Dan Abramov]

Concretely, in my example, it puts this ... = 0 hypothesis into the tactic state:

Screenshot 2025-08-18 at 23.11.47.png

Without the hi: , this information gets completely lost and I can't proceed with the proof:

Screenshot 2025-08-18 at 23.12.16.png

I would've never guessed to put it there, or even that this syntax exists.

[Dan Abramov]

To clarify, I understand hi itself is not syntax and could've been named anything. What confuses me is (1) what is the precise syntax here, and (2) why does the information get lost otherwise. In Lean, I'm used that important information doesn't just "disappear" and at worst things get implicit (empty) names. But here it actually gets lost otherwise.

[Kyle Miller]

That's an oversight that it's not documented for induction. That tactic didn't have this feature of cases until earlier this year; it's documented for cases.

The induction' tactic has had it for a long time. (This mathlib tactic is "old style". I think induction is now the preferred one.)

[Dan Abramov]

Is there any specific reason this hypothesis doesn’t get introduced implicitly (with no name) either way?

[Dan Abramov]

Since the thing I’m inducting on wasn’t in directly the goal, it just felt like induction wasn’t working in general. Could in this case it be implied that this hypothesis should be added to context?

[Aaron Liu]

it gives you a less general induction hypothesis I think

[Aaron Liu]

just having this hypothesis in context during the induction means your induction hypothesis has to be modified to also assume it, meaning when you use your induction hypothesis you have to prove an equality

[Kyle Miller]

Doing induction on something that's not a variable is sort of an "advanced" usage of the tactic. It's worth taking a look at the induction hypothesis to make sure it's what you think it should be.

Like Aaron said, including the equality means it'll appear in the induction hypothesis. The tactic lets you opt-in to having that equality.

It's also all just a convenience so that you don't have to use the generalize tactic and then include that new variable in the generalizing clause. With generalize, adding an equality hypothesis is also opt-in (though in that case you can clear it if you didn't want it).

[Dan Abramov]

Ah interesting, okay. This is more nuanced than I thought. I don't know the generalize tactic yet but I'll keep the connection in mind, thank you.

[Rado Kirov]

Btw I learned about this from Zulip https://leanprover.zulipchat.com/#narrow/stream/514017-Analysis-I/topic/exercise.203.2E5.2E12.20-.20how.20to.20do.20induction.20through.20an.20equivalence/near/529619964