In Lean, induction x generalizing y keeps y universally quantified during induction on x, rather than treating it as a fixed input.
For a statement , the induction hypotheses differ:
The generalised hypothesis can be applied at any input t, including a computed value. This does not add an induction on y or change the theorem’s mathematical statement.
Examples
Two ways to obtain the same induction hypothesis
With both inputs in the header, plain induction x gives only ih : 0 < Ackermann k y. Generalise y to obtain a hypothesis covering every input:
theorem positive_fixed (x y : ℕ) : 0 < Ackermann x y := by induction x generalizing y with | zero => sorry | succ k ih => sorry
Alternatively, write the quantifier explicitly and introduce y inside each branch:
theorem positive_row (x : ℕ) : ∀ (y : ℕ), 0 < Ackermann x y := by induction x with | zero => intro y sorry | succ k ih => intro y sorry
Both versions express and accept two arguments. Both successor branches have ih : ∀ t, 0 < Ackermann k t.
For example, ih (Ackermann (k + 1) y) proves . The fixed-input hypothesis cannot supply this claim unless the computed input happens to be y.
In the second version, moving intro y before induction x fixes y too early and loses this flexibility. The sorry placeholders leave the actual positivity proofs unfinished.