Generalize doing reductions?

Stream: lean4

[Daniel Patterson]

I'm wondering if the behavior of generalize is described precisely anywhere. I was a little surprised that it seemed to be doing a bit more than I thought it would. Forgive the somewhat contrived example (I know dsimp [Nat.beq], among other things, would make more sense than generalize) :

theorem nat_beq_succ_inj:
∀ (x y : Nat), (Nat.beq (Nat.succ x) (Nat.succ y)) → (Nat.beq x y)
:= by intros x y;  generalize Nat.beq (Nat.succ x) (Nat.succ y) = z

Results in the goal being z = true -> z = true. I would have thought it would just be z = true -> Nat.beq x y = true.

Is generalize doing definitional reductions in order to find more places it can rewrite (as clearly Nat.beq (Nat.succ x) (Nat.succ y) reduces to Nat.beq x y)?