Proving substitution property of successor over equality

I'm trying to understand inductive types from chapter 7 of "theorem proving in lean".

I set myself a task of proving that successor of natural numbers has a substitution property over equality:

inductive natural : Type
| zero : natural
| succ : natural -> natural

lemma succ_over_equality (a b : natural) (H : a = b) :
  (natural.succ a) = (natural.succ b) := sorry

After some guesswork and fairly exhaustive search I was able to satisfy the compiler with a couple of possibilities:

lemma succ_over_equality (a b : natural) (H : a = b) :
  (natural.succ a) = (natural.succ b) :=
    eq.rec_on H (eq.refl (natural.succ a))
    --eq.rec_on H rfl
    --eq.subst H rfl
    --eq.subst H (eq.refl (natural.succ a))
    --congr_arg (λ (n : natural), (natural.succ n)) H

I don't understand how any of the proofs I've just given actually work.

1. What is the full definition of the eq (inductive) type? In VSCode I can see the type signature of eq as eq Π {α : Type} α → α → Prop, but I can't see individual (inductive) constructors (analogues of zero and succ from natural). The best I could find in source code doesn't look quite right.
2. Why is eq.subst happy to accept a proof of (natural.succ a) = (natural.succ a) to provide a proof of (natural.succ a) = (natural.succ b)?
3. What is higher order unification and how does it apply to this particular example?
4. What is the meaning of the error I get when I type #check (eq.rec_on H (eq.refl (natural.succ a))), which is [Lean] invalid 'eq.rec_on' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but the expected type must be known eq.rec_on : Π {α : Sort u} {a : α} {C : α → Sort l} {a_1 : α}, a = a_1 → C a → C a_1