Here's how to prove Andrej Bauer's corrected statement using the induction tactic:

theorem foo (α : Type) (f : α → ℕ) (P : α → Prop)
  (ind : ∀ a, (∀ b, f b < f a → P b) → P a) :
  ∀ a, P a :=
begin
  intro a,
  induction hn : f a using nat.strong_induction_on with n ih generalizing a,
  apply ind,
  intros b fb_lt_fa,
  rw hn at fb_lt_fa,
  exact ih _ fb_lt_fa _ rfl,
end

We're lots of its features at once here:

• hn : _ lets us remember that the variable we're inducting on is equal to f a
• using nat.strong_induction_on tells it to use a non-default recursion scheme
• generalizing a ensure that a is in a binder in our inductive hypothesis ih

Note that we don't need base.

Here's how to prove Andrej Bauer's corrected statement using the induction tactic:

theorem foo (α : Type) (f : α → ℕ) (P : α → Prop)
  (ind : ∀ a, (∀ b, f b < f a → P b) → P a) :
  ∀ a, P a :=
begin
  intro a,
  induction hn : f a using nat.strong_induction_on with n ih generalizing a,
  apply ind,
  intros b fb_lt_fa,
  rw hn at fb_lt_fa,
  exact ih _ fb_lt_fa _ rfl,
end

We're using lots of its optional features at once here:

• hn : _ lets us remember that the variable we're inducting on is equal to f a
• using nat.strong_induction_on tells it to use a non-default recursion scheme
• generalizing a ensure that a is in a binder in our inductive hypothesis ih

Note that we don't need base.