eqn_hole.lean:3:7: error: don't know how to synthesize placeholder
context:
f : ℕ → ℕ
⊢ ℕ
eqn_hole.lean:2:11: error: non-exhaustive match, the following cases are missing:
f _
eqn_hole.lean:8:13: error: don't know how to synthesize placeholder
context:
g : ℕ → ℕ,
n : ℕ
⊢ ℕ
eqn_hole.lean:8:11: error: failed to prove recursive application is decreasing, well founded relation
  @has_well_founded.r ℕ (@has_well_founded_of_has_sizeof ℕ nat.has_sizeof)
Possible solutions: 
  - Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.
  - The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions.
The nested exception contains the failure state for the decreasing tactic.
nested exception message:
failed
state:
g : ℕ → ℕ,
n : ℕ
⊢ ⁇ < n + 1
